Verifying programs with arrays

In this section, we show how to verify programs that use arrays of fixed size (we will later see how to verify programs with slices, the length of which may not be statically known). Programs that access arrays often suffer from subtle bugs such as off-by-one errors or out-of-bounds accesses that may lead to runtime panics. Gobra prevents this by statically checking that every access to arrays is within bounds.

Go can find out-of-bounds indices for constant values when compiling a program.

func client1() int {
	a := [5]int{2, 3, 5, 7, 11}
	b1 := a[-1] // invalid index (too small)
	b2 := a[1]  // valid index
	b3 := a[10] // invalid index (too large)
	return b1 + b2 + b3
}

./array.go:8:16: invalid argument: index -1 (constant of type int) must not be negative
./array.go:10:16: invalid argument: index 10 out of bounds [0:5]

Unfortunately, the checks that the Go compiler performs may miss simple out-of-bounds errors, as shown in the example below that moves the array access to a different function:

func readArr(a [5]int, i int) int {
	b := a[i]
	return b
}

func main() {
	a := [5]int{2, 3, 5, 7, 11}
	readArr(a, -1)
	readArr(a, 1)
	readArr(a, 10)
}

Go is memory-safe and checks at runtime whether the index is within bounds:

panic: runtime error: index out of range [-1]

goroutine 1 [running]:
main.readArr(...)
        /home/gobra/array.go:20

If we check the program with Gobra, we can find the error statically at verification time.

ERROR Assignment might fail. 
Index i into a[i] might be negative.

The indexing operation a[i] implicitly has the precondition requires 0 <= i && i < len(a). By propagating this precondition to the contract of readArr, Gobra accepts the function.

// @ requires 0 <= i && i < len(a)
func readArr(a [5]int, i int) int {
	b := a[i]
	return b
}

Then the calls readArr(a, -1) and readArr(a, 10) will get rejected.

Gobra statically checks that every access to arrays is within bounds.