Merge branch 'main' into ref.null

spectec/spec/wasm-1.0/6-typing.watsup

@@ -136,7 +136,7 @@ rule Instrs_ok/empty:
 rule Instrs_ok/seq:
   C |- instr_1 instr_2* : t_1* -> t_3*
   -- Instr_ok: C |- instr_1 : t_1* -> t_2*
-  -- Instrs_ok: C |- instr_2 : t_2* -> t_3*
+  -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/frame:
   C |- instr* : t* t_1* -> t* t_2*

spectec/spec/wasm-1.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -21,12 +21,12 @@ rule Steps/refl:
 rule Steps/trans:
   z; admininstr*  ~>*  z''; admininstr''*
   -- Step: z; admininstr*  ~>  z'; admininstr'*
-  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+  -- Steps: z'; admininstr'*  ~>*  z''; admininstr''*
 
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-2.0/6-typing.watsup

@@ -153,7 +153,7 @@ rule Instrs_ok/empty:
 rule Instrs_ok/seq:
   C |- instr_1 instr_2* : t_1* -> t_3*
   -- Instr_ok: C |- instr_1 : t_1* -> t_2*
-  -- Instrs_ok: C |- instr_2 : t_2* -> t_3*
+  -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/sub:
   C |- instr* : t'_1* -> t'_2*

spectec/spec/wasm-2.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -21,12 +21,12 @@ rule Steps/refl:
 rule Steps/trans:
   z; admininstr*  ~>*  z''; admininstr''*
   -- Step: z; admininstr*  ~>  z'; admininstr'*
