Skip to content

Commit 836ccf1

Browse files
marcoeilersmarcoeilers
authored
Fixing issue #875 (#876)
1 parent b5701ec commit 836ccf1

2 files changed

Lines changed: 300 additions & 2 deletions

File tree

‎src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
140140
* introspection etc. It would be unsound in the presence of permission introspection, and possibly incomplete
141141
* in the presence of method calls etc.
142142
*/
143-
def removeConcretePermissionAmounts[N <: Node](n: N): N = n.transform{
143+
def removeConcretePermissionAmounts[N <: Node](n: N): N = n.transform({
144144
case u@Unfold(pap@PredicateAccessPredicate(loc, _)) =>
145145
// Assume the permission amount is strictly positive; if not, there will be a verification error anyway.
146146
Unfold(PredicateAccessPredicate(loc, Some(WildcardPerm()()))(pap.pos, pap.info, pap.errT))(u.pos, u.info, u.errT)
@@ -189,7 +189,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
189189
val completeImplies = Implies(lhs, rhsTransformed)(r.pos, r.info, r.errT)
190190
qp.copy(exp = completeImplies)(qp.pos, qp.info, qp.errT)
191191
}
192-
}
192+
}, Traverse.TopDown)
193193

194194

195195
/**

‎src/test/resources/all/issues/silver/0875.vpr‎

Lines changed: 298 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,298 @@
1+
// Any copyright is dedicated to the Public Domain.
2+
// http://creativecommons.org/publicdomain/zero/1.0/
3+
4+
5+
domain Equality[T] {
6+
7+
function eq(l: T, r: T): Bool
8+
9+
axiom {
10+
(forall l: T, r: T ::
11+
{ (eq(l, r): Bool) }
12+
(eq(l, r): Bool) == (l == r))
13+
}
14+
}
15+
16+
17+
18+
domain ShArray[T] {
19+
20+
function ShArrayfirst(r: T): ShArray[T]
21+
22+
function ShArraylen(a: ShArray[T]): Int
23+
24+
function ShArrayloc(a: ShArray[T], i: Int): T
25+
26+
function ShArraysecond(r: T): Int
27+
28+
axiom {
29+
(forall a: ShArray[T] ::
30+
{ (ShArraylen(a): Int) }
31+
(ShArraylen(a): Int) >= 0)
32+
}
33+
34+
axiom {
35+
(forall a: ShArray[T], i: Int ::
36+
{ (ShArrayloc(a, i): T) }
37+
0 <= i && i < (ShArraylen(a): Int) ==>
38+
(ShArrayfirst((ShArrayloc(a, i): T)): ShArray[T]) == a &&
39+
(ShArraysecond((ShArrayloc(a, i): T)): Int) == i)
40+
}
41+
}
42+
43+
domain ShStruct2[T0, T1] {
44+
45+
function ShStructget0of2(x: ShStruct2[T0, T1]): T0
46+
47+
function ShStructget1of2(x: ShStruct2[T0, T1]): T1
48+
49+
function ShStructrev0of2(v0: T0): ShStruct2[T0, T1]
50+
51+
function ShStructrev1of2(v1: T1): ShStruct2[T0, T1]
52+
53+
axiom {
54+
(forall x: ShStruct2[T0, T1] ::
55+
{ (ShStructget0of2(x): T0) }
56+
(ShStructrev0of2((ShStructget0of2(x): T0)): ShStruct2[T0, T1]) == x)
57+
}
58+
59+
axiom {
60+
(forall x: ShStruct2[T0, T1] ::
61+
{ (ShStructget1of2(x): T1) }
62+
(ShStructrev1of2((ShStructget1of2(x): T1)): ShStruct2[T0, T1]) == x)
63+
}
64+
65+
axiom {
66+
(forall x: ShStruct2[T0, T1], y: ShStruct2[T0, T1] ::
67+
{ (eq(x, y): Bool) }
68+
(eq(x, y): Bool) ==
69+
((ShStructget0of2(x): T0) == (ShStructget0of2(y): T0) &&
70+
(ShStructget1of2(x): T1) == (ShStructget1of2(y): T1)))
71+
}
72+
}
73+
74+
domain Slice[T] {
75+
76+
function sarray(s: Slice[T]): ShArray[T]
77+
78+
function scap(s: Slice[T]): Int
79+
80+
function slen(s: Slice[T]): Int
81+
82+
function smake(a: ShArray[T], o: Int, l: Int, c: Int): Slice[T]
83+
84+
function soffset(s: Slice[T]): Int
85+
86+
axiom deconstructor_over_constructor_array {
87+
(forall a: ShArray[T], o: Int, l: Int, c: Int ::
88+
{ (sarray((smake(a, o, l, c): Slice[T])): ShArray[T]) }
89+
0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
90+
(sarray((smake(a, o, l, c): Slice[T])): ShArray[T]) == a)
91+
}
92+
93+
axiom deconstructor_over_constructor_cap {
94+
(forall a: ShArray[T], o: Int, l: Int, c: Int ::
95+
{ (scap((smake(a, o, l, c): Slice[T])): Int) }
96+
0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
97+
(scap((smake(a, o, l, c): Slice[T])): Int) == c)
98+
}
99+
100+
axiom deconstructor_over_constructor_len {
101+
(forall a: ShArray[T], o: Int, l: Int, c: Int ::
102+
{ (slen((smake(a, o, l, c): Slice[T])): Int) }
103+
0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
104+
(slen((smake(a, o, l, c): Slice[T])): Int) == l)
105+
}
106+
107+
axiom deconstructor_over_constructor_offset {
108+
(forall a: ShArray[T], o: Int, l: Int, c: Int ::
109+
{ (soffset((smake(a, o, l, c): Slice[T])): Int) }
110+
0 <= o && (0 <= l && (l <= c && o + c <= (ShArraylen(a): Int))) ==>
111+
(soffset((smake(a, o, l, c): Slice[T])): Int) == o)
112+
}
113+
114+
axiom {
115+
(forall s: Slice[T] ::
116+
{ (sarray(s): ShArray[T]) }
117+
{ (soffset(s): Int) }
118+
{ (slen(s): Int) }
119+
{ (scap(s): Int) }
120+
s ==
121+
(smake((sarray(s): ShArray[T]), (soffset(s): Int), (slen(s): Int), (scap(s): Int)): Slice[T]))
122+
}
123+
124+
axiom {
125+
(forall s: Slice[T] ::
126+
{ (slen(s): Int) }
127+
{ (scap(s): Int) }
128+
(slen(s): Int) <= (scap(s): Int))
129+
}
130+
131+
axiom {
132+
(forall s: Slice[T] ::
133+
{ (soffset(s): Int), (scap(s): Int) }
134+
{ (ShArraylen((sarray(s): ShArray[T])): Int) }
135+
(soffset(s): Int) + (scap(s): Int) <=
136+
(ShArraylen((sarray(s): ShArray[T])): Int))
137+
}
138+
139+
axiom {
140+
(forall s: Slice[T] :: { (slen(s): Int) } 0 <= (slen(s): Int))
141+
}
142+
143+
axiom {
144+
(forall s: Slice[T] :: { (soffset(s): Int) } 0 <= (soffset(s): Int))
145+
}
146+
}
147+
148+
domain String {
149+
150+
function strConcat(l: Int, r: Int): Int
151+
152+
function strLen(id: Int): Int
153+
154+
unique function stringLit(): Int
155+
156+
axiom {
157+
(forall l: Int, r: Int ::
158+
{ strLen(strConcat(l, r)) }
159+
strLen(strConcat(l, r)) == strLen(l) + strLen(r))
160+
}
161+
162+
axiom {
163+
(forall str: Int :: { strLen(str) } 0 <= strLen(str))
164+
}
165+
166+
axiom {
167+
strLen(stringLit()) == 0
168+
}
169+
}
170+
171+
domain Tuple2[T0, T1] {
172+
173+
function get0of2(p: Tuple2[T0, T1]): T0
174+
175+
function get1of2(p: Tuple2[T0, T1]): T1
176+
177+
function tuple2(t0: T0, t1: T1): Tuple2[T0, T1]
178+
179+
axiom getter_over_tuple2 {
180+
(forall t0: T0, t1: T1 ::
181+
{ (tuple2(t0, t1): Tuple2[T0, T1]) }
182+
(get0of2((tuple2(t0, t1): Tuple2[T0, T1])): T0) == t0 &&
183+
(get1of2((tuple2(t0, t1): Tuple2[T0, T1])): T1) == t1)
184+
}
185+
186+
axiom tuple2_over_getter {
187+
(forall p: Tuple2[T0, T1] ::
188+
{ (get0of2(p): T0) }
189+
{ (get1of2(p): T1) }
190+
(tuple2((get0of2(p): T0), (get1of2(p): T1)): Tuple2[T0, T1]) == p)
191+
}
192+
}
193+
194+
domain WellFoundedOrder[T] {
195+
196+
function bounded(arg1: T): Bool
197+
198+
function decreasing(arg1: T, arg2: T): Bool
199+
}
200+
201+
field pointerBar: ShStruct2[Ref, Ref]
202+
203+
field sliceString: Slice[Ref]
204+
205+
field string: Int
206+
207+
208+
function sadd(left: Int, right: Int): Int
209+
ensures result == left + right
210+
decreases
211+
{
212+
left + right
213+
}
214+
215+
216+
function ssliceFromSlice_Ref(s: Slice[Ref], i: Int, j: Int): Slice[Ref]
217+
requires 0 <= i
218+
requires i <= j
219+
requires j <= (scap(s): Int)
220+
ensures (soffset(result): Int) == (soffset(s): Int) + i
221+
ensures (slen(result): Int) == j - i
222+
ensures (scap(result): Int) == (scap(s): Int) - i
223+
ensures (sarray(result): ShArray[Ref]) == (sarray(s): ShArray[Ref])
224+
decreases _
225+
226+
227+
function toAbstractChain2(bars_V0: Slice[Ref], perms_V0: Perm): Seq[Tuple2[Seq[Int], Seq[Int]]]
228+
requires perms_V0 > 0 / 1
229+
requires (forall k_V1: Int ::
230+
0 <= k_V1 && k_V1 < (slen(bars_V0): Int) ==>
231+
acc((ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
232+
k_V1)): Ref).pointerBar, write))
233+
requires (forall k_V2: Int ::
234+
0 <= k_V2 && k_V2 < (slen(bars_V0): Int) ==>
235+
acc(bar((ShArrayloc((sarray(bars_V0): ShArray[Ref]), sadd((soffset(bars_V0): Int),
236+
k_V2)): Ref).pointerBar, (slen(bars_V0): Int) -
237+
k_V2 -
238+
1), perms_V0))
239+
ensures (slen(bars_V0): Int) == |result|
240+
ensures (forall k_V3: Int ::
241+
0 <= k_V3 && k_V3 < (slen(bars_V0): Int) ==>
242+
(unfolding acc(bar((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
243+
sadd((soffset(bars_V0): Int), k_V3)): Ref).pointerBar,
244+
(slen(bars_V0): Int) - k_V3 - 1), perms_V0) in
245+
(unfolding acc(acc_strs((ShStructget0of2((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
246+
sadd((soffset(bars_V0): Int), k_V3)): Ref).pointerBar): Ref).sliceString), perms_V0) in
247+
toSeq2((ShStructget0of2((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
248+
sadd((soffset(bars_V0): Int), k_V3)): Ref).pointerBar): Ref).sliceString)) ==
249+
(get0of2(result[k_V3]): Seq[Int])))
250+
ensures (forall k_V4: Int ::
251+
0 <= k_V4 && k_V4 < (slen(bars_V0): Int) ==>
252+
(unfolding acc(bar((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
253+
sadd((soffset(bars_V0): Int), k_V4)): Ref).pointerBar,
254+
(slen(bars_V0): Int) - k_V4 - 1), perms_V0) in
255+
(unfolding acc(acc_strs((ShStructget1of2((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
256+
sadd((soffset(bars_V0): Int), k_V4)): Ref).pointerBar): Ref).sliceString), perms_V0) in
257+
toSeq2((ShStructget1of2((ShArrayloc((sarray(bars_V0): ShArray[Ref]),
258+
sadd((soffset(bars_V0): Int), k_V4)): Ref).pointerBar): Ref).sliceString)) ==
259+
(get1of2(result[k_V4]): Seq[Int])))
260+
decreases
261+
262+
263+
function toSeq2(s_V0: Slice[Ref]): Seq[Int]
264+
requires (forall j_V1: Int ::
265+
0 <= j_V1 && j_V1 < (slen(s_V0): Int) ==>
266+
acc((ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
267+
j_V1)): Ref).string, write))
268+
ensures |result| == (slen(s_V0): Int)
269+
ensures (forall j_V2: Int ::
270+
0 <= j_V2 && j_V2 < (slen(s_V0): Int) ==>
271+
(ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int), j_V2)): Ref).string ==
272+
result[j_V2])
273+
decreases (slen(s_V0): Int)
274+
{
275+
((slen(s_V0): Int) == 0 ?
276+
Seq[Int]() :
277+
toSeq2(ssliceFromSlice_Ref(s_V0, 0, (slen(s_V0): Int) - 1)) ++
278+
Seq((ShArrayloc((sarray(s_V0): ShArray[Ref]), sadd((soffset(s_V0): Int),
279+
(slen(s_V0): Int) - 1)): Ref).string))
280+
}
281+
282+
predicate bar(bar_V0: ShStruct2[Ref, Ref], k_V0: Int) {
283+
(let fn$$0 ==
284+
(bar_V0) in
285+
acc((ShStructget0of2(fn$$0): Ref).sliceString, write) &&
286+
acc((ShStructget1of2(fn$$0): Ref).sliceString, write)) &&
287+
acc(acc_strs((ShStructget0of2(bar_V0): Ref).sliceString), write) &&
288+
acc(acc_strs((ShStructget1of2(bar_V0): Ref).sliceString), write)
289+
}
290+
291+
predicate acc_strs(arr_V0: Slice[Ref]) {
292+
(forall k_V1: Int ::
293+
{ (ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
294+
k_V1)): Ref) }
295+
0 <= k_V1 && k_V1 < (slen(arr_V0): Int) ==>
296+
acc((ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
297+
k_V1)): Ref).string, write))
298+
}

0 commit comments

Comments
 (0)
⚡