Call precondition checking

cozy/desugar.py

@@ -70,19 +70,6 @@ def desugar(spec : Spec) -> Spec:
 
     assert retypecheck(spec, env={})
 
-    # organize queries by name
-    queries = { q.name : q for q in spec.methods if isinstance(q, Query) }
-
-    class V(BottomUpRewriter):
-        def visit_ECall(self, e):
-            q = queries.get(e.func)
-            if q is not None:
-                return self.visit(subst(q.ret, { arg_name: arg for ((arg_name, ty), arg) in zip(q.args, e.args) }))
-            else:
-                return ECall(e.func, tuple(self.visit(a) for a in e.args)).with_type(e.type)
-    spec = V().visit(spec)
-    spec.methods = [m for m in spec.methods if not (isinstance(m, Query) and m.visibility == Visibility.Private)]
-
     class V(BottomUpRewriter):
         def visit_Exp(self, e):
             return desugar_list_comprehensions(e)

cozy/invariant_preservation.py

@@ -3,7 +3,7 @@
 from cozy.common import typechecked
 from cozy.target_syntax import *
 from cozy.solver import valid
-from cozy.syntax_tools import pprint, enumerate_fragments, shallow_copy
+from cozy.syntax_tools import pprint, enumerate_fragments, shallow_copy, inline_calls, subst
 from cozy.handle_tools import reachable_handles_at_method, implicit_handle_assumptions_for_method
 from cozy.state_maintenance import mutate
 from cozy.opts import Option
@@ -53,3 +53,20 @@ def check_the_wf(spec : Spec):
             if not valid(EImplies(EAll(a), EAny([EIsSingleton(e.e), EEmpty(e.e)]))):
                 res.append("at {}: `the` is illegal since its argument may not be singleton".format(pprint(e)))
     return res
+
+def check_calls_wf(spec : Spec):
+    res = []
+    queries = { m.name : m for m in spec.methods if isinstance(m, Query) }
+    for ctx in enumerate_fragments(spec):
+        e = ctx.e
+        if isinstance(e, ECall):
+            q = queries.get(e.func)
+            if q is None:
+                continue
+            print("Checking call {}...".format(pprint(e)))
+            a = EAll(ctx.facts)
+            for precond in q.assumptions:
+                precond = subst(precond, { v : val for (v, t), val in zip(q.args, e.args) })
+                if not valid(inline_calls(spec, EImplies(a, precond))):
+                    res.append("at {}: call may not satisfy precondition {}".format(pprint(e), pprint(precond)))
+    return res

cozy/main.py

@@ -72,10 +72,15 @@ def run():
         ast = desugar.desugar(ast)
         ast = invariant_preservation.add_implicit_handle_assumptions(ast)
 
-        print("Checking assumptions...")
+        print("Checking call legality...")
+        call_errors = invariant_preservation.check_calls_wf(ast)
+        ast = syntax_tools.inline_calls(ast)
+
+        print("Checking invariant preservation...")
         errors = (
             invariant_preservation.check_ops_preserve_invariants(ast) +
-            invariant_preservation.check_the_wf(ast))
+            invariant_preservation.check_the_wf(ast) +
+            call_errors)
         if errors:
             for e in errors:
                 print("Error: {}".format(e))

cozy/syntax_tools.py

@@ -1503,7 +1503,10 @@ def visit_ELambda(self, e):
             assert False
     return res
 
-def inline_calls(spec):
+def inline_calls(spec, target=None):
+    if target is None:
+        target = spec
+
     extern_func_names = set(e.name for e in spec.extern_funcs)
     queries = {q.name : q for q in spec.methods if isinstance(q, syntax.Query)}
 
@@ -1520,11 +1523,11 @@ def visit_ECall(self, e):
             if query is None:
                 return e
 
-            return subst(query.ret,
-                {arg: self.visit(expr) for ((arg, argtype), expr) in zip(query.args, e.args)})
+            return self.visit(subst(query.ret,
+                {arg: self.visit(expr) for ((arg, argtype), expr) in zip(query.args, e.args)}))
 
     rewriter = CallInliner()
-    return rewriter.visit(spec)
+    return rewriter.visit(target)
 
 def get_modified_var(stm):
     """