-  -- Steps: z'; admininstr'  ~>*  z''; admininstr''*
+  -- Steps: z'; admininstr'*  ~>*  z''; admininstr''*
 
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -644,7 +644,7 @@ def $unrolldt(DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype
 
 def $expanddt(deftype) = comptype              -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
-relation Expand: deftype ~~ comptype hint(macro "%expanddt")
+relation Expand: deftype ~~ comptype hint(macro "%expanddt") hint(tabular)
 rule Expand: deftype ~~ comptype               -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
 

spectec/spec/wasm-3.0/6-typing.watsup

@@ -1402,5 +1402,5 @@ rule Globals_ok/empty:
 
 rule Globals_ok/cons:
   C |- global_1 global* : gt_1 gt*
-  -- Global_ok: C |- global : gt_1
+  -- Global_ok: C |- global_1 : gt_1
   -- Globals_ok: C ++ {GLOBALS gt_1} |- global* : gt*

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config       hint(show "E") hint(macro "stepto")
-relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto")
-relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto")
-relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar")
+relation Step: config ~> config       hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -21,12 +21,12 @@ rule Steps/refl:
 rule Steps/trans:
   z; instr*  ~>*  z''; instr''*
   -- Step: z; instr*  ~>  z'; instr'*
-  -- Steps: z'; instr'  ~>*  z''; instr''*
+  -- Steps: z'; instr'*  ~>*  z''; instr''*
 
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-3.0/C-conventions.watsup

@@ -52,7 +52,7 @@ rule NotationTypingInstrScheme/block:
 
 ;; Execution notation
 
-relation NotationReduct: ~> instr*
+relation NotationReduct: ~> instr* hint(tabular)
 
 rule NotationReduct/2:
   ~> (CONST F64 q_1) (CONST F64 q_4) (CONST F64 q_3) $($(BINOP F64 ADD)) $($(BINOP F64 MUL))

spectec/src/al/al_util.ml

@@ -58,7 +58,7 @@ let tupE ?(at = no) ~note el = TupE el |> mk_expr at note
 let caseE ?(at = no) ~note (op, el) = CaseE (op, el) |> mk_expr at note
 let callE ?(at = no) ~note (id, el) = CallE (id, el) |> mk_expr at note
 let invCallE ?(at = no) ~note (id, il, el) = InvCallE (id, il, el) |> mk_expr at note
-let iterE ?(at = no) ~note (e, idl, it) = IterE (e, idl, it) |> mk_expr at note
+let iterE ?(at = no) ~note (e, ite) = IterE (e, ite) |> mk_expr at note
 let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
 let listE ?(at = no) ~note el = ListE el |> mk_expr at note
 let arityE ?(at = no) ~note e = ArityE e |> mk_expr at note
@@ -105,6 +105,10 @@ let zero = numV Z.zero
 let one = numV Z.one
 let empty_list = listV [||]
 let singleton v = listV [|v|]
+let iter_var ?(at = no) x iter t =
+  let xs = x ^ (match iter with Opt -> "?" | _ -> "*") in
+  let il_iter = match iter with Opt -> Il.Ast.Opt | _ -> Il.Ast.List in
+  iterE (varE x ~at:at ~note:t, (iter, [x, varE xs ~at:at ~note:(Il.Ast.IterT (t, il_iter) $ t.at)])) ~at:at ~note:t
 
 
 let some x = caseV (x, [optV (Some (tupV []))])
@@ -191,6 +195,10 @@ let unwrap_listv: value -> value growable_array = function
 let unwrap_listv_to_array (v: value): value array = !(unwrap_listv v)
 let unwrap_listv_to_list (v: value): value list = unwrap_listv_to_array v |> Array.to_list
 
+let unwrap_seqv_to_list: value -> value list = function
+  | OptV opt -> Option.to_list opt
+  | ListV arr -> Array.to_list !arr
+  | v -> fail_value "unwrap_seqv_to_list" v
 let unwrap_seq_to_array: value -> value array = function
   | OptV opt -> opt |> Option.to_list |> Array.of_list
   | v -> unwrap_listv_to_array v

spectec/src/al/ast.ml

@@ -97,7 +97,7 @@ and expr' =
   | CaseE of mixop * expr list                    (* mixop `(` expr* `)` -- CaseE *)
   | CallE of id * arg list                        (* id `(` expr* `)` *)
   | InvCallE of id * int option list * arg list   (* id`_`int*`^-1(` expr* `)` *)
-  | IterE of expr * id list * iter                (* expr (`{` id* `}`)* *)
+  | IterE of expr * iterexp                       (* expr (`{` id* `}`)* *)
   | OptE of expr option                           (* expr?  *)
   | ListE of expr list                            (* `[` expr* `]` *)
   | ArityE of expr                                (* "the arity of expr" *)
@@ -137,6 +137,8 @@ and arg' =
   | TypA of typ
   | DefA of id
 
+and iterexp = iter * (id * expr) list
+
 (* Instructions *)
 
 type instr = (instr', int) note_phrase

spectec/src/al/eq.ml

@@ -4,10 +4,14 @@ open Source
 
 let eq_list eq l1 l2 =
   List.length l1 = List.length l2 && List.for_all2 eq l1 l2
+let eq_pair eqx eqy (x1, y1) (x2, y2) =
+  eqx x1 x2 && eqy y1 y2
+
+let eq_id = (=)
 
 let rec eq_expr e1 e2 =
   match e1.it, e2.it with
-  | VarE id1, VarE id2 -> id1 = id2
+  | VarE id1, VarE id2 -> eq_id id1 id2
   | NumE n1, NumE n2 -> n1 = n2
   | BoolE b1, BoolE b2 -> b1 = b2
   | UnE (unop1, e1), UnE (unop2, e2) -> unop1 = unop2 && eq_expr e1 e2
@@ -28,8 +32,8 @@ let rec eq_expr e1 e2 =
   | CallE (i1, al1), CallE (i2, al2) -> i1 = i2 && eq_args al1 al2
   | InvCallE (i1, nl1, al1), InvCallE (i2, nl2, al2) ->
     i1 = i2 && List.for_all2 (=) nl1 nl2 && eq_args al1 al2
-  | IterE (e1, il1, it1), IterE (e2, il2, it2) ->
-    eq_expr e1 e2 && il1 = il2 && it1 = it2
+  | IterE (e1, ie1), IterE (e2, ie2) ->
+    eq_expr e1 e2 && eq_iterexp ie1 ie2
   | OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
   | ListE el1, ListE el2 -> eq_exprs el1 el2
   | ArityE e1, ArityE e2 -> eq_expr e1 e2
@@ -73,6 +77,15 @@ and eq_expr_record r1 r2 =
 and eq_exprs el1 el2 = eq_list eq_expr el1 el2
 
 
+and eq_iter i1 i2 =
+  match i1, i2 with
+  | Opt, Opt -> true
+  | List, List -> true
+  | List1, List1 -> true
+  | ListN (e1, id_opt1), ListN (e2, id_opt2) -> eq_expr e1 e2 && Option.equal eq_id id_opt1 id_opt2
+  | _ -> false
+
+
 and eq_path p1 p2 =
   match p1.it, p2.it with
   | IdxP e1, IdxP e2 -> eq_expr e1 e2
@@ -92,6 +105,11 @@ and eq_arg a1 a2 =
 
 and eq_args al1 al2 = eq_list eq_arg al1 al2
 
+
+and eq_iterexp (iter1, xes1) (iter2, xes2) =
+  eq_iter iter1 iter2 && eq_list (eq_pair eq_id eq_expr) xes1 xes2
+
+
 let rec eq_instr i1 i2 =
   match i1.it, i2.it with
   | IfI (e1, il11, il12), IfI (e2, il21, il22) ->
@@ -111,7 +129,7 @@ let rec eq_instr i1 i2 =
   | ReturnI e_opt1, ReturnI e_opt2 -> eq_expr_opt e_opt1 e_opt2
   | ExecuteI e1, ExecuteI e2
   | ExecuteSeqI e1, ExecuteSeqI e2 -> eq_expr e1 e2
-  | PerformI (id1, al1), PerformI (id2, al2) -> id1 = id2 && eq_args al1 al2
+  | PerformI (id1, al1), PerformI (id2, al2) -> eq_id id1 id2 && eq_args al1 al2
   | ExitI a1, ExitI a2 -> El.Atom.eq a1 a2
   | ReplaceI (e11, p1, e12), ReplaceI (e21, p2, e22) ->
     eq_expr e11 e21 && eq_path p1 p2 && eq_expr e12 e22

spectec/src/al/free.ml

@@ -2,15 +2,18 @@ open Ast
 open Util
 open Source
 
-(* TODO: Change list to set *)
 module IdSet = Set.Make (String)
 
 (* Expressions *)
 
 let (@) = IdSet.union
+let (-) = IdSet.diff
 let free_opt free_x xo = Option.(value (map free_x xo) ~default:IdSet.empty)
 let free_list free_x xs = List.(fold_left IdSet.union IdSet.empty (map free_x xs))
 
+
+let free_id = IdSet.singleton
+
 let rec free_expr expr =
   match expr.it with
   | NumE _
@@ -22,7 +25,7 @@ let rec free_expr expr =
   | ContextKindE _
   | YetE _ -> IdSet.empty
   | VarE id
-  | SubE (id, _) -> IdSet.singleton id
+  | SubE (id, _) -> free_id id
   | UnE (_, e)
   | LenE e
   | ArityE e
@@ -44,7 +47,12 @@ let rec free_expr expr =
   | ExtE (e1, ps, e2, _)
   | UpdE (e1, ps, e2) -> free_expr e1 @ free_list free_path ps @ free_expr e2
   | OptE e_opt -> free_opt free_expr e_opt
-  | IterE (e, _, i) -> free_expr e @ free_iter i
+  | IterE (e, ie) ->
+    (* We look for semantic free variables, not the syntactic free variables. *)
+    (* Therefore, in the expression `x*{x <- xs}`, xs is free, but x is not. *)
+    let free1 = free_expr e in
+    let bound, free2 = free_iterexp ie in
+    (free1 - bound) @ free2
   | MatchE (e1, e2) -> free_expr e1 @ free_expr e2
   | TopLabelE
   | TopFrameE
@@ -76,13 +84,23 @@ and free_path path =
 
 
 (* Args *)
+
 and free_arg arg =
   match arg.it with
   | ExpA e -> free_expr e
   | TypA _
   | DefA _ -> IdSet.empty
 
 
+(* Iter exps *)
+
+and free_iterexp (iter, xes) =
+  let xs, es = List.split xes in
+  let bound = free_list free_id xs in
+  let free = free_iter iter @ free_list free_expr es in
+  bound, free
+
+
 (* Instructions *)
 
 let rec free_instr instr =

spectec/src/al/free.mli

@@ -1,6 +1,6 @@
 open Ast
 
-module IdSet : Set.S with type elt = string
+module IdSet : Set.S with type elt = string with type t = Set.Make(String).t
 
 val free_list : ('a -> IdSet.t) -> 'a list -> IdSet.t
 val free_expr : expr -> IdSet.t

spectec/src/al/print.ml

@@ -177,7 +177,7 @@ and string_of_expr expr =
     sprintf "label(%s, %s)" (string_of_expr e1) (string_of_expr e2)
   | VarE id -> id
   | SubE (id, _) -> id
-  | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
+  | IterE (e, ie) -> string_of_expr e ^ string_of_iterexp ie
   | CaseE ([{ it=Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
   | CaseE ([[ atom ]], []) -> string_of_atom atom
@@ -241,6 +241,14 @@ and string_of_arg arg =
 and string_of_args sep = string_of_list string_of_arg sep
 
 
+
+(* Iter exps *)
+
+and string_of_iterexp (iter, xes) =
+  string_of_iter iter ^ "{" ^ String.concat ", "
+    (List.map (fun (id, e) -> id ^ " <- " ^ string_of_expr e) xes) ^ "}"
+
+
 (* Instructions *)
 
 let _index = ref 0
@@ -382,11 +390,6 @@ let string_of_algorithm algo =
 
 (* Wasm type *)
 
-(* Names *)
-
-let structured_string_of_ids ids =
-  "[" ^ String.concat ", " ids ^ "]"
-
 
 (* Values *)
 
@@ -510,14 +513,14 @@ and structured_string_of_expr expr =
     ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
   | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
-  | IterE (e, ids, iter) ->
+  | IterE (e, (iter, xes)) ->
     "IterE ("
     ^ structured_string_of_expr e
-    ^ ", "
-    ^ structured_string_of_ids ids
-    ^ ", "
-    ^ string_of_iter iter
-    ^ ")"
+    ^ ", ("
+    ^ structured_string_of_iter iter
+    ^ ", {"
+    ^ string_of_list (fun (x, e) -> x ^ structured_string_of_expr e) ", " xes
+    ^ "}))"
   | CaseE (op, el) ->
     "CaseE (" ^ string_of_mixop op
     ^ ", [" ^ structured_string_of_exprs el ^ "])"