viperproject
Gobra doesn't terminate with unfold+fold and verification errors
In the following code, Gobra finds the verification error (the assert false) as expected:
type Foo struct {
Bar []*Bar
}
pred FooBar(foo *Foo, minBar int) {
acc(foo) && len(foo.Bar) >= minBar && (forall l int :: {foo.Bar[l]} 0 <= l && l < len(foo.Bar) ==> acc(&foo.Bar[l]) && acc(foo.Bar[l], _))
}
type Bar struct {
Val3 []byte
Val2 []byte
Val1 []byte
}
requires foo != nil ==> FooBar(foo, 1)
func tmp(foo *Foo) (res bool) {
if foo != nil {
val := unfolding FooBar(foo, 1) in foo.Bar[0]
// do something with val
assert false
return true
}
return false
}
However, if we use unfold+fold instead of unfolding, Gobra does not seem to terminate anymore if there are verification errors after the fold (and it then also doesn't show the error):
type Foo struct {
Bar []*Bar
}
pred FooBar(foo *Foo, minBar int) {
acc(foo) && len(foo.Bar) >= minBar && (forall l int :: {foo.Bar[l]} 0 <= l && l < len(foo.Bar) ==> acc(&foo.Bar[l]) && acc(foo.Bar[l], _))
}
type Bar struct {
Val3 []byte
Val2 []byte
Val1 []byte
}
requires foo != nil ==> FooBar(foo, 1)
func tmp(foo *Foo) (res bool) {
if foo != nil {
unfold FooBar(foo, 1)
val := foo.Bar[0]
// do something with val
fold FooBar(foo, 1)
assert false
return true
}
return false
}
This is only reproducible if the last acc in the predicate has the wildcard (most likely because otherwise the permission will not be kept after the fold). For some reason, there also need to be the three byte slices in Bar (even though they are unused) for the issue to show up.
To reproduce the issue also different verification errors can be inserted.
Unfortunately, in some instances, one has to use unfold+fold instead of unfolding.
Also the Viper code doesn't seem to terminate. However, e.g. removing the assert false manually in the generated Viper code, makes Viper terminate again, so this might be a Viper issue.
Here's a smaller example (not using predicates) where this issue occurs. In this instance, the struct needs to have at least three string slices and the permission must be less than 1, for the issue to show up:
type SomeStruct struct {
strs []string
strs2 []string
strs3 []string
}
requires len(arr) > 0
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k]) && acc(arr[k], 1/2)
func foo(arr []*SomeStruct) {
tmp := arr[0]
assert false
}
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k]) && acc(arr[k], 1/2) expands to
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k])
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k].strs, 1/2)
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k].strs2, 1/2)
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k].strs3, 1/2)
This probably leads to termination issues when Z3 tries to prove that the accesses are not equal. Essentially the issue is also reproducible if we use other datatypes instead of []string (e.g. using string directly also shows the issue). However, the same datatype must occur at least thrice in the struct. Z3 seems to still be able to handle only two fields or full permissions.
As a workaround, one could either not specify the trigger, s.t. Gobra adds more specific triggers after expanding, or do that manually, e.g. as follows:
requires forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k])
requires forall k int :: {&arr[k].strs} 0 <= k && k < len(arr) ==> acc(&arr[k].strs, 1/2)
requires forall k int :: {&arr[k].strs2} 0 <= k && k < len(arr) ==> acc(&arr[k].strs2, 1/2)
requires forall k int :: {&arr[k].strs3} 0 <= k && k < len(arr) ==> acc(&arr[k].strs3, 1/2)
However, it would be useful if Gobra automatically extends the original quantifier to the quantifiers with the more specific triggers.
Note: This only works for slices, not for maps. If we don't specify triggers for the same code just with maps, then Gobra will generate equal triggers for the different field accesses. If we specify triggers manually like {&m[str].strs} (assuming m is the map and it maps a string to a pointer to the struct as before), then Gobra will generate invalid triggers similar to #913
For example in the following code, we generate invalid triggers:
requires acc(m)
requires forall str string :: {&m[str].strs} str in domain(m) ==> acc(&m[str].strs, 1/2)
requires forall str string :: {&m[str].strs2} str in domain(m) ==> acc(&m[str].strs2, 1/2)
requires forall str string :: {&m[str].strs3} str in domain(m) ==> acc(&m[str].strs3, 1/2)
requires "test" in domain(m)
func foo2(m map[string]*SomeStruct) {
tmp := m["test"]
tmp1 := m["test"].strs
tmp2 := m["test"].strs2
tmp3 := m["test"].strs3
assert false
}
Gobra would come up with e.g. the following (invalid) trigger:
{ (ShStructget0of3(((m_V0 == null ?
false :
(str_V1 in
domain(m_V0.underlyingMapField$String$$$$_E_$$$$PointerDefinedSomeStruct_f97d51b0_T$$$_S_$$$$$$$_E_$$$))) ?
m_V0.underlyingMapField$String$$$$_E_$$$$PointerDefinedSomeStruct_f97d51b0_T$$$_S_$$$$$$$_E_$$$[str_V1] :
shStructDefault_$strsA_SliceString$$$_S_$$$$$$_S_$$$_a_strs2A_SliceString$$$_S_$$$$$$_S_$$$_a_strs3A_SliceString$$$_S_$$$$$$_S_$$$_a$())): Ref) }
For maps, a (not so nice) workaround, would be the following (note how we have to change the code from m["test"] to getElemsFromMap(m, "test") so that the triggers match):
requires acc(m)
ensures res == let elem, ok := m[str] in elem
decreases
pure func getElemsFromMap(m map[string]*SomeStruct, str string) (res *SomeStruct)
requires acc(m)
requires forall str string :: {&getElemsFromMap(m, str).strs} str in domain(m) ==> acc(&getElemsFromMap(m, str).strs, 1/2)
requires forall str string :: {&getElemsFromMap(m, str).strs2} str in domain(m) ==> acc(&getElemsFromMap(m, str).strs2, 1/2)
requires forall str string :: {&getElemsFromMap(m, str).strs3} str in domain(m) ==> acc(&getElemsFromMap(m, str).strs3, 1/2)
requires "test" in domain(m)
func foo2(m map[string]*SomeStruct) {
tmp := m["test"]
tmp1 := getElemsFromMap(m, "test").strs
tmp2 := getElemsFromMap(m, "test").strs2
tmp3 := getElemsFromMap(m, "test").strs3
assert false
}
Here we should definitely look for a solution, s.t. Gobra can generate valid triggers
Great, I just looked into the SMT stuff emitted by Silicon for the smaller example and tried to figure out what's happening, and it turns out I should have just read the next couple of comments.
Yes, essentially, the QPs for the individual fields of the struct have triggers that are too general. For example, the QP for the first field should get the trigger
{ (ShStructget0of3((ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
k_V2)): Ref).PointerDefinedSomeStruct_843256b2_T$$$_S_$$$$$$$_E_$$$): Ref) }
but instead, if the manual trigger is written as in the example, the trigger is
{ (ShArrayloc((sarray(arr_V0): ShArray[Ref]), sadd((soffset(arr_V0): Int),
k_V2)): Ref) }
Therefore, the three QPs for the three fields all have the same trigger. What happens is that Silicon first tries to prove false, this fails, and then Silicon performs state consolidation and emits additional information about the heap, in particular, permission upper bounds. So Z3 sees that it could get a contradiction if it could show that several of the string slices are actually the same reference, and then it keeps trying to do that and instantiates lots of internal QP axioms in the process. And somehow the fact that instantiating one QP axiom contains the exact expression needed to also trigger everything related to the other two QPs means it never terminates, although to be honest it's very difficult to see what exactly is happening on the SMT level and if there's something in Silicon's encoding that's not working as intended.
