DSL for module semantics #32

ShinWonho · 2023-06-26T05:28:26Z

DSL for module semantics.
This PR depends on #30

rossberg

Cool, thanks! I have some comments, see below.

rossberg · 2023-06-27T07:58:13Z

spectec/spec/1-syntax.watsup

@@ -57,7 +57,7 @@ syntax resulttype hint(desc "result type") =
  valtype*

 syntax limits hint(desc "limits") =
-  `[u32 .. u32]
+  `[u32 .. u32?]


FWIW, I dropped the option on purpose, since I figured it's simpler to just desugar an empty upper bound into 2^32-1 in the AST.

rossberg · 2023-06-27T08:01:51Z

spectec/spec/6-reduction.watsup

+  -- if $table(z, x) = ti
+  -- if $grow_table(ti, n, ref) = ti'


Suggested change

-- if $table(z, x) = ti

-- if $grow_table(ti, n, ref) = ti'

-- if $grow_table($table(z, x), n, ref) = ti'

rossberg · 2023-06-27T08:02:32Z

spectec/spec/6-reduction.watsup

+  z; ref (CONST I32 n) (TABLE.GROW x)  ~>  $with_tableinst(z, x, ti'); (CONST I32 $(|$table(z, x).ELEM|))
+  -- if $table(z, x) = ti
+  -- if $grow_table(ti, n, ref) = ti'
+  -- Tabletype_ok: |- ti'.TYPE : OK


This condition should probably be moved to $grow_table, such that that becomes a self-contained abstraction.

rossberg · 2023-06-27T08:03:01Z

spectec/spec/6-reduction.watsup

+  -- if $mem(z, 0) = mi
+  -- if $grow_memory(mi, n) = mi'


Suggested change

-- if $mem(z, 0) = mi

-- if $grow_memory(mi, n) = mi'

-- if $grow_memory($mem(z, 0), n) = mi'

rossberg · 2023-06-27T08:03:11Z

spectec/spec/6-reduction.watsup

+  z; (CONST I32 n) (MEMORY.GROW)  ~>  $with_meminst(z, 0, mi'); (CONST I32 $(|$mem(z, 0).DATA| / (64 * $Ki)))
+  -- if $mem(z, 0) = mi
+  -- if $grow_memory(mi, n) = mi'
+  -- Memtype_ok: |- mi'.TYPE : OK


Same comment as above.

rossberg · 2023-06-27T08:19:55Z

spectec/spec/7-module.watsup

+  -- if elem = ELEM reftype expr* elemmode
+  -- if n = |expr*|
+  -- if elemmode = TABLE x instr*
+  -- Step : s; f; instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT x i) (ELEM.DROP i) ~> s_new; f_new; epsilon


Oh. The run functions are supposed to be auxiliary functions that produce a program to run (i.e., desugar active segments), not actually execute the instructions.

rossberg · 2023-06-27T08:20:53Z

spectec/spec/7-module.watsup

+  -- if $run_data((s_elem; f_elem), data*, 0) = s_res; f_res
+
+def $instantiation(s, module, externval*) = (s_res, m)
+  -- if module = MODULE import* func* global* table* mem* elem* data* start export*


Can we avoid duplicating the definition? Why would the approach from the spec not work?

rossberg · 2023-06-27T08:23:42Z

spectec/spec/7-module.watsup

+
+;; Instantiation
+
+def $instantiation(store, module, externval*) : (store, moduleinst)


So, the instantiate (and similarly invoke) functions in the spec are meant to macro-expand into an actual instruction sequence, which then can be reduced separately by the usual means. This definition seems to be interleave expansion and execution and couple them together, which I'd rather like to avoid.

rossberg · 2023-06-27T08:27:46Z

spectec/spec/7-module.watsup

+  -- if m_res = $alloc_import(m_new, import'*, externval'*)
+
+
+def $alloc_func(state, func*) : (store, funcaddr*)


Here and below we are conflating the allocx functions with the allocx* liftings. Could we keep them separate? In particular, for the Latex spec, we will only want to include the allocx ones, and not write out each of the others.

rossberg · 2023-06-27T08:37:19Z

spectec/spec/7-module.watsup

+  -- if m_ex = m_im ++ { FUNC fa*, GLOBAL ga*, TABLE ta*, MEM ma*, ELEM ea*, DATA da*, EXPORT epsilon }
+  -- if xi* = $alloc_export(m_ex, export)*
+  -- if m_res = m_ex[.EXPORT = xi*]
+  -- if s_res = $replace_moduleinst(s_data, fa*, m_res)


I see why you did it this way, but now the alloc_module functions is not actually allocating one module instance, but an arbitrary number of them. Can we change this so that there is only one module instance being created in the end?

Also, Conrad suggested we can avoid resorting to mutating immutable parts of the store and instead break the cycle by precomputing the function addresses and the module instance before creating the function instances.

Co-authored-by: Andreas Rossberg <[email protected]>

ShinWonho · 2023-06-30T07:00:45Z

spectec/spec/7-module.watsup

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.

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

ShinWonho · 2023-06-30T07:00:48Z

spectec/spec/7-module.watsup

+def $funcs(externval*) = [fa|FUNC fa <- externval]
+def $globals(externval*) = [ga|GLOBAL ga <- externval]
+def $tables(externval*) = [ta|TABLE ta <- externval]
+def $mems(externval*) = [ma|MEM ma <- externval]


I suggest new syntax for order preserving filter in the spec.

Or, we can use recursion

def $funcs(externval*) : funcaddr* def $funcs(epsilon) = epsilon def $funcs((FUNC fa) externval'*) = fa $funcs(externval'*) def $funcs(externval externval'*) = $funcs(externval'*) -- otherwise

I updated the syntax in 236de04.

def $funcs(externval*) = `[fa|FUNC fa <- externval] def $globals(externval*) = `[ga|GLOBAL ga <- externval] def $tables(externval*) = `[ta|TABLE ta <- externval] def $mems(externval*) = `[ma|MEM ma <- externval]

Makes sense, though extending the DSL may be quite a cost for a one-off auxiliary definition like this. Let's perhaps discuss this on Thursday.

ShinWonho · 2023-06-30T07:00:59Z

spectec/spec/7-module.watsup

+  -- if ta* = |s.TABLE| ... $(|s.TABLE| + |table*| - 1)
+  -- if ma* = |s.MEM| ... $(|s.MEM| + |mem*| - 1)
+  -- if ea* = |s.ELEM| ... $(|s.ELEM| + |elem*| - 1)
+  -- if da* = |s.DATA| ... $(|s.DATA| + |data*| - 1)


I suggest new syntax for range to precomputing the addresses.
For example, 0 ... 5 means 0 1 2 3 4 5.

Can this perhaps be expressed by an auxiliary function?

def $range(nat_1, nat_2) : nat* hint(show %...%) def $range(n_1, n_2) = epsilon -- if n_1 > n_2 def $range(n_1, n_2) = n_1 $range(n_1+1, n_2) -- otherwise

Thanks for the idea. I'll reflect it.

ShinWonho · 2023-06-30T07:01:02Z

spectec/spec/7-module.watsup

+  -- if s_3 = s_2[.TABLE =.. $alloctable(tabletype)*]
+  -- if s_4 = s_3[.MEM =.. $allocmem(memtype)*]
+  -- if s_5 = s_4[.ELEM =.. $allocelem(rt, ref*)*]
+  -- if s_6 = s_5[.DATA =.. $allocdata(byte*)*]


Now, we don't need allocx* liftings.
But we can use allocx* liftings, if you want.

def $allocfunc(store, moduleinst, func) : store def $allocfunc(s, m, func) = s[.FUNC =.. fi] -- if fi = { MODULE m, CODE func } def $allocfunc*(store, moduleinst, func*) : store def $allocfunc*(s, m, epsilon) = s def $allocfunc*(s, m, func func'*) = $allocfunc*($allocfunc(s, m, func), m, func'*) ... def $allocmodule(store, module, externval*, val*, (ref*)*) : (store, moduleinst) def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, m) ... -- if s_1 = $allocfunc*(s, m, func*) ...

