зеркало из https://github.com/microsoft/ivy.git
toy_consensus now compiles and runs
This commit is contained in:
Ken McMillan
Родитель
93f2b8ec37
Коммит
b0a71c7737
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) = {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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()])
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -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'
|
||||
|
|
|
|||
|
|
@ -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])))
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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<D,R> {
|
|||
.format(classname,' '.join(map(varname,im.module.params))))
|
||||
impl.append(' __ivy_exit(1);\n }\n')
|
||||
impl.append(' std::vector<std::string> args;\n')
|
||||
impl.append(' std::vector<ivy_value> arg_values(1);\n')
|
||||
impl.append(' std::vector<ivy_value> 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)
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче