Merge pull request #101 from Wasm-DSL/bug.invoke-typechecks

Activate runtime type checks

spectec/spec/wasm-3.0/9-module.watsup

@@ -151,8 +151,8 @@ def $rundata_(x, DATA b^n (ACTIVE y instr*)) =
 def $instantiate(store, module, externval*) : config
 def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* instr_S?
   ---- ----
-  ;; TODO(1, ShinWonho rossberg, #101): -- Module_ok: |- module : xt_I* -> xt_E*
-  ;; TODO(1, ShinWonho rossberg, #101): -- (Externval_type: s |- externval : xt_I)*
+  -- Module_ok: |- module : xt_I* -> xt_E*
+  -- (Externval_type: s |- externval : xt_I)*
   ----
   -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
   -- if global* = (GLOBAL globaltype expr_G)*
@@ -185,5 +185,5 @@ def $invoke(store, funcaddr, val*) : config
 def $invoke(s, funcaddr, val*) = s; f; val* (REF.FUNC_ADDR funcaddr) (CALL_REF s.FUNCS[funcaddr].TYPE)
   ---- ----
   -- Expand: s.FUNCS[funcaddr].TYPE ~~ FUNC (t_1* -> t_2*)
-  ;; TODO(1, ShinWonho rossberg, #101): -- (Val_type: s |- val : t_1)*
+  -- (Val_type: s |- val : t_1)*
   -- if f = {MODULE {}}  ;; TODO(2, rossberg): inline

spectec/src/backend-interpreter/interpreter.ml

@@ -697,20 +697,20 @@ and create_context (name: string) (args: value list) : AlContext.mode =
 
   AlContext.al (name, body, env)
 
-and call_func (fname: string) (args: value list) : value option =
+and call_func (name: string) (args: value list) : value option =
   (* Module & Runtime *)
-  if bound_func fname then
-    [create_context fname args]
+  if bound_func name then
+    [create_context name args]
     |> run
     |> AlContext.get_return_value
   (* Numerics *)
-  else if Numerics.mem fname then
-    Some (Numerics.call_numerics fname args)
+  else if Numerics.mem name then
+    Some (Numerics.call_numerics name args)
   (* Manual *)
-  else if fname = "ref_type_of" then
-    Some (Manual.ref_type_of args)
+  else if Manual.mem name then
+    Some (Manual.call_func name args)
   else
-    raise (Exception.InvalidFunc ("Invalid DSL function: " ^ fname))
+    raise (Exception.InvalidFunc ("Invalid DSL function: " ^ name))
 
 
 (* Wasm interpreter entry *)

spectec/src/backend-interpreter/manual.ml

@@ -2,7 +2,9 @@ open Al
 open Ast
 open Al_util
 
-let ref_type_of =
+module FuncMap = Map.Make (String)
+
+let ref_type =
   (* TODO: some / none *)
   let null = caseV ("NULL", [ optV (Some (listV [||])) ]) in
   let nonull = caseV ("NULL", [ optV None ]) in
@@ -27,7 +29,7 @@ let ref_type_of =
     else if match_heap_type noextern ht then
       CaseV ("REF", [ null; noextern])
     else
-      Numerics.error_typ_value "$ref_type_of" "null reference" v
+      Numerics.error_typ_value "$Ref_type" "null reference" v
   (* i31 *)
   | [CaseV ("REF.I31_NUM", [ _ ])] -> CaseV ("REF", [ nonull; nullary "I31"])
   (* host *)
@@ -42,4 +44,12 @@ let ref_type_of =
   (* extern *)
   (* TODO: check null *)
   | [CaseV ("REF.EXTERN", [ _ ])] -> CaseV ("REF", [ nonull; nullary "EXTERN"])
-  | vs -> Numerics.error_values "$ref_type_of" vs
+  | vs -> Numerics.error_values "$Ref_type" vs
+
+let manual_map = FuncMap.add "Ref_type" ref_type FuncMap.empty
+
+let mem name = FuncMap.mem name manual_map
+
+let call_func name args =
+  let func = FuncMap.find name manual_map in
+  func args

spectec/src/backend-interpreter/manual.mli

@@ -1,3 +1,5 @@
 open Al.Ast
 
-val ref_type_of : value list -> value
+val mem : string -> bool
+
+val call_func : string -> value list -> value

spectec/src/exe-watsup/main.ml

@@ -19,7 +19,6 @@ type pass =
   | Unthe
   | Wild
   | Sideconditions
-  | Animate
 
 (* This list declares the intended order of passes.
 
@@ -28,7 +27,7 @@ passers (--all-passes, some targets), we do _not_ want to use the order of
 flags on the command line.
 *)
 let _skip_passes = [ Sub; Unthe ]  (* Not clear how to extend them to indexed types *)
-let all_passes = [ Totalize; Wild; Sideconditions; Animate ]
+let all_passes = [ Totalize; Wild; Sideconditions ]
 
 type file_kind =
   | Spec
@@ -74,23 +73,20 @@ let pass_flag = function
   | Unthe -> "the-elimination"
   | Wild -> "wildcards"
   | Sideconditions -> "sideconditions"
-  | Animate -> "animate"
 
 let pass_desc = function
   | Sub -> "Synthesize explicit subtype coercions"
   | Totalize -> "Run function totalization"
   | Unthe -> "Eliminate the ! operator in relations"
   | Wild -> "Eliminate wildcards and equivalent expressions"
   | Sideconditions -> "Infer side conditions"
-  | Animate -> "Animate equality conditions"
 
 let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | Sub -> Middlend.Sub.transform
   | Totalize -> Middlend.Totalize.transform
   | Unthe -> Middlend.Unthe.transform
   | Wild -> Middlend.Wild.transform
   | Sideconditions -> Middlend.Sideconditions.transform
-  | Animate -> Il2al.Animate.transform
 
 
 (* Argument parsing *)
@@ -177,9 +173,9 @@ let () =
 
     (match !target with
     | Prose | Splice _ | Interpreter _ ->
-      enable_pass Sideconditions; enable_pass Animate
+      enable_pass Sideconditions;
     | _ when !print_al || !print_al_o <> "" ->
-      enable_pass Sideconditions; enable_pass Animate
+      enable_pass Sideconditions;
     | _ -> ()
     );
 

spectec/src/il2al/animate.ml

@@ -220,6 +220,8 @@ let build_matrix prems known_vars =
 
 (* Pre-process a premise *)
 let rec pre_process prem = match prem.it with
+  | IterPr (prem, iterexp) ->
+    List.map (fun pr -> { prem with it=IterPr (pr, iterexp) }) (pre_process prem)
   (* HARDCODE: translation of `Expand: dt ~~ ct` into `$expanddt(dt) = ct` *)
   | RulePr (
       { it = "Expand"; _ },
@@ -228,6 +230,10 @@ let rec pre_process prem = match prem.it with
     ) ->
       let expanded_dt = { dt with it = CallE ("expanddt" $ no_region, [ExpA dt $ no_region]); note = ct.note } in
       [ { prem with it = IfPr (CmpE (EqOp, expanded_dt, ct) $$ no_region % (BoolT $ no_region)) } ]
+  | RulePr (id, _, { it=TupE [_context; lhs; rhs]; at; note })
+  when String.ends_with ~suffix:"_type" id.it ->
+    let typing_function_call = { it=CallE (id, [ExpA lhs $ lhs.at]); at; note } in
+    [ { prem with it=IfPr (CmpE (EqOp, typing_function_call, rhs) $$ at % note) } ]
   (* Split -- if e1 /\ e2 *)
   | IfPr ( { it = BinE (AndOp, e1, e2); _ } ) ->
     let p1 = { prem with it = IfPr ( e1 ) } in

spectec/src/il2al/translate.ml

@@ -804,10 +804,20 @@ let translate_rulepr id exp =
       letI (rhs, callE ("eval_expr", [ lhs ])) ~at:at;
       popI (frameE (None, z));
     ]
-  | "Ref_type", [_s; ref; rt] ->
-    [ letI (rt, callE ("ref_type_of", [ ref ]) ~at:at) ~at:at ]
-  | "Reftype_sub", [_C; rt1; rt2] ->
+  (* ".*_sub" *)
+  | name, [_C; rt1; rt2]
+    when String.ends_with ~suffix:"_sub" name ->
     [ ifI (matchE (rt1, rt2) ~at:at, [], []) ~at:at ]
+  (* ".*_ok" *)
+  | name, el when String.ends_with ~suffix: "_ok" name ->
+    (match el with
+    | [_; e; t] | [e; t] -> [ assertI (callE (name, [e; t]) ~at:at) ~at:at]
+    | _ -> error_exp exp "unrecognized form of argument in rule_ok"
+    )
+  (* ".*_const" *)
+  | name, el
+    when String.ends_with ~suffix: "_const" name ->
+    [ assertI (callE (name, el) ~at:at) ~at:at]
   | _ ->
     print_yet exp.at "translate_rulepr" ("`" ^ Il.Print.string_of_exp exp ^ "`");
     [ yetI ("TODO: translate_rulepr " ^ id.it) ~at:at ]
@@ -1261,5 +1271,5 @@ let translate_rules il =
 
 (* Entry *)
 let translate il =
-  let il = List.concat_map flatten_rec il in
-  translate_helpers il @ translate_rules il
+  let il' = il |> Animate.transform |> List.concat_map flatten_rec in
+  translate_helpers il' @ translate_rules il'

spectec/test-frontend/TEST.md

@@ -6297,7 +6297,9 @@ def $rundata_(dataidx : dataidx, data : data) : instr*
 ;; 9-module.watsup
 def $instantiate(store : store, module : module, externval*) : config
   ;; 9-module.watsup
-  def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, moduleinst : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr})
+  def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, xt_I* : externtype*, xt_E* : externtype*, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, moduleinst : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr})
+    -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I : externtype}, xt_E*{xt_E : externtype}))
+    -- (Externval_type: `%|-%:%`(s, externval, xt_I))*{externval : externval, xt_I : externtype}
     -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}))
     -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype})
     -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype})