The alloc functions are meant as an abstraction that encapsulates allocation (and they are used in other places, specifically, the embedding interface in the appendix). The formulation you suggest, while cute, would be problematic in that sense, because then these functions no longer actually allocate.

So I'd go with the liftings for now. (You probably need to name them without the star and make that a show-hint.)

Mid-term I'd like to revamp the module representation into a linear list of declaration that is processed sequentially. Then this mess should go away.

I have a few questions related to the comments you made:

To avoid mutation, we decided to precompute the addresses before allocation. As a result, the alloc functions no longer return address. Is it acceptable to return store only?

In the spec, the allocx lifting is defined for arbitrary object kinds, but DSL doesn't allow it. So I define a lifting function for each of the alloc functions. Is this approach acceptable?

You mentioned that it is necessary to name the lifting functions without a star. If we remove the star, the name of lifting function would be the same as the name of allocation function. To ensure distinct names, would it be appropriate to use the name allocfuncs for the lifting function?

I didn't fully understand the sentence: "Mid-term I'd like to revamp the module representation into a linear list of declaration that is processed sequentially." Could you provide further clarification on its meaning?

Re 1: Well, if you rephrase "precompute" as "predict", then no change to the allocation functions is necessary, I believe.

Re 2: Yes, defining a function for each type is fine for the DSL. We can probably still tweak it to produce a single template in the Latex output.

Re 3: allocfuncs sounds good to me.

Re 4: With some of the future extensions, module checking and instantiation becomes more sequential, with ordered dependencies between declarations. Also, there are ideas for allowing multiple appearances of section types, so that the order of different sorts of declarations can be mixed. So I would like to refactor modules to be more like a sequence of different declarations that is processed in order, which would also eliminate the specific iterations. I still have to work out the details, though, in particular wrt instantiation.

Thank you for your kind reply!

ShinWonho · 2023-06-30T07:01:07Z

spectec/spec/7-module.watsup

+
+def $instantiation(store, module, externval*) : config
+def $instantiation(s, module, externval*) =
+  s'; f; ...$runelem(elem*[i], i)* ...$rundata(data*[j], j)* (CALL x)?


We also need range for runelem and rundata.
Here, i* is a range 0 ... $(n-1), so $runelem(elem*[i], i)* means $runelem(elem*[0], 0) ... $runelem(elem*[$(n-1)]), $(n-1)) where n = |elem*|.
However, type of $runelem(..) is instr*, so type of $runelem(..)* is instr**.
Therefore, it requires new syntax for flattening.

...$runelem(..)* notation stands for kind of flattening which comes from JavaScript syntax spread.
Alternatively, we can use notations from Scala or Python
Scala repeated parameters: $runelem(..):_*
Python unpacking: *($runelem(..)*)

Rather than using *-notation, we can also use syntax similar to the spec
$runelem(elem*[0], 0) ... $runelem(elem*[$(n-1)], $(n-1))

Yeah, at this point I wonder if we shouldn't have a version of iteration with an index variable, e.g., exp^(i<n). Then this could be expressed as

(runelem_(i, elem))^(i<n)

when given elem^n. But maybe that's going too far?

Note that the spec also defines an auxiliary concat operator for flattening (see here).
A monomorphic version of that can already be defined in the DSL. For example, this works:

def $concat(nat**) : nat* def $concat(epsilon) = epsilon def $concat(n* n'**) = n* $concat(n'**) def $f(nat) : nat* def $f(n) = n n n def $g(nat*) : nat* def $g(n*) = $concat($f(n)*) $concat($f(n)*)

Oh, Thanks for the ideas! I'll reflect them.

ShinWonho · 2023-07-14T04:37:31Z

I updated module-semantics, filter with recursive version.

rossberg

Looks mostly good, module nits. However, I would suggest minor refactorings of the new AST node:

Instead of a separate IndexedListN, have single ListN of exp * id option. That avoids repeating the logic for the exponent.
Introduce the same in the EL and disambiguate the syntax in the parser.

rossberg · 2023-07-14T08:51:14Z

spectec/src/frontend/elab.ml

@@ -762,7 +766,7 @@ and elab_exp_notation' env e t : Il.exp list =
  | (EpsE | SeqE _), IterT (t1, iter) ->
    [elab_exp_notation_iter env (unseq_exp e) (t1, iter) t e.at]
  | IterE (e1, iter1), IterT (t1, iter) ->
-    if (iter = Opt) <> (iter1 = Opt) then
+    if (iter = Opt) && (iter1 <> Opt) then


Why is this change needed?

def $instantiation(s, module, externval*) = s'; f; instr_elem* instr_data* (CALL x)? ...

This is instantiation function in DSL.
In this context, (CALL x)? should be interpreted as admininstr*, which can either be epsilon (empty) or have a length of one.
So, it is intended to allow the optional iterative expression to have a list iteration type.

rossberg · 2023-07-14T08:52:31Z

spectec/src/frontend/elab.ml

+  | ListN e ->
+    match e.it with
+    | ParenE ({ it = CmpE ({ it = VarE id; _ }, LtOp, e); _}, _) ->
+      Il.IndexedListN (id, elab_exp env e (NatT $ e.at))
+    | _ -> Il.ListN (elab_exp env e (NatT $ e.at))


I suggest we introduce an IndexedListN constructor in the EL as well and disambiguate in the parser already.

Thanks for the comments. I have a few questions.

I want to check whether I understand correctly. As I understand, EL should include both ListN of id and IndexedListN of exp * id, while IL should only have ListN of exp * id option. Is it correct?

To have both ListN and IndexedListN in EL,

iter : | QUEST { Opt } | PLUS { List1 } | STAR { List } | UP arith_prim { match $2.it with | ParenE ({ it = CmpE({ it = VarE id; _ }, LtOp, e); _}, false) -> IndexedListN (e, id) | _ -> ListN $2 }

is it enough for parser code, or do I have to refactor parsing the iter?

Ah, sorry for the confusion, I wrote this comment about IndexedListN in EL before I arrived at the other. I'd prefer both to use ListN of exp * id option.

Oh, I see.
However, I believe pattern matching is still necessary to obtain id information if we do not intend to refactor the parser.

iter : | QUEST { Opt } | PLUS { List1 } | STAR { List } | UP arith_prim { match $2.it with | ParenE ({ it = CmpE({ it = VarE id; _ }, LtOp, e); _}, false) -> ListN (e, Some id) | _ -> ListN ($2, None) }

Is this pattern matching seems okay?

Yes, that's fine with me.

rossberg · 2023-07-14T08:53:43Z

spectec/src/il/validation.ml

+      | IndexedListN _
+      | ListN _ -> List


Suggested change

| IndexedListN _

| ListN _ -> List

| ListN _ | IndexedListN _ -> List

rossberg · 2023-07-14T08:57:26Z

spectec/src/backend-latex/render.ml

@@ -694,6 +694,16 @@ let render_conditions env = function
    " &\\quad\n  " ^ word "if" ^ "~" ^
    concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems

+let render_func_conditions env = function


The only difference between this function and render_red_conditions seems to be the number of tabs to insert. Instead of duplicating the entire definition, can we perhaps make tab string ("&&&" vs "&&&&") a parameter?

ShinWonho · 2023-07-20T05:34:24Z

I reflected your comments!
Thanks for the comments :)

rossberg

Thanks! I have mostly nits, but I think there are few things missing around checking the iteration variable.

rossberg · 2023-07-21T08:45:35Z

spectec/src/il/free.ml

-  | ListN (e, None) -> free_exp e
-  | ListN (e, Some id) ->
-    union (free_exp e) (free_varid id)
+  | ListN (e, _) -> free_exp e


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)

rossberg · 2023-07-21T08:48:15Z

spectec/src/frontend/multiplicity.ml

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


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

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.

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?

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.

rossberg · 2023-07-21T08:49:08Z

spectec/src/frontend/multiplicity.ml

