Skip to content

Commit 5f2b76a

Browse files
shazqadeershazqadeer
committed
first
1 parent d02c3de commit 5f2b76a

File tree

1 file changed

+65
-67
lines changed

1 file changed

+65
-67
lines changed

‎Test/civl/samples/two-lists.bpl‎

Lines changed: 65 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -1,73 +1,12 @@
11
// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert "%s" > "%t"
22
// RUN: %diff "%s.expect" "%t"
33

4-
type ListElem T = Node Loc T;
5-
6-
datatype Queue<T> { Queue(head: Loc, tail: Loc, {:linear} nodes: Map Loc (ListElem T)) }
7-
8-
var {:linear} {:layer 0, 1} lists: Map Loc (Queue int);
4+
datatype Queue<T> { Queue(head: Loc, tail: Loc, {:linear} nodes: Map Loc (Node Loc T)) }
95

6+
var {:linear} {:layer 0, 1} queues: Map Loc (Queue int);
107
var {:linear} {:layer 0, 1} pos: One (TaggedLoc Unit);
118
var {:linear} {:layer 0, 1} neg: One (TaggedLoc Unit);
129

13-
yield procedure {:layer 0} ReadPos() returns (loc: Loc);
14-
refines both action {:layer 1} _ {
15-
loc := pos->val->loc;
16-
}
17-
18-
yield procedure {:layer 0} ReadNeg() returns (loc: Loc);
19-
refines both action {:layer 1} _ {
20-
loc := neg->val->loc;
21-
}
22-
23-
yield procedure {:layer 0} Enqueue(loc_q: Loc, i: int);
24-
refines action {:layer 1} _
25-
{
26-
var {:linear} one_loc_q: One Loc;
27-
var {:linear} queue: Queue int;
28-
var head, tail: Loc;
29-
var {:linear} nodes: Map Loc (ListElem int);
30-
var {:linear} one_loc_n, new_one_loc_n: One Loc;
31-
var node: ListElem int;
32-
33-
call one_loc_q, queue := Map_Get(lists, loc_q);
34-
Queue(head, tail, nodes) := queue;
35-
36-
call new_one_loc_n := Loc_New();
37-
call Map_Put(nodes, new_one_loc_n, Node(None(), 0));
38-
39-
call one_loc_n, node := Map_Get(nodes, tail);
40-
node := Node(Some(new_one_loc_n->val), i);
41-
call Map_Put(nodes, one_loc_n, node);
42-
43-
queue := Queue(head, new_one_loc_n->val, nodes);
44-
call Map_Put(lists, one_loc_q, queue);
45-
}
46-
47-
yield procedure {:layer 0} Dequeue(loc_q: Loc) returns (i: int);
48-
refines action {:layer 1} _
49-
{
50-
var {:linear} one_loc_q: One Loc;
51-
var {:linear} queue: Queue int;
52-
var head, tail: Loc;
53-
var {:linear} nodes: Map Loc (ListElem int);
54-
var {:linear} one_loc_n: One Loc;
55-
var node: ListElem int;
56-
var next: Option Loc;
57-
58-
call one_loc_q, queue := Map_Get(lists, loc_q);
59-
Queue(head, tail, nodes) := queue;
60-
61-
assume head != tail;
62-
call one_loc_n, node := Map_Get(nodes, head);
63-
Node(next, i) := node;
64-
65-
assert next is Some;
66-
queue := Queue(next->t, tail, nodes);
67-
call Map_Put(lists, one_loc_q, queue);
68-
}
69-
70-
7110
function {:inline} IsAcyclic(q: Queue int): bool
7211
{
7312
Between(q->nodes->val, Some(q->head), Some(q->tail), None())
@@ -79,15 +18,15 @@ function {:inline} QueueElems(q: Queue int): [Loc]bool
7918
}
8019

8120
yield invariant {:layer 1} PosInv();
82-
invariant Map_Contains(lists, pos->val->loc);
83-
invariant (var q := Map_At(lists, pos->val->loc); IsAcyclic(q) &&
21+
invariant Map_Contains(queues, pos->val->loc);
22+
invariant (var q := Map_At(queues, pos->val->loc); IsAcyclic(q) &&
8423
(forall loc_n: Loc:: QueueElems(q)[loc_n] ==>
8524
Map_Contains(q->nodes, loc_n) &&
8625
(loc_n == q->tail || (var node := Map_At(q->nodes, loc_n); node->val > 0))));
8726

8827
yield invariant {:layer 1} NegInv();
89-
invariant Map_Contains(lists, neg->val->loc);
90-
invariant (var q := Map_At(lists, neg->val->loc); IsAcyclic(q) &&
28+
invariant Map_Contains(queues, neg->val->loc);
29+
invariant (var q := Map_At(queues, neg->val->loc); IsAcyclic(q) &&
9130
(forall loc_n: Loc:: QueueElems(q)[loc_n] ==>
9231
Map_Contains(q->nodes, loc_n) &&
9332
(loc_n == q->tail || (var node := Map_At(q->nodes, loc_n); node->val < 0))));
@@ -132,3 +71,62 @@ preserves call NegInv();
13271
call i := Dequeue(loc);
13372
assert {:layer 1} i < 0;
13473
}
74+
75+
// Primitives
76+
77+
yield procedure {:layer 0} ReadPos() returns (loc: Loc);
78+
refines both action {:layer 1} _ {
79+
loc := pos->val->loc;
80+
}
81+
82+
yield procedure {:layer 0} ReadNeg() returns (loc: Loc);
83+
refines both action {:layer 1} _ {
84+
loc := neg->val->loc;
85+
}
86+
87+
yield procedure {:layer 0} Enqueue(loc_q: Loc, i: int);
88+
refines action {:layer 1} _
89+
{
90+
var {:linear} one_loc_q: One Loc;
91+
var {:linear} queue: Queue int;
92+
var head, tail: Loc;
93+
var {:linear} nodes: Map Loc (Node Loc int);
94+
var {:linear} one_loc_n, new_one_loc_n: One Loc;
95+
var node: Node Loc int;
96+
97+
call one_loc_q, queue := Map_Get(queues, loc_q);
98+
Queue(head, tail, nodes) := queue;
99+
100+
call new_one_loc_n := Loc_New();
101+
call Map_Put(nodes, new_one_loc_n, Node(None(), 0));
102+
103+
call one_loc_n, node := Map_Get(nodes, tail);
104+
node := Node(Some(new_one_loc_n->val), i);
105+
call Map_Put(nodes, one_loc_n, node);
106+
107+
queue := Queue(head, new_one_loc_n->val, nodes);
108+
call Map_Put(queues, one_loc_q, queue);
109+
}
110+
111+
yield procedure {:layer 0} Dequeue(loc_q: Loc) returns (i: int);
112+
refines action {:layer 1} _
113+
{
114+
var {:linear} one_loc_q: One Loc;
115+
var {:linear} queue: Queue int;
116+
var head, tail: Loc;
117+
var {:linear} nodes: Map Loc (Node Loc int);
118+
var {:linear} one_loc_n: One Loc;
119+
var node: Node Loc int;
120+
var next: Option Loc;
121+
122+
call one_loc_q, queue := Map_Get(queues, loc_q);
123+
Queue(head, tail, nodes) := queue;
124+
125+
assume head != tail;
126+
call one_loc_n, node := Map_Get(nodes, head);
127+
Node(next, i) := node;
128+
129+
assert next is Some;
130+
queue := Queue(next->t, tail, nodes);
131+
call Map_Put(queues, one_loc_q, queue);
132+
}

0 commit comments

Comments
 (0)