Skip to content

Commit f27fda2

Browse files
marcoeilersmarcoeilers
committed
Nick Grasshopper examples
1 parent e9e1e8e commit f27fda2

35 files changed

+1798
-1
lines changed

‎src/main/scala/decider/TermToZ3APIConverter.scala‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -456,6 +456,8 @@ class TermToZ3APIConverter
456456
case Let(bindings, body) =>
457457
convert(body.replace(bindings))
458458

459+
case MagicWandSnapshot(snp) => convertTerm(snp)
460+
459461
case MWSFLookup(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
460462

461463
case _: MagicWandChunkTerm

‎src/main/scala/state/Utils.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ package object utils {
9191
case PredicatePermLookup(_, pm, args) => Seq(pm) ++ args
9292
case FieldTrigger(_, fvf, at) => fvf :: at :: Nil
9393
case PredicateTrigger(_, psf, args) => psf +: args
94-
94+
case MagicWandSnapshot(snp) => snp :: Nil
9595
}
9696

9797
/** @see [[viper.silver.ast.utility.Simplifier.simplify]] */

‎src/test/resources/kinduct/nick/grasshopper/nested_sl/destroy.vpr‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
import "./nested_def.vpr"
2+
3+
method destroy(x: Ref)
4+
requires OuterNode(x)
5+
{
6+
var currO: Ref := x
7+
8+
while(currO != null)
9+
//invariant OuterNode(currO)
10+
{
11+
var currO_old: Ref := currO
12+
unfold OuterNode(currO)
13+
var ic: Ref := currO.down
14+
var currI: Ref := ic
15+
while(currI != null)
16+
//invariant InnerNode(currI)
17+
{
18+
var currI_old: Ref := currI
19+
unfold InnerNode(currI)
20+
currI := currI.inext
21+
freeI(currI_old)
22+
}
23+
freeN(currI)
24+
currO := currO.onext
25+
freeO(currO_old)
26+
}
27+
}
28+
29+
30+
31+
method freeO(x: Ref)
32+
requires acc(x.onext) && acc(x.down)
33+
34+
method freeI(x: Ref)
35+
requires acc(x.inext)
36+
37+
method freeN(x: Ref)
38+
requires InnerNode(x) && x == null

‎src/test/resources/kinduct/nick/grasshopper/nested_sl/insert.vpr‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
import "./nested_def.vpr"
2+
3+
method insert(x: Ref) returns (res: Ref)
4+
requires OuterNode(x)
5+
ensures OuterNode(res)
6+
{
7+
var inn: Ref
8+
if(x == null){
9+
inn := new(inext)
10+
inn.inext := null
11+
fold InnerNode(inn.inext)
12+
fold InnerNode(inn)
13+
res := new(onext, down)
14+
res.down := inn
15+
res.onext := null
16+
fold OuterNode(res.onext)
17+
fold OuterNode(res)
18+
} else {
19+
var nondet: Bool
20+
var currO: Ref := x
21+
22+
package OuterNode(currO) --* OuterNode(x)
23+
unfold OuterNode(currO)
24+
25+
while(nondet && currO.onext != null)
26+
//invariant acc(currO.onext) && acc(currO.down) && InnerNode(currO.down)
27+
//invariant OuterNode(currO.onext)
28+
//invariant OuterNode(currO) --* OuterNode(x)
29+
{
30+
nondet := havoc()
31+
var currO_old: Ref := currO
32+
currO := currO.onext
33+
unfold OuterNode(currO)
34+
35+
package OuterNode(currO) --* OuterNode(x) {
36+
fold OuterNode(currO_old)
37+
apply OuterNode(currO_old) --* OuterNode(x)
38+
}
39+
}
40+
41+
nondet := havoc()
42+
43+
// New outer node
44+
if(nondet){
45+
var currO_old: Ref := currO
46+
var newO: Ref := new(*)
47+
newO.down := null
48+
fold InnerNode(newO.down)
49+
newO.onext := currO.onext
50+
currO.onext := newO
51+
currO := newO
52+
package OuterNode(currO) --* OuterNode(x) {
53+
fold OuterNode(currO_old)
54+
apply OuterNode(currO_old) --* OuterNode(x)
55+
}
56+
}
57+
58+
// Insert in inner list
59+
if(currO.down == null){
60+
var i: Ref := new(*)
61+
i.inext := null
62+
fold InnerNode(i)
63+
currO.down := i
64+
} else {
65+
66+
// Go through inner list
67+
var ic: Ref := currO.down
68+
var currI: Ref := ic
69+
package InnerNode(currI) --* InnerNode(ic)
70+
unfold InnerNode(currI)
71+
nondet := havoc()
72+
73+
while(nondet && currI.inext != null)
74+
//invariant acc(currI.inext)
75+
//invariant InnerNode(currI.inext)
76+
//invariant InnerNode(currI) --* InnerNode(ic)
77+
{
78+
nondet := havoc()
79+
80+
var currI_old: Ref := currI
81+
currI := currI.inext
82+
unfold InnerNode(currI)
83+
package InnerNode(currI) --* InnerNode(ic){
84+
fold InnerNode(currI_old)
85+
apply InnerNode(currI_old) --* InnerNode(ic)
86+
}
87+
}
88+
89+
var i: Ref := new(*)
90+
i.inext := currI.inext
91+
fold InnerNode(i)
92+
currI.inext := i
93+
fold InnerNode(currI)
94+
apply InnerNode(currI) --* InnerNode(ic)
95+
}
96+
97+
fold OuterNode(currO)
98+
apply OuterNode(currO) --* OuterNode(x)
99+
res := x
100+
}
101+
}
102+
103+
method havoc() returns (res: Bool)

‎src/test/resources/kinduct/nick/grasshopper/nested_sl/nested_def.vpr‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
field onext: Ref
2+
field down: Ref
3+
4+
field inext: Ref
5+
6+
predicate OuterNode(x: Ref) {
7+
x != null ==> acc(x.onext) && acc(x.down) && OuterNode(x.onext) && InnerNode(x.down)
8+
}
9+
10+
predicate InnerNode(x: Ref) {
11+
x != null ==> acc(x.inext) && InnerNode(x.inext)
12+
}

‎src/test/resources/kinduct/nick/grasshopper/nested_sl/remove.vpr‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
import "./nested_def.vpr"
2+
3+
method remove(x: Ref) returns (res: Ref)
4+
requires OuterNode(x)
5+
ensures OuterNode(res)
6+
{
7+
var iprev: Ref
8+
if(x != null) {
9+
var nondet: Bool
10+
var currO: Ref := x
11+
12+
package OuterNode(currO) --* OuterNode(x)
13+
unfold OuterNode(currO)
14+
15+
while(nondet && currO.onext != null)
16+
//invariant acc(currO.onext) && acc(currO.down) && InnerNode(currO.down)
17+
//invariant OuterNode(currO.onext)
18+
//invariant OuterNode(currO) --* OuterNode(x)
19+
{
20+
nondet := havoc()
21+
var currO_old: Ref := currO
22+
currO := currO.onext
23+
unfold OuterNode(currO)
24+
25+
package OuterNode(currO) --* OuterNode(x) {
26+
fold OuterNode(currO_old)
27+
apply OuterNode(currO_old) --* OuterNode(x)
28+
}
29+
}
30+
31+
nondet := havoc()
32+
33+
var prev: Ref := currO
34+
currO := currO.onext
35+
36+
var cond1: Bool := currO != null
37+
if(cond1){
38+
unfold OuterNode(currO)
39+
var cond2: Bool := currO.down != null
40+
if(cond2) {
41+
var ic: Ref := currO.down
42+
var currI: Ref := ic
43+
package InnerNode(currI) --* InnerNode(ic)
44+
unfold InnerNode(currI)
45+
nondet := havoc()
46+
47+
while(nondet && currI.inext != null)
48+
//invariant acc(currI.inext)
49+
//invariant InnerNode(currI.inext)
50+
//invariant InnerNode(currI) --* InnerNode(ic)
51+
{
52+
nondet := havoc()
53+
54+
var currI_old: Ref := currI
55+
currI := currI.inext
56+
unfold InnerNode(currI)
57+
package InnerNode(currI) --* InnerNode(ic){
58+
fold InnerNode(currI_old)
59+
apply InnerNode(currI_old) --* InnerNode(ic)
60+
}
61+
}
62+
63+
var cond3: Bool := !nondet && currI.inext == null && currO.down == currI
64+
if(cond3) {
65+
currO.down := null
66+
freeI(currI)
67+
} else {
68+
iprev := currI
69+
currI := currI.inext
70+
71+
var cond4: Bool := currI != null
72+
if(cond4){
73+
//unfold InnerNode(currI)
74+
iprev.inext := currI.inext
75+
freeI(currI)
76+
currI := iprev
77+
}
78+
fold InnerNode(iprev)
79+
apply InnerNode(iprev) --* InnerNode(ic)
80+
}
81+
82+
var cond5: Bool := currO.down == null
83+
if(cond5) {
84+
prev.onext := currO.onext
85+
freeO(currO)
86+
currO := prev.onext
87+
unfold OuterNode(currO)
88+
}
89+
90+
}
91+
fold OuterNode(currO)
92+
}
93+
fold OuterNode(prev)
94+
apply OuterNode(prev) --* OuterNode(x)
95+
}
96+
res := x
97+
}
98+
99+
method havoc() returns (res: Bool)
100+
101+
method freeO(x: Ref)
102+
requires acc(x.onext) && acc(x.down)
103+
104+
method freeI(x: Ref)
105+
requires acc(x.inext)

‎src/test/resources/kinduct/nick/grasshopper/nested_sl/traverse.vpr‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
import "./nested_def.vpr"
2+
3+
method traverse(x: Ref)
4+
requires OuterNode(x)
5+
ensures OuterNode(x)
6+
{
7+
var currO: Ref := x
8+
package OuterNode(currO) --* OuterNode(x)
9+
10+
while(currO != null)
11+
invariant OuterNode(currO)
12+
invariant OuterNode(currO) --* OuterNode(x)
13+
{
14+
var currO_old: Ref := currO
15+
16+
unfold OuterNode(currO)
17+
var ic: Ref := currO.down
18+
19+
var currI: Ref := ic
20+
21+
package InnerNode(currI) --* InnerNode(ic)
22+
23+
while(currI != null)
24+
//invariant InnerNode(currI)
25+
//invariant InnerNode(currI) --* InnerNode(ic)
26+
{
27+
var currI_old: Ref := currI
28+
unfold InnerNode(currI)
29+
currI := currI.inext
30+
package InnerNode(currI) --* InnerNode(ic){
31+
fold InnerNode(currI_old)
32+
apply InnerNode(currI_old) --* InnerNode(ic)
33+
}
34+
}
35+
apply InnerNode(currI) --* InnerNode(ic)
36+
37+
currO := currO.onext
38+
39+
40+
package OuterNode(currO) --* OuterNode(x) {
41+
fold OuterNode(currO_old)
42+
apply OuterNode(currO_old) --* OuterNode(x)
43+
}
44+
}
45+
apply OuterNode(currO) --* OuterNode(x)
46+
}

‎src/test/resources/kinduct/nick/grasshopper/sl/sl.vpr‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
field next: Ref
2+
field data: Int
3+
4+
predicate list(x: Ref) {
5+
x != null ==> (acc(x.next) && acc(x.data) && list(x.next))
6+
}

‎src/test/resources/kinduct/nick/grasshopper/sl/sl_concat.vpr‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
import "./sl.vpr"
2+
3+
method concat(x: Ref, y: Ref) returns (res: Ref)
4+
requires list(x)
5+
requires list(y)
6+
ensures list(res)
7+
{
8+
var curr: Ref
9+
if (x == null) {
10+
res := y
11+
} else {
12+
curr := x
13+
package list(curr) --* list(x)
14+
unfold list(curr)
15+
while (curr.next != null)
16+
//invariant acc(curr.next) && acc(curr.data)
17+
//invariant list(curr.next)
18+
//invariant list(curr) --* list(x)
19+
{
20+
var prev: Ref := curr
21+
curr := curr.next
22+
unfold list(curr)
23+
package list(curr) --* list(x) {
24+
fold list(prev)
25+
apply list(prev) --* list(x)
26+
}
27+
}
28+
curr.next := y
29+
res := x
30+
}
31+
if(x != null){
32+
fold list(curr)
33+
apply list(curr) --* list(x)
34+
}
35+
}

0 commit comments

Comments
 (0)