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

Merge branch 'testing2' of https://github.com/Microsoft/ivy into testing2

This commit is contained in:
Kenneth McMillan 2017-05-04 16:09:45 -07:00
Родитель 664cf947c4 3819ba0d59
Коммит b92efbe791
8 изменённых файлов: 35 добавлений и 23 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

2
doc/examples/account2_expect.py
Просмотреть файл

@ -7,7 +7,7 @@ def run(name,opts,res):
try:
child.expect('>')
child.sendline('account.withdraw(4)')
child.expect('account2.ivy: line 29: : assumption failed')
child.expect('assumption failed')
return True
except pexpect.EOF:
print child.before

2
doc/examples/leader_election_ring_repl_expect.py
Просмотреть файл

@ -16,7 +16,7 @@ def run(name,opts,res):
child.expect(r'serv.elect\(0\)')
child.expect('>')
child.sendline('trans.recv(0,0)')
child.expect(r'leader_election_ring_repl.ivy: line 113: : assumption failed')
child.expect(r'assumption failed')
return True
except pexpect.EOF:
print child.before

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

@ -44,7 +44,7 @@ module udp_wrapper(addr,pkt,me,port_base) = {
{ perror("getsockopt failed"); exit(1); }
std::vector<char> buf(len);
int bytes;
if ((bytes = recvfrom(sock,&buf[0],sizeof(`pkt`),0,0,0)) < 0)
if ((bytes = recvfrom(sock,&buf[0],len,0,0,0)) < 0)
{ std::cerr << "recvfrom failed\n"; exit(1); }
buf.resize(bytes);
`pkt` pkt;

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

@ -925,7 +925,8 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
for actname,action in mod.actions.iteritems():
if startswith_eq_some(actname,present,mod):
for c in action.iter_calls():
called = mod.actions[c]
imp = implementation_map.get(c,c)
called = mod.actions[imp]
if not startswith_eq_some(c,present,mod) and c not in extra_with and not c.startswith('imp__'):
if not(type(called) == ia.Sequence and not called.args):
if (isinstance(called,ia.NativeAction) or
@ -1167,7 +1168,7 @@ def create_isolate(iso,mod = None,**kwargs):
if name in orig_imports or not(iso and iso in mod.isolates
and isinstance(mod.isolates[iso],ivy_ast.ExtractDef)):
newimps.append(ivy_ast.ImportDef(ivy_ast.Atom(extname),ivy_ast.Atom('')))
extra_with.append(ivy_ast.Atom(impname))
extra_with.append(ivy_ast.Atom(impname))
# extra_with.append(ivy_ast.Atom(extname))
if iso and iso in mod.isolates and name in orig_imports:
ps = mod.isolates[iso].params()

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

@ -73,9 +73,8 @@ def indent_code(header,code):
def sym_decl(sym,c_type = None,skip_params=0,classname=None):
name, sort = sym.name,sym.sort
dims = []
if not c_type:
c_type,dims = ctype_function(sort,skip_params=skip_params,classname=classname)
res = c_type + ' '
the_c_type,dims = ctype_function(sort,skip_params=skip_params,classname=classname)
res = (c_type or the_c_type) + ' '
res += memname(sym) if skip_params else varname(sym.name)
for d in dims:
res += '[' + str(d) + ']'
@ -420,7 +419,7 @@ def emit_cpp_sorts(header):
sort_to_cpptype[il.sig.sorts[name]] = cpptype
elif name in il.sig.interp:
itp = il.sig.interp[name]
if not (itp.startswith('{') or itp.startswith('bv[') or itp in ['int','strlit']):
if not (isinstance(itp,il.EnumeratedSort) or itp.startswith('{') or itp.startswith('bv[') or itp in ['int','strlit']):
cpptype = ivy_cpp_types.get_cpptype_constructor(itp)(varname(name))
cpptypes.append(cpptype)
sort_to_cpptype[il.sig.sorts[name]] = cpptype
@ -431,6 +430,10 @@ def emit_sorts(header):
for name,sort in il.sig.sorts.iteritems():
if name == "bool":
continue
if name in il.sig.interp:
sortname = il.sig.interp[name]
if isinstance(sortname,il.EnumeratedSort):
sort = sortname
if not isinstance(sort,il.EnumeratedSort):
if name in il.sig.interp:
sortname = il.sig.interp[name]
@ -3935,11 +3938,16 @@ public:
}
model = slvr.get_model();
alits.clear();
""".replace('classname',classname))
if target.get() != "gen":
header.append("""
if(__ivy_modelfile.is_open()){
__ivy_modelfile << "begin sat:\\n" << slvr << "end sat:\\n" << std::endl;
__ivy_modelfile << model;
__ivy_modelfile.flush();
}
""")
header.append("""
return true;
}

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

