Overflow Checking

Usage

By default, Gobra performs no overflow checking. On the command line, you can enable overflow checking with the --overflow or -o flag. The size of int is implementation-specific in Go and either 32 or 64 bits. For overflow checking, Gobra assumes that ints have 64 bits by default. We may change the behavior of Gobra to consider ints with 32 bits by passing the --int32 flag. In a file, we can enable overflow checking by adding the following line:

// ##(--overflow)

Overflow in binary search

If we check our binary search program for large arrays with overflow checking enabled, Gobra detects a potential overflow.

package binarysearch

// ##(--overflow)

const MaxInt64 = 1<<63 - 1
const N = MaxInt64

// @ requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures 0 <= idx && idx <= len(arr)
// @ ensures idx > 0 ==> arr[idx-1] < target
// @ ensures idx < len(arr) ==> target <= arr[idx]
// @ ensures found == (idx < len(arr) && arr[idx] == target)
func BinarySearchOverflow(arr [N]int, target int) (idx int, found bool) {
	low := 0
	high := len(arr)
	mid := 0
	// @ invariant 0 <= low && low <= high && high <= len(arr)
	// @ invariant 0 <= mid && mid < len(arr)
	// @ invariant low > 0 ==> arr[low-1] < target
	// @ invariant high < len(arr) ==> target <= arr[high]
	for low < high {
		mid = (low + high) / 2  // <--- problematic expression
		if arr[mid] < target {
			low = mid + 1
		} else {
			high = mid
		}
	}
	if low < len(arr) {
	 	return low, arr[low] == target
	} else {
	 	return low, false
	}
}

ERROR Expression may cause integer overflow.
Expression (low + high) / 2 might cause integer overflow.

For example, for low = N/2 and high = N, the sum low + high cannot be represented by an int and the result will be negative. The solution is to replace the offending statement mid = (low + high) / 2 with:

mid = (high-low)/2 + low

The subtraction does not overflow since high >= low and low >= 0 holds. After this change, Gobra reports no errors.

If we tweak the const N that denotes the array length to 1<<31 which is larger than MaxInt32, we get an error when checking with --int32 --overflow. Verification succeeds when only check with --overflow.

A similar bug was present in Java's standard library (Read All About It: Nearly All Binary Searches and Mergesorts are Broken). This highlights why heavily used code such as packages from the standard library should be verified.