Ensure constraints are correct for testing for underflow/overflow for signed ints. Verified via SMT.

Bounded.hs

{-# LANGUAGE ScopedTypeVariables #-}

-- | Ensure constraints are correct for testing for underflow/overflow for
-- signed ints.  Verified via SMT.

-- author : Lee Pike
-- date   : Jan 2014
-- license: BSD3

--import Data.SBV.Bridge.CVC4

import Data.SBV.Bridge.Z3

import Prelude hiding (min, max, signum, abs)

--------------------------------------------------------------------------------

type SI = SBV Integer

-- We'll consider int8_t in this example.
max = 127
min = -128

sz :: SI -> SBool
sz x = (x .>= min) &&& (x .<= max)

szConstraint :: SI -> SI -> SBool
szConstraint x y = sz x &&& sz y

negative :: SI -> SBool
negative x = x .< 0

positive :: SI -> SBool
positive x = x .> 0

zero :: SI -> SBool
zero x = x .== 0

abs :: SI -> SI
abs x =
  ite (x .== min)
      -- XXX Warning! abs(MIN) is actually undefined for signed types.
      max
      $ ite (signum x .== -1)
            (0-x)
            x

signum :: SI -> SI
signum x =
  ite (negative x)
      (-1)
    $ ite (positive x)
          1
          0

preconditionCheck :: (SI -> SI -> SBool) -> IO ()
preconditionCheck pred = do
  let signChk :: SI -> SI -> Predicate
      signChk a b = forSome_ $ \(x::SI) (y::SI)
                 -> pred x y &&& signum x .== a &&& signum y .== b &&& sz x &&& sz y
  res <- mapM sat [ signChk 0 0   , signChk 0 (-1)   , signChk 0 1
                  , signChk 1 0   , signChk 1 (-1)   , signChk 1 1
                  , signChk (-1) 0, signChk (-1) (-1), signChk (-1) 1
                  ]
  let fstChk a = forSome_ $ \(x::SI) -> pred x a &&& sz x
  let sndChk a = forSome_ $ \(x::SI) -> pred a x &&& sz x
  res0 <- mapM sat [ fstChk max, sndChk max
                   , fstChk min, sndChk min ]
  mapM_ print res
  mapM_ print res0

--------------------------------------------------------------------------------

addConstraint :: SI -> SI -> SBool
addConstraint x y =
      (x .>= 0 &&& y .>= 0 &&& max - x .>= y)
  ||| (x .<= 0 &&& y .<= 0 &&& min - x .<= y)
  ||| (signum x ./= signum y)

addCorrect :: SI -> SI -> SBool
addCorrect x y = (sz x &&& sz y &&& addConstraint x y) ==> sz (x + y)

runAdd = do
  prove addCorrect >>= print
  preconditionCheck addConstraint

--------------------------------------------------------------------------------

subConstraint :: SI -> SI -> SBool
subConstraint x y =
      (x .>= 0 &&& y .<= 0 &&& max + y .>= x)
  ||| (x .<= 0 &&& y .>= 0 &&& min + y .<= x)
  ||| (signum x .== signum y)

subCorrect :: SI -> SI -> SBool
subCorrect x y = (sz x &&& sz y &&& subConstraint x y) ==> sz (x - y)

runSub = do
  prove subCorrect >>= print
  preconditionCheck subConstraint

--------------------------------------------------------------------------------

minNegOne :: SI -> SI -> SBool
minNegOne a b = a ./= min ||| b ./= (-1)

-- CVC4 doesn't handle the non-linear constraints.  Z3 does, but seems to have a
-- spurious warning that there is no neg. x and y==0 that satisfies the
-- constraints.
multConstraint :: SI -> SI -> SBool
multConstraint x y =
      (minNegOne x y ||| minNegOne y x)
  &&& (    x .== 0
       ||| y .== 0
       ||| (max `sQuot` abs x .>= abs y &&& min `sQuot` abs x .<= abs y))

-- multConstraint :: SI -> SI -> SBool
-- multConstraint x y =
--       (minNegOne x y &&& minNegOne y x)
--   &&& (    x .== 0
--        ||| y .== 0
--        ||| (max `sQuot` abs x .>= abs y &&& min `sQuot` abs x .<= abs y))

multCorrect :: SI -> SI -> SBool
multCorrect x y = (sz x &&& sz y &&& multConstraint x y) ==> sz (x * y)

runMult = do
  prove multCorrect >>= print
  preconditionCheck multConstraint

--------------------------------------------------------------------------------

divConstraint :: SI -> SI -> SBool
divConstraint x y = y ./= 0 &&& minNegOne x y

divCorrect :: SI -> SI -> SBool
divCorrect x y = (sz x &&& sz y &&& divConstraint x y) ==> sz (x `sQuot` y)

runDiv = do
  prove divCorrect >>= print
  preconditionCheck divConstraint

--------------------------------------------------------------------------------