From 0a7337a79c5bc7fa2ffe9fde73721a62c4426c73 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 2 Jul 2018 11:15:03 -0700 Subject: [PATCH 1/4] Recursively inline calls --- cozy/syntax_tools.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cozy/syntax_tools.py b/cozy/syntax_tools.py index c4c6133b..9adfaa37 100644 --- a/cozy/syntax_tools.py +++ b/cozy/syntax_tools.py @@ -1520,8 +1520,8 @@ 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) From 4270d75ab2471d2c5045f8413c5069986de191be Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 2 Jul 2018 11:15:27 -0700 Subject: [PATCH 2/4] Removed duplicated call inlining code --- cozy/desugar.py | 13 ------------- cozy/main.py | 1 + 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/cozy/desugar.py b/cozy/desugar.py index 4488e21e..bfebf8e7 100644 --- a/cozy/desugar.py +++ b/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) diff --git a/cozy/main.py b/cozy/main.py index 6ac5ebfd..81619f83 100755 --- a/cozy/main.py +++ b/cozy/main.py @@ -71,6 +71,7 @@ def run(): ast = desugar.desugar(ast) ast = invariant_preservation.add_implicit_handle_assumptions(ast) + ast = syntax_tools.inline_calls(ast) print("Checking assumptions...") errors = ( From b61a116650ad6e7803984ce4bc6a9fc74851c304 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 2 Jul 2018 11:17:37 -0700 Subject: [PATCH 3/4] Check call preconditions before inlining This addresses one of the points in #23. --- cozy/invariant_preservation.py | 19 ++++++++++++++++++- cozy/main.py | 6 +++++- cozy/syntax_tools.py | 7 +++++-- 3 files changed, 28 insertions(+), 4 deletions(-) diff --git a/cozy/invariant_preservation.py b/cozy/invariant_preservation.py index 8e648fc8..738e8a6a 100644 --- a/cozy/invariant_preservation.py +++ b/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 diff --git a/cozy/main.py b/cozy/main.py index 81619f83..916746b3 100755 --- a/cozy/main.py +++ b/cozy/main.py @@ -71,12 +71,16 @@ def run(): ast = desugar.desugar(ast) ast = invariant_preservation.add_implicit_handle_assumptions(ast) + + print("Checking call legality...") + call_errors = invariant_preservation.check_calls_wf(ast) ast = syntax_tools.inline_calls(ast) print("Checking assumptions...") 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)) diff --git a/cozy/syntax_tools.py b/cozy/syntax_tools.py index 9adfaa37..a41e6003 100644 --- a/cozy/syntax_tools.py +++ b/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)} @@ -1524,7 +1527,7 @@ def visit_ECall(self, e): {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): """ From 880aa37feef5779b1183aa389c6ef562a5184b41 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 2 Jul 2018 11:21:41 -0700 Subject: [PATCH 4/4] Reworded a confusing message --- cozy/main.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cozy/main.py b/cozy/main.py index 916746b3..972e97db 100755 --- a/cozy/main.py +++ b/cozy/main.py @@ -76,7 +76,7 @@ def run(): call_errors = invariant_preservation.check_calls_wf(ast) ast = syntax_tools.inline_calls(ast) - print("Checking assumptions...") + print("Checking invariant preservation...") errors = ( invariant_preservation.check_ops_preserve_invariants(ast) + invariant_preservation.check_the_wf(ast) +