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, whose length may not be statically known). Programs that access arrays often suffer from subtle bugs such as off-by-one errors, or other kinds of out-of-bounds accesses, that may lead to runtime panics. Gobra prevents these 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

Now 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.

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.