@@ -6320,6 +6322,7 @@ def $invoke(store : store, funcaddr : funcaddr, val*) : config
   ;; 9-module.watsup
   def $invoke{s : store, funcaddr : funcaddr, val* : val*, f : frame, t_1* : valtype*, t_2* : valtype*}(s, funcaddr, val*{val : val}) = `%;%`_config(`%;%`_state(s, f), (val : val <: instr)*{val : val} :: [REF.FUNC_ADDR_instr(funcaddr) CALL_REF_instr((s.FUNCS_store[funcaddr].TYPE_funcinst : deftype <: typeuse))])
     -- Expand: `%~~%`(s.FUNCS_store[funcaddr].TYPE_funcinst, FUNC_comptype(`%->%`_functype(`%`_resulttype(t_1*{t_1 : valtype}), `%`_resulttype(t_2*{t_2 : valtype}))))
+    -- (Val_type: `%|-%:%`(s, val, t_1))*{t_1 : valtype, val : val}
     -- if (f = {LOCALS [], MODULE {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], EXPORTS []}})
 
 ;; A-binary.watsup

spectec/test-interpreter/TEST.md

@@ -9,8 +9,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...
@@ -25,8 +23,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...
@@ -41,8 +37,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...
@@ -63,8 +57,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...
@@ -304,8 +296,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...
@@ -779,8 +769,6 @@ watsup 0.4 generator
 == IL Validation...
 == Running pass sideconditions...
 == IL Validation after pass sideconditions...
