зеркало из https://github.com/microsoft/ivy.git
working on per-assertion checking
This commit is contained in:
Ken McMillan
Родитель
1fcc80e22f
Коммит
4609fcfc86
|
|
@ -19,17 +19,12 @@ module table_shard(key,data) = {
|
|||
second(Y:range) : data
|
||||
}
|
||||
|
||||
instance iter : order_iterator(range)
|
||||
|
||||
function value(S:t,X:key):data
|
||||
|
||||
instance iter : order_iterator(range)
|
||||
|
||||
derived at(S,X,Y) = (first(S,Y) = X & second(S,Y) ~= 0)
|
||||
derived find(S,X) = some Y. at(S,X,Y)
|
||||
derived present(S,X) = at(S,X,find(S,X))
|
||||
|
||||
definition value(S,X) = second(S,find(S,X)) if present(S,X) else 0
|
||||
|
||||
conjecture at(S,X,Y) & at(S,X,Z) -> Y = Z
|
||||
definition value(S:t,x:key) = some Y. at(S,x,Y) in second(S,Y) else 0
|
||||
|
||||
object impl = {
|
||||
|
||||
|
|
|
|||
|
|
@ -36,8 +36,8 @@ module hash_table(key,value,shard) = {
|
|||
|
||||
after extract_ {
|
||||
assert shard.lo(res) = lo;
|
||||
assert shard.hi(res) = hi;
|
||||
assert (lo <= X & X <= hi) -> shard.value(res,X) = hash(X)
|
||||
assert shard.hi(res) <= hi;
|
||||
assert (shard.lo(res) <= X & X <= shard.hi(res)) -> shard.value(res,X) = hash(X)
|
||||
}
|
||||
|
||||
before incorporate(s:shard.t) {
|
||||
|
|
@ -69,6 +69,10 @@ module hash_table(key,value,shard) = {
|
|||
while ~shard.iter.iter_end(pos) & idx <= lim
|
||||
invariant ~shard.iter.done(X,pos) -> shard.second(res,X) = 0
|
||||
invariant lo <= X & key.iter.done(X,idx) -> shard.value(res,X) = hash(X)
|
||||
invariant ~key.iter.iter_end(idx) -> lo <= key.iter.iter_val(idx)
|
||||
invariant shard.iter.iter_end(pos) -> key.iter.done(lo,idx)
|
||||
invariant ~key.iter.done(X,idx) -> ~shard.at(res,X,Y)
|
||||
invariant shard.at(res,X,Y) & shard.at(res,X,Z) -> Y = Z
|
||||
{
|
||||
shard.first(res,shard.iter.val(pos)) := key.iter.val(idx);
|
||||
shard.second(res,shard.iter.val(pos)) := tab.get(key.iter.val(idx));
|
||||
|
|
@ -76,10 +80,10 @@ module hash_table(key,value,shard) = {
|
|||
pos := shard.iter.next(pos)
|
||||
};
|
||||
shard.lo(res) := lo;
|
||||
if key.iter.begin(hi) <= idx {
|
||||
if key.iter.done(hi,idx) {
|
||||
shard.hi(res) := hi
|
||||
} else {
|
||||
shard.hi(res) := key.iter.val(idx)
|
||||
shard.hi(res) := key.iter.val(key.iter.prev(idx))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -109,6 +113,7 @@ module hash_table(key,value,shard) = {
|
|||
|
||||
conjecture tab.s(X) & tab.r(X,Y) -> hash(X) = Y
|
||||
conjecture ~tab.s(X) -> hash(X) = 0
|
||||
conjecture tab.s(X) -> tab.r(X,hash(X))
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -284,7 +284,7 @@ module ordered_map(key,value) = {
|
|||
}
|
||||
|
||||
after get {
|
||||
assert r(k,v) & s(k) | v = 0
|
||||
assert r(k,v) & s(k) | ~s(k) & v = 0
|
||||
}
|
||||
|
||||
# erase elements in a closed interval
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ module order_iterator(range) = {
|
|||
action begin(x:range) returns (y:t)
|
||||
action end returns (y:t)
|
||||
action next(x:t) returns (y:t)
|
||||
action prev(y:t) returns (x:t)
|
||||
action val(x:t) returns (y:range)
|
||||
action over(x:t) returns (y:bool)
|
||||
|
||||
|
|
@ -40,6 +41,17 @@ module order_iterator(range) = {
|
|||
| ~(iter_val(x) < Y & Y < iter_val(y))
|
||||
& iter_val(x) < iter_val(y) & ~iter_end(y)
|
||||
}
|
||||
|
||||
before prev {
|
||||
assert iter_end(y) | exists X. X < iter_val(y)
|
||||
}
|
||||
after prev {
|
||||
assert ~iter_end(x);
|
||||
assert X <= iter_val(x) & iter_end(y)
|
||||
| ~(iter_val(x) < Y & Y < iter_val(y))
|
||||
& iter_val(x) < iter_val(y) & ~iter_end(y)
|
||||
}
|
||||
|
||||
before val {
|
||||
assert ~iter_end(x)
|
||||
}
|
||||
|
|
|
|||
|
|
@ -16,6 +16,13 @@ from ivy_ast import AST, compose_atoms, MixinAfterDef
|
|||
import ivy_module
|
||||
import ivy_utils as iu
|
||||
|
||||
def p_c_a(s):
|
||||
a = s.split(':')
|
||||
return (a[0]+'.ivy',int(a[1]))
|
||||
|
||||
checked_assert = iu.Parameter("assert","",check=lambda s: len(s.split(':'))==2,
|
||||
process=p_c_a)
|
||||
|
||||
class Schema(AST):
|
||||
def __init__(self,defn,fresh):
|
||||
self.defn,self.fresh = defn,fresh
|
||||
|
|
@ -232,6 +239,11 @@ class AssertAction(Action):
|
|||
def action_update(self,domain,pvars):
|
||||
type_check(domain,self.args[0])
|
||||
# print type(self.args[0])
|
||||
ca = checked_assert.get()
|
||||
if ca:
|
||||
if ca != self.lineno:
|
||||
return ([],formula_to_clauses(self.args[0]),false_clauses())
|
||||
iu.dbg('self')
|
||||
cl = formula_to_clauses(dual_formula(self.args[0]))
|
||||
# return ([],formula_to_clauses_tseitin(self.args[0]),cl)
|
||||
return ([],true_clauses(),cl)
|
||||
|
|
@ -677,22 +689,20 @@ class WhileAction(Action):
|
|||
def __str__(self):
|
||||
res = 'while ' + str(self.args[0]) + '\n'
|
||||
for inv in self.args[2:]:
|
||||
res += 'invariant ' + str(inv) + '\n'
|
||||
res += 'invariant ' + str(inv.args[0]) + '\n'
|
||||
res += bracket_action(self.args[1])
|
||||
return res
|
||||
def expand(self,domain,pvars):
|
||||
modset,pre,post = self.args[1].int_update(domain,pvars) # TODO:cheaper way to get modset
|
||||
asserts = [AssertAction(fmla) for fmla in self.args[2:]]
|
||||
assumes = [AssumeAction(fmla) for fmla in self.args[2:]]
|
||||
asserts = self.args[2:]
|
||||
assumes = [a.assert_to_assume() for a in asserts]
|
||||
havocs = [HavocAction(sym) for sym in modset]
|
||||
for a in asserts + assumes:
|
||||
a.lineno = self.lineno #TODO: get actual invariant lineno
|
||||
res = Sequence(*(
|
||||
asserts +
|
||||
havocs +
|
||||
assumes +
|
||||
[ChoiceAction(Sequence(),Sequence(*([AssumeAction(self.args[0]),
|
||||
self.args[1]]+asserts))),
|
||||
self.args[1]]+asserts+[AssumeAction(And())]))),
|
||||
AssumeAction(Not(self.args[0]))]))
|
||||
return res
|
||||
|
||||
|
|
|
|||
|
|
@ -58,6 +58,18 @@ def usage():
|
|||
print "usage: \n {} file.ivy".format(sys.argv[0])
|
||||
sys.exit(1)
|
||||
|
||||
def find_assertions():
|
||||
res = []
|
||||
for actname,action in im.module.actions.iteritems():
|
||||
for a in action.iter_subactions():
|
||||
if isinstance(a,act.AssertAction):
|
||||
res.append(a)
|
||||
return res
|
||||
|
||||
def show_assertions():
|
||||
for a in find_assertions():
|
||||
print '{}: {}'.format(a.lineno,a)
|
||||
|
||||
def check_module():
|
||||
# If user specifies an isolate, check it. Else, if any isolates
|
||||
# are specificied in the file, check all, else check globally.
|
||||
|
|
@ -86,6 +98,7 @@ def check_module():
|
|||
with im.module.copy():
|
||||
ivy_isolate.create_isolate(isolate) # ,ext='ext'
|
||||
with im.module.theory_context():
|
||||
print im.module.sig.symbols
|
||||
check_properties()
|
||||
ag = ivy_art.AnalysisGraph(initializer=ivy_alpha.alpha)
|
||||
if im.module.initializers:
|
||||
|
|
@ -94,12 +107,19 @@ def check_module():
|
|||
display_cex("safety failed in initializer",cex)
|
||||
with ivy_interp.EvalContext(check=False):
|
||||
check_conjectures('Initiation','These conjectures are false initially.',ag,ag.states[0])
|
||||
show_assertions()
|
||||
assertions = find_assertions()
|
||||
for a in sorted(im.module.public_actions):
|
||||
print "trying {}...".format(a)
|
||||
ag.execute_action(a,prestate=ag.states[0])
|
||||
cex = ag.check_bounded_safety(ag.states[-1])
|
||||
if cex is not None:
|
||||
display_cex("safety failed",cex)
|
||||
tried = set()
|
||||
for asn in assertions:
|
||||
if asn.lineno not in tried:
|
||||
tried.add(asn.lineno)
|
||||
act.checked_assert.value = asn.lineno
|
||||
ag.execute_action(a,prestate=ag.states[0])
|
||||
cex = ag.check_bounded_safety(ag.states[-1])
|
||||
if cex is not None:
|
||||
display_cex("safety failed",cex)
|
||||
check_conjectures('Consecution','These conjectures are not inductive.',ag,ag.states[-1])
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -357,23 +357,29 @@ def compile_action_def(a,sig):
|
|||
return res
|
||||
|
||||
def compile_defn(df):
|
||||
if isinstance(df.args[1],ivy_ast.SomeExpr):
|
||||
ifval = df.args[1].if_value() or df.args[1].params()[0]
|
||||
elseval = df.args[1].else_value() or ifval
|
||||
eqn = ivy_ast.Forall(df.args[1].params(),
|
||||
ivy_ast.Atom('=',(df.args[0],ivy_ast.Ite(df.args[1].fmla(),ifval,elseval))))
|
||||
fmla = sortify_with_inference(eqn)
|
||||
args = [list(fmla.variables)[0],fmla.body.args[1].args[0]]
|
||||
if df.args[1].if_value() :
|
||||
args.append(fmla.body.args[1].args[1])
|
||||
if df.args[1].else_value() :
|
||||
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])
|
||||
return df
|
||||
has_consts = any(not isinstance(p,ivy_ast.Variable) for p in df.args[0].args)
|
||||
sig = ivy_logic.sig.copy() if has_consts else ivy_logic.sig
|
||||
with sig:
|
||||
for p in df.args[0].args:
|
||||
if not isinstance(p,ivy_ast.Variable):
|
||||
compile_const(p,sig)
|
||||
if isinstance(df.args[1],ivy_ast.SomeExpr):
|
||||
ifval = df.args[1].if_value() or df.args[1].params()[0]
|
||||
elseval = df.args[1].else_value() or ifval
|
||||
eqn = ivy_ast.Forall(df.args[1].params(),
|
||||
ivy_ast.Atom('=',(df.args[0],ivy_ast.Ite(df.args[1].fmla(),ifval,elseval))))
|
||||
fmla = sortify_with_inference(eqn)
|
||||
args = [list(fmla.variables)[0],fmla.body.args[1].args[0]]
|
||||
if df.args[1].if_value() :
|
||||
args.append(fmla.body.args[1].args[1])
|
||||
if df.args[1].else_value() :
|
||||
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])
|
||||
return df
|
||||
|
||||
|
||||
class IvyDomainSetup(IvyDeclInterp):
|
||||
|
|
|
|||
|
|
@ -494,6 +494,22 @@ def is_epr_rec(term,uvars):
|
|||
def is_epr(term):
|
||||
return is_epr_rec(term,lu.free_variables(term))
|
||||
|
||||
def variables(sorts):
|
||||
return [Variable('V'+str(idx),s) for idx,s in enumerate(sorts)]
|
||||
|
||||
def extensionality(destrs):
|
||||
if not destrs:
|
||||
return Or()
|
||||
c = []
|
||||
sort = destrs[0].sort.dom[0]
|
||||
x,y = Variable("X",sort),Variable("Y",sort)
|
||||
for d in destrs:
|
||||
vs = variables(d.sort.dom[1:])
|
||||
c.append(Equals(d(*([x]+vs)),d(*([y]+vs))))
|
||||
res = Implies(And(*c),Equals(x,y))
|
||||
iu.dbg('res')
|
||||
return res
|
||||
|
||||
Variable = lg.Var
|
||||
Variable.args = property(lambda self: [])
|
||||
Variable.clone = lambda self,args: self
|
||||
|
|
@ -942,6 +958,8 @@ def close_formula(fmla):
|
|||
else:
|
||||
return ForAll(variables,fmla)
|
||||
|
||||
free_variables = lu.free_variables
|
||||
|
||||
def uninterpreted_sorts():
|
||||
return [s for s in sig.sorts.values() if isinstance(s,UninterpretedSort) and s.name not in sig.interp]
|
||||
|
||||
|
|
|
|||
|
|
@ -1119,9 +1119,9 @@ def dual_formula(fmla, skolemizer=None):
|
|||
fmla = negate(substitute_ast(fmla,sksubs))
|
||||
if instantiator != None:
|
||||
gts = ground_apps_ast(fmla)
|
||||
insts = instantiate(ground_terms)
|
||||
insts = clauses_to_formula(instantiator(gts))
|
||||
fmla = And(fmla,insts)
|
||||
return negate(fmla)
|
||||
return fmla
|
||||
|
||||
def reskolemize_clauses(clauses, skolemizer):
|
||||
print clauses
|
||||
|
|
|
|||
|
|
@ -84,18 +84,9 @@ class Module(object):
|
|||
return res
|
||||
|
||||
def background_theory(self, symbols=None):
|
||||
""" Return a set of clauses which represent the background theory
|
||||
restricted to the given symbols (should be like the result of used_symbols).
|
||||
"""
|
||||
theory = list(self.get_axioms())
|
||||
# axioms of the derived relations TODO: used only the
|
||||
# referenced ones, but we need to know abstract domain for
|
||||
# this
|
||||
for ldf in self.definitions:
|
||||
cnst = ldf.formula.to_constraint()
|
||||
if il.is_epr(cnst):
|
||||
theory.append(cnst) # TODO: make this a def?
|
||||
return lu.Clauses(theory)
|
||||
if hasattr(self,"theory"):
|
||||
return self.theory
|
||||
return lu.Clauses([])
|
||||
|
||||
def add_to_hierarchy(self,name):
|
||||
if iu.ivy_compose_character in name:
|
||||
|
|
@ -123,10 +114,28 @@ class Module(object):
|
|||
|
||||
def theory_context(self):
|
||||
""" Set up to instiate the non-epr axioms """
|
||||
""" Return a set of clauses which represent the background theory
|
||||
restricted to the given symbols (should be like the result of used_symbols).
|
||||
"""
|
||||
theory = list(self.get_axioms())
|
||||
# axioms of the derived relations TODO: used only the
|
||||
# referenced ones, but we need to know abstract domain for
|
||||
# this
|
||||
for ldf in self.definitions:
|
||||
cnst = ldf.formula.to_constraint()
|
||||
if all(isinstance(p,il.Variable) for p in ldf.formula.args[0].args):
|
||||
theory.append(cnst) # TODO: make this a def?
|
||||
# extensionality axioms for structs
|
||||
for sort in sorted(self.sort_destructors):
|
||||
destrs = self.sort_destructors[sort]
|
||||
if any(d.name in self.sig.symbols for d in destrs):
|
||||
theory.append(il.extensionality(destrs))
|
||||
self.theory = lu.Clauses(theory)
|
||||
|
||||
non_epr = {}
|
||||
for ldf in self.definitions:
|
||||
cnst = ldf.formula.to_constraint()
|
||||
if not il.is_epr(cnst):
|
||||
if not all(isinstance(p,il.Variable) for p in ldf.formula.args[0].args):
|
||||
non_epr[ldf.formula.defines()] = (ldf,cnst)
|
||||
return ModuleTheoryContext(functools.partial(instantiate_non_epr,non_epr))
|
||||
|
||||
|
|
@ -152,10 +161,11 @@ def instantiate_non_epr(non_epr,ground_terms):
|
|||
for term in ground_terms:
|
||||
if term.rep in non_epr and term not in matched:
|
||||
ldf,cnst = non_epr[term.rep]
|
||||
subst = dict((v.name,t) for v,t in zip(ldf.formula.args[0].args,term.args))
|
||||
inst = lu.substitute_ast(cnst,subst)
|
||||
if il.is_epr(inst):
|
||||
theory.append(inst)
|
||||
subst = dict((v,t) for v,t in zip(ldf.formula.args[0].args,term.args)
|
||||
if not isinstance(v,il.Variable))
|
||||
inst = lu.substitute_constants_ast(cnst,subst)
|
||||
theory.append(inst)
|
||||
iu.dbg('inst')
|
||||
matched.add(term)
|
||||
return lu.Clauses(theory)
|
||||
|
||||
|
|
|
|||
|
|
@ -1004,8 +1004,9 @@ else:
|
|||
'invariants : invariants INVARIANT fmla'
|
||||
p[0] = p[1]
|
||||
inv = p[3]
|
||||
inv.lineno = get_lineno(p,1)
|
||||
p[0].append(inv)
|
||||
a = AssertAction(inv)
|
||||
a.lineno = get_lineno(p,2)
|
||||
p[0].append(a)
|
||||
|
||||
def p_action_while_fmla_invariants_lcb_action_rcb(p):
|
||||
'action : WHILE fmla invariants LCB action RCB'
|
||||
|
|
@ -1166,10 +1167,33 @@ def p_defns_defns_comma_defn(p):
|
|||
p[0] = p[1]
|
||||
p[0].append(p[3])
|
||||
|
||||
def p_defnlhs_atom(p):
|
||||
'defnlhs : atom'
|
||||
p[0] = p[1]
|
||||
def p_defnlhs_symbol(p):
|
||||
'defnlhs : SYMBOL'
|
||||
p[0] = Atom(p[1],[])
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
def p_defnlhs_symbol_lparen_defargs_rparen(p):
|
||||
'defnlhs : SYMBOL LPAREN defargs RPAREN'
|
||||
p[0] = Atom(p[1],p[3])
|
||||
p[0].lineno = get_lineno(p,1)
|
||||
|
||||
def p_defargs_defarg(p):
|
||||
'defargs : defarg'
|
||||
p[0] = [p[1]]
|
||||
|
||||
def p_defargs_defargs_comma_defarg(p):
|
||||
'defargs : defargs COMMA defarg'
|
||||
p[0] = p[1]
|
||||
p[0].append(p[3])
|
||||
|
||||
def p_defarg_lparam(p):
|
||||
'defarg : lparam'
|
||||
p[0] = p[1]
|
||||
|
||||
def p_defarg_var(p):
|
||||
'defarg : var'
|
||||
p[0] = p[1]
|
||||
|
||||
def p_defnlhs_lp_term_relop_term_rp(p):
|
||||
'defnlhs : LPAREN term relop term RPAREN'
|
||||
p[0] = Atom(p[3],[p[2],p[4]])
|
||||
|
|
|
|||
|
|
@ -856,7 +856,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
|
|||
if res == z3.unsat:
|
||||
return None
|
||||
|
||||
# print "shrinking model {"
|
||||
print "shrinking model {"
|
||||
for x in chain(sorts_to_minimize, relations_to_minimize):
|
||||
for n in itertools.count(1):
|
||||
s.push()
|
||||
|
|
@ -867,7 +867,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
|
|||
break
|
||||
else:
|
||||
s.pop()
|
||||
# print "} shrinking model"
|
||||
print "} shrinking model"
|
||||
m = get_model(s)
|
||||
h = HerbrandModel(s,m,used_symbols_clauses(clauses))
|
||||
return h
|
||||
|
|
|
|||
|
|
@ -17,9 +17,11 @@ def get_qa_arcs(fmla,ast,pol,univs):
|
|||
is_e = il.is_exists(fmla)
|
||||
is_a = il.is_forall(fmla)
|
||||
if is_e and pol or is_a and not pol:
|
||||
fvs = set(il.free_variables(fmla))
|
||||
for u in univs:
|
||||
for e in il.quantifier_vars(fmla):
|
||||
yield (u.sort,e.sort,ast)
|
||||
if u in fvs:
|
||||
for e in il.quantifier_vars(fmla):
|
||||
yield (u.sort,e.sort,ast)
|
||||
if is_e and not pol or is_a and pol:
|
||||
for a in get_qa_arcs(fmla.args[0],ast,pol,univs+list(il.quantifier_vars(fmla))):
|
||||
yield a
|
||||
|
|
@ -84,6 +86,8 @@ def get_assumes_and_asserts():
|
|||
if isinstance(sa,ia.IfAction):
|
||||
asserts.append((sa.get_cond(),sa))
|
||||
|
||||
for ldf in im.module.definitions:
|
||||
assumes.append(ldf.formula.to_constraint())
|
||||
# TODO: check axioms, inits, conjectures
|
||||
|
||||
return assumes,asserts
|
||||
|
|
|
|||
|
|
@ -1,9 +1,22 @@
|
|||
#lang ivy1.6
|
||||
|
||||
type t
|
||||
type q
|
||||
type u
|
||||
|
||||
function ident(U:u,X:t):q
|
||||
relation r(U:u,X:t,Y:q)
|
||||
|
||||
definition ident(U:u,x:t) = some Y. r(U,x,Y) in Y else 0
|
||||
|
||||
action a = {
|
||||
assert r(U,X,ident(U,X)) | ident(U,X) = 0
|
||||
}
|
||||
|
||||
conjecture r(U,X,ident(U,X)) | ident(U,X) = 0
|
||||
|
||||
property r(U,X,ident(U,X)) | ident(U,X) = 0
|
||||
|
||||
|
||||
function ident(X:t):t
|
||||
|
||||
definition ident(X) = some Y. X = Y in Y else 0
|
||||
|
||||
property ident(Z) = Z
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче