Merge branch 'main' into prose-enter-exit

Wasm-DSL · Apr 9, 2024 · 7b68243 · 7b68243
2 parents b1064ed + 945af10
commit 7b68243
Show file tree

Hide file tree

Showing 8 changed files with 416 additions and 390 deletions.
diff --git a/papers/README.md b/papers/README.md
@@ -13,3 +13,11 @@
   ACM-SIGPLAN Conference on Object-Oriented Programming, Systems, Language and Architectures (OOSPLA 2019)
 
   *Describes and formalises the extension of WebAssembly with threads and a suitable memory model.*
+
+* [Bringing the WebAssembly Standard up to Speed with SpecTec](pldi2024.pdf)
+
+  Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Rao Xiaojia, Conrad Watt, Andreas Rossberg
+
+  ACM-SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024)
+
+  *Describes the design and implementation of Wasm SpecTec.*
diff --git a/papers/pldi2024.pdf b/papers/pldi2024.pdf
diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -419,7 +419,7 @@ syntax instr/vec hint(desc "vector instruction") = ...
     ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
   | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
-  | VCVTOP shape vcvtop half? shape sx? zero?
+  | VCVTOP shape shape vcvtop half? sx? zero?
     hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%#_#%)
     ;; TODO: missing constraints
   | ...

diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup
@@ -354,7 +354,7 @@ rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128
 
 rule Instr_ok/vcvtop:
-  C |- VCVTOP sh_1 vcvtop hf? sh_2 sx? zero? : V128 -> V128
+  C |- VCVTOP sh_1 sh_2 vcvtop hf? sx? zero? : V128 -> V128
 
 
 ;; Local instructions

diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -323,18 +323,18 @@ rule Step_pure/vnarrow:
 
 
 rule Step_pure/vcvtop-full:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop eps (lnn_1 X N_1) sx) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop eps sx) ~> (VCONST V128 c)
   -- if c'* = $lanes_(lnn_1 X N_1, c_1)
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx, c')*)
 
 var hf : half  ;; TODO: this declaration shouldn't be needed
 rule Step_pure/vcvtop-half:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop hf (lnn_1 X N_1) sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop hf sx?) ~> (VCONST V128 c)
   -- if ci* = $lanes_(lnn_1 X N_1, c_1)[$halfop(hf, 0, N_2) : N_2]
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx?, ci)*)
 
 rule Step_pure/vcvtop-zero:
-  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) vcvtop eps (nt_1 X N_1) sx? ZERO) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) (nt_1 X N_1) vcvtop eps sx? ZERO) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X N_1, c_1)
   -- if c = $invlanes_(nt_2 X N_2, $vcvtop(nt_1 X N_1, nt_2 X N_2, vcvtop, sx?, ci)* $zero(nt_2)^N_1)
 

diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -615,10 +615,10 @@ grammar Binstr/vector-v-i16x8 : instr = ...
   | 0xFD 132:Bu32 => VBITMASK (I16 X 8)
   | 0xFD 133:Bu32 => VNARROW (I16 X 8) (I32 X 4) S
   | 0xFD 134:Bu32 => VNARROW (I16 X 8) (I32 X 4) U
-  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) S
-  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) S
-  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) U
-  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) U
+  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW S
+  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH S
+  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW U
+  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH U
   | 0xFD 139:Bu32 => VSHIFTOP (I16 X 8) SHL
   | 0xFD 140:Bu32 => VSHIFTOP (I16 X 8) (SHR S)
   | 0xFD 141:Bu32 => VSHIFTOP (I16 X 8) (SHR U)
@@ -647,10 +647,10 @@ grammar Binstr/vector-v-i32x4 : instr = ...
   | 0xFD 161:Bu32 => VUNOP (I32 X 4) NEG
   | 0xFD 163:Bu32 => VTESTOP (I32 X 4) ALL_TRUE
   | 0xFD 164:Bu32 => VBITMASK (I32 X 4)
-  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) S
-  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) S
-  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) U
-  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) U
+  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW S
+  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH S
+  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW U
+  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH U
   | 0xFD 171:Bu32 => VSHIFTOP (I32 X 4) SHL
   | 0xFD 172:Bu32 => VSHIFTOP (I32 X 4) (SHR S)
   | 0xFD 173:Bu32 => VSHIFTOP (I32 X 4) (SHR U)
@@ -673,10 +673,10 @@ grammar Binstr/vector-v-i64x2 : instr = ...
   | 0xFD 193:Bu32 => VUNOP (I64 X 2) NEG
   | 0xFD 195:Bu32 => VTESTOP (I64 X 2) ALL_TRUE
   | 0xFD 196:Bu32 => VBITMASK (I64 X 2)
