Computers are great at crunching numbers. However, if programmers aren’t careful, their machines can end up biting off more than they can chew: simple arithmetic operations over very large (or very tiny) inputs can overflow leading to bizarre crashes or vulnerabilities. For example, Joshua Bloch’s classic post argues that nearly all binary searches are broken due to integer overflows. Lets see how we can teach LiquidHaskell to spot such overflows.

30: module Bounded where
31: 
32: import           Control.Exception (assert)
33: import           Prelude hiding (Num (..))
34: import qualified Prelude
35: 
36: plusStrict :: Int -> Int -> Int
37: plusLazy   :: Int -> Int -> Int
38: mono       :: Int -> Bool

1. The Problem

LiquidHaskell, like some programmers, likes to make believe that Int represents the set of integers. For example, you might define a function plus as:

51: {-@ plus :: x:Int -> y:Int -> {v:Int | v == x + y} @-}
52: plus :: Int -> Int -> Int
53: x1:Int -> x2:Int -> {v : Int | v == x1 + x2}plus Intx Inty = {v : Int | v == y}x x1:Int -> x2:Int -> {v : Int | v == x1 + x2}Prelude.+ y

The output type of the function states that the returned value is equal to the result of adding the two inputs.

The above signature lets us “prove” facts like addition by one yields a bigger number:

63: {-@ monoPlus :: Int -> {v:Bool | v <=> true } @-}
64: monoPlus :: Int -> Bool
65: Int -> {v : Bool | v <=> true}monoPlus Intx = {v : Int | v == x}x x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< {v : x1:Int -> x2:Int -> {v : Int | v == x1 + x2} | v == Bounded.plus}plus x 1

Unfortunately, the signature for plus and hence, the above “fact” are both lies.

LH checks plus as the same signature is assumed for the primitive Int addition operator Prelude.+. LH has to assume some signature for this “foreign” machine operation, and by default, LH assumes that machine addition behaves like logical addition.

However, this assumption, and its consequences are only true upto a point:

λ>  monoPlus 0
True
λ>  monoPlus 100
True
λ>  monoPlus 10000
True
λ>  monoPlus 1000000
True

Once we get to maxBound at the very edge of Int, a tiny bump is enough to send us tumbling backwards into a twilight zone.

λ> monoPlus maxBound
False

λ> plus maxBound 1
-9223372036854775808

2. Keeping Int In Their Place

The news isn’t all bad: the glass half full view is that for “reasonable” values like 10, 100, 10000 and 1000000, the machine’s arithmetic is the same as logical arithmetic. Lets see how to impart this wisdom to LH. We do this in two steps: define the biggest Int value, and then, use this value to type the arithmetic operations.

A. The Biggest Int

First, we need a way to talk about “the edge” – i.e. the largest Int value at which overflows occur.

We could use the concrete number

λ> maxBound :: Int
9223372036854775807

However, instead of hardwiring a particular number, a more general strategy is to define a symbolic constant maxInt to represent any arbitrary overflow value and thus, make the type checking robust to different machine integer widths.

135: -- defines an Int constant called `maxInt`
136: {-@ measure maxInt :: Int @-}

To tell LH that maxInt is the “biggest” Int, we write a predicate that describes values bounded by maxInt:

144: {-@ predicate Bounded N = 0 < N + maxInt && N < maxInt @-}

Thus, Bounded n means that the number n is in the range [-maxInt, maxInt].

B. Bounded Machine Arithmetic

Next, we can assign the machine arithmetic operations types that properly capture the possibility of arithmetic overflows. Here are two possible specifications.

Strict: Thou Shalt Not Overflow A strict specification simply prohibits any overflow:

160: {-@ plusStrict :: x:Int -> y:{Int|Bounded(x+y)} -> {v:Int|v = x+y} @-}
161: x1:Int -> x2:{y : Int | 0 < (x1 + y) + maxInt
                        && x1 + y < maxInt} -> {v : Int | v == x1 + x2}plusStrict Intx {y : Int | 0 < (x + y) + maxInt
           && x + y < maxInt}y = {v : Int | 0 < (x + v) + maxInt
           && x + v < maxInt
           && v == y}x x1:Int -> x2:Int -> {v : Int | v == x1 + x2}Prelude.+ y

The inputs x and y must be such that the result is Bounded, and in that case, the output value is indeed their logical sum.

Lazy: Overflow at Thine Own Risk Instead, a lazy specification could permit overflows but gives no guarantees about the output when they occur.

