microsoft
/
ivy
зеркало из https://github.com/microsoft/ivy.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

adding isolate = this

This commit is contained in:
Ken McMillan 2016-12-19 10:35:40 -08:00
Родитель 846e453743
Коммит a026360603
14 изменённых файлов: 224 добавлений и 42 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

28
doc/examples/paraminit3_expect.py Normal file
Просмотреть файл

@ -0,0 +1,28 @@
import pexpect
import sys
def run(name,opts,res):
child = pexpect.spawn('./{} 0'.format(name))
child.logfile = sys.stdout
try:
child.expect('>')
child.sendline('foo.get_bit')
child.expect(r'= 1')
except pexpect.EOF:
print child.before
return False
finally:
child.close()
child = pexpect.spawn('./{} 1'.format(name))
child.logfile = sys.stdout
try:
child.expect('>')
child.sendline('foo.get_bit')
child.expect(r'= 0')
return True
except pexpect.EOF:
print child.before
return False
finally:
child.close()

17
doc/examples/paraminit_expect.py Normal file
Просмотреть файл

@ -0,0 +1,17 @@
import pexpect
import sys
def run(name,opts,res):
child = pexpect.spawn('./{} 0'.format(name))
child.logfile = sys.stdout
try:
child.expect('>')
child.sendline('foo.get_bit')
child.expect(r'= 0')
return True
except pexpect.EOF:
print child.before
return False
finally:
child.close()

2
ivy/include/udp.ivy
Просмотреть файл

@ -82,7 +82,7 @@ module udp_wrapper(addr,pkt,me) = {
}
implement send(dst:addr,x:pkt) {
<<<
<<< impure
`rdr`->write(`dst`,`x`);
>>>
}

10
ivy/ivy_actions.py
Просмотреть файл

@ -778,6 +778,16 @@ class LetAction(Action):
class NativeAction(Action):
""" Quote native code in an action """
def __init__(self,*args):
self.args = list(args)
self.impure = False
if isinstance(args[0].code,str) and args[0].code.split('\n')[0].strip() == "impure":
args[0].code = '\n'.join(args[0].code.split('\n')[1:])
self.impure = True
def clone(self,args):
res = Action.clone(self,args)
res.impure = self.impure
return res
def name(self):
return 'native'
def __str__(self):

6
ivy/ivy_ast.py
Просмотреть файл

@ -156,6 +156,12 @@ class Exists(Quantifier):
pass
class This(AST):
@property
def rep(self):
return 'this'
@property
def relname(self):
return 'this'
pass
class Atom(Formula):

23
ivy/ivy_ev_parser.py
Просмотреть файл

@ -166,6 +166,27 @@ class EventRevGen(object):
for ev in self.rec(evs,self.addr):
yield ev
class EventFwdGen(object):
def __init__(self,addr):
self.addr = addr
def rec(self,things,addr,start=0):
if addr != None:
cs = addr.split('/',1)
num = int(cs[0])-start
thing = things[num]
caddr = cs[1] if len(cs) == 2 else None
for a,t in self.rec(thing.children,caddr,start=1):
yield (cs[0]+'/'+a,t)
else:
num = -1
for idx in range(num+1,len(things)):
thing = things[idx]
yield str(idx+start),thing
for a,t in self.rec(thing.children,None,start=1):
yield str(idx+start)+'/'+a,t
def __call__(self,evs):
for ev in self.rec(evs,self.addr):
yield ev
class Anchor(object):
def __init__(self,anchor):
@ -391,7 +412,7 @@ if __name__ == '__main__':
if not s: continue
result = parser.parse(s)
# print result
for a,x in EventRevGen("2/2")(result):
for a,x in EventFwdGen("2/2")(result):
print a + ':' + x.text()

13
ivy/ivy_ev_viewer.py
Просмотреть файл

