From b0a71c77372c87d2a2a8e532b8eea002a002b682 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 14 Dec 2017 17:47:05 -0800 Subject: [PATCH] toy_consensus now compiles and runs --- doc/examples/toy_consensus.ivy | 3 ++ ivy/include/1.6/udp.ivy | 1 + ivy/ivy_actions.py | 1 - ivy/ivy_ast.py | 7 ++++- ivy/ivy_compiler.py | 28 +++++++++--------- ivy/ivy_isolate.py | 7 +---- ivy/ivy_logic.py | 2 +- ivy/ivy_logic_parser.py | 30 ++++++++++++++------ ivy/ivy_parser.py | 52 +++++++++++++++++++++++----------- ivy/ivy_printer.py | 3 +- ivy/ivy_to_cpp.py | 28 +++++++++++------- 11 files changed, 105 insertions(+), 57 deletions(-) diff --git a/doc/examples/toy_consensus.ivy b/doc/examples/toy_consensus.ivy index d36d1fd..eb64a44 100644 --- a/doc/examples/toy_consensus.ivy +++ b/doc/examples/toy_consensus.ivy @@ -265,4 +265,7 @@ isolate toy_system = { export toy_system.request_vote +import shim.debug_sending +import shim.debug_recving + extract iso_impl(self:node) = toy_system(self),shim(self),net(self),nset,node diff --git a/ivy/include/1.6/udp.ivy b/ivy/include/1.6/udp.ivy index c16ff69..3d6d51a 100644 --- a/ivy/include/1.6/udp.ivy +++ b/ivy/include/1.6/udp.ivy @@ -172,6 +172,7 @@ module udp_simple(addr,pkt) = { } instance impl(X:addr) : udp_wrapper(addr,pkt,X,4990) + trusted isolate iso = this } module nondup_endpoint(port,pkt) = { diff --git a/ivy/ivy_actions.py b/ivy/ivy_actions.py index be30aaa..300f109 100644 --- a/ivy/ivy_actions.py +++ b/ivy/ivy_actions.py @@ -846,7 +846,6 @@ class WhileAction(Action): def decompose(self,pre,post,fail=False): return self.expand(ivy_module.module,[]).decompose(pre,post,fail) def assert_to_assume(self,kinds): - iu.dbg('kinds') res = self.clone([self.args[0]]+[x.assert_to_assume(kinds) for x in self.args[1:]]) if hasattr(self,'formal_params'): res.formal_params = self.formal_params diff --git a/ivy/ivy_ast.py b/ivy/ivy_ast.py index 0633360..d88daad 100644 --- a/ivy/ivy_ast.py +++ b/ivy/ivy_ast.py @@ -322,6 +322,11 @@ class Variable(Term): if hasattr(self,'sort'): res.sort = self.sort return res + def resort(self,sort): + res = Variable(self.rep,sort) + if hasattr(self,'lineno'): + res.lineno = self.lineno + return res class MethodCall(Term): @@ -1191,7 +1196,7 @@ def ast_rewrite(x,rewrite): if isinstance(x,tuple): return tuple(ast_rewrite(e,rewrite) for e in x) if isinstance(x,Variable): - return Variable(x.rep,rewrite_sort(rewrite,x.sort)) + return x.resort(rewrite_sort(rewrite,x.sort)) if isinstance(x,Atom) or isinstance(x,App): # print "rewrite: x = {!r}, type(x.rep) = {!r}".format(x,type(x.rep)) if isinstance(x.rep, NamedBinder): diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py index a5bd871..00344f2 100644 --- a/ivy/ivy_compiler.py +++ b/ivy/ivy_compiler.py @@ -241,6 +241,10 @@ def compile_app(self): if expr_context and top_context and self.rep in top_context.actions: return compile_inline_call(self,args) sym = self.rep.cmpl() if isinstance(self.rep,ivy_ast.NamedBinder) else ivy_logic.Equals if self.rep == '=' else ivy_logic.find_polymorphic_symbol(self.rep,throw=False) + if sym is not ivy_logic.Equals: + if ivy_logic.is_numeral(sym): + if hasattr(self,'sort') and self.sort != 'S': + sym = ivy_logic.Symbol(sym.name,variable_sort(self)) if sym is not None: return (sym)(*args) res = compile_field_reference(self.rep,args) @@ -288,7 +292,8 @@ 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) + with ASTContext(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) @@ -552,10 +557,7 @@ 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 - iu.dbg('res') - res1 = res.rename(resolve_alias(res.rep)) - iu.dbg('res1') - return res1 + return res.rename(resolve_alias(res.rep)) def compile_native_symbol(arg): @@ -585,9 +587,7 @@ 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:])] - cres = self.clone(args) - iu.dbg('cres') - return cres + return self.clone(args) def compile_action_def(a,sig): sig = sig.copy() @@ -644,9 +644,13 @@ def compile_defn(df): args.append(fmla.body.args[1].args[2]) df = ivy_logic.Definition(fmla.body.args[0],ivy_logic.Some(*args)) else: - eqn = ivy_ast.Atom('=',(df.args[0],df.args[1])) - eqn = sortify_with_inference(eqn) - df = ivy_logic.Definition(eqn.args[0],eqn.args[1]) + if False and isinstance(df.args[1],ivy_ast.NativeExpr): + df = ivy_logic.Definition(sortify_with_inference(df.args[0]),df.args[1]) + df.args[1].sort = df.args[0].sort + else: + eqn = ivy_ast.Atom('=',(df.args[0],df.args[1])) + eqn = sortify_with_inference(eqn) + df = ivy_logic.Definition(eqn.args[0],eqn.args[1]) return df def compile_schema_prem(self,sig): @@ -791,7 +795,6 @@ class IvyDomainSetup(IvyDeclInterp): return sym def parameter(self,v): sym = self.individual(v) - iu.dbg('v') self.domain.params.append(sym) return sym def destructor(self,v): @@ -915,7 +918,6 @@ class IvyDomainSetup(IvyDeclInterp): 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): if lhs in interp or 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 d79820c..f787465 100644 --- a/ivy/ivy_isolate.py +++ b/ivy/ivy_isolate.py @@ -376,7 +376,6 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip): ivy_logic.sig.symbols.clear() ivy_logic.sig.symbols.update(new_symbols) - iu.dbg('mod.params') if iu.version_le(iu.get_string_version(),"1.6"): del mod.params[:] add_map = dict((s.name,s) for s in strip_added_symbols) @@ -644,7 +643,6 @@ def set_privates(mod,isolate,suff=None): if suff in mod.hierarchy: mod.privates.add(suff) for n,l in mod.hierarchy.iteritems(): - print n nsuff = get_private_from_attributes(mod,n,suff) if nsuff in l: mod.privates.add(iu.compose_names(n,nsuff)) @@ -1346,15 +1344,12 @@ def apply_present_conjectures(isol,mod): posts[actname].append(conj_to_assume(conj)) for actname,assumes in posts.iteritems(): brackets.append((actname,[],assumes)) - iu.dbg('brackets') return brackets def create_isolate(iso,mod = None,**kwargs): mod = mod or im.module - iu.dbg('mod.params') - # from version 1.7, if no isolate specified on command line and # there is only one, use it. if iso is None and iu.version_le("1.7",iu.get_string_version()): @@ -1477,7 +1472,7 @@ def create_isolate(iso,mod = None,**kwargs): action1,action2 = (lookup_action(mixin,mod,a.relname) for a in mixin.args) mixed_name = mixin.args[1].relname if mixed_name in orig_exports and isinstance(mixin,ivy_ast.MixinBeforeDef): - action1 = action1.assert_to_assume() + action1 = action1.assert_to_assume([ia.AssertAction]) mixed = ia.apply_mixin(mixin,action1,action2) mod.actions[mixed_name] = mixed triple = (mixin.mixer(),mixin.mixee(),mod.actions[mixin.mixer()]) diff --git a/ivy/ivy_logic.py b/ivy/ivy_logic.py index f474418..667bb96 100644 --- a/ivy/ivy_logic.py +++ b/ivy/ivy_logic.py @@ -1037,7 +1037,7 @@ def check_concretely_sorted(term,no_error=False,unsorted_var_names=()): if x.name not in unsorted_var_names: if no_error: raise lg.SortError - raise IvyError(None,"cannot infer sort of {} in {}".format(x,term)) + raise IvyError(None,"cannot infer sort of {} in {}".format(x,repr(term))) def sort_infer(term,sort=None,no_error=False): diff --git a/ivy/ivy_logic_parser.py b/ivy/ivy_logic_parser.py index 1476f94..77fe028 100644 --- a/ivy/ivy_logic_parser.py +++ b/ivy/ivy_logic_parser.py @@ -354,15 +354,29 @@ def p_fmla_fmla_iff_fmla(p): p[0] = Iff(p[1],p[3]) p[0].lineno = get_lineno(p,2) -def p_fmla_forall_vars_dot_fmla(p): - 'fmla : FORALL simplevars DOT fmla %prec SEMI' - p[0] = Forall(p[2],p[4]) - p[0].lineno = get_lineno(p,1) +if (iu.get_numeric_version() <= [1,6]): -def p_fmla_exists_vars_dot_fmla(p): - 'fmla : EXISTS simplevars DOT fmla %prec SEMI' - p[0] = Exists(p[2],p[4]) - p[0].lineno = get_lineno(p,1) + def p_fmla_forall_vars_dot_fmla(p): + 'fmla : FORALL simplevars DOT fmla' + 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' + p[0] = Exists(p[2],p[4]) + p[0].lineno = get_lineno(p,1) + +else: + + def p_fmla_forall_vars_dot_fmla(p): + '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 %prec SEMI' + p[0] = Exists(p[2],p[4]) + p[0].lineno = get_lineno(p,1) def p_fmla_globally_fmla(p): 'fmla : GLOBALLY fmla' diff --git a/ivy/ivy_parser.py b/ivy/ivy_parser.py index 459048e..181efad 100644 --- a/ivy/ivy_parser.py +++ b/ivy/ivy_parser.py @@ -632,13 +632,15 @@ def p_tatom_lp_symbol_relop_symbol_rp(p): p[0].lineno = get_lineno(p,3) def p_fun_defnlhs_colon_atype(p): - 'fun : defnlhs COLON atype' - p[1].sort = p[3] + 'fun : typeddefn' +# p[1].sort = p[3] p[0] = ConstantDecl(p[1]) def p_fun_defn(p): - 'fun : defn' - p[0] = DerivedDecl(addlabel(mk_lf(p[1]),'def')) + 'fun : typeddefn EQ defnrhs' + df = Definition(app_to_atom(p[1]),p[3]) + df.lineno = get_lineno(p,2) + p[0] = DerivedDecl(addlabel(mk_lf(df),'def')) def p_funs_fun(p): 'funs : fun' @@ -1853,16 +1855,39 @@ def p_defnlhs_lp_term_infix_term_rp(p): p[0] = App(p[3],[p[2],p[4]]) p[0].lineno = get_lineno(p,3) +def p_typeddefn_defnlhs(p): + 'typeddefn : defnlhs' + p[0] = p[1] + +def p_typeddefn_defnlhs_colon_atype(p): + 'typeddefn : defnlhs COLON atype' + p[0] = p[1] + p[0].sort = p[3] + +def p_defnrhs_fmla(p): + 'defnrhs : fmla' + p[0] = check_non_temporal(p[1]) + +def p_defnrhs_somevarfmla(p): + 'defnrhs : somevarfmla' + p[0] = check_non_temporal(p[1]) + +def p_defnrhs_nativequote(p): + 'defnrhs : NATIVEQUOTE' + text,bqs = parse_nativequote(p,1) + p[0] = NativeExpr(*([text] + bqs)) + p[0].lineno = get_lineno(p,1) + def p_defn_atom_fmla(p): - 'defn : defnlhs EQ fmla' - p[0] = Definition(app_to_atom(p[1]),check_non_temporal(p[3])) + 'defn : typeddefn EQ defnrhs' + p[0] = Definition(app_to_atom(p[1]),p[3]) p[0].lineno = get_lineno(p,2) -def p_defn_defnlhs_eq_nativequote(p): - 'defn : defnlhs EQ NATIVEQUOTE' - text,bqs = parse_nativequote(p,3) - p[0] = Definition(app_to_atom(p[1]),NativeExpr(*([text] + bqs))) - p[0].lineno = get_lineno(p,2) +# def p_defn_defnlhs_eq_(p): +# 'defn : typeddefn EQ NATIVEQUOTE' +# text,bqs = parse_nativequote(p,3) +# p[0] = Definition(app_to_atom(p[1]),NativeExpr(*([text] + bqs))) +# p[0].lineno = get_lineno(p,2) def p_optin(p): 'optin : ' @@ -1885,11 +1910,6 @@ def p_somevarfmla_some_simplevar_dot_fmla(p): p[0] = SomeExpr(*([p[2],p[4]]+p[5]+p[6])) p[0].lineno = get_lineno(p,1) -def p_defn_atom_somevarfmla(p): - 'defn : defnlhs EQ somevarfmla' - p[0] = Definition(app_to_atom(p[1]),check_non_temporal(p[3])) - p[0].lineno = get_lineno(p,2) - def p_expr_fmla(p): 'expr : LCB fmla RCB' p[0] = NamedSpace(Literal(1,check_non_temporal(p[2]))) diff --git a/ivy/ivy_printer.py b/ivy/ivy_printer.py index 152274e..35c4308 100644 --- a/ivy/ivy_printer.py +++ b/ivy/ivy_printer.py @@ -18,7 +18,8 @@ def print_module(mod): ('property',mod.labeled_props), ('init',mod.labeled_inits), ('conjecture',mod.labeled_conjs), - ('definition',mod.definitions),]: + ('definition',mod.definitions), + ('definition',mod.native_definitions),]: thing += labeled_fmlas_to_str(kwd,lst) diff --git a/ivy/ivy_to_cpp.py b/ivy/ivy_to_cpp.py index 82171ac..fd1fb06 100755 --- a/ivy/ivy_to_cpp.py +++ b/ivy/ivy_to_cpp.py @@ -108,6 +108,18 @@ def varname(name): name = re.sub(puncs,'__',name) return name.split(':')[-1] +def funname(name): + if not isinstance(name,str): + name = name.name + if name[0].isdigit(): + return '__num' + name + if name[0] == '-': + return '__negnum'+name + if name[0] == '"': + raise IvyError(None,"cannot compile a function whose name is a quoted string") + return varname(name) + + def mk_nondet(code,v,rng,name,unique_id): global nondet_cnt indent(code) @@ -373,7 +385,6 @@ def gather_referenced_symbols(expr,res,ignore=[]): def make_thunk(impl,vs,expr): - print 'im.module.destructor_sorts.keys(): {}'.format(im.module.destructor_sorts.keys()) global the_classname dom = [v.sort for v in vs] D = ctuple(dom,classname=the_classname) @@ -1025,7 +1036,7 @@ def may_alias(x,y): # emit parameter declarations of the approriate parameter types def emit_param_decls(header,name,params,extra=[],classname=None,ptypes=None): - header.append(varname(name) + '(') + header.append(funname(name) + '(') header.append(', '.join(extra + [ctype(p.sort,classname=classname,ptype = ptypes[idx] if ptypes else None) + ' ' + varname(p.name) for idx,p in enumerate(params)])) header.append(')') @@ -2407,7 +2418,7 @@ class z3_thunk : public thunk { .format(classname,' '.join(map(varname,im.module.params)))) impl.append(' __ivy_exit(1);\n }\n') impl.append(' std::vector args;\n') - impl.append(' std::vector arg_values(1);\n') + impl.append(' std::vector arg_values({});\n'.format(len(im.module.params))) impl.append(' for(int i = 1; i < argc;i++){args.push_back(argv[i]);}\n') for idx,s in enumerate(im.module.params): impl.append(' int p__'+varname(s)+';\n') @@ -2539,13 +2550,11 @@ def emit_one_initial_state(header): 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 raise IvyError(None,'Initial condition is inconsistent') used = ilu.used_symbols_clauses(clauses) - iu.dbg('used') for sym in all_state_symbols(): if sym.name in im.module.destructor_sorts: continue @@ -2556,7 +2565,6 @@ def emit_one_initial_state(header): if sym in used: assign_symbol_from_model(header,sym,m) else: - iu.dbg('sym') mk_nondet_sym(header,sym,'init',0) action = ia.Sequence(*[a for n,a in im.module.initializers]) action.emit(header) @@ -2564,6 +2572,9 @@ def emit_one_initial_state(header): def emit_constant(self,header,code): + if self in is_derived: + code.append(funname(self.name)+'()') + return if isinstance(self,il.Symbol) and self.is_numeral(): if is_native_sym(self) or self.sort.name in im.module.sort_destructors: raise iu.IvyError(None,"cannot compile symbol {} of sort {}".format(self.name,self.sort)) @@ -2575,7 +2586,6 @@ def emit_constant(self,header,code): code.append(sort_to_cpptype[self.sort].literal(self.name)) return code.append(varname(self.name)) - global is_derived if self in is_derived: code.append('()') @@ -2679,7 +2689,7 @@ def emit_app(self,header,code,capture_args=None): skip_params = 1 # handle uninterpreted ops else: - code.append(varname(self.func.name)) + code.append(funname(self.func.name)) global is_derived if self.func in is_derived: code.append('(') @@ -2812,8 +2822,6 @@ 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)