Skip to content

Commit 4093acc

Browse files
marcoeilersmarcoeilers
authored
Adding tests Silicon issues 715 and 926
1 parent 63c30b1 commit 4093acc

3 files changed

Lines changed: 238 additions & 0 deletions

File tree

‎src/test/resources/all/issues/silicon/0715.vpr‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
field ref_f: Ref
5+
predicate ref_p(self: Ref) {
6+
acc(self.ref_f)
7+
}
8+
function snap_ref(self: Ref): Ref_s
9+
requires ref_p(self)
10+
{
11+
unfolding ref_p(self) in cons_Ref(self.ref_f)
12+
}
13+
adt Ref_s {
14+
cons_Ref(ref: Ref)
15+
}
16+
17+
function f_RefMut_i32_borrow(self: Ref): Ref
18+
function f_RefMut_i32_borrow_rev(self: Ref): Ref
19+
20+
function map_f_RefMut_i32_borrow(s: Set[Ref]): Set[Ref]
21+
requires forall x: Ref :: x in s ==> RefMut_i32_p(x)
22+
ensures forall x: Ref :: x in s ==> (unfolding RefMut_i32_p(x) in snap_ref(f_RefMut_i32_borrow(x)).ref) in result
23+
ensures forall z: Ref :: (f_RefMut_i32_borrow_rev(z)) in s && (unfolding RefMut_i32_p((f_RefMut_i32_borrow_rev(z))) in snap_ref(f_RefMut_i32_borrow((f_RefMut_i32_borrow_rev(z)))).ref) == z
24+
25+
predicate RefMut_i32_p(self: Ref) {
26+
ref_p(f_RefMut_i32_borrow(self))
27+
}

‎src/test/resources/all/issues/silicon/0715_2.vpr‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
import <decreases/int.vpr>
5+
import <decreases/set.vpr>
6+
import <decreases/seq.vpr>
7+
8+
field left : Ref // true case
9+
field right: Ref // false case
10+
field id : Int // var from code
11+
field val : Bool
12+
13+
function isLeaf(r:Ref) : Bool // type information
14+
15+
method allocLeaf() returns (r: Ref)
16+
ensures isLeaf(r) && acc(r.val)
17+
decreases 0
18+
19+
method allocCompound() returns (r: Ref)
20+
ensures !isLeaf(r) && acc(r.left) && acc(r.right) && acc(r.id)
21+
decreases 0
22+
23+
define nodePerms(r)
24+
(isLeaf(r) ? acc(r.val) : acc(r.left) && acc(r.right) && acc(r.id))
25+
26+
define mapInv(m) (forall k1: Ref, k2: Ref :: {k1 in m,k2 in m}
27+
(k1 != k2 && k1 in m && k2 in m ==> m[k1] != m[k2])) // no dups
28+
&& forall k: Ref :: {k in m}{k in range(m)} k in m ==> nodePerms(m[k]) && m[k] == k &&
29+
(!isLeaf(k) ==> k.left in m && k.right in m)
30+
31+
32+
field table : Map[Ref,Ref]
33+
34+
define BDD(this) acc(this.table) && mapInv(this.table)
35+
36+
37+
// we use this to abstract over the hashMap get function itself
38+
function tableGet(this:Ref, node:Ref) : Ref
39+
requires BDD(this) && (!(node in this.table) ==> nodePerms(node))
40+
ensures result != null ==> result in range(this.table) && toKNode(result) == toKNode(node)
41+
ensures result == null ==> !isLeaf(node) && forall k:Ref :: {k in this.table} k in this.table ==> toKNode(k) != toKNode(node)
42+
43+
method getNode(this:Ref, node:Ref) returns (res:Ref)
44+
requires BDD(this) && (nodePerms(node)) && (!isLeaf(node) ==> node.left in this.table && node.right in this.table) // TODO? Maybe (!(toKNode(node) in this.table) ==> nodePerms(node))
45+
ensures BDD(this) && res in this.table && forall k: Ref :: {k in this.table} old(k in this.table) ==> k in this.table && this.table[k] == old(this.table[k])
46+
ensures isLeaf(node) ==> isLeaf(res) && res.val == old(node.val)
47+
decreases 0 // termination is trivial
48+
{
49+
var returned : Bool := false// models whether we hit "return" already
50+
if(!isLeaf(node)) { // if (node instanceof CompoundNode) {
51+
var that : Ref := node // no need to "cast" - type info is in logic
52+
if (that.left == that.right) {// if (that.low == that.high)
53+
res := that.left; // return that.low;
54+
returned := true // skip rest of code
55+
}
56+
}
57+
if(!returned) { // to model early return
58+
res := tableGet(this, node) // Node result = table.get(node);
59+
60+
if (res == null) {
61+
node.id := |this.table| // table.size();
62+
this.table := this.table[node := node] // table.put(node, node);
63+
res := node // return node;
64+
}
65+
}
66+
}
67+
68+
69+
70+
///BOUNDARY///
71+
72+
//
73+
74+
function isTrue(n: Ref): Bool
75+
requires nodePerms(n)
76+
{
77+
isLeaf(n) && n.val
78+
}
79+
80+
function isFalse(n: Ref): Bool
81+
requires nodePerms(n)
82+
{
83+
isLeaf(n) && !n.val
84+
}
85+
86+
method node1(this: Ref, v: Bool) returns (res: Ref)
87+
requires BDD(this)
88+
ensures BDD(this) && res in range(this.table) && isLeaf(res) && res.val == v
89+
ensures forall k: Ref :: {k in this.table} old(k in this.table) ==> k in this.table && this.table[k] == old(this.table[k])
90+
decreases 1
91+
{
92+
var l: Ref
93+
l := allocLeaf()
94+
l.val := v
95+
res := getNode(this, l)
96+
}
97+
98+
method node2(this: Ref, v: Int, l: Ref, r: Ref) returns (res: Ref)
99+
requires BDD(this) && l in range(this.table) && r in range(this.table)
100+
ensures BDD(this)
101+
//ensures res in range(this.table) && !isLeaf(res) // && TODO
102+
decreases 1
103+
{
104+
var c: Ref
105+
c := allocCompound()
106+
c.left := l
107+
c.right := r
108+
c.id := v
109+
res := getNode(this, c)
110+
}
111+
112+
method not(this: Ref, node: Ref) returns (res: Ref)
113+
requires BDD(this) && node in range(this.table)
114+
ensures BDD(this)
115+
decreases 2
116+
//ensures forall s: State :: eval(toPNode(this, res), s) == !(eval(toPNode(this, node), s))
117+
{
118+
if (isTrue(node)) {
119+
assert forall s: State :: eval(toPNode(this, node), s)
120+
res := node1(this, false)
121+
//assert forall s: State :: eval(toPNode(this, node), s)
122+
//assert forall s: State :: !eval(toPNode(this, res), s)
123+
124+
} else {
125+
if (isFalse(node)) {
126+
res := node1(this, true)
127+
assert forall s: State :: eval(toPNode(this, res), s)
128+
} else {
129+
res := node2(this, node.id, node.left, node.right)
130+
}
131+
}
132+
}
133+
134+
function toKNode(r: Ref): KNode
135+
requires isLeaf(r) ==> acc(r.val)
136+
requires !isLeaf(r) ==> acc(r.left) && acc(r.right) && acc(r.id)
137+
{
138+
isLeaf(r) ?
139+
(KLeaf(r.val)) :
140+
(KCompound(r.id, r.left, r.right))
141+
}
142+
143+
144+
adt KNode {
145+
KLeaf(v: Bool)
146+
KCompound(i: Int, kleft: Ref, kright: Ref)
147+
}
148+
149+
adt PNode {
150+
PLeafTrue()
151+
PLeafFalse()
152+
PCompound(vl: Int, lft: PNode, rght: PNode)
153+
}
154+
155+
function toPNode(bdd: Ref, n: Ref): PNode
156+
requires BDD(bdd) && n in range(bdd.table)
157+
{
158+
isLeaf(n) ?
159+
(n.val ? PLeafTrue() : PLeafFalse()) :
160+
(PCompound(n.id, toPNode(bdd, n.left), toPNode(bdd, n.right)))
161+
}
162+
163+
domain State {
164+
function getVal(s: State, v: Int): Bool
165+
}
166+
167+
domain Evaluator {
168+
169+
function eval(n: PNode, s: State): Bool
170+
171+
axiom {
172+
forall s: State :: { eval(PLeafTrue(), s) } eval(PLeafTrue(), s)
173+
}
174+
175+
axiom {
176+
forall s: State :: { eval(PLeafFalse(), s) } !eval(PLeafFalse(), s)
177+
}
178+
179+
axiom {
180+
forall s: State, n1: PNode, n2: PNode, vall: Int :: { eval(PCompound(vall, n1, n2), s) }
181+
eval(PCompound(vall, n1, n2), s) == (getVal(s, vall) ? eval(n1, s) : eval(n2, s) )
182+
}
183+
}

‎src/test/resources/all/issues/silicon/0926.vpr‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
field f: Int
2+
3+
function fn(x: Ref, y: Ref): Int
4+
requires acc(x.f)
5+
requires acc(y.f)
6+
{
7+
(let z == (x) in z.f) +
8+
(let z == (y) in z.f)
9+
}
10+
11+
method m(x: Ref, y: Ref)
12+
requires acc(x.f) && x.f == 3
13+
requires acc(y.f) && y.f == 4
14+
{
15+
var tmp: Int
16+
tmp := fn(x, y)
17+
assert tmp == 7
18+
}
19+
20+
method m2(x: Ref, y: Ref)
21+
requires acc(x.f) && x.f == 3
22+
requires acc(y.f) && y.f == 4
23+
{
24+
var tmp: Int
25+
tmp := fn(x, y)
26+
//:: ExpectedOutput(assert.failed:assertion.false)
27+
assert tmp == 6
28+
}

0 commit comments

Comments
 (0)
⚡