Gobra does not immediately realize semantics of copying arrays by assignment

[felixlinker]

In Go, assigning arrays copies them. Gobra fails to realize this immediately. I got the following to verify:

func f() {
	a1 /*@@@*/ := [1]int{0}
	// @ assert acc(&a1)
	a2 /*@@@*/ := a1
	// @ assert a1[0] == 0 // required for verification
	// @ assert &a1 != &a2
}

Removing assert a1[0] == 0 leads to a failure in verification of &a1 != &a2. This seems like unwanted behavior as the semantics of copying arrays and how that affects the respective addresses seem quite fundamental.

[jcp19]

yeah, this is one of the logical incompletenesses we currently have with the slice encoding (for reference, #191 seems related). This is not a soundness issue, but I agree it is less than ideal. Fixing this probably requires deep changes to our slice encoding, and thus, I find it unlikely to change soon.

[felixlinker]

Maybe related, I'm struggling to verify memory safety of a function that constructs a slice of arrays. In my code, the error reported by gobra is related to injectivity. While trying to create a minimal example, I ran into a permission error on unknown.

I asked AI for help, and they managed to verify it when copying every element of rec into a fresh slice. Maybe the issue is around append? Or am I missing something entirely?

Here's the function:

// @ requires 0 <= x
// @ ensures 0 < len(r) && acc(r)
// @ decreases x
func f(x int) (r [][1]int) {
	r = [][1]int{[1]int{x}}
	// @ assert acc(r)
	if x == 0 {
		return r
	} else {
		rec := f(x - 1)
		return append( /*@ writePerm, @*/ r, rec...)
	}
}

[felixlinker]

The function verifies immediately if I refactor the return type to []*[1]int.

[ArquintL]

I briefly looked at the function and the problem is that the specification for the append function that Gobra creates as part of the encoding ends up causing a verification error. More specifically, the postcondition calls arrayConversion_1_Intint$$$_S_$$$ in an old expression and Viper beliefs that we don't have sufficient permissions to the array (r in the code above) to call this (heap-dependent) function. However, it seems to me that we would have sufficient permissions and this error is caused due to an incompleteness.
Since the error lies in a built-in spec, the options are limited:

• address the incompleteness in the encoding, or
• do not use append on slices of type [][1]int

[ArquintL]

Wouldn't the behavior of caller be equivalent to the behavior of f?
(I was trying to preserve the same recursive structure in g as used in f; one could probably do this nicer using a loop instead. In addition, this performs a single memory allocation (not counting the [1]int allocations) and avoids the potential copy operations that append causes if the slice cannot grow anymore due to reaching its capacity)

requires 0 <= n
ensures  0 < len(r) && acc(r)
decreases
func caller(n int) (r [][1]int) {
	r := make([][1]int, n + 1)
	g(r, n)
	return
}

requires 0 <= x && x < len(r)
preserves acc(r)
decreases x
func g(r [][1]int, x int) {
	r[len(r) - x - 1] = [1]int{ x }
	if x != 0 {
		g(r, x - 1)
	}
	return
}

[ArquintL]

And one can strengthen the specifications to the following, which fully determines the length and content of the returned slice:

requires 0 <= n
ensures  len(r) == n + 1
ensures  forall i int :: { &r[i] } 0 <= i && i < len(r) ==> acc(&r[i]) && r[i] == [1]int{ len(r) - 1 - i }
decreases
func caller(n int) (r [][1]int) {
	r := make([][1]int, n + 1)
	g(r, n)
	return
}

requires 0 <= x && x < len(r)
requires forall i int :: { &r[i] } len(r) - x - 1 <= i && i < len(r) ==> acc(&r[i])
ensures  forall i int :: { &r[i] } len(r) - x - 1 <= i && i < len(r) ==> acc(&r[i]) && r[i] == [1]int{ len(r) - 1 - i }
decreases x
func g(r [][1]int, x int) {
	r[len(r) - x - 1] = [1]int{ x }
	i := len(r) - x - 1
	if x != 0 {
		g(r, x - 1)
	}
	return
}