----------------------------------------------------------------------------- -- | -- Module : TestSuite.Basics.ArithSolver -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- Test suite for basic non-concrete arithmetic, i.e., testing all -- basic arithmetic reasoning using an SMT solver without any -- constant folding. ----------------------------------------------------------------------------- {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-} module TestSuite.Basics.ArithSolver(testSuite) where import Data.SBV import SBVTest -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $ genReals ++ genQRems ++ genBinTest True "+" (+) ++ genBinTest True "-" (-) ++ genBinTest True "*" (*) ++ genUnTest True "negate" negate ++ genUnTest True "abs" abs ++ genUnTest True "signum" signum ++ genBinTest False ".&." (.&.) ++ genBinTest False ".|." (.|.) ++ genBoolTest "<" (<) (.<) ++ genBoolTest "<=" (<=) (.<=) ++ genBoolTest ">" (>) (.>) ++ genBoolTest ">=" (>=) (.>=) ++ genBoolTest "==" (==) (.==) ++ genBoolTest "/=" (/=) (./=) ++ genBinTest False "xor" xor ++ genUnTest False "complement" complement ++ genIntTest "shift" shift ++ genIntTest "rotate" rotate ++ genIntTestS False "setBit" setBit ++ genIntTestS False "clearBit" clearBit ++ genIntTestS False "complementBit" complementBit ++ genIntTest "shift" shift ++ genIntTestS True "shiftL" shiftL ++ genIntTestS True "shiftR" shiftR ++ genIntTest "rotate" rotate ++ genIntTestS True "rotateL" rotateL ++ genIntTestS True "rotateR" rotateR ++ genBlasts ++ genCasts genBinTest :: Bool -> String -> (forall a. Bits a => a -> a -> a) -> [Test] genBinTest unboundedOK nm op = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs] where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `op` b genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test] genBoolTest nm op opS = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs] where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `opS` b genUnTest :: Bool -> String -> (forall a. Bits a => a -> a) -> [Test] genUnTest unboundedOK nm op = map mkTest $ [(show x, mkThm x (op x)) | x <- w8s ] ++ [(show x, mkThm x (op x)) | x <- w16s] ++ [(show x, mkThm x (op x)) | x <- w32s] ++ [(show x, mkThm x (op x)) | x <- w64s] ++ [(show x, mkThm x (op x)) | x <- i8s ] ++ [(show x, mkThm x (op x)) | x <- i16s] ++ [(show x, mkThm x (op x)) | x <- i32s] ++ [(show x, mkThm x (op x)) | x <- i64s] ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs] where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t mkThm x r = isTheorem $ do a <- free "x" constrain $ a .== literal x return $ literal r .== op a genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test] genIntTest nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is] ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is] ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is] ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is] ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- is] ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is] ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is] ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is] where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t is = [-10 .. 10] mkThm2 x y r = isTheorem $ do a <- free "x" constrain $ a .== literal x return $ literal r .== a `op` y genIntTestS :: Bool -> String -> (forall a. Bits a => a -> Int -> a) -> [Test] genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (bitSize x - 1)]] ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (bitSize x - 1)]] ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (bitSize x - 1)]] ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (bitSize x - 1)]] ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (bitSize x - 1)]] ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (bitSize x - 1)]] ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (bitSize x - 1)]] ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]] where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isTheorem $ do a <- free "x" constrain $ a .== literal x return $ literal r .== a `op` y genBlasts :: [Test] genBlasts = map mkTest $ [(show x, mkThm fromBitsLE blastLE x) | x <- w8s ] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w8s ] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i8s ] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i8s ] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w16s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w16s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i16s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i16s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w32s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w32s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i32s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i32s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w64s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w64s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s] where mkTest (x, t) = "blast-" ++ show x ~: assert t mkThm from to v = isTheorem $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a) genCasts :: [Test] genCasts = map mkTest $ [(show x, mkThm unsignCast signCast x) | x <- w8s ] ++ [(show x, mkThm unsignCast signCast x) | x <- w16s] ++ [(show x, mkThm unsignCast signCast x) | x <- w32s] ++ [(show x, mkThm unsignCast signCast x) | x <- w64s] ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ] ++ [(show x, mkThm signCast unsignCast x) | x <- i16s] ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ] ++ [(show x, mkThm signCast unsignCast x) | x <- i16s] ++ [(show x, mkThm signCast unsignCast x) | x <- i32s] ++ [(show x, mkThm signCast unsignCast x) | x <- i64s] ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w8s ] ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w16s] ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w32s] ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w64s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i8s ] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i16s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s] where mkTest (x, t) = "cast-" ++ show x ~: assert t mkThm from to v = isTheorem $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a) mkFEq f g v = isTheorem $ do a <- free "x" constrain $ a .== literal v return $ f a .== g a genReals :: [Test] genReals = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- rs, y <- rs ] ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- rs, y <- rs ] ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- rs, y <- rs ] ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- rs, y <- rs, y /= 0] ++ [("<", show x, show y, mkThm2 (.<) x y (x < y)) | x <- rs, y <- rs ] ++ [("<=", show x, show y, mkThm2 (.<=) x y (x <= y)) | x <- rs, y <- rs ] ++ [(">", show x, show y, mkThm2 (.>) x y (x > y)) | x <- rs, y <- rs ] ++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- rs, y <- rs ] ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs ] ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs ] where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `op` b genQRems :: [Test] genQRems = map mkTest $ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w8s, y <- w8s ] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w16s, y <- w16s] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w32s, y <- w32s] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w64s, y <- w64s] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i8s, y <- i8s , noOverflow x y] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i16s, y <- i16s, noOverflow x y] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i32s, y <- i32s, noOverflow x y] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i64s, y <- i64s, noOverflow x y] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- iUBs, y <- iUBs] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w8s, y <- w8s ] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w16s, y <- w16s] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w32s, y <- w32s] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w64s, y <- w64s] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i8s, y <- i8s , noOverflow x y] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i16s, y <- i16s, noOverflow x y] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i32s, y <- i32s, noOverflow x y] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i64s, y <- i64s, noOverflow x y] ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- iUBs, y <- iUBs] where divMod' x y = if y == 0 then (0, x) else x `divMod` y quotRem' x y = if y == 0 then (0, x) else x `quotRem` y mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y (e1, e2) = isTheorem $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ (literal e1, literal e2) .== a `op` b -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for signed types; so avoid that case noOverflow x y = not (x == minBound && y == -1) -- Concrete test data xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a] xsUnsigned = [minBound, 0, maxBound] xsSigned = xsUnsigned ++ [-1, 1] w8s :: [Word8] w8s = xsUnsigned w16s :: [Word16] w16s = xsUnsigned w32s :: [Word32] w32s = xsUnsigned w64s :: [Word64] w64s = xsUnsigned i8s :: [Int8] i8s = xsSigned i16s :: [Int16] i16s = xsSigned i32s :: [Int32] i32s = xsSigned i64s :: [Int64] i64s = xsSigned iUBs :: [Integer] iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000] rs :: [AlgReal] rs = [fromRational (i % d) | i <- is, d <- ds] where is = [-1000000] ++ [-1 .. 1] ++ [10000001] ds = [5,100,1000000] {-# ANN module "HLint: ignore Reduce duplication" #-}