172: {-@ plusLazy :: x:Int -> y:Int -> {v:Int|Bounded(x+y) => v = x+y} @-}
173: x1:Int -> x2:Int -> {v : Int | 0 < (x1 + x2) + maxInt
                               && x1 + x2 < maxInt => v == x1 + x2}plusLazy Intx Inty = {v : Int | v == y}x x1:Int -> x2:Int -> {v : Int | v == x1 + x2}Prelude.+ y

The lazy specification says that while plusLazy can be called with any values you like, the result is the logical sum only if there is no overflow.

To understand the difference between the two specifications, lets revisit the monoPlus property using the new machine-arithmetic sensitive signatures:

188: {-@ monoPlusStrict :: Int -> {v:Bool | v <=> true } @-}
189: Int -> {v : Bool | v <=> true}monoPlusStrict Intx = {v : Int | v == x}x x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< {v : x1:Int -> x2:{v : Int | 0 < (x1 + v) + maxInt
                             && x1 + v < maxInt} -> {v : Int | v == x1 + x2} | v == Bounded.plusStrict}plusStrict x 1
190: 
191: {-@ monoPlusLazy :: Int -> {v:Bool | v <=> true } @-}
192: Int -> {v : Bool | v <=> true}monoPlusLazy Intx = {v : Int | v == x}x x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< {v : x1:Int -> x2:Int -> {v : Int | 0 < (x1 + x2) + maxInt
                                    && x1 + x2 < maxInt => v == x1 + x2} | v == Bounded.plusLazy}plusLazy x 1

Both are rejected by LH, since, as we saw earlier, the functions do not always evaluate to True. However, in the strict version the error is at the possibly overflowing call to plusStrict. In the lazy version, the call to plusLazy is accepted, but as the returned value is some arbitrary Int (not the logical x+1), the comparison may return False hence the output is not always True.

Exercise: Can you fix the specification for monoPlusStrict and monoPlusLazy to get LH to verify the implementation?

3. A Typeclass for Machine Arithmetic

Its a bit inconvenient to write plusStrict and plusLazy, and really, we’d just like to write + and - and so on. We can do so, by tucking the above specifications into a bounded numeric typeclass whose signatures capture machine arithmetic. First, we define a BoundedNum variant of Num

220: class BoundedNum a where
221:   (+) :: a -> a -> a
222:   (-) :: a -> a -> a
223:   -- other operations ...

and now, we can define its Int instance just as wrappers around the Prelude operations:

230: instance BoundedNum Int where
231:   Intx x1:Int -> x2:{y : Int | 0 < (x1 + y) + maxInt
                        && x1 + y < maxInt} -> {v : Int | v == x1 + x2}+ {y : Int | 0 < (x + y) + maxInt
           && x + y < maxInt}y = {v : Int | 0 < (x + v) + maxInt
           && x + v < maxInt
           && v == y}x x1:Int -> x2:Int -> {v : Int | v == x1 + x2}Prelude.+ y
232:   Intx x1:Int -> x2:{y : Int | 0 < (x1 - y) + maxInt
                        && x1 - y < maxInt} -> {v : Int | v == x1 - x2}- {y : Int | 0 < (x - y) + maxInt
           && x - y < maxInt}y = {v : Int | 0 < (x - v) + maxInt
           && x - v < maxInt
           && v == y}x x1:Int -> x2:Int -> {v : Int | v == x1 - x2}Prelude.- y

Finally, we can tell LH that the above above instance obeys the (strict) specifications for machine arithmetic:

239: {-@ instance BoundedNum Int where
240:       + :: x:Int -> y:{Int | Bounded (x+y)} -> {v:Int | v == x+y };
241:       - :: x:Int -> y:{Int | Bounded (x-y)} -> {v:Int | v == x-y }
242:   @-}

With the above instance in scope, we can just use the plain + operator and have LH flag potential overflows:

249: {-@ mono :: Int -> {v:Bool | v <=> true} @-}
250: Int -> {v : Bool | v <=> true}mono Intx = {v : Int | v == x}x x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< Intx + 1

4. An Application: Binary Search

The above seems a bit paranoid. Do overflows really matter? And if they do, is it really practical to check for them using the above?

Joshua Bloch’s famous article describes a tricky overflow bug in an implementation of binary-search that lay hidden in plain sight in classic textbooks and his own implementation in the JDK for nearly a decade. Gabriel Gonzalez wrote a lovely introduction to LH using binary-search as an example, and a careful reader pointed out that it had the same overflow bug!

Lets see how we might spot and fix such bugs using BoundedNum. (Hover over the images to animate.)