@ -57,10 +57,16 @@ class EventTree(Tix.Tree,uu.WithMenuBar):
ask_pat(self,self.do_find_reverse,"Find")
def do_find_reverse(self,pats):
self.do_find(pats,ev.EventRevGen)
def do_find_forward(self,pats):
self.do_find(pats,ev.EventFwdGen)
def do_find(self,pats,gen):
sel = self.hlist.info_selection()
anchor_addr = sel[0] if len(sel) else None
anchor_ev = lookup(self.evs,anchor_addr) if anchor_addr else None
res = ev.find(ev.EventRevGen(anchor_addr)(self.evs),pats,anchor=anchor_ev)
res = ev.find(gen(anchor_addr)(self.evs),pats,anchor=anchor_ev)
if res == None:
uu.ok_dialog(the_ui.tk,self,'Pattern not found')
return
@ -134,7 +140,10 @@ class PatternList(Tix.Frame):
self.notebook.current().do_find_reverse(self.patlist[item])
def forward(self):
pass
sel = self.tlist.info_selection()
if len(sel):
item = int(sel[0])
self.notebook.current().do_find_forward(self.patlist[item])
def plus(self):
ask_pat(self,self.do_plus,command_label="Add")

27
ivy/ivy_isolate.py
Просмотреть файл

