Gobra crashes in some situations involving maps

[henriman]

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19, however this bug is unrelated to hyperGobra and also occurs using "normal" Gobra.

I believe these are two separate, but related bugs.

1. Using "comma ok" idiom with let crashes when trying to subsequently access ok

requires acc(inputMap)
requires let x, ok := inputMap[0] in ok
ensures res
func test2(inputMap map[int]int) (res bool) {
    x, ok := inputMap[0]
    return ok
}

Trying to verify the above code crashes with java.util.NoSuchElementException: key not found: ok_V1, as there is no definition for ok in the Viper encoding. Note that accessing x in let works.

This can be worked around by instead using 0 in domain(inputMap), of course.

2. Comparing result of map access of a map with pointer-type elements crashes

requires acc(inputMap) && (0 in domain(inputMap) ==> inputMap[0] != nil)
func test3(inputMap map[int](*int)) int

requires acc(inputMap) && (0 in domain(inputMap) ==> inputMap[0] != 0)
func test4(inputMap map[int](int)) int

While verifying test4 succeeds, verifying test3 crashes with:

15:10:05.519 [main] ERROR viper.gobra.GobraRunner$ - An assumption was violated during execution.
15:10:05.521 [main] ERROR viper.gobra.GobraRunner$ - Logic error: got unexpected type InternalSingleMulti(*int,(*int,bool))
viper.gobra.util.Violation$LogicException: Logic error: got unexpected type InternalSingleMulti(*int,(*int,bool))
        at viper.gobra.util.Violation$.violation(Violation.scala:27)
        at viper.gobra.frontend.Desugar$Desugarer.typeD(Desugar.scala:3833)
        at viper.gobra.frontend.Desugar$Desugarer.litD(Desugar.scala:2997)
        at viper.gobra.frontend.Desugar$Desugarer.exprD(Desugar.scala:2723)
        at viper.gobra.frontend.Desugar$Desugarer.exprAndTypeAsExpr(Desugar.scala:2956)
        ...

This can be worked around by first assigning the result of inputMap[0] to a variable using let, and then comparing on that variable.

(This has no urgency for me.)