@@ -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) ->


Nit:

Suggested change

| ListN (e, opt) ->

| ListN (e, id_opt) ->

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

rossberg · 2023-07-21T08:49:21Z

spectec/src/frontend/multiplicity.ml

-    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


Suggested change

ListN (e', opt), occur

ListN (e', id_opt), occur

rossberg · 2023-07-21T08:51:17Z

spectec/src/frontend/multiplicity.ml

@@ -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;


Don't we still need this check?

rossberg · 2023-07-21T09:02:56Z

spectec/src/il/validation.ml

+    let iter' =
+      match fst iter with
+      | ListN _ -> List
+      | iter' -> iter'
+    in


Nit: I think you can undo the reformatting now.

rossberg · 2023-07-21T09:03:24Z

spectec/src/middlend/sub.ml

@@ -119,7 +119,7 @@ and t_exp' env = function
  | SubE (e, t1, t2) -> SubE (e, t1, t2)

 and t_iter env = function
-  | ListN e -> ListN (t_exp env e)
+  | ListN (e, id) -> ListN (t_exp env e, id)


Suggested change

| ListN (e, id) -> ListN (t_exp env e, id)

| ListN (e, id_opt) -> ListN (t_exp env e, id_opt)

rossberg · 2023-07-21T09:03:40Z

spectec/src/middlend/totalize.ml

@@ -78,7 +78,7 @@ and t_exp' env = function
  | SubE (e, t1, t2) -> SubE (e, t1, t2)

 and t_iter env = function
-  | ListN e -> ListN (t_exp env e)
+  | ListN (e, id) -> ListN (t_exp env e, id)


Suggested change

| ListN (e, id) -> ListN (t_exp env e, id)

| ListN (e, id_opt) -> ListN (t_exp env e, id_opt)

rossberg · 2023-07-21T09:03:56Z

spectec/src/middlend/unthe.ml

@@ -156,7 +156,7 @@ and t_iterexp n (iter, vs) =
  unary t_iter n iter (fun iter' -> (iter', vs))

 and t_iter n iter = match iter with
-  | ListN e -> unary t_exp n e (fun e' -> ListN e')
+  | ListN (e, id) -> unary t_exp n e (fun e' -> ListN (e', id))


Suggested change

| ListN (e, id) -> unary t_exp n e (fun e' -> ListN (e', id))

| ListN (e, id_opt) -> unary t_exp n e (fun e' -> ListN (e', id_opt))

rossberg · 2023-07-21T09:04:09Z

spectec/src/middlend/wild.ml

@@ -180,7 +180,7 @@ and t_iterexp env (iter, vs) =
  unary t_iter env iter (fun iter' -> (iter', vs))

 and t_iter env iter = match iter with
-  | ListN e -> unary t_exp env e (fun e' -> ListN e')
+  | ListN (e, id) -> unary t_exp env e (fun e' -> ListN (e', id))


Suggested change

| ListN (e, id) -> unary t_exp env e (fun e' -> ListN (e', id))

| ListN (e, id_opt) -> unary t_exp env e (fun e' -> ListN (e', id_opt))

ShinWonho · 2023-07-24T07:38:34Z

I introduced a check for the 'iter with index.'
If we check IterE where iter is of the form ListN (e, Some id), I treat the dimension of id as [ListN (e, Some id)], which is recursive.
Should we allow this recursion? If you prefer to avoid recursion, I can modify the dimension as [ListN (e)] or [List]

rossberg

Good point. Now that you mention it, I think no iteration variables should occur in any variable dimension. They are not part of the "dimension type". I believe this means that in multiplicity.ml:

check_iter needs to strip the variable, like you suggest
both check_exp and check_prem also need to strip any variable from the iter that they add to the ctx list in the cases of IterE and IterPr,
the equality assertion in annot_iterexp must strip iter before comparing it.

And in il/validation.ml:

in valid_iter the iter must be stripped before comparing to dim

Perhaps some other places I am missing?

rossberg · 2023-07-24T08:05:20Z

spectec/src/el/print.ml