@ -161,7 +161,7 @@ def startswith_some_rec(s,prefixes,mod):
if s in mod.privates:
return False
parts = s.rsplit(iu.ivy_compose_character,1)
return len(parts)==2 and startswith_eq_some_rec(parts[0],prefixes,mod)
return startswith_eq_some_rec(parts[0],prefixes,mod) if len(parts)==2 else 'this' in prefixes
#def startswith_eq_some(s,prefixes):
# return any(s.startswith(name+iu.ivy_compose_character) or s == name for name in prefixes)
@ -382,6 +382,9 @@ def has_side_effect_rec(mod,new_actions,actname,memo):
memo.add(actname)
action = new_actions[actname]
for sub in action.iter_subactions():
if isinstance(sub,ia.NativeAction):
if sub.impure:
return True
for sym in sub.modifies():
if sym.name in mod.sig.symbols:
return True
@ -571,10 +574,12 @@ def set_privates_prefer(mod,isolate,preferred):
verified = set(a.relname for a in (isolate.verified()))
suff = "impl" if preferred == "spec" else "spec"
mod.privates = set(mod.privates)
if 'this' not in verified and suff in mod.hierarchy and preferred in mod.hierarchy:
mod.privates.add(suff)
for n,l in mod.hierarchy.iteritems():
if n not in verified:
if suff in l and preferred in l:
mod.privates.add(n+iu.ivy_compose_character+suff)
mod.privates.add(iu.compose_names(n,suff))
def set_privates(mod,isolate,suff=None):
if suff == None and opt_prefer_impls.get():
@ -582,9 +587,11 @@ def set_privates(mod,isolate,suff=None):
return
suff = suff or ("spec" if isinstance(isolate,ivy_ast.ExtractDef) else "impl")
mod.privates = set(mod.privates)
if suff in mod.hierarchy:
mod.privates.add(suff)
for n,l in mod.hierarchy.iteritems():
if suff in l:
mod.privates.add(n+iu.ivy_compose_character+suff)
mod.privates.add(iu.compose_names(n,suff))
def get_props_proved_in_isolate(mod,isolate):
save_privates = mod.privates
@ -605,7 +612,7 @@ def get_isolate_info(mod,isolate,kind,extra_with=[]):
derived = set(ldf.formula.args[0].rep.name for ldf in mod.definitions)
for name in present:
if (name not in mod.hierarchy
if (name != 'this' and name not in mod.hierarchy
and name not in ivy_logic.sig.sorts
and name not in derived
and name not in ivy_logic.sig.interp
@ -613,7 +620,7 @@ def get_isolate_info(mod,isolate,kind,extra_with=[]):
and name not in ivy_logic.sig.symbols):
raise iu.IvyError(None,"{} is not an object, action, sort, definition, or interpreted function".format(name))
xtra = set(a.relname + iu.ivy_compose_character + kind for a in isolate.verified())
xtra = set(iu.compose_names(a.relname,kind) for a in isolate.verified())
verified.update(xtra)
present.update(xtra)
@ -651,9 +658,13 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
global implementation_map
implementation_map = {}
if isolate_name not in mod.isolates:
raise iu.IvyError(None,"undefined isolate: {}".format(isolate_name))
isolate = mod.isolates[isolate_name]
if isolate_name == None:
isolate = ivy_ast.IsolateDef(ivy_ast.Atom('iso'),ivy_ast.Atom('this'))
isolate.with_args = 0
else:
if isolate_name not in mod.isolates:
raise iu.IvyError(None,"undefined isolate: {}".format(isolate_name))
isolate = mod.isolates[isolate_name]
set_privates(mod,isolate)
verified,present = get_isolate_info(mod,isolate,'impl',extra_with)

7
ivy/ivy_parser.py
Просмотреть файл

@ -1187,6 +1187,13 @@ def p_callatom_atom(p):
'callatom : atom'
p[0] = p[1]
if not (iu.get_numeric_version() <= [1,5]):
def p_callatom_this(p):
'callatom : THIS'
p[0] = This()
p[0].lineno = get_lineno(p,1)
if iu.get_numeric_version() <= [1,2]:
def p_callatom_callatom_colon_callatom(p):

39
ivy/ivy_to_cpp.py
Просмотреть файл

@ -1437,7 +1437,9 @@ class z3_thunk : public thunk<D,R> {
enum_sort_names = [s for s in sorted(il.sig.sorts) if isinstance(il.sig.sorts[s],il.EnumeratedSort)]
if True or target.get() == "repl":
for sort_name in sorted(im.module.sort_destructors):
for sort_name in im.module.sort_order:
if sort_name not in sorted(im.module.sort_destructors):
continue
destrs = im.module.sort_destructors[sort_name]
sort = im.module.sig.sorts[sort_name]
csname = varname(sort_name)
@ -1608,21 +1610,22 @@ class z3_thunk : public thunk<D,R> {
code_line(impl,'__deser(inp,pos,__res)')
code_line(impl,'res = ({})__res'.format(cfsname))
close_scope(impl)
impl.append('template <>\n')
open_scope(impl,line='z3::expr __to_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &val)')
code_line(impl,'int thing = val')
code_line(impl,'return __to_solver<int>(g,v,thing)')
close_scope(impl)
impl.append('template <>\n')
open_scope(impl,line='void __from_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &res)')
code_line(impl,'int temp')
code_line(impl,'__from_solver<int>(g,v,temp)')
code_line(impl,'res = ('+cfsname+')temp')
close_scope(impl)
impl.append('template <>\n')
open_scope(impl,line='void __randomize<' + cfsname + '>( gen &g, const z3::expr &v)')
code_line(impl,'__randomize<int>(g,v)')
close_scope(impl)
if target.get() in ["test","gen"]:
impl.append('template <>\n')
open_scope(impl,line='z3::expr __to_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &val)')
code_line(impl,'int thing = val')
code_line(impl,'return __to_solver<int>(g,v,thing)')
close_scope(impl)
impl.append('template <>\n')
open_scope(impl,line='void __from_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &res)')
code_line(impl,'int temp')
code_line(impl,'__from_solver<int>(g,v,temp)')
code_line(impl,'res = ('+cfsname+')temp')
close_scope(impl)
impl.append('template <>\n')
open_scope(impl,line='void __randomize<' + cfsname + '>( gen &g, const z3::expr &v)')
code_line(impl,'__randomize<int>(g,v)')
close_scope(impl)
@ -1683,6 +1686,8 @@ class z3_thunk : public thunk<D,R> {
def check_representable(sym,ast=None,skip_args=0):
return True
def really_check_representable(sym,ast=None,skip_args=0):
sort = sym.sort
if hasattr(sort,'dom'):
for domsort in sort.dom[skip_args:]:
@ -1737,7 +1742,7 @@ def assign_symbol_from_model(header,sym,m):
if sym.name in im.module.destructor_sorts:
return # skip structs
name, sort = sym.name,sym.sort
check_representable(sym)
really_check_representable(sym)
fun = lambda v: cstr(m.eval_to_constant(v))
if hasattr(sort,'dom'):
for args in itertools.product(*[range(sort_card(s)) for s in sym.sort.dom]):

2
ivy/ivy_utils.py
Просмотреть файл

@ -470,6 +470,8 @@ def get_numeric_version():
return map(int,string.split(ivy_language_version,'.'))
def compose_names(*names):
if names[0] == 'this':
return ivy_compose_character.join(names[1:])
return ivy_compose_character.join(names)
def split_name(name):

33
test/run_expects.py
Просмотреть файл

@ -73,17 +73,19 @@ tests = [
repls = [
['../doc/examples',
[
# ['leader_election_ring_repl','isolate=iso_impl','leader_election_ring_repl_iso_impl_expect'],
# ['helloworld',None],
# ['account',None],
# ['account2',None],
# ['account3',None],
# ['leader_election_ring_repl',None],
# ['udp_test','isolate=iso_impl',None],
# ['udp_test2','isolate=iso_impl',None],
# ['leader_election_ring_udp','isolate=iso_impl',None],
['leader_election_ring_repl','isolate=iso_impl','leader_election_ring_repl_iso_impl_expect'],
['helloworld',None],
['account',None],
['account2',None],
['account3',None],
['leader_election_ring_repl',None],
['udp_test','isolate=iso_impl',None],
['udp_test2','isolate=iso_impl',None],
['leader_election_ring_udp','isolate=iso_impl',None],
['timeout_test',None],
['leader_election_ring_udp2','isolate=iso_impl',None],
['paraminit','isolate=iso_foo',None],
['paraminit3','isolate=iso_foo',None],
]
]
]
@ -92,7 +94,10 @@ to_cpps = [
['../doc/examples',
[
['leader_election_ring_repl_err','target=repl','isolate=iso_impl','leader_election_ring_repl_err.ivy: line 90: error: relevant axiom asgn.injectivity not enforced'],
# ['leader_election_ring_repl_err2','target=repl','isolate=iso_impl','leader_election_ring_repl.ivy: error: No implementation for action node.get_next'],
['leader_election_ring_repl_err2','target=repl','isolate=iso_impl','leader_election_ring_repl.ivy: error: No implementation for action node.get_next'],
['leader_election_ring_udp2_warn','target=repl','isolate=iso_impl','leader_election_ring_udp2_warn.ivy: line 131: warning: action sec.timeout is implicitly exported'],
['paraminit','target=repl','error: cannot compile "foo.bit" because type t is uninterpreted'],
['paraminit2','target=repl','isolate=iso_foo','paraminit2.ivy: line 7: error: initial condition depends on stripped parameter'],
]
]
]
@ -156,7 +161,9 @@ class IvyRepl(Test):
class IvyToCpp(Test):
def command(self):
return 'ivy_to_cpp ' + ' '.join(self.opts) + ' '+self.name+'.ivy'
res = 'ivy_to_cpp ' + ' '.join(self.opts) + ' '+self.name+'.ivy'
print 'compiling: {}'.format(res)
return res
all_tests = []
@ -168,8 +175,8 @@ def get_tests(cls,arr):
#get_tests(IvyCheck,checks)
#get_tests(IvyTest,tests)
get_tests(IvyRepl,repls)
#get_tests(IvyToCpp,to_cpps)
#get_tests(IvyRepl,repls)
get_tests(IvyToCpp,to_cpps)
num_failures = 0
for test in all_tests:

24
test/this1.ivy Normal file
Просмотреть файл

@ -0,0 +1,24 @@
#lang ivy1.6
action foo(inp:bool)
object spec = {
before foo {
assert inp
}
}
object impl = {
individual thing : bool
implement foo {
thing := inp
}
}
export foo
isolate iso_this = this

35
test/this2.ivy Normal file
Просмотреть файл

@ -0,0 +1,35 @@
#lang ivy1.6
action foo(inp:bool)
object spec = {
before foo {
assert inp
}
}
object impl = {
individual thing : bool
object bar = {
object spec = {
after foo {
assert thing
}
}
object impl = {
implement foo {
thing := inp
}
}
}
}
export foo
isolate iso_this = this