Gobra generates invalid triggers

[ThomasMayerl]

In some cases Gobra generates invalid triggers. For example, in the following code Gobra generates invalid triggers when the element Bar in Foo is of type Bar instead of *Bar:

type Bar struct {
}

type FooCacheEntry struct {
	Bar Bar
}

var fooCache = map[string]*FooCacheEntry{}

preserves acc(fooCache, _) 
preserves forall str string :: str in fooCache ==> (forall str2 string :: str2 in fooCache && str != str2 ==> fooCache[str] != fooCache[str2])
preserves forall str string :: str in fooCache ==> acc(fooCache[str], _) 
func FooBar() (res int)

If one looks at the generated Viper output, there are invalid triggers making Viper unable to generate an AST.

Now we change Bar to be a pointer and add the necessary permissions:

package map_struct_elem_acc

type Bar struct {
}

type FooCacheEntry struct {
	Bar *Bar
}

var fooCache = map[string]*FooCacheEntry{}

preserves acc(fooCache, _) 
preserves forall str string :: str in fooCache ==> (forall str2 string :: str2 in fooCache && str != str2 ==> fooCache[str] != fooCache[str2])
preserves forall str string :: str in fooCache ==> acc(fooCache[str], _) 
preserves forall str string :: str in fooCache ==> (forall str2 string :: str2 in fooCache && str != str2 ==> fooCache[str].Bar != fooCache[str2].Bar)
preserves forall str string :: str in fooCache ==> acc(fooCache[str].Bar, _)
func FooBar() (res int)

The generated Viper output can now be verified.

[ArquintL]

--checkConsistency does not complain but pointing Viper-IDE at the generated Viper program results in 2 invalid trigger errors as the inferred triggers are ternary expressions

[ArquintL]

Manually specifying the following triggers solves the problem:

package test5

type Bar struct {
}

type FooCacheEntry struct {
	Bar Bar
}

var fooCache = map[string]*FooCacheEntry{}

preserves acc(fooCache, _)
preserves forall str string :: {fooCache[str]} str in fooCache ==> (forall str2 string :: {fooCache[str2]} str2 in fooCache && str != str2 ==> fooCache[str] != fooCache[str2])
preserves forall str string :: { fooCache[str] } str in fooCache ==> acc(fooCache[str], _)
func FooBar() (res int)

[ArquintL]

This seems to be a minimal example to reproduce this issue. Note that Bar is needed and replacing the b field by an int makes the issue disappear:

package test5

type Bar struct {
    i int
}

type FooCacheEntry struct {
	b Bar
}

var fooCache = map[string]*FooCacheEntry{}

requires acc(fooCache)
requires forall str string :: str in fooCache ==> acc(fooCache[str])
func FooBar() (res int)

[ThomasMayerl]

Manually specifying the following triggers solves the problem:

package test5

type Bar struct {
}

type FooCacheEntry struct {
	Bar Bar
}

var fooCache = map[string]*FooCacheEntry{}

preserves acc(fooCache, _)
preserves forall str string :: {fooCache[str]} str in fooCache ==> (forall str2 string :: {fooCache[str2]} str2 in fooCache && str != str2 ==> fooCache[str] != fooCache[str2])
preserves forall str string :: { fooCache[str] } str in fooCache ==> acc(fooCache[str], _)
func FooBar() (res int)

The example from https://github.com/viperproject/gobra/issues/912 seems to be one where invalid triggers are generated even if we manually add some

[ThomasMayerl]

The following is another example of where the issue shows up. Gobra cannot prove that we have access to arr[k] for the second acc(..) in the invariant even though the access is specified just before. The error message says Loop invariant is not well-formed. [info] Permission to arr[k] might not suffice. If we look at the Viper code then it again says that invalid triggers were found.

func tmp() {
    someMap := map[string][]*int{}
    invariant acc(someMap)
    invariant forall str string :: {someMap[str]} str in domain(someMap) ==> (let arr, _ := someMap[str] in (forall k int :: {&arr[k]} 0 <= k && k < len(arr) ==> acc(&arr[k]) && acc(arr[k])))
    for i := 0; i < 10; i++ {

    }
}

The Viper error message:

Constructing the AST has failed: { someMap_V0.underlyingMapField$String$$$$_E_$$$$SlicePointerIntint$$$_S_$$$$$$_S_$$$$$$$_E_$$$[str_V2],
(ShArrayloc((sarray(((someMap_V0 == null ?
  false :
  (str_V2 in
  domain(someMap_V0.underlyingMapField$String$$$$_E_$$$$SlicePointerIntint$$$_S_$$$$$$_S_$$$$$$$_E_$$$))) ?
  someMap_V0.underlyingMapField$String$$$$_E_$$$$SlicePointerIntint$$$_S_$$$$$$_S_$$$$$$$_E_$$$[str_V2] :
  sliceDefault_PointerIntint$$$_S_$$$$$$_S_$$$())): ShArray[Ref]), sadd((soffset(((someMap_V0 ==
null ?
  false :
  (str_V2 in
  domain(someMap_V0.underlyingMapField$String$$$$_E_$$$$SlicePointerIntint$$$_S_$$$$$$_S_$$$$$$$_E_$$$))) ?
  someMap_V0.underlyingMapField$String$$$$_E_$$$$SlicePointerIntint$$$_S_$$$$$$_S_$$$$$$$_E_$$$[str_V2] :
  sliceDefault_PointerIntint$$$_S_$$$$$$_S_$$$())): Int), k_V3)): Ref) } is not a valid Trigger

[jcp19]

yes, our current encoding of maps leads to very bad encodings for the "obvious" triggers. I tried to refactor the map encoding at some point to introduce Viper functions for operations over maps like map lookups and obtaining domains and so on (https://github.com/viperproject/gobra/pull/606).

This would guarantee that triggers obtained from performing map lookups would be valid. In the end, this did not get merged because (1) this solution leads to bad error messages. A failed map lookup would be reported by Gobra as "precondition of function unknown might not hold" - this has to do with the fact that the map lookup function does not have a counterpart in Gobra. I didn't explore solutions to this, but this is a strict requirement for us to merge such a PR, (2) I was facing some weird incompletenesses with the new encoding on some files from scion. I no longer now if this is actually a problem and I believe that we would be able to find a way to deal with these shortcomings.

I will definitely not allocate time to do this in the short to medium term, but I would be happy to guide anyone who would like to take over this PR.