@ -9,7 +9,7 @@ from ivy import ivy_to_cpp as i2c
from ivy import ivy_actions as ia
from ivy import ivy_solver as slv
from ivy import ivy_isolate as iso
from ivy import ivy_cpp
prog = """#lang ivy1.5
@ -44,7 +44,8 @@ with im.Module():
ivy_from_string(prog,create_isolate=True)
classname = 'foo'
header,impl = i2c.module_to_cpp_class(classname,classname)
with ivy_cpp.CppContext():
header,impl = i2c.module_to_cpp_class(classname,classname)
print header
print impl

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

@ -7,8 +7,8 @@ checks = [
['../doc/examples/testing',
[
['pingpong','trusted=true','OK'],
['interference','trusted=true','interference.ivy: line 30: error: Call out to right_player.intf_ping'],
['coveragefail','trusted=true','coveragefail.ivy: line 20: error: assertion is not checked'],
['interference','trusted=true','error: Call out to right_player.intf_ping'],
['coveragefail','trusted=true','error: assertion is not checked'],
]
],
['../doc/examples',
@ -27,7 +27,7 @@ checks = [
['interference2','OK'],
['interference3','OK'],
['interference4','OK'],
['interference','interference.ivy: line 30: error: Call out to right_player.intf_ping'],
['interference','error: Call out to right_player.intf_ping'],
['leader_election_ring2','error: Some assertions are not checked'],
['leader_election_ring_btw','error: Some assertions are not checked'],
['leader_election_ring','error: Some assertions are not checked'],
@ -56,14 +56,14 @@ tests = [
[
['trivnet','test_completed'],
['pingpong','isolate=iso_l','test_completed'],
['pingpong_bad','isolate=iso_l','pingpong_bad.ivy: line 15: : assertion failed'],
['pingpong_bad','isolate=iso_l','assertion failed'],
['pingpong','isolate=iso_r','test_completed'],
['leader_election_ring','isolate=iso_p','test_completed'],
['leader_election_ring','isolate=iso_n','test_completed'],
['leader_election_ring','isolate=iso_t test_iters=5','test_completed'],
['token_ring','isolate=iso_p','test_completed'],
['token_ring','isolate=iso_t','test_completed'],
['token_ring_buggy','isolate=iso_t','trans_buggy.ivy: line 26: : assertion failed'],
['token_ring_buggy','isolate=iso_t','assertion failed'],
['token_ring','isolate=iso_n','test_completed'],
['token_ring','isolate=iso_pt','test_completed'],
]
@ -93,11 +93,11 @@ repls = [
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_udp2_warn','target=repl','isolate=iso_impl','leader_election_ring_udp2_warn.ivy: line 131: warning: action sec.timeout is implicitly exported'],
['leader_election_ring_repl_err','target=repl','isolate=iso_impl','error: relevant axiom asgn.injectivity not enforced'],
['leader_election_ring_repl_err2','target=repl','isolate=iso_impl','error: No implementation for action node.get_next'],
['leader_election_ring_udp2_warn','target=repl','isolate=iso_impl','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'],
['paraminit2','target=repl','isolate=iso_foo','initial condition depends on stripped parameter'],
]
]
]
@ -173,9 +173,9 @@ def get_tests(cls,arr):
for check in checkl:
all_tests.append(cls(dir,check))
#get_tests(IvyCheck,checks)
#get_tests(IvyTest,tests)
#get_tests(IvyRepl,repls)
get_tests(IvyCheck,checks)
get_tests(IvyTest,tests)
get_tests(IvyRepl,repls)
get_tests(IvyToCpp,to_cpps)
num_failures = 0

2
test/tilelink_unit_test.sh
Просмотреть файл

@ -2,3 +2,5 @@
cd ../examples/tilelink/unit_test
ivy_to_cpp isolate=iso_b tilelink_coherence_manager_tester.ivy
g++ -c tilelink_coherence_manager_tester.cpp