-  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) S
-  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) S
-  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) U
-  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) U
+  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW S
+  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH S
+  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW U
+  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH U
   | 0xFD 203:Bu32 => VSHIFTOP (I64 X 2) SHL
   | 0xFD 204:Bu32 => VSHIFTOP (I64 X 2) (SHR S)
   | 0xFD 205:Bu32 => VSHIFTOP (I64 X 2) (SHR U)
@@ -726,16 +726,16 @@ grammar Binstr/vector-v-f64x2 : instr = ...
   | ...
 
 grammar Binstr/vector-cvt : instr = ...
-  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) S
-  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) U
-  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) S
-  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) U
-  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) S ZERO
-  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) U ZERO
-  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) S
-  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) U
-  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) DEMOTE (F64 X 2) ZERO
-  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) PROMOTE LOW (F32 X 4)
+  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT S
+  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT U
+  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT S
+  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT U
+  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT S ZERO
+  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT U ZERO
+  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW S
+  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW U
+  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) (F64 X 2) DEMOTE ZERO
+  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) (F32 X 4) PROMOTE LOW
 
 
 ;; Expressions

diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml
@@ -107,66 +107,72 @@ let _unified_idx = ref 0
 let init_unified_idx () = _unified_idx := 0
 let get_unified_idx () = let i = !_unified_idx in _unified_idx := (i+1); i
 let gen_new_unified ty = (type_to_id ty) ^ "_" ^ unified_prefix ^ (string_of_int (get_unified_idx())) $ no_region
-let to_iter e iterexp = IterE (e, iterexp)
 let is_unified_id id = String.split_on_char '_' id |> Util.Lib.List.last |> String.starts_with ~prefix:unified_prefix
 
 let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else
-  let it =
-    match e1.it, e2.it with
-    | VarE id, _
-    | IterE ({ it = VarE id; _}, _) , _
-      when is_unified_id id.it -> e1.it
+  let replace_it it = { e1 with it = it } in
+  match e1.it, e2.it with
+    (* Already unified *)
+    | VarE id, _ when is_unified_id id.it ->
+      e1
+    | IterE ({ it = VarE id; _} as e, (iter, _)), _  when is_unified_id id.it ->
+      let t = overlap_typ e1.note e2.note in
+      let i = (iter, [(id, t)]) in
+      { e1 with it = IterE (e, i); note = t }
+    (* Not unified *)
     | UnE (unop1, e1), UnE (unop2, e2) when unop1 = unop2 ->
-      UnE (unop1, overlap e1 e2)
+      UnE (unop1, overlap e1 e2) |> replace_it
     | BinE (binop1, e1, e1'), BinE (binop2, e2, e2') when binop1 = binop2 ->
-      BinE (binop1, overlap e1 e2, overlap e1' e2')
+      BinE (binop1, overlap e1 e2, overlap e1' e2') |> replace_it
     | CmpE (cmpop1, e1, e1'), CmpE (cmpop2, e2, e2') when cmpop1 = cmpop2 ->
-      CmpE (cmpop1, overlap e1 e2, overlap e1' e2')
+      CmpE (cmpop1, overlap e1 e2, overlap e1' e2') |> replace_it
     | IdxE (e1, e1'), IdxE (e2, e2') ->
-      IdxE (overlap e1 e2, overlap e1' e2')
+      IdxE (overlap e1 e2, overlap e1' e2') |> replace_it
     | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') ->
-      SliceE (overlap e1 e2, overlap e1' e2', overlap e1'' e2'')
+      SliceE (overlap e1 e2, overlap e1' e2', overlap e1'' e2'') |> replace_it
     | UpdE (e1, path1, e1'), UpdE (e2, path2, e2') when eq_path path1 path2 ->
-      UpdE (overlap e1 e2, path1, overlap e1' e2')
+      UpdE (overlap e1 e2, path1, overlap e1' e2') |> replace_it
     | ExtE (e1, path1, e1'), ExtE (e2, path2, e2') when eq_path path1 path2 ->
-      ExtE (overlap e1 e2, path1, overlap e1' e2')
+      ExtE (overlap e1 e2, path1, overlap e1' e2') |> replace_it
     | StrE efs1, StrE efs2 when List.map fst efs1 = List.map fst efs2 ->
-      StrE (List.map2 (fun (a1, e1) (_, e2) -> (a1, overlap e1 e2)) efs1 efs2)
+      StrE (List.map2 (fun (a1, e1) (_, e2) -> (a1, overlap e1 e2)) efs1 efs2) |> replace_it
     | DotE (e1, atom1), DotE (e2, atom2) when eq_atom atom1 atom2 ->
