From 30d3beea2b1d7f157b76a39115418f3da7bba2c8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 12 Dec 2017 18:37:42 -0800 Subject: [PATCH] toy_consensus verifies but does not compile --- doc/examples/toy_consensus.ivy | 134 ++++++++++++++++++--------------- ivy/ivy_ast.py | 2 +- ivy/ivy_compiler.py | 54 ++++++++++--- ivy/ivy_isolate.py | 20 ++--- ivy/ivy_logic_parser.py | 6 +- ivy/ivy_logic_parser_gen.py | 1 + ivy/ivy_to_cpp.py | 11 ++- 7 files changed, 144 insertions(+), 84 deletions(-) diff --git a/doc/examples/toy_consensus.ivy b/doc/examples/toy_consensus.ivy index d8fe78c..d36d1fd 100644 --- a/doc/examples/toy_consensus.ivy +++ b/doc/examples/toy_consensus.ivy @@ -19,9 +19,6 @@ isolate nset = { action add(s:nset, n : node) returns (s:nset) specification { - invariant [majorities_intersect] - (majority(S) & majority(T)) -> exists N. member(N,S) & member(N,T) - after emptyset { ensure ~member(N, s) } @@ -31,6 +28,11 @@ isolate nset = { } } + private { + invariant [majorities_intersect] + (majority(S) & majority(T)) -> exists N. member(N,S) & member(N,T) + } + implementation { interpret index -> int function card(S:nset) : index @@ -55,7 +57,6 @@ isolate nset = { card(S) := card(S) + 1 if member(i.val, S) else card(S); i := i.next }; - assume member(N,all) } implement emptyset { @@ -106,29 +107,30 @@ isolate toy_protocol = { } } } -with nset +with nset, nset.majorities_intersect -instance net : udp_simple(node,msg.t) +object msg_kind = { + type this = {request_vote, vote, leader} +} + +object msg = { + type this = struct { + kind : msg_kind, + src : node, + vote : node + } +} + +instance net : udp_simple(node,msg) isolate shim = { - object msg_kind = { - type this = {request_vote, vote, leader} - } - - object msg = { - type this = struct { - kind : msg_kind, - src : node, - vote : node - } - } module handler(p_kind) = { - action handle(dst:node,m:msg.t) + action handle(dst:node,m:msg) specification { before handle { - require sent(m,dst) & m.m_kind = p_kind + require sent(m,dst) & m.kind = p_kind } } } @@ -153,18 +155,18 @@ isolate shim = { implementation { - action debug_sending(src:node,dst:node,m:msg.t) - action debug_recving(dst:node,m:msg.t) + action debug_sending(src:node,dst:node,m:msg) + action debug_recving(dst:node,m:msg) - implement net.recv(dst:node,m:msg.t) { + implement net.recv(dst:node,m:msg) { call debug_recving(dst,m); - if m.m_kind = msg_kind.request_vote { + if m.kind = msg_kind.request_vote { call request_vote.handle(dst,m) } - else if m.m_kind = msg_kind.vote { + else if m.kind = msg_kind.vote { call vote.handle(dst,m) } - else if m.m_kind = msg_kind.leader { + else if m.kind = msg_kind.leader { call leader.handle(dst,m) } } @@ -181,6 +183,9 @@ isolate shim = { } } + } + + private { invariant net.spec.sent(M,D) -> sent(M,D) } @@ -189,60 +194,66 @@ isolate shim = { isolate toy_system = { - invariant [safe] shim.sent(M1) & M1.kind = shim.msg_kind.leader - & shim.sent(M2) & M2.kind = shim.msg_kind.leader - -> M1.src = M2.src relation alreadyvoted(N:node) function voters(N:node) : nset - after init procedure init(self : node) { + specification { + invariant [safe] forall M1:msg, M2:msg. + shim.sent(M1,N1) & M1.kind = msg_kind.leader + & shim.sent(M2,N2) & M2.kind = msg_kind.leader + -> M1.src = M2.src + } + + after init (self : node) { alreadyvoted(self) := false; voters(self) := nset.emptyset() } - action request_vote(self : node) { - var msg : shim.msg; - msg.kind := shim.msg_kind.request_vote; - msg.src = self; - shim.bcast(msg); - if ~alreadyvoted(self) { - alreadyvoted(self) := true - voters(self) := voters.add(self); - toy_protocol.vote(self,self) # ghost - } - } - - - implement shim.request_vote.handle(self : node, req : shim.msg) { + action request_vote(self : node) = { + var msg : msg; + msg.kind := msg_kind.request_vote; + msg.src := self; + call shim.bcast(self,msg); if ~alreadyvoted(self) { alreadyvoted(self) := true; - var reply : shim.msg; - reply.kind := shim.msg_kind.vote; - reply.src := self; - reply.vote := req.src; - shim.bcast(self,reply); - toy_protocol.vote(self,req.src) + voters(self) := voters(self).add(self); + call toy_protocol.vote(self,self) # ghost } } - action receive vote(self : node, req : shim.msg) { - voters(self) := voters.self.add(req.src); - if nset.majority(voters(self)) { - reply : shim.msg; - reply.kind := shim.msg.leader; + + implement shim.request_vote.handle(self : node, req : msg) { + if ~alreadyvoted(self) { + alreadyvoted(self) := true; + var reply : msg; + reply.kind := msg_kind.vote; reply.src := self; - shim.bcast(self,reply); - toy protocol.become_leader(self, voters(self)) # ghost + reply.vote := req.src; + call shim.bcast(self,reply); + call toy_protocol.vote(self,req.src) + } + } + + implement shim.vote.handle(self : node, req : msg) { + if req.vote = self { + voters(self) := voters(self).add(req.src); + if nset.majority(voters(self)) { + var reply : msg; + reply.kind := msg_kind.leader; + reply.src := self; + call shim.bcast(self,reply); + call toy_protocol.become_leader(self, voters(self)) # ghost + } } } private { - invariant shim.sent(M) & M.kind = shim.msg_kind.vote -> toy_protocol.voted(M.src, M.vote) -# invariant shim.sent(M) & M.kind = shim.msg_kind.request -> toy_protocol.voted(M.src,M.src) + invariant forall M:msg. shim.sent(M,N) & M.kind = msg_kind.vote -> toy_protocol.voted(M.src, M.vote) +# invariant shim.sent(M) & M.kind = msg_kind.request -> toy_protocol.voted(M.src,M.src) invariant nset.member(N1 ,voters(N2)) -> toy_protocol.voted(N1,N2) - invariant shim.sent(M) & M.kind = shim.msg_kind.leader -> toy protocol.isleader(M.src) + invariant forall M:msg. shim.sent(M,N) & M.kind = msg_kind.leader -> toy_protocol.isleader(M.src) invariant toy_protocol.voted(N1,N2) -> alreadyvoted(N1) } @@ -252,5 +263,6 @@ isolate toy_system = { } with nset, toy_protocol, shim -export toy_protocol.vote -export toy_protocol.become_leader +export toy_system.request_vote + +extract iso_impl(self:node) = toy_system(self),shim(self),net(self),nset,node diff --git a/ivy/ivy_ast.py b/ivy/ivy_ast.py index 6288772..41c6549 100644 --- a/ivy/ivy_ast.py +++ b/ivy/ivy_ast.py @@ -326,7 +326,7 @@ class Variable(Term): class MethodCall(Term): def __str__(self): - return str(args[0]) + '.' + str(args[1]) + return str(self.args[0]) + '.' + str(self.args[1]) class Literal(AST): """ diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py index b7e37b7..0dc1abc 100644 --- a/ivy/ivy_compiler.py +++ b/ivy/ivy_compiler.py @@ -121,9 +121,21 @@ class TopContext(Context): self.actions = actions self.name = 'top_context' +class EmptyVariableContext(object): + def __init__(self): + self.map = dict() + +class VariableContext(Context): + def __init__(self,vs): + self.map = dict(variable_context.map.iteritems()) + for v in vs: + self.map[v.name] = v.sort + self.name = 'variable_context' + return_context = None expr_context = None top_context = None +variable_context = EmptyVariableContext() def pull_args(args,num,sym,top): if len(args) < num: @@ -236,10 +248,13 @@ def compile_app(self): def compile_method_call(self): with ReturnContext(None): - obj = self.args[0].compile() - child_name = self.args[1].relname + base = self.args[0].compile() + child_name = self.args[1].rep args = [a.compile() for a in self.args[1].args] sort = base.sort + if ivy_logic.is_topsort(sort): + raise IvyError(self,'cannot apply method notation to {} because its type is not inferred'.format(base)) + # trucky: we first look for the method as a child of the sort. # if not found, we look for a sibling of the sort destr_name = iu.compose_names(sort.name,child_name) @@ -255,7 +270,7 @@ def compile_method_call(self): args.insert(0,base) return sym(*args) - +ivy_ast.MethodCall.cmpl = compile_method_call def cmpl_sort(sortname): return ivy_logic.find_sort(resolve_alias(sortname)) @@ -269,7 +284,16 @@ ivy_ast.NativeExpr.cmpl = cmpl_native_expr ivy_ast.App.cmpl = ivy_ast.Atom.cmpl = compile_app -ivy_ast.Variable.cmpl = lambda self: ivy_logic.Variable(self.rep,cmpl_sort(self.sort) if isinstance(self.sort,str) else self.sort) +def variable_sort(self): + return cmpl_sort(self.sort) if isinstance(self.sort,str) else self.sort + +def compile_variable(self): + sort = variable_sort(self) + if ivy_logic.is_topsort(sort): + sort = variable_context.map.get(self.rep,sort) + return ivy_logic.Variable(self.rep,sort) + +ivy_ast.Variable.cmpl = compile_variable ivy_ast.ConstantSort.cmpl = lambda self,name: ivy_logic.ConstantSort(name) @@ -280,7 +304,12 @@ SymbolList.cmpl = lambda self: self.clone([find_symbol(s) for s in self.symbols] def cquant(q): return ivy_logic.ForAll if isinstance(q,ivy_ast.Forall) else ivy_logic.Exists -ivy_ast.Quantifier.cmpl = lambda self: cquant(self)([v.compile() for v in self.bounds],self.args[0].compile()) +def compile_quantifier(self): + bounds = [ivy_logic.Variable(v.rep,variable_sort(v)) for v in self.bounds] + with VariableContext(bounds): + return cquant(self)(bounds,self.args[0].compile()) + +ivy_ast.Quantifier.cmpl = compile_quantifier ivy_ast.NamedBinder.cmpl = lambda self: ivy_logic.NamedBinder( self.name, @@ -523,7 +552,11 @@ def compile_native_arg(arg): if arg.rep in ivy_logic.sig.symbols: return sortify_with_inference(arg) res = arg.clone(map(sortify_with_inference,arg.args)) # handles action names - return res.rename(resolve_alias(res.rep)) + iu.dbg('res') + res1 = res.rename(resolve_alias(res.rep)) + iu.dbg('res1') + return res1 + def compile_native_symbol(arg): name = arg.rep @@ -552,7 +585,9 @@ def compile_native_name(atom): def compile_native_def(self): fields = self.args[1].code.split('`') args = [compile_native_name(self.args[0]),self.args[1]] + [compile_native_arg(a) if not fields[i*2].endswith('"') else compile_native_symbol(a) for i,a in enumerate(self.args[2:])] - return self.clone(args) + cres = self.clone(args) + iu.dbg('cres') + return cres def compile_action_def(a,sig): sig = sig.copy() @@ -874,13 +909,14 @@ class IvyDomainSetup(IvyDeclInterp): def interpret(self,thing): sig = self.domain.sig interp = sig.interp + lhs = resolve_alias(thing.formula.args[0].rep) + iu.dbg('lhs') if isinstance(thing.formula.args[1],ivy_ast.NativeType): - lhs = thing.formula.args[0].rep if lhs in interp or lhs in self.domain.native_types : raise IvyError(thing,"{} is already interpreted".format(lhs)) self.domain.native_types[lhs] = thing.formula.args[1] return - lhs,rhs = (a.rep for a in thing.formula.args) + rhs = thing.formula.args[1].rep self.domain.interps[lhs].append(thing) if lhs in self.domain.native_types : raise IvyError(thing,"{} is already interpreted".format(lhs)) diff --git a/ivy/ivy_isolate.py b/ivy/ivy_isolate.py index 26b8aeb..9827384 100644 --- a/ivy/ivy_isolate.py +++ b/ivy/ivy_isolate.py @@ -220,26 +220,27 @@ def strip_sort(sort,strip_params): return ivy_logic.FunctionSort(*(dom+[sort.rng])) return sort.rng -def strip_action(ast,strip_map,strip_binding): +def strip_action(ast,strip_map,strip_binding,is_init=False): if isinstance(ast,ia.CallAction): name = canon_act(ast.args[0].rep) - args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args[0].args] + args = [strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args[0].args] strip_params = get_strip_params(name,ast.args[0].args,strip_map,strip_binding,ast) call = ast.args[0].clone(args[len(strip_params):]) - return ast.clone([call]+[strip_action(arg,strip_map,strip_binding) for arg in ast.args[1:]]) + return ast.clone([call]+[strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args[1:]]) if isinstance(ast,ia.Action): for sym in ast.modifies(): if sym.name in ivy_logic.sig.symbols: lhs_params = strip_map_lookup(sym.name,strip_map) if len(lhs_params) != num_isolate_params: - raise iu.IvyError(ast,"assignment may be interfering") + if not (len(lhs_params) == 0 and len(strip_binding) == 0 and is_init): + raise iu.IvyError(ast,"assignment may be interfering") if (ivy_logic.is_constant(ast) or ivy_logic.is_variable(ast)) and ast in strip_binding: sname = strip_binding[ast] if sname not in ivy_logic.sig.symbols: ivy_logic.add_symbol(sname,ast.sort) strip_added_symbols.append(ivy_logic.Symbol(sname,ast.sort)) return ivy_logic.Symbol(sname,ast.sort) - args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args] + args = [strip_action(arg,strip_map,strip_binding,is_init) for arg in ast.args] if ivy_logic.is_app(ast): name = ast.rep.name strip_params = get_strip_params(name,ast.args,strip_map,strip_binding,ast) @@ -348,7 +349,7 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip): strip_binding = dict(zip(action.formal_params,strip_params)) # if isinstance(action,ia.NativeAction) and len(strip_params) != num_isolate_params: # raise iu.IvyError(None,'foreign function {} may be interfering'.format(name)) - new_action = strip_action(action,strip_map,strip_binding) + new_action = strip_action(action,strip_map,strip_binding,is_init=name.endswith('init[after]')) new_action.formal_params = action.formal_params[len(strip_params):] new_action.formal_returns = action.formal_returns new_actions[name] = new_action @@ -1687,13 +1688,14 @@ def check_isolate_completeness(mod = None): def iter_isolate(mod,iso,fun,verified=True,present=True): + suff = "spec" if isinstance(iso,ivy_ast.ExtractDef) else "impl" def recur(name): fun(name) for child in mod.hierarchy[name]: cname = iu.compose_names(name,child) - if not(child == "impl" - or iu.compose_names(name,'impl') in mod.attributes - or iu.compose_names(name,'private') in mod.attributes): + if not(child == suff + or iu.compose_names(cname,suff) in mod.attributes + or iu.compose_names(cname,'private') in mod.attributes): recur(cname) if verified: diff --git a/ivy/ivy_logic_parser.py b/ivy/ivy_logic_parser.py index 9d0d3e5..1476f94 100644 --- a/ivy/ivy_logic_parser.py +++ b/ivy/ivy_logic_parser.py @@ -355,12 +355,12 @@ def p_fmla_fmla_iff_fmla(p): p[0].lineno = get_lineno(p,2) def p_fmla_forall_vars_dot_fmla(p): - 'fmla : FORALL simplevars DOT fmla' + 'fmla : FORALL simplevars DOT fmla %prec SEMI' p[0] = Forall(p[2],p[4]) p[0].lineno = get_lineno(p,1) def p_fmla_exists_vars_dot_fmla(p): - 'fmla : EXISTS simplevars DOT fmla' + 'fmla : EXISTS simplevars DOT fmla %prec SEMI' p[0] = Exists(p[2],p[4]) p[0].lineno = get_lineno(p,1) @@ -382,7 +382,7 @@ def p_term_namedbinder_vars_dot_fmla(p): p[0].lineno = get_lineno(p,2) def p_term_namedbinder_dot_fmla(p): - 'term : DOLLAR SYMBOL DOT fmla' + 'term : DOLLAR SYMBOL DOT fmla %prec SEMI' p[0] = NamedBinder(p[2], [],p[4]) p[0].lineno = get_lineno(p,1) diff --git a/ivy/ivy_logic_parser_gen.py b/ivy/ivy_logic_parser_gen.py index e47d3b4..c8be792 100644 --- a/ivy/ivy_logic_parser_gen.py +++ b/ivy/ivy_logic_parser_gen.py @@ -7,6 +7,7 @@ import ply.yacc as yacc # Parser for formulas precedence = ( + ('left', 'SEMI'), ('left', 'GLOBALLY', 'EVENTUALLY'), ('left', 'IF'), ('left', 'ELSE'), diff --git a/ivy/ivy_to_cpp.py b/ivy/ivy_to_cpp.py index 66262bf..12234ec 100755 --- a/ivy/ivy_to_cpp.py +++ b/ivy/ivy_to_cpp.py @@ -2511,7 +2511,14 @@ def emit_one_initial_state(header): check_init_cond("initial condition",im.module.labeled_inits) check_init_cond("axiom",im.module.labeled_axioms) - clauses = ilu.and_clauses(im.module.init_cond,im.module.background_theory()) + constraints = [ilu.clauses_to_formula(im.module.init_cond)] + for a in im.module.axioms: + constraints.append(a) + for ldf in im.relevant_definitions(ilu.symbols_asts(constraints)): + constraints.append(fix_definition(ldf.formula).to_constraint()) + clauses = ilu.formula_to_clauses(il.And(*constraints)) +# clauses = ilu.and_clauses(im.module.init_cond,im.module.background_theory()) + iu.dbg('clauses') m = slv.get_model_clauses(clauses) if m == None: print clauses @@ -2780,6 +2787,8 @@ def get_all_bounds(header,variables,body,exists,varnames): def emit_quant(variables,body,header,code,exists=False): + iu.dbg('variables') + iu.dbg('body') global indent_level if len(variables) == 0: body.emit(header,code)