sbv-14.1: SBVTestSuite/TestSuite/Basics/ArithSolver.hs
-----------------------------------------------------------------------------
-- |
-- 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 DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns -Wno-x-partial #-}
module TestSuite.Basics.ArithSolver(tests) where
import Data.SBV.Internals hiding (free, free_, (#))
import Utils.SBVTestFramework
import Data.List (genericIndex, isInfixOf, isPrefixOf, isSuffixOf, genericTake, genericDrop, genericLength)
import qualified Data.Char as C
import qualified Data.SBV.Char as SC
import qualified Data.SBV.List as SL
data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun deriving (Show, Bounded, Enum, Eq)
mkSymbolic [''Day]
-- Test suite
tests :: TestTree
tests =
testGroup "Basics.ArithSolver"
( genExtends
++ genConcats
++ genReals
++ genFloats
++ genDoubles
++ genFPConverts
++ genQRems
++ genBinTest True "+" (+)
++ genBinTest True "-" (-)
++ genBinTest True "*" (*)
++ genUnTest True "negate" negate
++ genUnTest True "abs" abs
++ genUnTest True "signum" signum
++ genBitTest False ".&." (.&.)
++ genBitTest False ".|." (.|.)
++ genBoolTest "<" (<) (.<)
++ genBoolTest "<=" (<=) (.<=)
++ genBoolTest ">" (>) (.>)
++ genBoolTest ">=" (>=) (.>=)
++ genBoolTest "==" (==) (.==)
++ genBoolTest "/=" (/=) (./=)
++ genBitTest False "xor" xor
++ genUnTestBit False "complement" complement
++ genIntTest False "setBit" setBit
++ genIntTest False "clearBit" clearBit
++ genIntTest False "complementBit" complementBit
++ genIntTest True "shift" shift
++ genIntTest True "shiftL" shiftL
++ genIntTest True "shiftR" shiftR
++ genIntTest True "rotate" rotate
++ genIntTest True "rotateL" rotateL
++ genIntTest True "rotateR" rotateR
++ genShiftRotTest "shiftL_gen" sShiftLeft
++ genShiftRotTest "shiftR_gen" sShiftRight
++ genShiftRotTest "rotateL_gen" sRotateLeft
++ genShiftRotTest "rotateR_gen" sRotateRight
++ genShiftMixSize
++ genBlasts
++ genCounts
++ genIntCasts
++ genChars
++ genStrings
++ genLists
++ genEnums
++ misc
)
genExtends :: [TestTree]
genExtends = map mkTest $ [("signExtend-word", show x, mkThm signExtend x (signExtend (literal x) :: SWord 16)) | x <- wn8s]
++ [("signExtend-int", show x, mkThm signExtend x (signExtend (literal x) :: SInt 16)) | x <- in8s]
++ [("zeroExtend-word", show x, mkThm zeroExtend x (zeroExtend (literal x) :: SWord 16)) | x <- wn8s]
++ [("zeroExtend-int", show x, mkThm zeroExtend x (zeroExtend (literal x) :: SInt 16)) | x <- in8s]
where
mkTest (nm, x, t) = testCase ("genExtends-" ++ nm ++ "." ++ x) (assert t)
mkThm op x sr
| Just r <- unliteral sr
= isTheorem $ do a <- free "x"
constrain $ a .== literal x
return $ literal r .== op a
| True
= return False
genConcats :: [TestTree]
genConcats = map mkTest $ [("word", show x, show y, mkThm2 (#) x y (literal x # literal y)) | x <- wn8s, y <- wn8s]
++ [("int", show x, show y, mkThm2 (#) x y (literal x # literal y)) | x <- in8s, y <- in8s]
where
mkTest (nm, x, y, t) = testCase ("genConcats-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t)
mkThm2 op x y sr
| Just r <- unliteral sr
= isTheorem $ do [a, b] <- mapM free ["a", "b"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `op` b
| True
= return False
genBinTest :: Bool -> String -> (forall a. Num a => a -> a -> a) -> [TestTree]
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)) | x <- rs, y <- rs]
++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]
where mkTest (x, y, t) = testCase ("genBinTest.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
genBitTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]
genBitTest 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) = testCase ("genBitTest.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) -> [TestTree]
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 ]
++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- reducedCS, y <- reducedCS]
++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- fs, y <- fs ]
++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ds, y <- ds ]
++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ss, y <- ss ]
++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- rs, y <- rs ]
++ [(show x, show y, mkThm2L x y (x `op` y)) | nm `elem` allowedListComps, x <- sl, y <- sl ]
++ [(show x, show y, mkThm2M x y (x `op` y)) | x <- sm, y <- sm ]
++ [(show x, show y, mkThm2E x y (x `op` y)) | x <- se, y <- se ]
++ [(show x, show y, mkThm2T x y (x `op` y)) | x <- st, y <- st ]
where -- Currently Z3 doesn't allow for list comparisons, so only test equals and distinct
-- And there's no way for us to desugar this like we do for tuple/maybe etc; since the datatype itself is recursive.
allowedListComps = ["==", "/="]
mkTest (x, y, t) = testCase ("genBoolTest.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
mkThm2L x y r = isTheorem $ do [a, b :: SList Integer] <- mapM free ["x", "y"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `opS` b
mkThm2M x y r = isTheorem $ do [a, b :: SMaybe Integer] <- mapM free ["x", "y"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `opS` b
mkThm2E x y r = isTheorem $ do [a, b :: SEither Integer Integer] <- mapM free ["x", "y"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `opS` b
mkThm2T x y r = isTheorem $ do [a, b :: STuple Integer Integer] <- mapM free ["x", "y"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `opS` b
genUnTest :: Bool -> String -> (forall a. Num a => a -> a) -> [TestTree]
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)) | x <- rs ]
++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]
where mkTest (x, t) = testCase ("genUnTest.arithmetic-" ++ nm ++ "." ++ x) (assert t)
mkThm x r = isTheorem $ do a <- free "x"
constrain $ a .== literal x
return $ literal r .== op a
genUnTestBit :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree]
genUnTestBit 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) = testCase ("genUnTestBit.arithmetic-" ++ nm ++ "." ++ x) (assert t)
mkThm x r = isTheorem $ do a <- free "x"
constrain $ a .== literal x
return $ literal r .== op a
genIntTest :: Bool -> String -> (forall a. (Num a, Bits a) => (a -> Int -> a)) -> [TestTree]
genIntTest overSized nm op = map mkTest $
[("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is (intSizeOf x)]
++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is (intSizeOf x)]
++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is (intSizeOf x)]
++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is (intSizeOf x)]
++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- is (intSizeOf x)]
++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is (intSizeOf x)]
++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is (intSizeOf x)]
++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is (intSizeOf x)]
-- No size based tests for unbounded integers
where is sz = [0 .. sz - 1] ++ extras
where extras
| overSized = map (sz +) ([0 .. 1] ++ [sz, sz+1])
| True = []
mkTest (l, x, y, t) = testCase ("genIntTest.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
genShiftRotTest :: String -> (forall a. (SIntegral a, SDivisible (SBV a)) => (SBV a -> SBV a -> SBV a)) -> [TestTree]
genShiftRotTest nm op = map mkTest $
[("u8", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w8s, y <- is (intSizeOf x)]
++ [("u16", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w16s, y <- is (intSizeOf x)]
++ [("u32", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w32s, y <- is (intSizeOf x)]
++ [("u64", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w64s, y <- is (intSizeOf x)]
++ [("s8", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i8s, y <- is (intSizeOf x)]
++ [("s16", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i16s, y <- is (intSizeOf x)]
++ [("s32", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i32s, y <- is (intSizeOf x)]
++ [("s64", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i64s, y <- is (intSizeOf x)]
-- NB. No generic shift/rotate for SMTLib unbounded integers
where is sz = let b :: Word32
b = fromIntegral sz
in [0 .. b - 1] ++ [b, b+1, 2*b, 2*b+1]
mkTest (l, x, y, t) = testCase ("genShiftRotTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y) (assert t)
mkThm2 x y sr
| Just r <- unliteral sr
= isTheorem $ do [a, b] <- mapM free ["x", "y"]
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `op` b
| True
= return False
-- A few tests for mixed-size shifts
genShiftMixSize :: [TestTree]
genShiftMixSize = map mkTest $ [(show x, show y, "shl_w8_w16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w8s, y <- yw16s]
++ [(show x, show y, "shr_w8_w16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w8s, y <- yw16s]
++ [(show x, show y, "shl_w16_w8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w16s, y <- w8s]
++ [(show x, show y, "shr_w16_w8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w16s, y <- w8s]
++ [(show x, show y, "shl_i8_i16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i8s, y <- yi16s]
++ [(show x, show y, "shr_i8_i16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i8s, y <- yi16s]
++ [(show x, show y, "shl_i16_i8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i16s, y <- i8s, y >= 0]
++ [(show x, show y, "shr_i16_i8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i16s, y <- i8s, y >= 0]
++ [(show x, show y, "shl_w8_i16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w8s, y <- yi16s]
++ [(show x, show y, "shr_w8_i16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w8s, y <- yi16s]
++ [(show x, show y, "shl_w16_i8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w16s, y <- i8s, y >= 0]
++ [(show x, show y, "shr_w16_i8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w16s, y <- i8s, y >= 0]
++ [(show x, show y, "shl_i8_w16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i8s, y <- yw16s]
++ [(show x, show y, "shr_i8_w16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i8s, y <- yw16s]
++ [(show x, show y, "shl_i16_w8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i16s, y <- w8s]
++ [(show x, show y, "shr_i16_w8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i16s, y <- w8s]
where yi16s :: [Int16]
yi16s = [0, 255, 256, 257, maxBound]
yw16s :: [Word16]
yw16s = [0, 255, 256, 257, maxBound]
mkTest (x, y, l, t) = testCase ("genShiftMixSize." ++ l ++ "." ++ x ++ "_" ++ y) (assert t)
mk :: (Eq a, Eq b, SymVal a, SymVal b) => (SBV a -> SBV b -> SBV a) -> a -> b -> a -> IO Bool
mk o x y r
= isTheorem $ do a <- free "x"
b <- free "y"
constrain $ a .== literal x
constrain $ b .== literal y
return $ literal r .== a `o` b
genBlasts :: [TestTree]
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) = testCase ("genBlasts.blast-" ++ show x) (assert t)
mkThm from to v = isTheorem $ do a <- free "x"
constrain $ a .== literal v
return $ a .== from (to a)
genCounts :: [TestTree]
genCounts = map mkTest $ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord8 ) blastBE x) | x <- w8s ]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord8 ) blastLE x) | x <- w8s ]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt8 ) blastBE x) | x <- i8s ]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt8 ) blastLE x) | x <- i8s ]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord16) blastBE x) | x <- w16s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord16) blastLE x) | x <- w16s]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt16 ) blastBE x) | x <- i16s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt16 ) blastLE x) | x <- i16s]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord32) blastBE x) | x <- w32s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord32) blastLE x) | x <- w32s]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt32 ) blastBE x) | x <- i32s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt32 ) blastLE x) | x <- i32s]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord64) blastBE x) | x <- w64s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord64) blastLE x) | x <- w64s]
++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt64 ) blastBE x) | x <- i64s]
++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt64 ) blastLE x) | x <- i64s]
where mkTest (x, t) = testCase ("genCounts.count-" ++ show x) (assert t)
mkThm from to v = isTheorem $ do a <- free "x"
constrain $ a .== literal v
return $ sCountTrailingZeros a .== sCountLeadingZeros (from (to a))
genIntCasts :: [TestTree]
genIntCasts = map mkTest $ cast w8s ++ cast w16s ++ cast w32s ++ cast w64s
++ cast i8s ++ cast i16s ++ cast i32s ++ cast i64s
++ cast iUBs
where mkTest (x, t) = testCase ("sIntCast-" ++ x) (assert t)
cast :: forall a. (Show a, Integral a, SymVal a) => [a] -> [(String, IO Bool)]
cast xs = toWords xs ++ toInts xs
toWords xs = [(show x, mkThm x (fromIntegral x :: Word8 )) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Word16)) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Word32)) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Word64)) | x <- xs]
toInts xs = [(show x, mkThm x (fromIntegral x :: Int8 )) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Int16)) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Int32)) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Int64)) | x <- xs]
++ [(show x, mkThm x (fromIntegral x :: Integer)) | x <- xs]
mkThm v res = isTheorem $ do a <- free "x"
constrain $ a .== literal v
return $ literal res .== sFromIntegral a
genReals :: [TestTree]
genReals = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- ars, y <- ars ]
++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- ars, y <- ars ]
++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- ars, y <- ars ]
++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- ars, y <- ars, y /= 0]
++ [("<", show x, show y, mkThm2 (.<) x y (x < y)) | x <- ars, y <- ars ]
++ [("<=", show x, show y, mkThm2 (.<=) x y (x <= y)) | x <- ars, y <- ars ]
++ [(">", show x, show y, mkThm2 (.>) x y (x > y)) | x <- ars, y <- ars ]
++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- ars, y <- ars ]
++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- ars, y <- ars ]
++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- ars, y <- ars ]
where mkTest (nm, x, y, t) = testCase ("genReals.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
genFloats :: [TestTree]
genFloats = genIEEE754 "genFloats" fs
genDoubles :: [TestTree]
genDoubles = genIEEE754 "genDoubles" ds
genIEEE754 :: (IEEEFloating a, OrdSymbolic (SBV a), Num (SBV a), Show a) => String -> [a] -> [TestTree]
genIEEE754 origin vs = [tst1 ("pred_" ++ nm, x, y) | (nm, x, y) <- preds]
++ [tst1 ("unary_" ++ nm, x, y) | (nm, x, y) <- uns]
++ [tst2 ("binary_" ++ nm, x, y, r) | (nm, x, y, r) <- bins]
where uns = [("abs", show x, mkThm1 abs x (abs x)) | x <- vs]
++ [("negate", show x, mkThm1 negate x (negate x)) | x <- vs]
++ [("signum", show x, mkThm1 signum x (signum x)) | x <- vs]
++ [("fpAbs", show x, mkThm1 fpAbs x (abs x)) | x <- vs]
++ [("fpNeg", show x, mkThm1 fpNeg x (negate x)) | x <- vs]
++ [("fpSqrt", show x, mkThm1 (m fpSqrt) x (sqrt x)) | x <- vs]
++ [("fpRoundToIntegral", show x, mkThm1 (m fpRoundToIntegral) x (fpRoundToIntegralH x)) | x <- vs]
bins = [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- vs, y <- vs]
++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- vs, y <- vs]
++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- vs, y <- vs]
++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- vs, y <- vs]
++ [("<", show x, show y, mkThm2C False (.<) x y (x < y)) | x <- vs, y <- vs]
++ [("<=", show x, show y, mkThm2C False (.<=) x y (x <= y)) | x <- vs, y <- vs]
++ [(">", show x, show y, mkThm2C False (.>) x y (x > y)) | x <- vs, y <- vs]
++ [(">=", show x, show y, mkThm2C False (.>=) x y (x >= y)) | x <- vs, y <- vs]
++ [("==", show x, show y, mkThm2C False (.==) x y (x == y)) | x <- vs, y <- vs]
++ [("/=", show x, show y, mkThm2C True (./=) x y (x /= y)) | x <- vs, y <- vs]
-- TODO. Can't possibly test fma, unless we FFI out to C. Leave it out for the time being
++ [("fpAdd", show x, show y, mkThm2 (m fpAdd) x y ((+) x y)) | x <- vs, y <- vs]
++ [("fpSub", show x, show y, mkThm2 (m fpSub) x y ((-) x y)) | x <- vs, y <- vs]
++ [("fpMul", show x, show y, mkThm2 (m fpMul) x y ((*) x y)) | x <- vs, y <- vs]
++ [("fpDiv", show x, show y, mkThm2 (m fpDiv) x y ((/) x y)) | x <- vs, y <- vs]
++ [("fpMin", show x, show y, mkThm2 fpMin x y (fpMinH x y)) | x <- vs, y <- vs, not (alt0 x y || alt0 y x)]
++ [("fpMax", show x, show y, mkThm2 fpMax x y (fpMaxH x y)) | x <- vs, y <- vs, not (alt0 x y || alt0 y x)]
++ [("fpIsEqualObject", show x, show y, mkThm2P fpIsEqualObject x y (fpIsEqualObjectH x y)) | x <- vs, y <- vs]
++ [("fpRem", show x, show y, mkThm2 fpRem x y (fpRemH x y)) | x <- vsFPRem, y <- vsFPRem]
-- TODO: For doubles fpRem takes too long, so we only do a subset
vsFPRem
| origin == "genDoubles" = [nan, infinity, 0, 0.5, -infinity, -0, -0.5]
| True = vs
-- fpMin/fpMax: skip +0/-0 case as this is underspecified
alt0 x y = isNegativeZero x && y == 0 && not (isNegativeZero y)
m f = f sRNE
preds = [(pn, show x, mkThmP ps x (pc x)) | (pn, ps, pc) <- predicates, x <- vs]
tst2 (nm, x, y, t) = testCase (origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t)
tst1 (nm, x, t) = testCase (origin ++ ".arithmetic-" ++ nm ++ "." ++ x) (assert t)
eqF v val
| isNaN val = constrain $ fpIsNaN v
| isNegativeZero val = constrain $ fpIsNegativeZero v
| val == 0 = constrain $ fpIsPositiveZero v
| isInfinite val && val > 0 = constrain $ fpIsInfinite v .&& fpIsPositive v
| isInfinite val && val < 0 = constrain $ fpIsInfinite v .&& fpIsNegative v
| True = constrain $ v .== literal val
-- Quickly pick which solver to use. Currently z3 or mathSAT supports FP
fpProver :: SMTConfig
fpProver = z3 -- mathSAT
fpThm = isTheoremWith fpProver
mkThmP op x r = fpThm $ do a <- free "x"
eqF a x
return $ literal r .== op a
mkThm2P op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"]
eqF a x
eqF b y
return $ literal r .== a `op` b
mkThm1 op x r = fpThm $ do a <- free "x"
eqF a x
return $ literal r `fpIsEqualObject` op a
mkThm2 op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"]
eqF a x
eqF b y
return $ literal r `fpIsEqualObject` (a `op` b)
mkThm2C neq op x y r = fpThm $ do [a, b] <- mapM free ["x", "y"]
eqF a x
eqF b y
return $ if isNaN x || isNaN y
then (if neq then a `op` b else sNot (a `op` b))
else literal r .== a `op` b
predicates :: (IEEEFloating a) => [(String, SBV a -> SBool, a -> Bool)]
predicates = [ ("fpIsNormal", fpIsNormal, fpIsNormalizedH)
, ("fpIsSubnormal", fpIsSubnormal, isDenormalized)
, ("fpIsZero", fpIsZero, (== 0))
, ("fpIsInfinite", fpIsInfinite, isInfinite)
, ("fpIsNaN", fpIsNaN, isNaN)
, ("fpIsNegative", fpIsNegative, \x -> x < 0 || isNegativeZero x)
, ("fpIsPositive", fpIsPositive, \x -> x >= 0 && not (isNegativeZero x))
, ("fpIsNegativeZero", fpIsNegativeZero, isNegativeZero)
, ("fpIsPositiveZero", fpIsPositiveZero, \x -> x == 0 && not (isNegativeZero x))
, ("fpIsPoint", fpIsPoint, \x -> not (isNaN x || isInfinite x))
]
genFPConverts :: [TestTree]
genFPConverts = [tst1 ("fpCast_" ++ nm, x, y) | (nm, x, y) <- converts]
where converts = [("toFP_Int8_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i8s ]
++ [("toFP_Int16_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i16s]
++ [("toFP_Int32_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i32s]
++ [("toFP_Int64_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- i64s]
++ [("toFP_Word8_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- w8s ]
++ [("toFP_Word16_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- w16s]
++ [("toFP_Word32_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- w32s]
++ [("toFP_Word64_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- w64s]
++ [("toFP_Float_ToFloat", show x, mkThm1 (m toSFloat) x x ) | x <- fs ]
++ [("toFP_Double_ToFloat", show x, mkThm1 (m toSFloat) x ( fp2fp x )) | x <- ds ]
++ [("toFP_Integer_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- iUBs]
++ [("toFP_Real_ToFloat", show x, mkThmC (m toSFloat) x (fromRational (toRational x))) | x <- ars ]
++ [("toFP_Int8_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- i8s ]
++ [("toFP_Int16_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- i16s]
++ [("toFP_Int32_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- i32s]
++ [("toFP_Int64_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- i64s]
++ [("toFP_Word8_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- w8s ]
++ [("toFP_Word16_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- w16s]
++ [("toFP_Word32_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- w32s]
++ [("toFP_Word64_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- w64s]
++ [("toFP_Float_ToDouble", show x, mkThm1 (m toSDouble) x ( fp2fp x )) | x <- fs ]
++ [("toFP_Double_ToDouble", show x, mkThm1 (m toSDouble) x x ) | x <- ds ]
++ [("toFP_Integer_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- iUBs]
++ [("toFP_Real_ToDouble", show x, mkThmC (m toSDouble) x (fromRational (toRational x))) | x <- ars ]
-- Conversions from floats are only well-defined if the input is in-bounds. So we just check round-trip for these.
-- Also note that we clamp Int32/Word32/Int64/Word64 conversions further as floats become too sparse to handle those.
++ [("fromFP_Float_ToInt8", show x, mkThmC' (m fromSFloat :: SFloat -> SInt8) x ((round :: Float -> Int8 ) x)) | i <- i8s, let x = fromIntegral i]
++ [("fromFP_Float_ToInt16", show x, mkThmC' (m fromSFloat :: SFloat -> SInt16) x ((round :: Float -> Int16 ) x)) | i <- i16s, let x = fromIntegral i]
++ [("fromFP_Float_ToInt32", show x, mkThmC' (m fromSFloat :: SFloat -> SInt32) x ((round :: Float -> Int32 ) x)) | i <- i16s, let x = fromIntegral i]
++ [("fromFP_Float_ToInt64", show x, mkThmC' (m fromSFloat :: SFloat -> SInt64) x ((round :: Float -> Int64 ) x)) | i <- i16s, let x = fromIntegral i]
++ [("fromFP_Float_ToWord8", show x, mkThmC' (m fromSFloat :: SFloat -> SWord8) x ((round :: Float -> Word8 ) x)) | i <- w8s, let x = fromIntegral i]
++ [("fromFP_Float_ToWord16", show x, mkThmC' (m fromSFloat :: SFloat -> SWord16) x ((round :: Float -> Word16) x)) | i <- w16s, let x = fromIntegral i]
++ [("fromFP_Float_ToWord32", show x, mkThmC' (m fromSFloat :: SFloat -> SWord32) x ((round :: Float -> Word32) x)) | i <- w16s, let x = fromIntegral i]
++ [("fromFP_Float_ToWord64", show x, mkThmC' (m fromSFloat :: SFloat -> SWord64) x ((round :: Float -> Word64) x)) | i <- w16s, let x = fromIntegral i]
++ [("fromFP_Float_ToFloat", show x, mkThm1 (m fromSFloat :: SFloat -> SFloat) x x) | x <- fs]
++ [("fromFP_Float_ToDouble", show x, mkThm1 (m fromSFloat :: SFloat -> SDouble) x ( fp2fp x)) | x <- fs]
-- Neither Z3 nor MathSAT support Float->Integer/Float->Real conversion for the time being; so we skip those. See GitHub issue: #191
-- Conversions from doubles are only well-defined if the input is in-bounds. So we just check round-trip for these.
-- Also note that we clamp Int64/Word64 conversions further as floats become too sparse to handle those.
++ [("fromFP_Double_ToInt8", show x, mkThmC' (m fromSDouble :: SDouble -> SInt8) x ((round :: Double -> Int8 ) x)) | i <- i8s, let x = fromIntegral i]
++ [("fromFP_Double_ToInt16", show x, mkThmC' (m fromSDouble :: SDouble -> SInt16) x ((round :: Double -> Int16 ) x)) | i <- i16s, let x = fromIntegral i]
++ [("fromFP_Double_ToInt32", show x, mkThmC' (m fromSDouble :: SDouble -> SInt32) x ((round :: Double -> Int32 ) x)) | i <- i32s, let x = fromIntegral i]
++ [("fromFP_Double_ToInt64", show x, mkThmC' (m fromSDouble :: SDouble -> SInt64) x ((round :: Double -> Int64 ) x)) | i <- i32s, let x = fromIntegral i]
++ [("fromFP_Double_ToWord8", show x, mkThmC' (m fromSDouble :: SDouble -> SWord8) x ((round :: Double -> Word8 ) x)) | i <- w8s, let x = fromIntegral i]
++ [("fromFP_Double_ToWord16", show x, mkThmC' (m fromSDouble :: SDouble -> SWord16) x ((round :: Double -> Word16) x)) | i <- w16s, let x = fromIntegral i]
++ [("fromFP_Double_ToWord32", show x, mkThmC' (m fromSDouble :: SDouble -> SWord32) x ((round :: Double -> Word32) x)) | i <- w32s, let x = fromIntegral i]
++ [("fromFP_Double_ToWord64", show x, mkThmC' (m fromSDouble :: SDouble -> SWord64) x ((round :: Double -> Word64) x)) | i <- w32s, let x = fromIntegral i]
++ [("fromFP_Double_ToFloat", show x, mkThm1 (m fromSDouble :: SDouble -> SFloat) x ( fp2fp x)) | x <- ds]
++ [("fromFP_Double_ToDouble", show x, mkThm1 (m fromSDouble :: SDouble -> SDouble) x x ) | x <- ds]
-- Neither Z3 nor MathSAT support Double->Integer/Double->Real conversion for the time being; so we skip those. See GitHub issue: #191
++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (wordToFloat x)) | x <- w32s]
++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (wordToDouble x)) | x <- w64s]
++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN
++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN
m f = f sRNE
tst1 (nm, x, t) = testCase ("fpConverts.arithmetic-" ++ nm ++ "." ++ x) (assert t)
eqF v val
| isNaN val = constrain $ fpIsNaN v
| isNegativeZero val = constrain $ fpIsNegativeZero v
| val == 0 = constrain $ fpIsPositiveZero v
| isInfinite val && val > 0 = constrain $ fpIsInfinite v .&& fpIsPositive v
| isInfinite val && val < 0 = constrain $ fpIsInfinite v .&& fpIsNegative v
| True = constrain $ v .== literal val
-- Quickly pick which solver to use. Currently z3 or mathSAT supports FP
fpProver :: SMTConfig
fpProver = z3 -- mathSAT
fpThm = isTheoremWith fpProver
mkThmP op x r = fpThm $ do a <- free "x"
eqF a x
return $ literal r .== op a
mkThm1 op x r = fpThm $ do a <- free "x"
eqF a x
return $ literal r `fpIsEqualObject` op a
mkThmC op x r = fpThm $ do a <- free "x"
constrain $ a .== literal x
return $ literal r `fpIsEqualObject` op a
mkThmC' op x r = fpThm $ do a <- free "x"
eqF a x
return $ literal r .== op a
genQRems :: [TestTree]
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) = testCase ("genQRems.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)
genChars :: [TestTree]
genChars = [ testCase "solver_genChars" (assert (isTheorem t)) ]
where t = do a <- free "a"
i <- free "i"
let chk sop cop v = (a .== literal v) .=> sop a .== literal (cop v)
chkI sop cop v = (i .== literal v) .=> sop i .== literal (cop v)
pure $ sAnd $ [chk SC.ord cord c | c <- cs]
++ [chk SC.toLowerL1 C.toLower c | c <- cs]
++ [chk SC.toUpperL1 C.toUpper c | c <- cs]
++ [chk SC.digitToInt dig2Int c | c <- cs, digitToIntRange c]
++ [chkI SC.intToDigit int2Dig c | c <- [0 .. 15]]
++ [chk SC.isControlL1 C.isControl c | c <- cs]
++ [chk SC.isSpaceL1 C.isSpace c | c <- cs]
++ [chk SC.isLowerL1 C.isLower c | c <- cs]
++ [chk SC.isUpperL1 C.isUpper c | c <- cs]
++ [chk SC.isAlphaL1 C.isAlpha c | c <- cs]
++ [chk SC.isAlphaNumL1 C.isAlphaNum c | c <- cs]
++ [chk SC.isPrintL1 C.isPrint c | c <- cs]
++ [chk SC.isDigit C.isDigit c | c <- cs]
++ [chk SC.isOctDigit C.isOctDigit c | c <- cs]
++ [chk SC.isHexDigit C.isHexDigit c | c <- cs]
++ [chk SC.isLetterL1 C.isLetter c | c <- cs]
++ [chk SC.isMarkL1 C.isMark c | c <- cs]
++ [chk SC.isNumberL1 C.isNumber c | c <- cs]
++ [chk SC.isPunctuationL1 C.isPunctuation c | c <- cs]
++ [chk SC.isSymbolL1 C.isSymbol c | c <- cs]
++ [chk SC.isSeparatorL1 C.isSeparator c | c <- cs]
++ [chk SC.isAscii C.isAscii c | c <- cs]
++ [chk SC.isLatin1 C.isLatin1 c | c <- cs]
++ [chk SC.isAsciiUpper C.isAsciiUpper c | c <- cs]
++ [chk SC.isAsciiLower C.isAsciiLower c | c <- cs]
digitToIntRange = (`elem` "0123456789abcdefABCDEF")
cord :: Char -> Integer
cord = fromIntegral . C.ord
dig2Int :: Char -> Integer
dig2Int = fromIntegral . C.digitToInt
int2Dig :: Integer -> Char
int2Dig = C.intToDigit . fromIntegral
genStrings :: [TestTree]
genStrings = map mkTest1 ( [("length", show s, mkThm1 SL.length strLen s ) | s <- ss ]
++ [("null", show s, mkThm1 SL.null null s ) | s <- ss ]
++ [("head", show s, mkThm1 SL.head head s ) | s <- ss, not (null s) ]
++ [("tail", show s, mkThm1 SL.tail tail s ) | s <- ss, not (null s) ]
++ [("singleton", show c, mkThm1 SL.singleton (: []) c ) | c <- cs ]
++ [("implode", show s, mkThmI SL.implode s ) | s <- ss ]
++ [("strToNat", show s, mkThm1 SL.strToNat strToNat s ) | s <- ss ]
++ [("natToStr", show i, mkThm1 SL.natToStr natToStr i ) | i <- iUBs ])
++ map mkTest2 ( [("strToCharAt", show s, show i, mkThm2 SL.elemAt strToCharAt s i ) | s <- ss, i <- range s ]
++ [("++", show s, show s1, mkThm2 (SL.++) (++) s s1 ) | s <- ss, s1 <- ss ]
++ [("isInfixOf", show s, show s1, mkThm2 SL.isInfixOf isInfixOf s s1 ) | s <- ss, s1 <- ss ]
++ [("isSuffixOf", show s, show s1, mkThm2 SL.isSuffixOf isSuffixOf s s1 ) | s <- ss, s1 <- ss ]
++ [("isPrefixOf", show s, show s1, mkThm2 SL.isPrefixOf isPrefixOf s s1 ) | s <- ss, s1 <- ss ]
++ [("take", show s, show i, mkThm2 SL.take genericTake i s ) | s <- ss, i <- iUBs ]
++ [("drop", show s, show i, mkThm2 SL.drop genericDrop i s ) | s <- ss, i <- iUBs ]
++ [("indexOf", show s, show s1, mkThm2 SL.indexOf indexOf s s1 ) | s <- ss, s1 <- ss ])
++ map mkTest3 ( [("subStr", show s, show i, show j, mkThm3 SL.subList subStr s i j ) | s <- ss, i <- range s, j <- range s, i + j <= genericLength s]
++ [("replace", show s, show s1, show s2, mkThm3 SL.replace replace s s1 s2) | s <- ss, s1 <- ss, s2 <- ss ]
++ [("offsetIndexOf", show s, show s1, show i, mkThm3 SL.offsetIndexOf offsetIndexOf s s1 i ) | s <- ss, s1 <- ss, i <- range s ])
where strLen :: String -> Integer
strLen = fromIntegral . length
strToNat :: String -> Integer
strToNat s
| all C.isDigit s && not (null s) = read s
| True = -1
natToStr :: Integer -> String
natToStr i
| i >= 0 = show i
| True = ""
range :: String -> [Integer]
range s = map fromIntegral [0 .. length s - 1]
indexOf :: String -> String -> Integer
indexOf s1 s2 = go 0 s1
where go i x
| s2 `isPrefixOf` x = i
| True = case x of
"" -> -1
(_:r) -> go (i+1) r
strToCharAt :: String -> Integer -> Char
s `strToCharAt` i = s `genericIndex` i
subStr :: String -> Integer -> Integer -> String
subStr s i j = genericTake j (genericDrop i s)
replace :: String -> String -> String -> String
replace s "" y = y ++ s
replace s x y = go s
where go "" = ""
go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h
| True = c : go rest
offsetIndexOf :: String -> String -> Integer -> Integer
offsetIndexOf x y i = case indexOf (genericDrop i x) y of
-1 -> -1
r -> r+i
mkTest1 (nm, x, t) = testCase ("genStrings-" ++ nm ++ "." ++ x) (assert t)
mkTest2 (nm, x, y, t) = testCase ("genStrings-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t)
mkTest3 (nm, x, y, z, t) = testCase ("genStrings-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t)
mkThmI sop s = isTheorem $ do let v c = do sc <- free_
constrain $ sc .== literal c
return sc
vs <- mapM v s
return $ literal s .== sop vs
mkThm1 sop cop arg = isTheorem $ do a <- free "a"
constrain $ a .== literal arg
return $ literal (cop arg) .== sop a
mkThm2 sop cop arg1 arg2 = isTheorem $ do a <- free "a"
b <- free "b"
constrain $ a .== literal arg1
constrain $ b .== literal arg2
return $ literal (cop arg1 arg2) .== sop a b
mkThm3 sop cop arg1 arg2 arg3 = isTheorem $ do a <- free "a"
b <- free "b"
c <- free "c"
constrain $ a .== literal arg1
constrain $ b .== literal arg2
constrain $ c .== literal arg3
return $ literal (cop arg1 arg2 arg3) .== sop a b c
genLists :: [TestTree]
genLists = map mkTest1 ( [("length", show l, mkThm1 SL.length llen l ) | l <- sl ]
++ [("null", show l, mkThm1 SL.null null l ) | l <- sl ]
++ [("head", show l, mkThm1 SL.head head l ) | l <- sl, not (null l) ]
++ [("tail", show l, mkThm1 SL.tail tail l ) | l <- sl, not (null l) ]
++ [("singleton", show i, mkThm1 SL.singleton (: []) i ) | i <- iUBs ]
++ [("implode", show l, mkThmI SL.implode id l ) | l <- sl ]
++ [("concat", show l, mkThm1 SL.concat concat l ) | l <- sll ]
)
++ map mkTest2 ( [("listToListAt", show l, show i, mkThm2 SL.listToListAt listToListAt l i ) | l <- sl, i <- range l ]
++ [("elemAt", show l, show i, mkThm2 SL.elemAt elemAt l i ) | l <- sl, i <- range l ]
++ [("append", show l, show l1, mkThm2 (SL.++) (++) l l1 ) | l <- sl, l1 <- sl ]
++ [("isInfixOf", show l, show l1, mkThm2 SL.isInfixOf isInfixOf l l1 ) | l <- sl, l1 <- sl ]
++ [("isSuffixOf", show l, show l1, mkThm2 SL.isSuffixOf isSuffixOf l l1 ) | l <- sl, l1 <- sl ]
++ [("isPrefixOf", show l, show l1, mkThm2 SL.isPrefixOf isPrefixOf l l1 ) | l <- sl, l1 <- sl ]
++ [("take", show l, show i, mkThm2 SL.take genericTake i l ) | l <- sl, i <- iUBs ]
++ [("drop", show l, show i, mkThm2 SL.drop genericDrop i l ) | l <- sl, i <- iUBs ]
++ [("indexOf", show l, show l1, mkThm2 SL.indexOf indexOf l l1 ) | l <- sl, l1 <- sl ]
)
++ map mkTest3 ( [("subList", show l, show i, show j, mkThm3 SL.subList subList l i j ) | l <- sl, i <- range l, j <- range l, i + j <= genericLength l]
++ [("replace", show l, show l1, show l2, mkThm3 SL.replace replace l l1 l2) | l <- sl, l1 <- sl, l2 <- sl ]
++ [("offsetIndexOf", show l, show l1, show i, mkThm3 SL.offsetIndexOf offsetIndexOf l l1 i ) | l <- sl, l1 <- sl, i <- range l ]
)
where llen :: [Integer] -> Integer
llen = fromIntegral . length
range :: [Integer] -> [Integer]
range l = map fromIntegral [0 .. length l - 1]
indexOf :: [Integer] -> [Integer] -> Integer
indexOf s1 s2 = go 0 s1
where go i x
| s2 `isPrefixOf` x = i
| True = case x of
[] -> -1
(_:r) -> go (i+1) r
listToListAt :: [Integer] -> Integer -> [Integer]
s `listToListAt` i = [s `elemAt` i]
elemAt :: [Integer] -> Integer -> Integer
l `elemAt` i = l `genericIndex` i
subList :: [Integer] -> Integer -> Integer -> [Integer]
subList s i j = genericTake j (genericDrop i s)
replace :: [Integer] -> [Integer] -> [Integer] -> [Integer]
replace s [] y = y ++ s
replace s x y = go s
where go [] = []
go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h
| True = c : go rest
offsetIndexOf :: [Integer] -> [Integer] -> Integer -> Integer
offsetIndexOf x y i = case indexOf (genericDrop i x) y of
-1 -> -1
r -> r+i
mkTest1 (nm, x, t) = testCase ("genLists-" ++ nm ++ "." ++ x) (assert t)
mkTest2 (nm, x, y, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t)
mkTest3 (nm, x, y, z, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t)
mkThmI sop cop arg = isTheorem $ do let v c = do sc <- free_
constrain $ sc .== literal c
return sc
vs <- mapM v arg
return $ literal (cop arg) .== sop vs
mkThm1 sop cop arg = isTheorem $ do a <- free "a"
constrain $ a .== literal arg
return $ literal (cop arg) .== sop a
mkThm2 sop cop arg1 arg2 = isTheorem $ do a <- free "a"
b <- free "b"
constrain $ a .== literal arg1
constrain $ b .== literal arg2
return $ literal (cop arg1 arg2) .== sop a b
mkThm3 sop cop arg1 arg2 arg3 = isTheorem $ do a <- free "a"
b <- free "b"
c <- free "c"
constrain $ a .== literal arg1
constrain $ b .== literal arg2
constrain $ c .== literal arg3
return $ literal (cop arg1 arg2 arg3) .== sop a b c
-- Concrete test data
xsSigned, xsUnsigned :: (Num a, Bounded a) => [a]
xsUnsigned = [0, 1, maxBound - 1, maxBound]
xsSigned = xsUnsigned ++ [minBound, minBound + 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
wn8s :: [WordN 8]
wn8s = xsUnsigned
in8s :: [IntN 8]
in8s = xsSigned
iUBs :: [Integer]
iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000]
ars :: [AlgReal]
ars = map fromRational rs
rs :: [Ratio Integer]
rs = [i % d | i <- is, d <- dens]
where is = [-1000000] ++ [-1 .. 1] ++ [1000001]
dens = [5,100,1000000]
-- Admittedly paltry test-cases for float/double
fs :: [Float]
fs = xs ++ map (* (-1)) (filter (not . isNaN) xs) -- -nan is the same as nan
where xs = [nan, infinity, 0, 0.5, 0.68302244, 0.5268265, 0.10283524, 5.8336496e-2, 1.0e-45]
ds :: [Double]
ds = xs ++ map (* (-1)) (filter (not . isNaN) xs) -- -nan is the same as nan
where xs = [nan, infinity, 0, 0.5, 2.516632060108026e-2, 0.8601891300751106, 5.0e-324]
-- Currently we test over all latin-1 characters. Maybe we should add some unicode when the
-- underlying operation is supported. Oh well.
cs :: String
cs = map C.chr [0..255]
-- For pair char ops, take a subset.
reducedCS :: String
reducedCS = map C.chr $ [0..5] ++ [98..102] ++ [250..255]
-- Ditto for strings, just a few things
ss :: [String]
ss = ["", "palTRY", "teSTing", "SBV", "sTRIngs", "123", "surely", "thIS", "hI", "ly", "0"]
-- Lists are the worst in coverage!
sl :: [[Integer]]
sl = [[], [0], [-1, 1], [-10, 0, 10], [3, 4, 5, 4, 5, 3]]
-- List of lists are similarly inadequate
sll :: [[[Integer]]]
sll = [[x, x, x] | x <- [[], [0], [-1, 1], [-10, 0, 10], [3, 4, 5, 4, 5, 3]]]
-- Ditto for maybe, either and tuple
sm :: [Maybe Integer]
sm = [Nothing, Just (-5), Just 0, Just 5]
se :: [Either Integer Integer]
se = [Left 3, Right 5]
st :: [(Integer, Integer)]
st = [(1, 2), (-1, -5), (0, 9), (5, 5)]
misc :: [TestTree]
misc = [ testCase "misc-t1" $ assertIsSat t1
]
where -- https://stackoverflow.com/questions/69033969/trivial-rationals-problems-without-variables-in-sbv-solver-in-haskell
t1 = do _xs <- sRationals []
constrain $ (5.%1:: SRational) .<= (5.%1:: SRational)
-- Test these with make test TGT=sEnum_
genEnums :: [TestTree]
genEnums =
-- Only bounded for from, otherwise infinite (or too big for chars)
[mkTest1 "from" s (from [s.. ] s) | s <- univ @(WordN 4)]
++ [mkTest1 "from" s (from [s.. ] s) | s <- univ @(IntN 4)]
++ [mkTest1 "from" s (from [s.. ] s) | s <- univ @Day]
++ [mkTest1 "from" s (from [s.. ] s) | s <- w8s]
++ [mkTest1 "from" s (from [s.. ] s) | s <- i8s]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- univ @(WordN 4), t <- univ @(WordN 4)]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- univ @(IntN 4), t <- univ @(IntN 4)]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- univ @Day , t <- univ @Day ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- w8s , t <- w8s ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- i8s , t <- i8s ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- ints , t <- ints ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- floats , t <- floats ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- doubles , t <- doubles ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- fps , t <- fps ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- lcs , t <- lcs ]
++ [mkTest2 "fromTo" s t (fromTo [s..t ] s t) | s <- rrs , t <- rrs ]
-- Only bounded for fromThen, otherwise infinite (or too big for chars)
++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- univ @(WordN 4), t <- univ @(WordN 4), s /= t]
++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- univ @(IntN 4), t <- univ @(IntN 4), s /= t]
++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- univ @Day , t <- univ @Day , s /= t]
++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- w8s , t <- w8s , s /= t]
++ [mkTest2 "fromThen" s t (fromThen [s, t.. ] s t) | s <- i8s , t <- i8s , s /= t]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- univ @(WordN 4), t <- univ @(WordN 4), s /= t, u <- univ @(WordN 4)]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- univ @(IntN 4), t <- univ @(IntN 4), s /= t, u <- univ @(IntN 4)]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- univ @Day , t <- univ @Day , s /= t, u <- univ @Day ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- w8s , t <- w8s , s /= t, u <- w8s ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- i8s , t <- i8s , s /= t, u <- i8s ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- ints , t <- ints , s /= t, u <- ints ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- floats , t <- floats , s /= t, u <- floats ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- doubles , t <- doubles , s /= t, u <- doubles ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- fps , t <- fps , s /= t, u <- fps ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- lcs , t <- lcs , s /= t, u <- lcs ]
++ [mkTest3 "fromThenTo" s t u (fromThenTo [s, t..u] s t u) | s <- rrs , t <- rrs , s /= t, u <- rrs ]
where mkTest1 pre a = testCase ("sEnum_" ++ pre ++ "_|" ++ show (kindOf a) ++ "|_" ++ show a)
mkTest2 pre a b = testCase ("sEnum_" ++ pre ++ "_|" ++ show (kindOf a) ++ "|_" ++ show (a, b))
mkTest3 pre a b c = testCase ("sEnum_" ++ pre ++ "_|" ++ show (kindOf a) ++ "|_" ++ show (a, b, c))
from cr a1 = assert $ isTheorem $ do
sa1 <- free_
constrain $ sa1 .== literal a1
pure $ [sEnum|sa1..|] .== literal cr
fromTo cr a1 a2 = assert $ isTheorem $ do
sa1 <- free_
constrain $ sa1 .== literal a1
sa2 <- free_
constrain $ sa2 .== literal a2
pure $ [sEnum|sa1..sa2|] .== literal cr
fromThen cr a1 a2 = assert $ isTheorem $ do
sa1 <- free_
constrain $ sa1 .== literal a1
sa2 <- free_
constrain $ sa2 .== literal a2
pure $ [sEnum|sa1, sa2 ..|] .== literal cr
fromThenTo cr a1 a2 a3 = assert $ isTheorem $ do
sa1 <- free_
constrain $ sa1 .== literal a1
sa2 <- free_
constrain $ sa2 .== literal a2
sa3 <- free_
constrain $ sa3 .== literal a3
pure $ [sEnum|sa1, sa2 .. sa3|] .== literal cr
univ :: (Enum n, Bounded n) => [n]
univ = [minBound .. maxBound]
ints :: [Integer]
ints = [-3 .. 3]
-- Floats create too big a problem for z3, even though we have ground terms. So, skip
floats :: [Float]
-- floats = [-3.4, -3.2 .. 3.5]
floats = []
-- Ditto here
doubles :: [Double]
-- doubles = [-3.4, -3.2 .. 3.5]
doubles = []
-- NB. Precision here is important. If you pick too small of a significand
-- size then you can turn this enumeration into an infinite list, busting the tests.
fps :: [FloatingPoint 5 8]
-- fps = [-3.4, -3.2 .. 3.5]
fps = []
-- This one works, but is way too slow. So we further reduce the range
rrs :: [AlgReal]
-- rrs = [-3.4, -3.2 .. 3.5]
rrs = [-0.4, -0.2 .. 0.4]
-- don't add min/max bounds here. causes too big lists.
lcs :: [Char]
lcs = map C.chr [5, 10, 30, 40, 41, 42, 43, 90, 100]
-- Quiet GHC about unused enum elts
_unused :: SDay
_unused = undefined sMon sTue sWed sThu sFri sSat sSun
isMon isTue isWed isThu isFri isSat isSun
(sCaseDay @SInteger)
{- HLint ignore module "Reduce duplication" -}