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

working on testing tutorial

This commit is contained in:
Ken McMillan 2016-09-30 18:45:09 -07:00
Родитель 19e1eee7cc
Коммит bfca910450
5 изменённых файлов: 77 добавлений и 65 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

29
doc/examples/testing/token_ring.ivy
Просмотреть файл

@ -41,7 +41,7 @@ instance trans : transport(net,packet.t,node.t)
################################################################################ ################################################################################
include udp include udp
instance net : udp_simple(node.t,trans.impl.net_msg.t) instance net : udp_simple(node.t,trans.net_msg.t)
@ -79,21 +79,24 @@ object serv = {
# #
################################################################################ ################################################################################
object proto = { object proto(me:node.t) = {
relation token(X:node.t) relation token
init token(X) <-> X = 0 after init {
individual pkt : packet.t token := me = 0
}
implement serv.release(me:node.t) { implement serv.release {
if token(me) { if token {
token(me) := false; token := false;
call trans.send(me,node.next(me),pkt) local pkt : packet.t {
call trans.send(me,node.next(me),pkt)
}
} }
} }
implement trans.recv(me:node.t,pkt:packet.t) { implement trans.recv(pkt:packet.t) {
token(me) := true; token := true;
call serv.grant(me) call serv.grant(me)
} }
} }
@ -105,4 +108,6 @@ trusted isolate iso_p = proto with serv,node,trans
trusted isolate iso_t = trans with net,node trusted isolate iso_t = trans with net,node
trusted isolate iso_n = net with node trusted isolate iso_n = net with node
#extract iso_impl(me:node.t) = proto(me),net(me),timer(me),node,id,asgn trusted isolate iso_pt = proto with serv,trans.impl,net.impl,node
extract iso_impl(me:node.t) = proto(me),trans.impl(me),net(me),node,trans.seq_num

29
doc/examples/testing/trans.ivy
Просмотреть файл

@ -28,23 +28,24 @@ module transport(lower,packet,id) = {
} }
} }
instance seq_num : sequence_numbers
# these type describe the format of messages
type mtype = {msg_t, ack_t}
object net_msg = {
type t = struct {
mty : mtype,
src : id,
num : seq_num.t,
payload : packet
}
}
object impl(me:id) = { object impl(me:id) = {
# these type describe the format of messages
type mtype = {msg_t, ack_t}
instance seq_num : sequence_numbers
object net_msg = {
type t = struct {
mty : mtype,
src : id,
num : seq_num.t,
payload : packet
}
}
# Create one outgoing message queue for each host # Create one outgoing message queue for each host
# and a timout for each queue. # and a timout for each queue.

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

@ -34,10 +34,10 @@ module udp_wrapper(addr,pkt,me) = {
} }
virtual void read() { virtual void read() {
//std::cout << "RECEIVING\n"; //std::cout << "RECEIVING\n";
int len; int len=0;
socklen_t lenlen; socklen_t lenlen=4;
if (getsockopt(sock,SOL_SOCKET,SO_RCVBUF,&len,&lenlen)) if (getsockopt(sock,SOL_SOCKET,SO_RCVBUF,&len,&lenlen))
{ std::cerr << "getsockopt failed\n"; exit(1); } { perror("getsockopt failed"); exit(1); }
std::vector<char> buf(len); std::vector<char> buf(len);
int bytes; int bytes;
if ((bytes = recvfrom(sock,&buf[0],sizeof(`pkt`),0,0,0)) < 0) if ((bytes = recvfrom(sock,&buf[0],sizeof(`pkt`),0,0,0)) < 0)

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

@ -230,8 +230,9 @@ def strip_action(ast,strip_map,strip_binding):
new_args = args[len(strip_params):] new_args = args[len(strip_params):]
new_symbol = ivy_logic.Symbol(name,new_sort) new_symbol = ivy_logic.Symbol(name,new_sort)
return new_symbol(*new_args) return new_symbol(*new_args)
if isinstance(ast,ivy_ast.Atom): if isinstance(ast,ivy_ast.Atom) and ast.rep not in im.module.sig.sorts:
name = ast.rep name = ast.rep
iu.dbg('ast')
strip_params = get_strip_params(name,ast.args,strip_map,strip_binding,ast) strip_params = get_strip_params(name,ast.args,strip_map,strip_binding,ast)
if strip_params: if strip_params:
new_args = args[len(strip_params):] new_args = args[len(strip_params):]
@ -330,6 +331,7 @@ def strip_isolate(mod,isolate,impl_mixins,extra_strip):
strip_binding = dict(zip(action.formal_params,strip_params)) strip_binding = dict(zip(action.formal_params,strip_params))
# if isinstance(action,ia.NativeAction) and len(strip_params) != num_isolate_params: # if isinstance(action,ia.NativeAction) and len(strip_params) != num_isolate_params:
# raise iu.IvyError(None,'foreign function {} may be interfering'.format(name)) # raise iu.IvyError(None,'foreign function {} may be interfering'.format(name))
iu.dbg('name')
new_action = strip_action(action,strip_map,strip_binding) new_action = strip_action(action,strip_map,strip_binding)
new_action.formal_params = action.formal_params[len(strip_params):] new_action.formal_params = action.formal_params[len(strip_params):]
new_action.formal_returns = action.formal_returns new_action.formal_returns = action.formal_returns

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

@ -1124,6 +1124,9 @@ void __deser<bool>(const std::vector<char> &inp, unsigned &pos, bool &res) {
class gen; class gen;
""")
if target.get() in ["gen","test"]:
impl.append("""
template <class T> void __from_solver( gen &g, const z3::expr &v, T &res); template <class T> void __from_solver( gen &g, const z3::expr &v, T &res);
template <> template <>
@ -1399,41 +1402,42 @@ class z3_thunk : public thunk<D,R> {
for v in vs: for v in vs:
close_loop(impl,[v]) close_loop(impl,[v])
close_scope(impl) close_scope(impl)
impl.append('template <>\n') if target.get() in ["gen","test"]:
open_scope(impl,line='void __from_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &res)') impl.append('template <>\n')
for idx,sym in enumerate(destrs): open_scope(impl,line='void __from_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &res)')
fname = memname(sym) for idx,sym in enumerate(destrs):
vs = variables(sym.sort.dom[1:]) fname = memname(sym)
for v in vs: vs = variables(sym.sort.dom[1:])
open_loop(impl,[v]) for v in vs:
code_line(impl,'__from_solver(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'),res.'+fname+''.join('[{}]'.format(varname(v)) for v in vs) + ')') open_loop(impl,[v])
for v in vs: code_line(impl,'__from_solver(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'),res.'+fname+''.join('[{}]'.format(varname(v)) for v in vs) + ')')
close_loop(impl,[v]) for v in vs:
close_scope(impl) close_loop(impl,[v])
impl.append('template <>\n') close_scope(impl)
open_scope(impl,line='z3::expr __to_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &val)') impl.append('template <>\n')
code_line(impl,'z3::expr res = g.ctx.bool_val(1)') open_scope(impl,line='z3::expr __to_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &val)')
for idx,sym in enumerate(destrs): code_line(impl,'z3::expr res = g.ctx.bool_val(1)')
fname = memname(sym) for idx,sym in enumerate(destrs):
vs = variables(sym.sort.dom[1:]) fname = memname(sym)
for v in vs: vs = variables(sym.sort.dom[1:])
open_loop(impl,[v]) for v in vs:
code_line(impl,'res = res && __to_solver(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'),val.'+fname+''.join('[{}]'.format(varname(v)) for v in vs) + ')') open_loop(impl,[v])
for v in vs: code_line(impl,'res = res && __to_solver(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'),val.'+fname+''.join('[{}]'.format(varname(v)) for v in vs) + ')')
close_loop(impl,[v]) for v in vs:
code_line(impl,'return res') close_loop(impl,[v])
close_scope(impl) code_line(impl,'return res')
impl.append('template <>\n') close_scope(impl)
open_scope(impl,line='void __randomize<' + cfsname + '>( gen &g, const z3::expr &v)') impl.append('template <>\n')
for idx,sym in enumerate(destrs): open_scope(impl,line='void __randomize<' + cfsname + '>( gen &g, const z3::expr &v)')
fname = memname(sym) for idx,sym in enumerate(destrs):
vs = variables(sym.sort.dom[1:]) fname = memname(sym)
for v in vs: vs = variables(sym.sort.dom[1:])
open_loop(impl,[v]) for v in vs:
code_line(impl,'__randomize<'+ctypefull(sym.sort.rng,classname=classname)+'>(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'))') open_loop(impl,[v])
for v in vs: code_line(impl,'__randomize<'+ctypefull(sym.sort.rng,classname=classname)+'>(g,g.apply("'+sym.name+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'))')
close_loop(impl,[v]) for v in vs:
close_scope(impl) close_loop(impl,[v])
close_scope(impl)
emit_all_ctuples_to_solver(impl,classname) emit_all_ctuples_to_solver(impl,classname)