Skip to content

Commit

Permalink
Merge pull request #39 from CozySynthesizer/call-checking
Browse files Browse the repository at this point in the history
Call precondition checking
  • Loading branch information
anhnamtran authored Jul 3, 2018
2 parents c46b02a + 880aa37 commit 0846d1c
Show file tree
Hide file tree
Showing 4 changed files with 32 additions and 20 deletions.
13 changes: 0 additions & 13 deletions cozy/desugar.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
19 changes: 18 additions & 1 deletion cozy/invariant_preservation.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
9 changes: 7 additions & 2 deletions cozy/main.py
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
11 changes: 7 additions & 4 deletions cozy/syntax_tools.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)}

Expand All @@ -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):
"""
Expand Down

0 comments on commit 0846d1c

Please sign in to comment.