@@ -71,8 +71,7 @@ let rec string_of_iter iter =
  | List -> "*"
  | List1 -> "+"
  | ListN (e, None) -> "^" ^ string_of_exp e
-  | ListN (e, Some (id)) ->
-      "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"
+  | ListN (e, Some (id)) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"


I missed this nit before:

Suggested change

| ListN (e, Some (id)) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"

| ListN (e, Some id) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"

rossberg · 2023-07-24T08:06:39Z

spectec/src/frontend/multiplicity.ml

+  | ListN (e, opt) ->
+      Option.iter (fun id -> check_id env (iter::ctx) id) opt;
      check_exp env ctx e


Suggested change

| ListN (e, opt) ->

Option.iter (fun id -> check_id env (iter::ctx) id) opt;

check_exp env ctx e

| ListN (e, id_opt) ->

Option.iter (fun id -> check_id env (ListN (e, None) :: ctx) id) id_opt;

check_exp env ctx e

rossberg · 2023-07-24T08:31:58Z

spectec/src/frontend/multiplicity.ml

+  | ListN (e, None) ->
    let e', occur = annot_exp env e in
-    ListN (e', opt), occur
+    ListN (e', None), occur
+  | ListN (e, Some id) ->
+    let e', occur1 = annot_exp env e in
+    let occur2 = Env.singleton id.it [] in
+    ListN (e', Some id), union occur1 occur2


Suggested change

| ListN (e, None) ->

let e', occur = annot_exp env e in

ListN (e', opt), occur

ListN (e', None), occur

| ListN (e, Some id) ->

let e', occur1 = annot_exp env e in

let occur2 = Env.singleton id.it [] in

ListN (e', Some id), union occur1 occur2

| ListN (e, id_opt) ->

let e', occur1 = annot_exp env e in

let occur2 =

match id_opt with None -> Env.empty | Some id -> Env.singleton id.it [] in

ListN (e', id_opt), union occur1 occur2

rossberg · 2023-07-24T17:25:57Z

spectec/src/frontend/multiplicity.ml

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


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?

rossberg · 2023-07-24T17:26:07Z

spectec/src/frontend/elab.ml

@@ -336,7 +336,7 @@ let rec elab_iter env iter : Il.iter =
  | Opt -> Il.Opt
  | List -> Il.List
  | List1 -> Il.List1
-  | ListN (e, opt) -> Il.ListN (elab_exp env e (NatT $ e.at), opt)
+  | ListN (e, id_opt) -> Il.ListN (elab_exp env e (NatT $ e.at), id_opt)


This also needs to check the type of the id.

ShinWonho · 2023-07-26T07:02:07Z

spectec/src/frontend/elab.ml

+  | ListN (e, id_opt) ->
+    Option.iter (fun id ->
+      let t = find "variable" env.vars (prefix_id id) in
+      if (t.it <> NatT) then error_typ e.at "iteration index" (NatT $ e.at)


I add type check for index variable.
However, there is no region information of index, the error prints the wrong region.

rossberg · 2023-07-26T07:32:57Z

spectec/src/frontend/multiplicity.ml

@@ -160,16 +164,18 @@ type occur = Il.Ast.iter list Env.t
 let union = Env.union (fun _ ctx1 ctx2 -> assert (ctx1 = ctx2); Some ctx1)


+let strip_index = function


This seems to be defined twice in this module.

I defined strip_index for both El and Il. Would it better to use distinct names?

Ah, sorry, missed that. It's fine then.

spectec/src/frontend/elab.ml

rossberg · 2023-07-26T07:43:33Z

spectec/src/frontend/multiplicity.ml

@@ -286,16 +292,12 @@ and annot_iterexp env occur1 (iter, ids) at : Il.Ast.iterexp * occur =
    Env.filter_map (fun _ iters ->
      match iters with
      | [] -> None
-      | iter1::iters' -> assert (Il.Eq.eq_iter iter iter1); Some iters'
+      | iter1::iters' ->
+        assert (Il.Eq.eq_iter (strip_index iter) iter1); Some iters'
    ) occur1
  in
  let ids' = List.map (fun (x, _) -> x $ at) (Env.bindings occur1') in



Suggested change

rossberg · 2023-07-26T07:46:54Z

spectec/src/il/validation.ml

@@ -241,15 +241,7 @@ let valid_list valid_x_y env xs ys at =
 let rec valid_iter env iter =
  match iter with
  | Opt | List | List1 -> ()
-  | ListN (e, None) -> valid_exp env e (NatT $ e.at)
-  | ListN (e, Some id) ->


I think you still need to validate the id here, see comment below.

rossberg · 2023-07-26T07:52:34Z

spectec/src/il/validation.ml

@@ -478,6 +470,11 @@ and valid_path env p t : typ =
  t'

 and valid_iterexp env (iter, ids) : env =
+  let iter =


Ah, sorry for not being clearer. We still need to validate the variable. We only need to strip it for the purpose of the eq_iter check below. Because this combination should be legal:

(...x...)^n (...x...)^(i<n)

Oh, I see. I've fixed it.
Thanks for the comments.

Nit: can we name this iter' to avoid confusion?

Co-authored-by: Andreas Rossberg <[email protected]>

rossberg

Looks good, modulo the two comments below. Thanks!

rossberg · 2023-07-26T08:29:47Z

spectec/src/il/validation.ml

@@ -478,6 +470,11 @@ and valid_path env p t : typ =
  t'

 and valid_iterexp env (iter, ids) : env =
+  let iter =


Nit: can we name this iter' to avoid confusion?

spectec/src/il/validation.ml

Co-authored-by: Andreas Rossberg <[email protected]>

rossberg · 2023-07-27T06:42:45Z

@ShinWonho, I fixed a couple of bugs in the multiplicity annotation and the renderer backend that I had overlooked during the code review. However, the bigger issue I really only noticed now is that the index variable is completely ignored in all the middlend phases. Who will implement this? Or is the plan to have a pass that eliminates the variable first?

ShinWonho · 2023-07-27T07:56:10Z

My naive thought was that introducing 'iter with index' wouldn't affect the middle-end phases.
I'm willing to implement that, but I don't have a deep understanding of middle-end phases, so there could be someone more suited for this task.
Therefore, I suggest discussing it in today's meeting.

Merge with upstream/`wasm-3.0+exn`

ShinWonho and others added 16 commits June 13, 2023 17:30

Change instance representation as record

152b2d0

Add limits check in grow reduction rules

a1c51f9

Add type field in eleminst

5380d76

Type check from updated store

2b82dcc

Consider free variables in premises of DefD

6b6bd32

Add grow helper functions

835bf0d

Fix typos

7d757da

Fix typo in data segment

7aaff60

Draft for module semantics

cecacb5

Add premises for updating store

2a158db

Add premises for start function

066f8c3

Add export allocation

6c7d379

Add import allocation

97d3fe6

Add 7-module.watsup

68c6067

Update TEST.md

b8681db

Fix typo in instantiation

9b3e6e3

rossberg reviewed Jun 27, 2023

View reviewed changes

ShinWonho and others added 8 commits June 28, 2023 16:17

Update grow helper functions

030a3a8

Update spectec/src/frontend/elab.ml

d967107

Co-authored-by: Andreas Rossberg <[email protected]>

Update spectec/src/il/validation.ml

8f6c590

Co-authored-by: Andreas Rossberg <[email protected]>

Refactor module semantics

0f48772

Minor changes

35be3dd

Minor changes

edda75e

Update module semantics

ff216fb

Minor change

21e0a94

ShinWonho commented Jun 30, 2023

View reviewed changes

Minor change

65e6777

rossberg reviewed Jul 14, 2023

View reviewed changes

ShinWonho added 2 commits July 19, 2023 14:08

Merge two render_condition functions

edb1fbf

Merge ListN

8bb5fe0

Fix bug in iter with index

6872abe

rossberg reviewed Jul 21, 2023

View reviewed changes

ShinWonho added 3 commits July 24, 2023 13:19

Minor changes

616eded

Minor change

d764e97

Check iter with index

5c9aed2

rossberg reviewed Jul 24, 2023

View reviewed changes

ShinWonho added 4 commits July 26, 2023 15:04

Minor changes

ba5b056

Strip index variable in iter

31213dd

Add type check for index variable

474c65f

Remove wrong assertion

384016d

ShinWonho commented Jul 26, 2023

View reviewed changes

rossberg reviewed Jul 26, 2023

View reviewed changes

ShinWonho and others added 2 commits July 26, 2023 17:04

Update spectec/src/frontend/elab.ml

fd8ec1f

Co-authored-by: Andreas Rossberg <[email protected]>

Add validation for iter with index

97e95c3

rossberg approved these changes Jul 26, 2023

View reviewed changes

ShinWonho and others added 3 commits July 26, 2023 19:13

Update spectec/src/il/validation.ml

0e45bef

Co-authored-by: Andreas Rossberg <[email protected]>

Minor change

199efd1

Merge branch 'main' into module-semantics

cb45bce

ShinWonho merged commit 056aebe into main Jul 26, 2023
1 check passed

rossberg deleted the module-semantics branch July 27, 2023 06:35

Alan-Liang pushed a commit to Alan-Liang/spectec that referenced this pull request Sep 1, 2024

Merge pull request Wasm-DSL#32 from dhil/wasmfx-merge

0c0fed4

Merge with upstream/`wasm-3.0+exn`

	-- if $table(z, x) = ti
	-- if $grow_table(ti, n, ref) = ti'
	-- if $grow_table($table(z, x), n, ref) = ti'

	-- if $mem(z, 0) = mi
	-- if $grow_memory(mi, n) = mi'
	-- if $grow_memory($mem(z, 0), n) = mi'


		;; Instantiation

		def $instantiation(store, module, externval*) : (store, moduleinst)

		-- if m_res = $alloc_import(m_new, import', externval')


		def $alloc_func(state, func) : (store, funcaddr)

	\| IndexedListN _
	\| ListN _ -> List
	\| ListN _ \| IndexedListN _ -> List

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

	\| ListN (e, id) -> ListN (t_exp env e, id)
	\| ListN (e, id_opt) -> ListN (t_exp env e, id_opt)

	\| ListN (e, id) -> unary t_exp n e (fun e' -> ListN (e', id))
	\| ListN (e, id_opt) -> unary t_exp n e (fun e' -> ListN (e', id_opt))

	\| ListN (e, id) -> unary t_exp env e (fun e' -> ListN (e', id))
	\| ListN (e, id_opt) -> unary t_exp env e (fun e' -> ListN (e', id_opt))

	\| ListN (e, Some (id)) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"
	\| ListN (e, Some id) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"

		@@ -160,16 +164,18 @@ type occur = Il.Ast.iter list Env.t
		let union = Env.union (fun _ ctx1 ctx2 -> assert (ctx1 = ctx2); Some ctx1)


		let strip_index = function

DSL for module semantics #32

DSL for module semantics #32

Conversation

ShinWonho commented Jun 26, 2023

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jun 30, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jun 30, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jun 30, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jul 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jun 30, 2023 • edited Loading

Choose a reason for hiding this comment

rossberg Jul 4, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jul 5, 2023 • edited Loading

Choose a reason for hiding this comment

ShinWonho commented Jul 14, 2023

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jul 19, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jul 19, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho commented Jul 20, 2023

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho commented Jul 24, 2023

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ShinWonho Jun 30, 2023 •

edited

Loading

ShinWonho Jun 30, 2023 •

edited

Loading

ShinWonho Jun 30, 2023 •

edited

Loading

ShinWonho Jul 5, 2023 •

edited

Loading

ShinWonho Jun 30, 2023 •

edited

Loading

rossberg Jul 4, 2023 •

edited

Loading

ShinWonho Jul 5, 2023 •

edited

Loading

ShinWonho Jul 19, 2023 •

edited

Loading

ShinWonho Jul 19, 2023 •

edited

Loading

ShinWonho Jul 26, 2023 •

edited

Loading