-      DotE (overlap e1 e2, atom1)
+      DotE (overlap e1 e2, atom1) |> replace_it
     | CompE (e1, e1'), CompE (e2, e2') ->
-      CompE (overlap e1 e2, overlap e1' e2')
+      CompE (overlap e1 e2, overlap e1' e2') |> replace_it
     | LenE e1, LenE e2 ->
-      LenE (overlap e1 e2)
+      LenE (overlap e1 e2) |> replace_it
     | TupE es1, TupE es2 when List.length es1 = List.length es2 ->
-      TupE (List.map2 overlap es1 es2)
+      TupE (List.map2 overlap es1 es2) |> replace_it
     | CallE (id1, as1), CallE (id2, as2) when eq_id id1 id2 ->
-      CallE (id1, List.map2 overlap_arg as1 as2)
+      CallE (id1, List.map2 overlap_arg as1 as2) |> replace_it
     | IterE (e1, itere1), IterE (e2, itere2) when eq_iterexp itere1 itere2 ->
-      IterE (overlap e1 e2, itere1)
+      IterE (overlap e1 e2, itere1) |> replace_it
     | ProjE (e1, i1), ProjE (e2, i2) when i1 = i2 ->
-      ProjE (overlap e1 e2, i1)
+      ProjE (overlap e1 e2, i1) |> replace_it
     | UncaseE (e1, op1), UncaseE (e2, op2) when eq_mixop op1 op2 ->
-      UncaseE (overlap e1 e2, op1)
+      UncaseE (overlap e1 e2, op1) |> replace_it
     | OptE (Some e1), OptE (Some e2) ->
-      OptE (Some (overlap e1 e2))
+      OptE (Some (overlap e1 e2)) |> replace_it
     | TheE e1, TheE e2 ->
-      TheE (overlap e1 e2)
+      TheE (overlap e1 e2) |> replace_it
     | ListE es1, ListE es2 when List.length es1 = List.length es2 ->
-      ListE (List.map2 overlap es1 es2)
+      ListE (List.map2 overlap es1 es2) |> replace_it
     | CatE (e1, e1'), CatE (e2, e2') ->
-      CatE (overlap e1 e2, overlap e1' e2')
+      CatE (overlap e1 e2, overlap e1' e2') |> replace_it
     | CaseE (mixop1, e1), CaseE (mixop2, e2) when eq_mixop mixop1 mixop2 ->
-      CaseE (mixop1, overlap e1 e2)
+      CaseE (mixop1, overlap e1 e2) |> replace_it
     | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' ->
-      SubE (overlap e1 e2, typ1, typ1')
+      SubE (overlap e1 e2, typ1, typ1') |> replace_it
     | _ ->
-      let ty = e1.note in
+      let ty = overlap_typ e1.note e2.note in
       let id = gen_new_unified ty in
-      match ty.it with
-      | IterT (ty, iter) -> to_iter (VarE id $$ no_region % ty) (iter, [(id, ty)])
-      | _ -> VarE id
-  in { e1 with it }
+      let it =
+        match ty.it with
+        | IterT (ty, iter) -> IterE (VarE id $$ no_region % ty, (iter, [(id, ty)]))
+        | _ -> VarE id
+      in
+      { e1 with it = it; note = ty }
 
 and overlap_arg a1 a2 = if eq_arg a1 a2 then a1 else
   (match a1.it, a2.it with
@@ -175,6 +181,17 @@ and overlap_arg a1 a2 = if eq_arg a1 a2 then a1 else
     | _, _ -> assert false
   ) $ a1.at
 
+and overlap_typ t1 t2 = if eq_typ t1 t2 then t1 else
+  (match t1.it, t2.it with
+    | VarT (id1, args1), VarT (id2, args2) when id1 = id2 ->
+      VarT (id1, List.map2 overlap_arg args1 args2)
+    | TupT ets1, TupT ets2 when List.for_all2 (fun (e1, _) (e2, _) -> eq_exp e1 e2) ets1 ets2 ->
+      TupT (List.map2 (fun (e1, t1) (_, t2) -> (e1, overlap_typ t1 t2)) ets1 ets2)
+    | IterT (t1, iter1), IterT (t2, iter2) when eq_iter iter1 iter2 ->
+      IterT (overlap_typ t1 t2, iter1)
+    | _ -> assert false (* Unreachable due to IL validation *)
+  ) $ t1.at
+
 let pairwise_concat (a,b) (c,d) = (a@c, b@d)
 
 let rec collect_unified template e = if eq_exp template e then [], [] else