Check that variables in rules and defs are bound

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

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

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 a 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 *)
 

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

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

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}
 $$