-== Running pass animate...
-== IL Validation after pass animate...
 == Translating to AL...
 == Initializing interpreter...
 == Interpreting...

spectec/test-latex/TEST.md

@@ -8949,7 +8949,9 @@ $$
 $$
 \begin{array}{@{}lcl@{}l@{}}
 {\mathrm{instantiate}}(s, {\mathit{module}}, {{\mathit{externval}}^\ast}) &=& \multicolumn{2}{l@{}}{ {s'} ; f ; {{\mathit{instr}}_{\mathsf{e}}^\ast}~{{\mathit{instr}}_{\mathsf{d}}^\ast}~{{\mathit{instr}}_{\mathsf{s}}^?} } \\
-   \multicolumn{4}{@{}l@{}}{\qquad\quad \mbox{if}~{\mathit{module}} = \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^\ast}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}} \\
+   \multicolumn{4}{@{}l@{}}{\qquad\quad \mbox{if}~{\vdash}\, {\mathit{module}} : {{\mathit{xt}}_{\mathsf{i}}^\ast} \rightarrow {{\mathit{xt}}_{\mathsf{e}}^\ast}} \\
+   \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~(s \vdash {\mathit{externval}} : {\mathit{xt}}_{\mathsf{i}})^\ast} \\
+   \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{\mathit{module}} = \mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\ast}~{{\mathit{func}}^\ast}~{{\mathit{global}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{elem}}^\ast}~{{\mathit{data}}^\ast}~{{\mathit{start}}^?}~{{\mathit{export}}^\ast}} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{global}}^\ast} = {(\mathsf{global}~{\mathit{globaltype}}~{\mathit{expr}}_{\mathsf{g}})^\ast}} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{table}}^\ast} = {(\mathsf{table}~{\mathit{tabletype}}~{\mathit{expr}}_{\mathsf{t}})^\ast}} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{elem}}^\ast} = {(\mathsf{elem}~{\mathit{reftype}}~{{\mathit{expr}}_{\mathsf{e}}^\ast}~{\mathit{elemmode}})^\ast}} \\
@@ -8979,6 +8981,7 @@ $$
 \begin{array}{@{}lcl@{}l@{}}
 {\mathrm{invoke}}(s, {\mathit{funcaddr}}, {{\mathit{val}}^\ast}) &=& \multicolumn{2}{l@{}}{ s ; f ; {{\mathit{val}}^\ast}~(\mathsf{ref{.}func}~{\mathit{funcaddr}})~(\mathsf{call\_ref}~s{.}\mathsf{funcs}{}[{\mathit{funcaddr}}]{.}\mathsf{type}) } \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad \mbox{if}~s{.}\mathsf{funcs}{}[{\mathit{funcaddr}}]{.}\mathsf{type} \approx \mathsf{func}~({t_1^\ast} \rightarrow {t_2^\ast})} \\
+   \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~(s \vdash {\mathit{val}} : t_1)^\ast} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~f = \{ \begin{array}[t]{@{}l@{}}
 \mathsf{module}~\{ \begin{array}[t]{@{}l@{}}
  \}\end{array} \}\end{array}} \\