Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

DSL for module semantics #32

Merged
merged 50 commits into from
Jul 26, 2023
Merged

DSL for module semantics #32

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
152b2d0
Change instance representation as record
ShinWonho Jun 13, 2023
a1c51f9
Add limits check in grow reduction rules
ShinWonho Jun 13, 2023
5380d76
Add type field in eleminst
ShinWonho Jun 14, 2023
2b82dcc
Type check from updated store
Jun 15, 2023
6b6bd32
Consider free variables in premises of DefD
ShinWonho Jun 16, 2023
835bf0d
Add grow helper functions
ShinWonho Jun 16, 2023
7d757da
Fix typos
ShinWonho Jun 16, 2023
7aaff60
Fix typo in data segment
Jun 22, 2023
cecacb5
Draft for module semantics
Jun 22, 2023
2a158db
Add premises for updating store
Jun 22, 2023
066f8c3
Add premises for start function
Jun 22, 2023
6c7d379
Add export allocation
Jun 22, 2023
97d3fe6
Add import allocation
Jun 22, 2023
68c6067
Add 7-module.watsup
ShinWonho Jun 26, 2023
b8681db
Update TEST.md
ShinWonho Jun 26, 2023
9b3e6e3
Fix typo in instantiation
ShinWonho Jun 26, 2023
030a3a8
Update grow helper functions
ShinWonho Jun 28, 2023
d967107
Update spectec/src/frontend/elab.ml
ShinWonho Jun 28, 2023
8f6c590
Update spectec/src/il/validation.ml
ShinWonho Jun 28, 2023
0f48772
Refactor module semantics
ShinWonho Jun 29, 2023
35be3dd
Minor changes
Jun 29, 2023
edda75e
Minor changes
Jun 29, 2023
ff216fb
Update module semantics
Jun 30, 2023
21e0a94
Minor change
Jun 30, 2023
236de04
Minor change
ShinWonho Jul 3, 2023
1560490
Fix typo
ShinWonho Jul 4, 2023
e7a5252
Add iter with index
ShinWonho Jul 5, 2023
6bc75a6
Update elab and validation
ShinWonho Jul 5, 2023
506306e
Compute address in alloc func
ShinWonho Jul 7, 2023
eb57512
Minor changes
ShinWonho Jul 13, 2023
5aeb393
Add iter with an index
ShinWonho Jul 12, 2023
a453c69
Allow opt iter to have list iter type
ShinWonho Jul 7, 2023
88fe94b
Fix location of \land for conditions of funcdef
f52985 Jun 28, 2023
42b276f
Filter with recursive
ShinWonho Jul 14, 2023
65e6777
Minor change
ShinWonho Jul 14, 2023
edb1fbf
Merge two render_condition functions
ShinWonho Jul 19, 2023
8bb5fe0
Merge ListN
ShinWonho Jul 20, 2023
6872abe
Fix bug in iter with index
ShinWonho Jul 21, 2023
616eded
Minor changes
ShinWonho Jul 24, 2023
d764e97
Minor change
ShinWonho Jul 24, 2023
5c9aed2
Check iter with index
ShinWonho Jul 24, 2023
ba5b056
Minor changes
ShinWonho Jul 26, 2023
31213dd
Strip index variable in iter
ShinWonho Jul 26, 2023
474c65f
Add type check for index variable
ShinWonho Jul 26, 2023
384016d
Remove wrong assertion
ShinWonho Jul 26, 2023
fd8ec1f
Update spectec/src/frontend/elab.ml
ShinWonho Jul 26, 2023
97e95c3
Add validation for iter with index
ShinWonho Jul 26, 2023
0e45bef
Update spectec/src/il/validation.ml
ShinWonho Jul 26, 2023
199efd1
Minor change
ShinWonho Jul 26, 2023
cb45bce
Merge branch 'main' into module-semantics
ShinWonho Jul 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions spectec/spec/7-module.watsup
View file
Open in desktop
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I refined the module semantics. To reflect the aforementioned comments, I extended the DSL (you can see the detailed explanation below). This change requires updating the EL parser, IL validation and other components, and we're planning to update them. Before that, I'd like to know whether the updated DSL looks good enough.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm implementing this in dsl branch. It might be helpful to see the implementation to understand the extended syntax.

