-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.BitPrecise.BrokenSearch
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The classic "binary-searches are broken" example:
--     <http://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html>
-----------------------------------------------------------------------------

{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.BitPrecise.BrokenSearch where

import Data.SBV
import Data.SBV.Tools.Overflow

#ifndef HADDOCK
-- $setup
-- >>> import Data.SBV
-- >>> import Data.Int
#endif

-- | 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:43:32:+!: SInt32 addition overflows: Violated. Model:
--   low  = 1073741832 :: Int32
--   high = 1107296257 :: Int32
--
-- Indeed:
--
-- >>> (1073741832 + 1107296257) `div` (2::Int32)
-- -1056964604
--
-- giving us quite a large negative mid-point value!
midPointBroken :: SInt32 -> SInt32 -> SInt32
midPointBroken :: SInt32 -> SInt32 -> SInt32
midPointBroken SInt32
low SInt32
high = (SInt32
low SInt32 -> SInt32 -> SInt32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
+! SInt32
high) SInt32 -> SInt32 -> SInt32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
/! SInt32
2

-- | 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.
midPointFixed :: SInt32 -> SInt32 -> SInt32
midPointFixed :: SInt32 -> SInt32 -> SInt32
midPointFixed SInt32
low SInt32
high = SInt32
low SInt32 -> SInt32 -> SInt32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
+! ((SInt32
high SInt32 -> SInt32 -> SInt32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
-! SInt32
low) SInt32 -> SInt32 -> SInt32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
/! SInt32
2)

-- | 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.
midPointAlternative :: SInt32 -> SInt32 -> SInt32
midPointAlternative :: SInt32 -> SInt32 -> SInt32
midPointAlternative SInt32
low SInt32
high = SBV Word32 -> SInt32
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral ((SBV Word32
low' SBV Word32 -> SBV Word32 -> SBV Word32
forall a.
(CheckedArithmetic a, ?loc::CallStack) =>
SBV a -> SBV a -> SBV a
+! SBV Word32
high') SBV Word32 -> Int -> SBV Word32
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)
  where low', high' :: SWord32
        low' :: SBV Word32
low'  = SInt32 -> SBV Word32
forall a b.
(?loc::CallStack, Integral a, HasKind a, HasKind b, Num a,
 SymVal a, HasKind b, Num b, SymVal b) =>
SBV a -> SBV b
sFromIntegralChecked SInt32
low
        high' :: SBV Word32
high' = SInt32 -> SBV Word32
forall a b.
(?loc::CallStack, Integral a, HasKind a, HasKind b, Num a,
 SymVal a, HasKind b, Num b, SymVal b) =>
SBV a -> SBV b
sFromIntegralChecked SInt32
high

-------------------------------------------------------------------------------------
-- * Helpers
-------------------------------------------------------------------------------------

-- | A helper predicate to check safety under the conditions that @low@ is at least 0
-- and @high@ is at least @low@.
checkArithOverflow :: (SInt32 -> SInt32 -> SInt32) -> IO ()
checkArithOverflow :: (SInt32 -> SInt32 -> SInt32) -> IO ()
checkArithOverflow SInt32 -> SInt32 -> SInt32
f = do sr <- SymbolicT IO SInt32 -> IO [SafeResult]
forall a. SExecutable IO a => a -> IO [SafeResult]
safe (SymbolicT IO SInt32 -> IO [SafeResult])
-> SymbolicT IO SInt32 -> IO [SafeResult]
forall a b. (a -> b) -> a -> b
$ do low   <- String -> SymbolicT IO SInt32
sInt32 String
"low"
                                          high <- sInt32 "high"

                                          constrain $ low .>= 0
                                          constrain $ low .<= high

                                          output $ f low high

                          case filter (not . isSafe) sr of
                                 [] -> String -> IO ()
putStrLn String
"No violations detected."
                                 [SafeResult]
xs -> (SafeResult -> IO ()) -> [SafeResult] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SafeResult -> IO ()
forall a. Show a => a -> IO ()
print [SafeResult]
xs

-- | 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.
checkCorrectMidValue :: (SInt32 -> SInt32 -> SInt32) -> IO ThmResult
checkCorrectMidValue :: (SInt32 -> SInt32 -> SInt32) -> IO ThmResult
checkCorrectMidValue SInt32 -> SInt32 -> SInt32
f = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do low  <- String -> SymbolicT IO SInt32
sInt32 String
"low"
                                    high <- sInt32 "high"

                                    constrain $ low .>= 0
                                    constrain $ low .<= high

                                    let low', high' :: SInt64
                                        low'  = SInt32 -> SBV Int64
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInt32
low
                                        high' = SInt32 -> SBV Int64
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInt32
high
                                        mid'  = (SBV Int64
low' SBV Int64 -> SBV Int64 -> SBV Int64
forall a. Num a => a -> a -> a
+ SBV Int64
high') SBV Int64 -> SBV Int64 -> SBV Int64
forall a. SDivisible a => a -> a -> a
`sDiv` SBV Int64
2

                                        mid   = SInt32 -> SInt32 -> SInt32
f SInt32
low SInt32
high

                                    return $ sFromIntegral mid .== mid'

{- HLint ignore module "Reduce duplication" -}