From 550f17179a334f12145f2b85de683408f230f026 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 3 Nov 2023 09:39:13 +0100 Subject: [PATCH 1/2] Check that variables in rules and defs are bound --- spectec/spec/6-reduction.watsup | 2 +- spectec/spec/7-module.watsup | 2 +- spectec/src/el/free.ml | 83 +++++++++++++++++++++++++++++++-- spectec/src/el/free.mli | 4 ++ spectec/src/frontend/elab.ml | 29 ++++++++++-- spectec/test-frontend/TEST.md | 14 +++--- spectec/test-middlend/TEST.md | 79 +++++++++++++++---------------- spectec/test-prose/TEST.md | 5 +- 8 files changed, 157 insertions(+), 61 deletions(-) diff --git a/spectec/spec/6-reduction.watsup b/spectec/spec/6-reduction.watsup index df37e221f2..36edb246b8 100644 --- a/spectec/spec/6-reduction.watsup +++ b/spectec/spec/6-reduction.watsup @@ -105,7 +105,7 @@ rule Step_read/call_indirect-call: z; (CONST I32 i) (CALL_INDIRECT x y) ~> (CALL_ADDR a) -- if $table(z, x).ELEM[i] = (REF.FUNC_ADDR a) -- if $funcinst(z)[a].CODE = FUNC y' (LOCAL t)* instr* - -- if C.TYPE[y] = C.TYPE[y'] + -- if $type(z, y) = $type(z, y') rule Step_read/call_indirect-trap: z; (CONST I32 i) (CALL_INDIRECT x y) ~> TRAP diff --git a/spectec/spec/7-module.watsup b/spectec/spec/7-module.watsup index 16ac90a77a..95b1c43d9d 100644 --- a/spectec/spec/7-module.watsup +++ b/spectec/spec/7-module.watsup @@ -35,7 +35,7 @@ def $mems(externval externval'*) = $mems(externval'*) def $allocfunc(store, moduleinst, func) : (store, funcaddr) def $allocfunc(s, mm, func) = (s[.FUNC =.. fi], |s.FUNC|) - -- if fi = { TYPE moduleinst.TYPE[x], MODULE mm, CODE func } + -- if fi = { TYPE mm.TYPE[x], MODULE mm, CODE func } -- if func = FUNC x local* expr def $allocfuncs(store, moduleinst, func*) : (store, funcaddr*) diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml index 4b9c22ae2b..501123662c 100644 --- a/spectec/src/el/free.ml +++ b/spectec/src/el/free.ml @@ -33,6 +33,10 @@ let free_list free_x xs = List.(fold_left union empty (map free_x xs)) let free_nl_elem free_x = function Nl -> empty | Elem x -> free_x x let free_nl_list free_x xs = List.(fold_left union empty (map (free_nl_elem free_x) xs)) +let bound_opt = free_opt +let bound_list = free_list +let bound_nl_list = free_nl_list + (* Identifiers *) @@ -42,6 +46,8 @@ let free_relid id = {empty with relid = Set.singleton id.it} let free_varid id = {empty with varid = Set.singleton id.it} let free_defid id = {empty with defid = Set.singleton id.it} +let bound_varid = free_varid + (* Iterations *) @@ -82,13 +88,13 @@ and free_typenum (e, eo) = and free_exp e = match e.it with | VarE id -> free_varid id - | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ | EpsE | HoleE _ -> empty + | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ | EpsE | HoleE _ -> + empty | UnE (_, e1) | DotE (e1, _) | LenE e1 | ParenE (e1, _) | BrackE (_, e1) -> free_exp e1 | BinE (e1, _, e2) | CmpE (e1, _, e2) | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) - | InfixE (e1, _, e2) | FuseE (e1, e2) -> - free_list free_exp [e1; e2] + | InfixE (e1, _, e2) | FuseE (e1, e2) -> free_list free_exp [e1; e2] | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3] | SeqE es | TupE es -> free_list free_exp es | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> @@ -108,6 +114,68 @@ and free_path p = union (free_path p1) (union (free_exp e1) (free_exp e2)) | DotP (p1, _) -> free_path p1 +(* We consider all variables "bound" that occur as iteration variable + * or in an equation in "pattern" position. *) +and bound_exp e = + match e.it with + | CmpE (e1, EqOp, e2) -> union (pat_exp e1) (pat_exp e2) + | VarE _ | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ + | SizeE _ | EpsE | HoleE _ -> empty + | UnE (_, e1) | DotE (e1, _) | LenE e1 + | ParenE (e1, _) | BrackE (_, e1) -> bound_exp e1 + | BinE (e1, _, e2) | CmpE (e1, _, e2) -> union (bound_exp e1) (bound_exp e2) + | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) + | InfixE (e1, _, e2) | FuseE (e1, e2) -> bound_list bound_exp [e1; e2] + | SliceE (e1, e2, e3) -> bound_list bound_exp [e1; e2; e3] + | SeqE es | TupE es -> bound_list bound_exp es + | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> + union (bound_list bound_exp [e1; e2]) (bound_path p) + | StrE efs -> bound_nl_list bound_expfield efs + | CallE (_, e1) -> bound_exp e1 + | IterE (e1, iter) -> union (bound_exp e1) (bound_iter iter) + +and bound_expfield (_, e) = bound_exp e + +and bound_path p = + match p.it with + | RootP -> empty + | IdxP (p1, e) -> union (bound_path p1) (bound_exp e) + | SliceP (p1, e1, e2) -> + union (bound_path p1) (union (bound_exp e1) (bound_exp e2)) + | DotP (p1, _) -> bound_path p1 + +and bound_iter iter = + match iter with + | Opt | List | List1 -> empty + | ListN (e, id_opt) -> union (bound_exp e) (bound_opt bound_varid id_opt) + +and pat_exp e = + match e.it with + | VarE id -> bound_varid id + | UnE ((PlusOp | MinusOp), e1) + | ParenE (e1, _) | BrackE (_, e1) -> pat_exp e1 + (* We consider all arithmetic expressions patterns, + * since we sometimes need to use invertible formulas. *) + | BinE (e1, (AddOp | SubOp | MulOp | DivOp | ExpOp), e2) + | InfixE (e1, _, e2) | FuseE (e1, e2) -> bound_list pat_exp [e1; e2] + | SeqE es | TupE es -> bound_list pat_exp es + | StrE efs -> bound_nl_list pat_expfield efs + | IterE (e1, iter) -> union (pat_exp e1) (pat_iter iter) + (* As a special hack to work with bijective functions, + * we treat last position of a call as a pattern, too. *) + | CallE (_, {it = TupE (_::_ as es); _}) -> + let es', eN = Util.Lib.List.split_last es in + union (bound_list bound_exp es') (pat_exp eN) + | CallE (_, e1) -> pat_exp e1 + | _ -> bound_exp e + +and pat_expfield (_, e) = pat_exp e + +and pat_iter iter = + match iter with + | Opt | List | List1 -> empty + | ListN (e, id_opt) -> union (pat_exp e) (bound_opt bound_varid id_opt) + (* Premises *) @@ -118,6 +186,15 @@ and free_prem prem = | ElsePr -> empty | IterPr (prem', iter) -> union (free_prem prem') (free_iter iter) +(* We consider all variables "bound" that occur in judgement + * or are bound in a condition *) +and bound_prem prem = + match prem.it with + | RulePr (_id, e) -> free_exp e + | IfPr e -> bound_exp e + | ElsePr -> empty + | IterPr (prem', _iter) -> bound_prem prem' + (* Grammars *) diff --git a/spectec/src/el/free.mli b/spectec/src/el/free.mli index 3f2e8d167a..8851724bb3 100644 --- a/spectec/src/el/free.mli +++ b/spectec/src/el/free.mli @@ -13,3 +13,7 @@ val free_exp : exp -> sets val free_path : path -> sets val free_prem : premise -> sets val free_def : def -> sets + +val pat_exp : exp -> sets +val bound_exp : exp -> sets +val bound_prem : premise -> sets diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index dd6bc8c454..3ef4c2b7d0 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -1333,6 +1333,18 @@ let elab_def env d : Il.def list = let es' = List.map (Multiplicity.annot_exp dims') (elab_exp_notation' env e t) in let prems' = List.map (Multiplicity.annot_prem dims') (map_nl_list (elab_prem env) prems) in + let free_rh = + Free.(Set.diff + (free_nl_list free_prem prems).varid + (Set.union + (pat_exp e).varid + (free_nl_list bound_prem prems).varid + ) + ) + in + if free_rh <> Free.Set.empty then + error d.at ("rule contains unbound variable(s) `" ^ + String.concat "`, `" (Free.Set.elements free_rh) ^ "`"); let free = (Free.free_def d).Free.varid in let binds' = make_binds env free dims d.at in let rule' = Il.RuleD (id2, binds', mixop, tup_exp' es' e.at, prems') $ d.at in @@ -1357,15 +1369,24 @@ let elab_def env d : Il.def list = let e2' = Multiplicity.annot_exp dims' (elab_exp env e2 t2) in let prems' = List.map (Multiplicity.annot_prem dims') (map_nl_list (elab_prem env) prems) in -(* let free_rh = - Free.(Set.diff (Set.diff (free_exp e2).varid - (free_exp e1).varid) (free_nl_list free_prem prems).varid) + Free.(Set.diff + (Set.union + (free_exp e2).varid + (free_nl_list free_prem prems).varid + ) + (Set.union + (Set.union + (pat_exp e1).varid + (bound_exp e2).varid + ) + (free_nl_list bound_prem prems).varid + ) + ) in if free_rh <> Free.Set.empty then error d.at ("definition contains unbound variable(s) `" ^ String.concat "`, `" (Free.Set.elements free_rh) ^ "`"); -*) let free = Free.(Set.union (Set.union (free_exp e1).varid (free_exp e2).varid) (free_nl_list free_prem prems).varid) in let binds' = make_binds env free dims d.at in diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 8dc1ca39db..d9ddd2da9b 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -1648,12 +1648,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -1962,8 +1962,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -4332,7 +4332,7 @@ $$ {[\textsc{\scriptsize E{-}call\_indirect{-}call}]} \quad & {\mathit{z}} ; (\mathsf{i{\scriptstyle32}}.\mathsf{const}~{\mathit{i}})~(\mathsf{call\_indirect}~{\mathit{x}}~{\mathit{y}}) &\hookrightarrow& (\mathsf{call}~{\mathit{a}}) &\quad \mbox{if}~{{\mathit{z}}.\mathsf{table}}{[{\mathit{x}}]}.\mathsf{elem}[{\mathit{i}}] = (\mathsf{ref.func}~{\mathit{a}}) \\ &&&&\quad {\land}~{\mathit{z}}.\mathsf{func}[{\mathit{a}}].\mathsf{code} = \mathsf{func}~{\mathit{y}'}~{(\mathsf{local}~{\mathit{t}})^\ast}~{{\mathit{instr}}^\ast} \\ - &&&&\quad {\land}~{\mathit{C}}.\mathsf{type}[{\mathit{y}}] = {\mathit{C}}.\mathsf{type}[{\mathit{y}'}] \\ + &&&&\quad {\land}~{{\mathit{z}}.\mathsf{type}}{[{\mathit{y}}]} = {{\mathit{z}}.\mathsf{type}}{[{\mathit{y}'}]} \\ {[\textsc{\scriptsize E{-}call\_indirect{-}trap}]} \quad & {\mathit{z}} ; (\mathsf{i{\scriptstyle32}}.\mathsf{const}~{\mathit{i}})~(\mathsf{call\_indirect}~{\mathit{x}}~{\mathit{y}}) &\hookrightarrow& \mathsf{trap} &\quad \mbox{otherwise} \\ {[\textsc{\scriptsize E{-}call\_addr}]} \quad & {\mathit{z}} ; {{\mathit{val}}^{{\mathit{k}}}}~(\mathsf{call}~{\mathit{a}}) &\hookrightarrow& ({{\mathsf{frame}}_{{\mathit{n}}}}{\{{\mathit{f}}\}}~({{\mathsf{label}}_{{\mathit{n}}}}{\{\epsilon\}}~{{\mathit{instr}}^\ast})) &\quad @@ -4689,7 +4689,7 @@ $$ \begin{array}{@{}lcl@{}l@{}} {\mathrm{allocfunc}}({\mathit{s}},\, {\mathit{mm}},\, {\mathit{func}}) &=& ({\mathit{s}}[\mathsf{func} = ..{\mathit{fi}}],\, {|{\mathit{s}}.\mathsf{func}|}) &\quad \mbox{if}~{\mathit{fi}} = \{ \begin{array}[t]{@{}l@{}} -\mathsf{type}~{\mathit{moduleinst}}.\mathsf{type}[{\mathit{x}}],\; \mathsf{module}~{\mathit{mm}},\; \mathsf{code}~{\mathit{func}} \}\end{array} \\ +\mathsf{type}~{\mathit{mm}}.\mathsf{type}[{\mathit{x}}],\; \mathsf{module}~{\mathit{mm}},\; \mathsf{code}~{\mathit{func}} \}\end{array} \\ &&&\quad {\land}~{\mathit{func}} = \mathsf{func}~{\mathit{x}}~{{\mathit{local}}^\ast}~{\mathit{expr}} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 2ce654f9bd..1307ea7eb0 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -1647,12 +1647,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -1961,8 +1961,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -3942,12 +3942,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -4256,8 +4256,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -6241,12 +6241,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -6555,8 +6555,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -8550,12 +8550,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -8873,8 +8873,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -10868,12 +10868,12 @@ relation Step_read: `%~>%*`(config, admininstr*) rule call {x : idx, z : state}: `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -11191,8 +11191,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -13239,16 +13239,14 @@ relation Step_read: `%~>%*`(config, admininstr*) `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) -- if (x < |$funcaddr(z)|) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if (i < |$table(z, x).ELEM_tableinst|) -- if (a < |$funcinst(z)|) - -- if (y < |C.TYPE_context|) - -- if (y' < |C.TYPE_context|) -- if ($table(z, x).ELEM_tableinst[i] = REF.FUNC_ADDR_ref(a)) -- if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) + -- if ($type(z, y) = $type(z, y')) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -13571,8 +13569,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 @@ -13823,9 +13821,8 @@ syntax code = (local*, expr) == IL Validation after pass sideconditions... == Running pass animate... -Animation failed:if (y < |C.TYPE_context|) -Animation failed:if (y' < |C.TYPE_context|) -Animation failed:if (C.TYPE_context[y] = C.TYPE_context[y']) +Animation failed:if ($type(z, y) = $type(z, y')) +Animation failed:if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) Animation failed:if ($ntbytes(nt, c) = $mem(z, 0).DATA_meminst[(i + mo.OFFSET_memop) : (o0 / 8)]) Animation failed:if ($ibytes(n, c) = $mem(z, 0).DATA_meminst[(i + mo.OFFSET_memop) : (n / 8)]) @@ -15624,16 +15621,14 @@ relation Step_read: `%~>%*`(config, admininstr*) `%~>%*`(`%;%*`(z, [CALL_admininstr(x)]), [CALL_ADDR_admininstr($funcaddr(z)[x])]) -- if (x < |$funcaddr(z)|) - ;; 6-reduction.watsup:104.1-108.31 - rule call_indirect-call {C : context, a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: + ;; 6-reduction.watsup:104.1-108.35 + rule call_indirect-call {a : addr, i : nat, instr* : instr*, t* : valtype*, x : idx, y : idx, y' : idx, z : state}: `%~>%*`(`%;%*`(z, [CONST_admininstr(I32_numtype, i) CALL_INDIRECT_admininstr(x, y)]), [CALL_ADDR_admininstr(a)]) -- if (i < |$table(z, x).ELEM_tableinst|) -- where REF.FUNC_ADDR_ref(a) = $table(z, x).ELEM_tableinst[i] + -- where $type(z, y') = $type(z, y) -- if (a < |$funcinst(z)|) -- where `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr}) = $funcinst(z)[a].CODE_funcinst - -- if (y < |C.TYPE_context|) - -- if (y' < |C.TYPE_context|) - -- if (C.TYPE_context[y] = C.TYPE_context[y']) ;; 6-reduction.watsup:110.1-112.15 rule call_indirect-trap {i : nat, x : idx, y : idx, z : state}: @@ -15956,8 +15951,8 @@ def mems : externval* -> memaddr* ;; 7-module.watsup:36.1-36.60 def allocfunc : (store, moduleinst, func) -> (store, funcaddr) ;; 7-module.watsup:37.1-39.34 - def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, moduleinst : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) - -- if (fi = {TYPE moduleinst.TYPE_moduleinst[x], MODULE mm, CODE func}) + def {expr : expr, fi : funcinst, func : func, local* : local*, mm : moduleinst, s : store, x : idx} allocfunc(s, mm, func) = (s[FUNC_store =.. [fi]], |s.FUNC_store|) + -- if (fi = {TYPE mm.TYPE_moduleinst[x], MODULE mm, CODE func}) -- if (func = `FUNC%%*%`(x, local*{local}, expr)) ;; 7-module.watsup:41.1-41.63 diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 6a4979c578..d5f3ca549f 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -9,9 +9,8 @@ watsup 0.4 generator == Running pass sideconditions... == IL Validation after pass sideconditions... == Running pass animate... -Animation failed:if (y < |C.TYPE_context|) -Animation failed:if (y' < |C.TYPE_context|) -Animation failed:if (C.TYPE_context[y] = C.TYPE_context[y']) +Animation failed:if ($type(z, y) = $type(z, y')) +Animation failed:if ($funcinst(z)[a].CODE_funcinst = `FUNC%%*%`(y', LOCAL(t)*{t}, instr*{instr})) Animation failed:if ($ntbytes(nt, c) = $mem(z, 0).DATA_meminst[(i + mo.OFFSET_memop) : ($size(nt <: valtype) / 8)]) Animation failed:if ($ibytes(n, c) = $mem(z, 0).DATA_meminst[(i + mo.OFFSET_memop) : (n / 8)]) == IL Validation after pass animate... From 8d0eb66356c1d66dffbbd180b0da5f70f1bed88d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 3 Nov 2023 10:37:35 +0100 Subject: [PATCH 2/2] Typo --- spectec/src/el/free.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml index 501123662c..e8ad597826 100644 --- a/spectec/src/el/free.ml +++ b/spectec/src/el/free.ml @@ -186,8 +186,8 @@ and free_prem prem = | ElsePr -> empty | IterPr (prem', iter) -> union (free_prem prem') (free_iter iter) -(* We consider all variables "bound" that occur in judgement - * or are bound in a condition *) +(* We consider all variables "bound" that occur in a judgement + * or are bound in a condition. *) and bound_prem prem = match prem.it with | RulePr (_id, e) -> free_exp e