Original file line number Diff line number Diff line change
Expand Up @@ -111,12 +111,12 @@ def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, m)
-- if ga_ex* = $globals(externval*)
-- if ta_ex* = $tables(externval*)
-- if ma_ex* = $mems(externval*)
-- if fa* = $(|s.FUNC|+i)^(i<n_func)
-- if ga* = $(|s.GLOBAL|+i)^(i<n_global)
-- if ta* = $(|s.TABLE|+i)^(i<n_table)
-- if ma* = $(|s.MEM|+i)^(i<n_mem)
-- if ea* = $(|s.ELEM|+i)^(i<n_elem)
-- if da* = $(|s.DATA|+i)^(i<n_data)
-- if fa* = $(|s.FUNC|+i_func)^(i_func<n_func)
-- if ga* = $(|s.GLOBAL|+i_global)^(i_global<n_global)
-- if ta* = $(|s.TABLE|+i_table)^(i_table<n_table)
-- if ma* = $(|s.MEM|+i_mem)^(i_mem<n_mem)
-- if ea* = $(|s.ELEM|+i_elem)^(i_elem<n_elem)
-- if da* = $(|s.DATA|+i_data)^(i_data<n_data)
-- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
-- if m = {
FUNC fa_ex* fa*,
Expand Down
4 changes: 1 addition & 3 deletions spectec/src/el/free.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
let rec free_iter iter =
match iter with
| Opt | List | List1 -> empty
| ListN (e, None) -> free_exp e
| ListN (e, Some (id)) ->
union (free_exp e) (free_varid id)
| ListN (e, _) -> free_exp e
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doesn't this need to be:

Suggested change
| ListN (e, _) -> free_exp e
| ListN (e, id_opt) -> union (free_exp e) (free_opt free_varid id_opt)



(* Types *)
Expand Down
17 changes: 9 additions & 8 deletions spectec/src/frontend/multiplicity.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,7 @@ let iter_nl_list f xs = List.iter (function Nl -> () | Elem x -> f x) xs
let rec check_iter env ctx iter =
match iter with
| Opt | List | List1 -> ()
| ListN (e, opt) ->
Option.iter (fun id -> check_id env ctx id) opt;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't we still need this check?

| ListN (e, _) ->
check_exp env ctx e

and check_exp env ctx e =
Expand Down Expand Up @@ -163,13 +162,9 @@ let union = Env.union (fun _ ctx1 ctx2 -> assert (ctx1 = ctx2); Some ctx1)
let rec annot_iter env iter : Il.Ast.iter * occur =
match iter with
| Opt | List | List1 -> iter, Env.empty
| ListN (e, None) ->
| ListN (e, opt) ->
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit:

Suggested change
| ListN (e, opt) ->
| ListN (e, id_opt) ->

Also, I believe this needs to check that the variable has the right type.

let e', occur = annot_exp env e in
ListN (e', None), occur
| ListN (e, Some id) ->
let e', occur1 = annot_exp env e in
let occur2 = Env.singleton id.it (Env.find id.it env) in
ListN (e', Some id), union occur1 occur2
ListN (e', opt), occur
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
ListN (e', opt), occur
ListN (e', id_opt), occur


and annot_exp env e : Il.Ast.exp * occur =
let it, occur =
Expand Down Expand Up @@ -290,6 +285,12 @@ and annot_iterexp env occur1 (iter, ids) at : Il.Ast.iterexp * occur =
) occur1
in
let ids' = List.map (fun (x, _) -> x $ at) (Env.bindings occur1') in

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change

(match iter' with
| ListN (_, Some id) ->
assert (List.length ids' = 1 && id.it = (List.hd ids').it)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand this assertion. Why can't there be any other ids in that case?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is because I would like to block the use of "iter with index" like this:

def $foo() : nat
def $foo() = 0
  -- if x* = 0 1 2
  -- if (x*[i] = y)^(i<3)

If you think we should allow semantics like this, I will remove the assertion.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think I follow, what problem do you see with that example? In Shouldn't using them for indexing be one of the primary use cases for iter vars?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I apologize for not providing sufficient explanation earlier.
My intention was to use 'iter with index' in a way that restricts iteration on variables other than the index variable.
However, upon further consideration, I realized that 'iter with index' merely introduces an index for iteration, so there shouldn't be such a restriction. I'll erase the assertion.

| _ -> ());

(iter', ids'), union occur1' occur2


Expand Down
4 changes: 1 addition & 3 deletions spectec/src/il/free.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,9 +55,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
let rec free_iter iter =
match iter with
| Opt | List | List1 -> empty
| ListN (e, None) -> free_exp e
| ListN (e, Some id) ->
union (free_exp e) (free_varid id)
| ListN (e, _) -> free_exp e
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't his be

Suggested change
| ListN (e, _) -> free_exp e
| ListN (e, id_opt) → union (free_exp e) (free_opt free_varid id_opt)



(* Types *)
Expand Down
32 changes: 16 additions & 16 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1865,18 +1865,18 @@ def allocdatas : (store, byte**) -> (store, dataaddr*)
;; 7-module.watsup:97.1-97.81
def allocmodule : (store, module, externval*, val*, ref**) -> (store, moduleinst)
;; 7-module.watsup:98.1-135.54
def {byte*^n_data : byte*^n_data, da* : dataaddr*, datamode?^n_data : datamode?^n_data, ea* : elemaddr*, elemmode?^n_elem : elemmode?^n_elem, export* : export*, expr_1^n_global : expr^n_global, expr_2*^n_elem : expr*^n_elem, externval* : externval*, fa* : funcaddr*, fa_ex* : funcaddr*, func^n_func : func^n_func, ga* : globaladdr*, ga_ex* : globaladdr*, globaltype^n_global : globaltype^n_global, i : nat, import* : import*, m : moduleinst, ma* : memaddr*, ma_ex* : memaddr*, memtype^n_mem : memtype^n_mem, module : module, n_data : n, n_elem : n, n_func : n, n_global : n, n_mem : n, n_table : n, ref** : ref**, rt^n_elem : reftype^n_elem, s : store, s_1 : store, s_2 : store, s_3 : store, s_4 : store, s_5 : store, s_6 : store, start? : start?, ta* : tableaddr*, ta_ex* : tableaddr*, tabletype^n_table : tabletype^n_table, val* : val*, xi* : exportinst*} allocmodule(s, module, externval*{externval}, val*{val}, ref*{ref}*{ref}) = (s_6, m)
def {byte*^n_data : byte*^n_data, da* : dataaddr*, datamode?^n_data : datamode?^n_data, ea* : elemaddr*, elemmode?^n_elem : elemmode?^n_elem, export* : export*, expr_1^n_global : expr^n_global, expr_2*^n_elem : expr*^n_elem, externval* : externval*, fa* : funcaddr*, fa_ex* : funcaddr*, func^n_func : func^n_func, ga* : globaladdr*, ga_ex* : globaladdr*, globaltype^n_global : globaltype^n_global, i_data^(i_data<n_data) : nat^(i_data<n_data), i_elem^(i_elem<n_elem) : nat^(i_elem<n_elem), i_func^(i_func<n_func) : nat^(i_func<n_func), i_global^(i_global<n_global) : nat^(i_global<n_global), i_mem^(i_mem<n_mem) : nat^(i_mem<n_mem), i_table^(i_table<n_table) : nat^(i_table<n_table), import* : import*, m : moduleinst, ma* : memaddr*, ma_ex* : memaddr*, memtype^n_mem : memtype^n_mem, module : module, n_data : n, n_elem : n, n_func : n, n_global : n, n_mem : n, n_table : n, ref** : ref**, rt^n_elem : reftype^n_elem, s : store, s_1 : store, s_2 : store, s_3 : store, s_4 : store, s_5 : store, s_6 : store, start? : start?, ta* : tableaddr*, ta_ex* : tableaddr*, tabletype^n_table : tabletype^n_table, val* : val*, xi* : exportinst*} allocmodule(s, module, externval*{externval}, val*{val}, ref*{ref}*{ref}) = (s_6, m)
-- if (module = `MODULE%*%*%*%*%*%*%*%?%*`(import*{import}, func^n_func{func}, GLOBAL(globaltype, expr_1)^n_global{expr_1 globaltype}, TABLE(tabletype)^n_table{tabletype}, MEMORY(memtype)^n_mem{memtype}, `ELEM%%*%?`(rt, expr_2*{expr_2}, elemmode?{elemmode})^n_elem{elemmode expr_2 rt}, `DATA%*%?`(byte*{byte}, datamode?{datamode})^n_data{byte datamode}, start?{start}, export*{export}))
-- if (fa_ex*{fa_ex} = $funcs(externval*{externval}))
-- if (ga_ex*{ga_ex} = $globals(externval*{externval}))
-- if (ta_ex*{ta_ex} = $tables(externval*{externval}))
-- if (ma_ex*{ma_ex} = $mems(externval*{externval}))
-- if (fa*{fa} = (|s.FUNC_store| + i)^(i<n_func){})
-- if (ga*{ga} = (|s.GLOBAL_store| + i)^(i<n_global){})
-- if (ta*{ta} = (|s.TABLE_store| + i)^(i<n_table){})
-- if (ma*{ma} = (|s.MEM_store| + i)^(i<n_mem){})
-- if (ea*{ea} = (|s.ELEM_store| + i)^(i<n_elem){})
-- if (da*{da} = (|s.DATA_store| + i)^(i<n_data){})
-- if (fa*{fa} = (|s.FUNC_store| + i_func)^(i_func<n_func){i_func})
-- if (ga*{ga} = (|s.GLOBAL_store| + i_global)^(i_global<n_global){i_global})
-- if (ta*{ta} = (|s.TABLE_store| + i_table)^(i_table<n_table){i_table})
-- if (ma*{ma} = (|s.MEM_store| + i_mem)^(i_mem<n_mem){i_mem})
-- if (ea*{ea} = (|s.ELEM_store| + i_elem)^(i_elem<n_elem){i_elem})
-- if (da*{da} = (|s.DATA_store| + i_data)^(i_data<n_data){i_data})
-- if (xi*{xi} = $instexport(fa_ex*{fa_ex} :: fa*{fa}, ga_ex*{ga_ex} :: ga*{ga}, ta_ex*{ta_ex} :: ta*{ta}, ma_ex*{ma_ex} :: ma*{ma}, export)*{export})
-- if (m = {FUNC fa_ex*{fa_ex} :: fa*{fa}, GLOBAL ga_ex*{ga_ex} :: ga*{ga}, TABLE ta_ex*{ta_ex} :: ta*{ta}, MEM ma_ex*{ma_ex} :: ma*{ma}, ELEM ea*{ea}, DATA da*{da}, EXPORT xi*{xi}})
-- if ((s_1, fa*{fa}) = $allocfuncs(s, m, func^n_func{func}))
Expand Down Expand Up @@ -1918,7 +1918,7 @@ def concat_instr : instr** -> instr*
;; 7-module.watsup:157.1-157.55
def instantiation : (store, module, externval*) -> config
;; 7-module.watsup:158.1-180.28
def {data* : data*, elem* : elem*, elemmode?* : elemmode?*, export* : export*, externval* : externval*, f : frame, f_init : frame, func* : func*, global* : global*, globaltype* : globaltype*, i : nat, import* : import*, instr_1** : instr**, instr_2*** : instr***, instr_data* : instr*, instr_elem* : instr*, j : nat, m : moduleinst, m_init : moduleinst, mem* : mem*, module : module, n_data : n, n_elem : n, ref** : ref**, reftype* : reftype*, s : store, s' : store, start? : start?, table* : table*, val* : val*, x? : idx?} instantiation(s, module, externval*{externval}) = `%;%*`(`%;%`(s', f), (instr_elem <: admininstr)*{instr_elem} :: (instr_data <: admininstr)*{instr_data} :: CALL_admininstr(x)?{x})
def {data* : data*, elem* : elem*, elemmode?* : elemmode?*, export* : export*, externval* : externval*, f : frame, f_init : frame, func* : func*, global* : global*, globaltype* : globaltype*, i^(i<n_elem) : nat^(i<n_elem), import* : import*, instr_1** : instr**, instr_2*** : instr***, instr_data* : instr*, instr_elem* : instr*, j^(j<n_data) : nat^(j<n_data), m : moduleinst, m_init : moduleinst, mem* : mem*, module : module, n_data : n, n_elem : n, ref** : ref**, reftype* : reftype*, s : store, s' : store, start? : start?, table* : table*, val* : val*, x? : idx?} instantiation(s, module, externval*{externval}) = `%;%*`(`%;%`(s', f), (instr_elem <: admininstr)*{instr_elem} :: (instr_data <: admininstr)*{instr_data} :: CALL_admininstr(x)?{x})
-- if (module = `MODULE%*%*%*%*%*%*%*%?%*`(import*{import}, func*{func}, global*{global}, table*{table}, mem*{mem}, elem*{elem}, data*{data}, start?{start}, export*{export}))
-- if (m_init = {FUNC $funcs(externval*{externval}), GLOBAL $globals(externval*{externval}), TABLE [], MEM [], ELEM [], DATA [], EXPORT []})
-- if (f_init = {LOCAL [], MODULE m_init})
Expand All @@ -1929,9 +1929,9 @@ def instantiation : (store, module, externval*) -> config
-- if ((s', m) = $allocmodule(s, module, externval*{externval}, val*{val}, ref*{ref}*{ref}))
-- if (f = {LOCAL [], MODULE m})
-- if (n_elem = |elem*{elem}|)
-- if (instr_elem*{instr_elem} = $concat_instr($runelem(elem*{elem}[i], i)^(i<n_elem){}))
-- if (instr_elem*{instr_elem} = $concat_instr($runelem(elem*{elem}[i], i)^(i<n_elem){i}))
-- if (n_data = |data*{data}|)
-- if (instr_data*{instr_data} = $concat_instr($rundata(data*{data}[j], j)^(j<n_data){}))
-- if (instr_data*{instr_data} = $concat_instr($rundata(data*{data}[j], j)^(j<n_data){j}))
-- if (start?{start} = START(x)?{x})

;; 7-module.watsup:183.1-183.48
Expand Down Expand Up @@ -4270,12 +4270,12 @@ $$
&&&\quad {\land}~{\mathit{ga}_{\mathit{ex}}^\ast} = \mathrm{globals}({\mathit{externval}^\ast}) \\
&&&\quad {\land}~{\mathit{ta}_{\mathit{ex}}^\ast} = \mathrm{tables}({\mathit{externval}^\ast}) \\
&&&\quad {\land}~{\mathit{ma}_{\mathit{ex}}^\ast} = \mathrm{mems}({\mathit{externval}^\ast}) \\
&&&\quad {\land}~{\mathit{fa}^\ast} = {{|\mathit{s}.\mathsf{func}|} + \mathit{i}^(i<\mathit{n}_{\mathit{func}})} \\
&&&\quad {\land}~{\mathit{ga}^\ast} = {{|\mathit{s}.\mathsf{global}|} + \mathit{i}^(i<\mathit{n}_{\mathit{global}})} \\
&&&\quad {\land}~{\mathit{ta}^\ast} = {{|\mathit{s}.\mathsf{table}|} + \mathit{i}^(i<\mathit{n}_{\mathit{table}})} \\
&&&\quad {\land}~{\mathit{ma}^\ast} = {{|\mathit{s}.\mathsf{mem}|} + \mathit{i}^(i<\mathit{n}_{\mathit{mem}})} \\
&&&\quad {\land}~{\mathit{ea}^\ast} = {{|\mathit{s}.\mathsf{elem}|} + \mathit{i}^(i<\mathit{n}_{\mathit{elem}})} \\
&&&\quad {\land}~{\mathit{da}^\ast} = {{|\mathit{s}.\mathsf{data}|} + \mathit{i}^(i<\mathit{n}_{\mathit{data}})} \\
&&&\quad {\land}~{\mathit{fa}^\ast} = {{|\mathit{s}.\mathsf{func}|} + \mathit{i}_{\mathit{func}}^(i_func<\mathit{n}_{\mathit{func}})} \\
&&&\quad {\land}~{\mathit{ga}^\ast} = {{|\mathit{s}.\mathsf{global}|} + \mathit{i}_{\mathit{global}}^(i_global<\mathit{n}_{\mathit{global}})} \\
&&&\quad {\land}~{\mathit{ta}^\ast} = {{|\mathit{s}.\mathsf{table}|} + \mathit{i}_{\mathit{table}}^(i_table<\mathit{n}_{\mathit{table}})} \\
&&&\quad {\land}~{\mathit{ma}^\ast} = {{|\mathit{s}.\mathsf{mem}|} + \mathit{i}_{\mathit{mem}}^(i_mem<\mathit{n}_{\mathit{mem}})} \\
&&&\quad {\land}~{\mathit{ea}^\ast} = {{|\mathit{s}.\mathsf{elem}|} + \mathit{i}_{\mathit{elem}}^(i_elem<\mathit{n}_{\mathit{elem}})} \\
&&&\quad {\land}~{\mathit{da}^\ast} = {{|\mathit{s}.\mathsf{data}|} + \mathit{i}_{\mathit{data}}^(i_data<\mathit{n}_{\mathit{data}})} \\
&&&\quad {\land}~{\mathit{xi}^\ast} = {\mathrm{instexport}({\mathit{fa}_{\mathit{ex}}^\ast}~{\mathit{fa}^\ast},\, {\mathit{ga}_{\mathit{ex}}^\ast}~{\mathit{ga}^\ast},\, {\mathit{ta}_{\mathit{ex}}^\ast}~{\mathit{ta}^\ast},\, {\mathit{ma}_{\mathit{ex}}^\ast}~{\mathit{ma}^\ast},\, \mathit{export})^\ast} \\
&&&\quad {\land}~\mathit{m} = \{ \begin{array}[t]{@{}l@{}}
\mathsf{func}~{\mathit{fa}_{\mathit{ex}}^\ast}~{\mathit{fa}^\ast},\; \\
Expand Down
Loading