sbv-8.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Documentation.SBV.Examples.BitPrecise.BrokenSearch

Contents

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

Synopsis

Documentation

Model the mid-point computation of the binary search, which is broken due to arithmetic overflow. Note how we use the overflow checking variants of the arithmetic operators. We have:

>>> checkArithOverflow midPointBroken
Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs:33:28:+!: SInt32 addition overflows: Violated. Model:
low  = 1073741824 :: Int32
high = 1073742336 :: Int32


Indeed:

>>> (1073741824 + 1073742336) div (2::Int32)
-1073741568


giving us a negative mid-point value!

The correct version of how to compute the mid-point. As expected, this version doesn't have any underflow or overflow issues:

>>> checkArithOverflow midPointFixed
No violations detected.


As expected, the value is computed correctly too:

>>> checkCorrectMidValue midPointFixed
Q.E.D.


Show that the variant suggested by the blog post is good as well:

mid = ((unsigned int)low + (unsigned int)high) >> 1;

In this case the overflow is eliminated by doing the computation at a wider range:

>>> checkArithOverflow midPointAlternative
No violations detected.


And the value computed is indeed correct:

>>> checkCorrectMidValue midPointAlternative
Q.E.D.


Helpers

checkArithOverflow :: (SInt32 -> SInt32 -> SInt32) -> IO () Source #

A helper predicate to check safety under the conditions that low is at least 0 and high is at least low.

Another helper to show that the result is actually the correct value, if it was done over 64-bit integers, which is sufficiently large enough.