Encoding bug when using `rel()` and a wrapper

[AkasakaJelos]

Consider the following dummy example when using rel():

package exercises

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

/*@
ghost
pure
decreases
func Return_pure(x int, y int) (r int) {
    return 0
}

ghost
requires acc(r1, _)
pure
decreases
func Return_wrapper(t2 int, target int, r1 []int) bool{
	return exists idx int :: {r1[idx]} target < t2 ==> 0 <= idx && idx < len(r1) && Return_pure(target, t2) == r1[idx]
}
@*/

// @ requires target >= 0
// @ ensures acc(r1)
// @ ensures len(r1) > 0
// @ ensures forall t2 int :: {Return_wrapper(t2,target,r1)} Return_wrapper(t2,target,r1)
// @ ensures forall t2 int :: {Return_wrapper(target,t2,r1)} Return_wrapper(target,t2,r1)
// @ ensures forall j int :: 0 <= j && j < len(r1) ==> r1[j] >= 0
func ComputeSteps(target int) (r1 []int) {
	r1 = make([]int, 1)
	r1[0] = 0
	return r1
}

// @ requires t >= 0
// @ requires rel(t,0) != rel(t,1)
func UseStepsSamePackage(t int) {
	steps := ComputeSteps(t)
	// assert forall t2 int :: exists idx int :: t < t2 ==> 0 <= idx && idx < len(steps) && Return_pure(t, t2) == steps[idx]
	//@ assert forall t2 int :: {Return_wrapper(t2,t, steps)} Return_wrapper(t2,t,steps)
	//@ assert forall t2 int :: {Return_wrapper(t,t2,steps)} Return_wrapper(t, t2, steps)

	//@ assert Return_wrapper(rel(t,0), rel(t,1), rel(steps,0))
	//@ assert Return_wrapper(rel(t,1), rel(t,0), rel(steps,1))
	//@ assert rel(steps,1)[0] == 0
}

This issue would cause the following error:

No changes detected in the antlr4 files. Skipping parser generation.
[info] running (fork) viper.gobra.GobraRunner -i /.../exercises/relIssue.go
[info] Gobra 1.1-SNAPSHOT (351ad1fe@(detached))
[info] (c) Copyright ETH Zurich 2012 - 2024
[info] Verifying package .. - exercises [14:03:17]
[info] Error at: </.../exercises/relIssue.go:46:9> Precondition of call Return_wrapper(rel(t,1), rel(t,0), rel(steps,1)) might not hold.
[info] Permission to r1 might not suffice.
[info] Gobra found 1 error.
[info]

Based on Linard’s analysis, the issue stems from an incorrect encoding:
Return_wrapper(rel(t,1), rel(t,0), rel(steps,1)) is incorrectly resolved to a call to Return_wrapper_2a4eccf_F instead of Return_wrapper_2a4eccf_F_0.

According to Linard, this happens because rel(steps,1) selects the slice corresponding to the second execution, and therefore does not refer to the intended Return_wrapper_… function instance.

My proposed workaround was to use
//@ inhale acc(rel(steps,1), 1/18); however, this is a dangerous fix, as it may introduce unsoundness by artificially granting permissions.

Linard’s suggested fix is to replace
//@ assert Return_wrapper(rel(t,1), rel(t,0), rel(steps,1))
with
//@ assert rel(Return_wrapper(rel(t,1), rel(t,0), rel(steps,1)), 1)

This encoding issue is critical to address, since it leads to permission errors when accessing elements of slices from the first execution. For example, the assertion
//@ assert rel(steps,1)[0] == 0
will again result in a permission error during evaluation.

[info] Error at: </.../exercises/relIssue.go:46:9> Precondition of call Return_wrapper(rel(t,1), rel(t,0), rel(steps,1)) might not hold.
[info] Permission to r1 might not suffice.
[info] Gobra found 1 error.

If we use //@ assume acc(rel(steps,1),1) , we will have another Java.concurrency error:

[info] An unknown Exception was thrown.
[info] java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: Unexpected expression rel(steps_V1, 1) cannot be symbolically evaluated

[ArquintL]

Let me try to break this issue down:

• The RuntimeException related to assume acc(rel(steps,1),1) occurs if steps is a slice because the Gobra encoding leads to (pure) quantifiers that use rel in their bodies & triggers. However, the SIFPlugin seems to leave the rel expressions in the trigger unmodified (--> Silver #901)

package relacc

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

requires acc(s)
func bar(s []int) {
    assume acc(rel(s, 1), 1) // `rel` ends up in the trigger
    assert acc(rel(s, 1), 1) // encoded correctly
}

• The "selection" of the correct wrapper function in the encoding and assert rel(steps,1)[0] == 0 suffer from the same underlying problem. The SIF plugin uses separate Viper fields and heap-dependent functions for the first & second execution, and chooses by default the first execution's field & heap-dependent function. The following example illustrates this well: acc(rel(p, 1)) is encoded by Gobra to acc(rel(p, 1).Int, write), i.e., picking the second execution's reference and then takes the Int field that stores the integer value. The SIF plugin correctly encodes rel(p, 1) to the second execution's reference but leaves the Int field unchanged (as it's not within a low or rel expression ^^). This however results in insufficient permissions as the SIF plugin uses distinct fields for the 1st and 2nd execution Int and Int_p.

package relacc2

// ##(--hyperMode extended --enableExperimentalHyperFeatures)

requires acc(p)
func foo(p *int) {
    assert acc(rel(p, 0)) // succeeds
    // assert rel(acc(p), 1) // fails in the desugarer
    assert acc(rel(p, 1)) // fails due to insufficient permissions
}

requires acc(s) && 0 < len(s)
requires s[0] == 0
func bar(s []int) {
    assert rel(s[0], 1) == 0 // succeeds
    assert rel(s, 1)[0] == 0 // fails due to insufficient permissions
}

While "pulling" the rel expression out fixes the issue in some cases, a "smarter" encoding would need to be consider its context. E.g., acc(rel(p, 1)) should be encoded by Gobra as acc(rel(p.Int, 1), write) such that the SIF plugin correctly encodes the field. Note however that this trick does not work for p as rel(acc(p), 1) as this causes an error in Gobra's desugarer ("unexpected type 'assertion'").