working on token ring example

doc/examples/testing/queue.ivy

@@ -0,0 +1,70 @@
+#lang ivy1.6
+
+include order
+include collections
+
+module message_queue(net_msg,seq_num) = {
+
+    relation contents(M:net_msg.t)
+
+    action enqueue(msg:net_msg.t)
+    action empty returns (res:bool)
+    action pick_one returns (res:net_msg.t)
+    action delete_all(seq:seq_num.t)
+
+
+    object spec = {
+	init ~contents(M)
+
+	before enqueue {
+	    assert contents(X) -> net_msg.num(X) ~= net_msg.num(msg)
+	}
+
+	after enqueue {
+	    contents(msg) := true
+	}
+
+	after empty returns (res:bool) {
+	    assert contents(M) -> ~res;
+	    assert ~res -> exists M. contents(M)
+	}
+
+	before pick_one {
+	    assert exists M. contents(M)
+	}
+
+	after pick_one {
+	    assert contents(res)
+	}
+    
+	before delete_all  {
+	    contents(M) := contents(M) & ~(net_msg.num(M) <= seq)
+	}
+    }
+    
+    object impl = {
+
+	instance imap : ordered_map(seq_num,net_msg.t)
+
+	implement enqueue {
+	    call imap.set(net_msg.num(msg),msg)
+	}
+
+	implement empty {
+	    res := seq_num.iter.is_end(imap.lub(seq_num.iter.create(0)))
+	}
+	
+	implement delete_all(seq:seq_num.t) {
+	    call imap.erase(seq_num.iter.create(0),seq_num.iter.create(seq_num.next(seq)))
+	}
+
+	implement pick_one {
+	    res := imap.get(seq_num.iter.val(imap.lub(seq_num.iter.create(0))),res)
+	}
+
+	conjecture imap.maps(X,Y) -> X = net_msg.num(Y)
+	conjecture contents(Y) <-> imap.maps(net_msg.num(Y),Y)
+
+    }
+
+}

doc/examples/testing/seqnum.ivy

@@ -0,0 +1,29 @@
+#lang ivy1.6
+
+include order
+
+module sequence_numbers = {
+
+    type t
+    instance props : totally_ordered_with_zero(t)
+    instance iter : order_iterator(this)
+
+    action next(seq:t) returns (res:t)
+
+    object spec = {
+
+	after next {
+	    assume exists X. seq < X;
+	    assert seq < res & (X < res -> X <= seq)
+	}
+    }
+
+    object impl = {
+	interpret t->bv[16]
+	implement next {
+	    res := seq + 1
+	}
+    }
+
+    isolate iso_props = iter,props,spec,impl
+}

doc/examples/testing/token_ring.ivy

@@ -0,0 +1,108 @@
+#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
+instance trans : transport(net,packet.t,node.t)
+
+################################################################################
+#
+# The network service specification
+#
+################################################################################
+
+include udp
+instance net : udp_simple(node.t,trans.impl.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 = {
+
+    relation token(X:node.t)
+    init token(X) <-> X = 0
+    individual pkt : packet.t
+
+    implement serv.release(me:node.t) {
+	if token(me) {
+	    token(me) := false;
+	    call trans.send(me,node.next(me),pkt)
+	}
+    }
+
+    implement trans.recv(me:node.t,pkt:packet.t) {
+	token(me) := 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,trans.mq,trans.seq_num with net,node
+trusted isolate iso_n = net with node
+
+#extract iso_impl(me:node.t) = proto(me),net(me),timer(me),node,id,asgn

doc/examples/testing/trans.ivy

@@ -0,0 +1,113 @@
+#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 = {
+
+	init ~sent(D,P)
+
+	before send {
+	    assert ~sent(dst,pkt);
+	    sent(dst,pkt) := true
+	}
+
+	before recv {
+	    assert sent(dst,pkt);
+	    sent(dst,pkt) := false
+	}
+    }
+
+    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
+	# 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)
+	    }
+	}
+
+
+    }
+
+}

ivy/ivy_logic.py

@@ -704,6 +704,8 @@ class Sig(object):
 
 alpha = lg.TopSort('alpha')
 
+lg.BooleanSort.name = 'bool'
+
 polymorphic_symbols_list = [
     ('<' , [alpha,alpha,lg.Boolean]),
     ('<=' , [alpha,alpha,lg.Boolean]),

ivy/ivy_to_cpp.py

@@ -70,10 +70,10 @@ def sym_decl(sym,c_type = None,skip_params=0):
     name, sort = sym.name,sym.sort
     dims = []
     if not c_type:
-        c_type,dims = ctype_function(sort)
+        c_type,dims = ctype_function(sort,skip_params=skip_params)
     res = c_type + ' '
     res += memname(sym) if skip_params else varname(sym.name)
-    for d in dims[skip_params:]:
+    for d in dims:
         res += '[' + str(d) + ']'
     return res
     
@@ -237,8 +237,8 @@ def is_large_type(sort):
     cards = map(sort_card,sort.dom if hasattr(sort,'dom') else [])
     return not(all(cards) and reduce(mul,cards,1) <= 16)
 
-def ctype_function(sort,classname=None):
-    cards = map(sort_card,sort.dom if hasattr(sort,'dom') else [])
+def ctype_function(sort,classname=None,skip_params=0):
+    cards = map(sort_card,sort.dom[skip_params:] if hasattr(sort,'dom') else [])
     cty = ctypefull(sort.rng,classname)
     if all(cards) and reduce(mul,cards,1) <= 16:
         return (cty,cards)
@@ -298,7 +298,9 @@ def emit_sorts(header):
                 indent(header)
                 header.append('mk_bv("{}",{});\n'.format(name,width))
                 continue
-            raise iu.IvyError(None,'sort {} has no finite interpretation'.format(name))
+            header.append('mk_sort("{}");\n'.format(name))
+            continue
+#            raise iu.IvyError(None,'sort {} has no finite interpretation'.format(name))
         card = sort.card
         cname = varname(name)
         indent(header)
@@ -358,6 +360,26 @@ def emit_eval(header,symbol,obj=None):
     for idx,dsort in enumerate(domain):
         indent_level -= 1    
 
+def emit_set_field(header,symbol,lhs,rhs,nvars=0):
+    global indent_level
+    name = symbol.name
+    sname = slv.solver_name(symbol)
+    cname = varname(name)
+    sort = symbol.sort
+    domain = sort.dom[1:]
+    vs = variables(domain,start=nvars)
+    open_loop(header,vs)
+    lhs1 = 'apply("'+symbol.name+'"'+''.join(','+s for s in ([lhs]+map(varname,vs))) + ')'
+    rhs1 = rhs + ''.join('[{}]'.format(varname(v)) for v in vs) + '.' + varname(symbol)
+    if sort.rng.name in im.module.sort_destructors:
+        destrs = im.module.sort_destructors[sort.name]
+        for destr in destrs:
+            emit_set_field(header,destr,lhs1,rhs1,nvars+len(vs))
+    else:
+        code_line(header,'slvr.add('+lhs1+'==int_to_z3(enum_sorts.find("'+sort.rng.name+'")->second,'+rhs1+'))')
+    close_loop(header,vs)
+
+
 def emit_set(header,symbol): 
     global indent_level
     name = symbol.name
@@ -365,6 +387,16 @@ def emit_set(header,symbol):
     cname = varname(name)
     sort = symbol.sort
     domain = sort_domain(sort)
+    if sort.rng.name in im.module.sort_destructors:
+        destrs = im.module.sort_destructors[sort.name]
+        for destr in destrs:
+            vs = variables(domain)
+            open_loop(header,vs)
+            lhs = 'apply("'+symbol.name+'"'+''.join(','+s for s in map(varname,vs)) + ')'
+            rhs = 'obj.' + varname(symbol) + ''.join('[{}]'.format(varname(v)) for v in vs)
+            emit_set_field(header,destr,lhs,rhs,len(vs))
+            close_loop(header,vs)
+        return
     for idx,dsort in enumerate(domain):
         dcard = sort_card(dsort)
         indent(header)
@@ -1283,8 +1315,8 @@ def cstr(term):
 def subscripts(vs):
     return ''.join('['+varname(v)+']' for v in vs)
 
-def variables(sorts):
-    return [il.Variable('X__'+str(idx),s) for idx,s in enumerate(sorts)]
+def variables(sorts,start=0):
+    return [il.Variable('X__'+str(idx+start),s) for idx,s in enumerate(sorts)]
 
 
 def assign_symbol_value(header,lhs_text,m,v,same=False):
@@ -2395,6 +2427,39 @@ public:
         return eval_apply(decl_name,3,args);
     }
 
+    z3::expr apply(const char *decl_name, std::vector<z3::expr> &expr_args) {
+        z3::func_decl decl = decls_by_name.find(decl_name)->second;
+        unsigned arity = decl.arity();
+        assert(arity == expr_args.size());
+        return decl(arity,&expr_args[0]);
+    }
+
+    z3::expr apply(const char *decl_name) {
+        std::vector<z3::expr> a;
+        return apply(decl_name,a);
+    }
+
+    z3::expr apply(const char *decl_name, z3::expr arg0) {
+        std::vector<z3::expr> a;
+        a.push_back(arg0);
+        return apply(decl_name,a);
+    }
+    
+    z3::expr apply(const char *decl_name, z3::expr arg0, z3::expr arg1) {
+        std::vector<z3::expr> a;
+        a.push_back(arg0);
+        a.push_back(arg1);
+        return apply(decl_name,a);
+    }
+    
+    z3::expr apply(const char *decl_name, z3::expr arg0, z3::expr arg1, z3::expr arg2) {
+        std::vector<z3::expr> a;
+        a.push_back(arg0);
+        a.push_back(arg1);
+        a.push_back(arg2);
+        return apply(decl_name,a);
+    }
+
     z3::expr int_to_z3(const z3::sort &range, int value) {
         if (range.is_bool())
             return ctx.bool_val(value);
@@ -2510,6 +2575,12 @@ public:
         enum_sorts.insert(std::pair<std::string, z3::sort>(sort_name,sort));
     }
 
+    void mk_sort(const char *sort_name) {
+        z3::sort sort = ctx.uninterpreted_sort(sort_name);
+        // can't use operator[] here because the value classes don't have nullary constructors
+        enum_sorts.insert(std::pair<std::string, z3::sort>(sort_name,sort));
+    }
+
     void mk_decl(const char *decl_name, unsigned arity, const char **domain_names, const char *range_name) {
         std::vector<z3::sort> domain;
         for (unsigned i = 0; i < arity; i++)

test/genstruct.ivy

@@ -0,0 +1,18 @@
+#lang ivy1.6
+
+type t
+
+interpret t -> bv[1]
+
+type s = struct {
+  x : t,
+  y : t
+}
+
+individual foo : s
+
+action bar(q:t) = {
+  assume q = x(foo)
+}
+
+export bar