зеркало из https://github.com/microsoft/ivy.git
adding testing regression tests
This commit is contained in:
Ken McMillan
Родитель
c6923c8e76
Коммит
a66466ef36
|
|
@ -345,7 +345,7 @@ a read-eval-print loop as the environment:
|
|||
g++ -I $Z3DIR/include -L $Z3DIR/lib -g -o leader_election_ring leader_election_ring.cpp -lz3
|
||||
|
||||
This produces an executable that takes one parameter `me` on the
|
||||
command line. Let's create two terminals A annd B to run process 0 and
|
||||
command line. Let's create two terminals A and B to run process 0 and
|
||||
process 1 respectively:
|
||||
|
||||
A: $ ./leader_election_ring 0
|
||||
|
|
|
|||
|
|
@ -0,0 +1,113 @@
|
|||
#lang ivy1.6
|
||||
|
||||
object packet = {
|
||||
type t
|
||||
|
||||
interpret t -> bv[1]
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Concrete type of node addresses.
|
||||
#
|
||||
################################################################################
|
||||
|
||||
|
||||
object node = {
|
||||
type t
|
||||
|
||||
interpret t -> bv[1]
|
||||
|
||||
action next(x:t) returns (y:t) = {
|
||||
y := x + 1
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# The transport service specification
|
||||
#
|
||||
################################################################################
|
||||
|
||||
include trans_buggy
|
||||
instance trans : transport(net,packet.t,node.t)
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# The network service specification
|
||||
#
|
||||
################################################################################
|
||||
|
||||
include udp
|
||||
instance net : udp_simple(node.t,trans.net_msg.t)
|
||||
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# The high-level service specification
|
||||
#
|
||||
################################################################################
|
||||
|
||||
|
||||
object serv = {
|
||||
|
||||
action grant(v:node.t) # grant lock to client
|
||||
action release(v:node.t) # client releases lock
|
||||
|
||||
object spec = {
|
||||
relation lock(X:node.t)
|
||||
init lock(X) <-> X = 0
|
||||
|
||||
before grant {
|
||||
assert ~lock(X);
|
||||
lock(v) := true
|
||||
}
|
||||
|
||||
before release {
|
||||
assert lock(v);
|
||||
lock(v) := false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# The high-level protocol
|
||||
#
|
||||
################################################################################
|
||||
|
||||
object proto(me:node.t) = {
|
||||
|
||||
relation token
|
||||
after init {
|
||||
token := me = 0
|
||||
}
|
||||
|
||||
implement serv.release {
|
||||
if token {
|
||||
token := false;
|
||||
local pkt : packet.t {
|
||||
call trans.send(me,node.next(me),pkt)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
implement trans.recv(pkt:packet.t) {
|
||||
token := true;
|
||||
call serv.grant(me)
|
||||
}
|
||||
}
|
||||
|
||||
export serv.release
|
||||
import serv.grant
|
||||
|
||||
trusted isolate iso_p = proto with serv,node,trans
|
||||
trusted isolate iso_t = trans with net,node
|
||||
trusted isolate iso_n = net with node
|
||||
|
||||
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
|
||||
|
|
@ -94,7 +94,7 @@ module transport(lower,packet,id) = {
|
|||
if net_msg.mty(msg) = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq >= recv_seq(src) {
|
||||
else if seq = recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,net_msg.payload(msg))
|
||||
}
|
||||
|
|
|
|||
|
|
@ -0,0 +1,116 @@
|
|||
#lang ivy1.6
|
||||
|
||||
include queue
|
||||
include timeout
|
||||
include seqnum
|
||||
|
||||
module transport(lower,packet,id) = {
|
||||
|
||||
relation sent(D:id,P:packet)
|
||||
|
||||
action send(src:id,dst:id,pkt:packet)
|
||||
action recv(dst:id,pkt:packet)
|
||||
|
||||
object spec = {
|
||||
|
||||
after init {
|
||||
sent(D,P) := false
|
||||
}
|
||||
|
||||
before send {
|
||||
assert ~sent(dst,pkt);
|
||||
sent(dst,pkt) := true
|
||||
}
|
||||
|
||||
before recv {
|
||||
assert sent(dst,pkt);
|
||||
sent(dst,pkt) := false
|
||||
}
|
||||
}
|
||||
|
||||
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) = {
|
||||
|
||||
|
||||
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num)
|
||||
instance timer(D:id) : timeout_sec
|
||||
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
|
||||
individual send_seq(S:id) : seq_num.t
|
||||
individual recv_seq(S:id) : seq_num.t
|
||||
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
|
||||
# Implementations of interface actions
|
||||
|
||||
implement send(dst:id,pkt:packet) {
|
||||
local msg : net_msg.t, seq : seq_num.t {
|
||||
net_msg.mty(msg) := msg_t;
|
||||
net_msg.src(msg) := me;
|
||||
net_msg.num(msg) := send_seq(dst);
|
||||
net_msg.payload(msg) := pkt;
|
||||
send_seq(dst) := seq_num.next(send_seq(dst));
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(me,dst,msg)
|
||||
}
|
||||
}
|
||||
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
|
||||
implement lower.recv(msg:net_msg.t) {
|
||||
local src:id,seq:seq_num.t {
|
||||
seq := net_msg.num(msg);
|
||||
src := net_msg.src(msg);
|
||||
if seq <= recv_seq(src) & net_msg.mty(msg) ~= ack_t {
|
||||
local ack : net_msg.t {
|
||||
net_msg.mty(ack) := ack_t;
|
||||
net_msg.src(ack) := me;
|
||||
net_msg.num(ack) := seq;
|
||||
call lower.send(me,src,ack)
|
||||
}
|
||||
};
|
||||
if net_msg.mty(msg) = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq >= recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,net_msg.payload(msg))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send(me,dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -483,20 +483,11 @@ module map_wrapper(key,value) = {
|
|||
implement erase(lo:key.iter.t,hi:key.iter.t) {
|
||||
<<<
|
||||
|
||||
std::cout << "before: {";
|
||||
for(std::map<`key.t`,`value`>::iterator __it = `s`.begin(), __en = `s`.end(); __it != __en; ++__it)
|
||||
std::cout << __it->first << ":" << __it->second << ",";
|
||||
std::cout << "}" << std::endl;
|
||||
|
||||
if (!`lo`.is_end && (`hi`.is_end || `lo`.val < `hi`.val))
|
||||
`s`.erase(`lo`.is_end ? `s`.end() : `s`.lower_bound(`lo`.val),
|
||||
`hi`.is_end ? `s`.end() : `s`.lower_bound(`hi`.val));
|
||||
|
||||
std::cout << "after: {";
|
||||
for(std::map<`key.t`,`value`>::iterator __it = `s`.begin(), __en = `s`.end(); __it != __en; ++__it)
|
||||
std::cout << __it->first << ":" << __it->second << ",";
|
||||
std::cout << "}" << std::endl;
|
||||
|
||||
>>>
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -98,7 +98,7 @@ def varname(name):
|
|||
if name in special_names:
|
||||
return special_names[name]
|
||||
|
||||
name = name.replace('loc:','loc__').replace('ext:','ext__').replace('___branch:','__branch__')
|
||||
name = name.replace('loc:','loc__').replace('ext:','ext__').replace('___branch:','__branch__').replace('prm:','prm__')
|
||||
name = re.sub(puncs,'__',name)
|
||||
return name.split(':')[-1]
|
||||
|
||||
|
|
@ -439,7 +439,7 @@ def emit_eval(header,symbol,obj=None,classname=None):
|
|||
else:
|
||||
header.append((obj + '.' if obj else '')
|
||||
+ cname + ''.join("[X{}]".format(idx) for idx in range(len(domain)))
|
||||
+ ' = eval_apply("{}"'.format(sname)
|
||||
+ ' = ({})eval_apply("{}"'.format(ctype(sort.rng,classname=classname),sname)
|
||||
+ ''.join(",X{}".format(idx) for idx in range(len(domain)))
|
||||
+ ");\n")
|
||||
for idx,dsort in enumerate(domain):
|
||||
|
|
@ -879,7 +879,8 @@ def open_loop(impl,vs,declare=True,bounds=None):
|
|||
check_iterable_sort(idx.sort)
|
||||
indent(impl)
|
||||
bds = bounds[num] if bounds else ["0",str(sort_card(idx.sort))]
|
||||
impl.append('for ('+ ('int ' if declare else '') + idx.name + ' = ' + bds[0] + '; ' + idx.name + ' < ' + bds[1] + '; ' + idx.name + '++) {\n')
|
||||
vn = varname(idx.name)
|
||||
impl.append('for ('+ ('int ' if declare else '') + vn + ' = ' + bds[0] + '; ' + vn + ' < ' + bds[1] + '; ' + vn + '++) {\n')
|
||||
indent_level += 1
|
||||
|
||||
def close_loop(impl,vs):
|
||||
|
|
@ -2242,7 +2243,8 @@ def emit_assign(self,header):
|
|||
header.append(';\n')
|
||||
for idx in vs:
|
||||
indent(header)
|
||||
header.append('for (int ' + idx.name + ' = 0; ' + idx.name + ' < ' + str(sort_card(idx.sort)) + '; ' + idx.name + '++) {\n')
|
||||
vn = varname(idx.name)
|
||||
header.append('for (int ' + vn + ' = 0; ' + vn + ' < ' + str(sort_card(idx.sort)) + '; ' + vn + '++) {\n')
|
||||
indent_level += 1
|
||||
code = []
|
||||
indent(code)
|
||||
|
|
@ -2256,7 +2258,8 @@ def emit_assign(self,header):
|
|||
header.append('}\n')
|
||||
for idx in vs:
|
||||
indent(header)
|
||||
header.append('for (int ' + idx.name + ' = 0; ' + idx.name + ' < ' + str(sort_card(idx.sort)) + '; ' + idx.name + '++) {\n')
|
||||
vn = varname(idx.name)
|
||||
header.append('for (int ' + vn + ' = 0; ' + vn + ' < ' + str(sort_card(idx.sort)) + '; ' + vn + '++) {\n')
|
||||
indent_level += 1
|
||||
code = []
|
||||
indent(code)
|
||||
|
|
@ -2777,7 +2780,7 @@ def emit_repl_boilerplate3test(header,impl,classname):
|
|||
impl.append(" generators.push_back(new {}_gen);\n".format(varname(actname)))
|
||||
impl.append("""
|
||||
|
||||
for(int cycle = 0; cycle < 1000; cycle++) {
|
||||
for(int cycle = 0; cycle < TEST_ITERS; cycle++) {
|
||||
|
||||
int choices = generators.size() + readers.size() + timers.size();
|
||||
int rnd = choices ? (rand() % choices) : 0;
|
||||
|
|
@ -2834,8 +2837,7 @@ def emit_repl_boilerplate3test(header,impl,classname):
|
|||
}
|
||||
std::cout << "test_completed" << std::endl;
|
||||
}
|
||||
""".replace('classname',classname))
|
||||
|
||||
""".replace('classname',classname).replace('TEST_ITERS',opt_test_iters.get()))
|
||||
|
||||
def emit_boilerplate1(header,impl,classname):
|
||||
header.append("""
|
||||
|
|
@ -3171,11 +3173,11 @@ public:
|
|||
z3::expr_vector core = slvr.unsat_core();
|
||||
if (core.size() == 0)
|
||||
return false;
|
||||
for (unsigned i = 0; i < core.size(); i++)
|
||||
std::cout << "core: " << core[i] << std::endl;
|
||||
//for (unsigned i = 0; i < core.size(); i++)
|
||||
// std::cout << "core: " << core[i] << std::endl;
|
||||
unsigned idx = rand() % core.size();
|
||||
z3::expr to_delete = core[idx];
|
||||
std::cout << "to delete: " << to_delete << std::endl;
|
||||
// std::cout << "to delete: " << to_delete << std::endl;
|
||||
for (unsigned i = 0; i < alits.size(); i++)
|
||||
if (z3::eq(alits[i],to_delete)) {
|
||||
alits[i] = alits.back();
|
||||
|
|
@ -3202,6 +3204,7 @@ target = iu.EnumeratedParameter("target",["impl","gen","repl","test"],"gen")
|
|||
opt_classname = iu.Parameter("classname","")
|
||||
opt_build = iu.BooleanParameter("build",False)
|
||||
opt_trace = iu.BooleanParameter("trace",False)
|
||||
opt_test_iters = iu.Parameter("test_iters","1000")
|
||||
|
||||
def main():
|
||||
ia.set_determinize(True)
|
||||
|
|
|
|||
|
|
@ -40,16 +40,32 @@ checks = [
|
|||
['udp_test2','OK'],
|
||||
['udp_test','OK'],
|
||||
]
|
||||
]
|
||||
]
|
||||
],
|
||||
['../doc/examples/testing',
|
||||
[
|
||||
['pingpong','trusted=true','OK'],
|
||||
['interference','trusted=true','interference.ivy: line 30: error: Call out to right_player.intf_ping[implement] may have visible effect on left_player.ball'],
|
||||
['coveragefail','trusted=true','coveragefail.ivy: line 20: error: assertion is not checked'],
|
||||
]
|
||||
],
|
||||
]
|
||||
|
||||
tests = [
|
||||
['../doc/examples/testing',
|
||||
[
|
||||
['trivnet','test_completed'],
|
||||
['pingpong','isolate=iso_l','test_completed'],
|
||||
['token_ring','isolate=iso_n','test_completed'],
|
||||
# ['trivnet','test_completed'],
|
||||
# ['pingpong','isolate=iso_l','test_completed'],
|
||||
# ['pingpong_bad','isolate=iso_l','pingpong_bad.ivy: line 15: : 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'],
|
||||
]
|
||||
]
|
||||
]
|
||||
]
|
||||
|
||||
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче