grisette-0.9.0.0: test/Grisette/SymPrim/SymPrimTests.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NegativeLiterals #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Grisette.SymPrim.SymPrimTests (symPrimTests) where
import Control.DeepSeq (NFData (rnf), force)
import Control.Exception
( ArithException (DivideByZero, Overflow, Underflow),
catch,
evaluate,
)
import Control.Monad.Except (ExceptT, MonadError (throwError), runExceptT)
import Data.Bits
( Bits
( bit,
bitSizeMaybe,
complement,
isSigned,
popCount,
rotate,
shift,
testBit,
xor,
(.&.),
(.|.)
),
)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Int (Int8)
import Data.Proxy (Proxy (Proxy))
import Data.Word (Word8)
import Grisette
( AlgReal,
Apply (apply),
BV (bv),
EvalSym (evalSym),
ExtractSym (extractSym),
FP,
FP32,
FPRoundingMode,
Function ((#)),
IEEEFPConstants (fpNaN),
IEEEFPConvertible (fromFPOr),
ITEOp (symIte),
LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),
Mergeable (rootStrategy),
MergingStrategy (SimpleStrategy),
ModelOps (emptyModel, insertValue),
ModelRep (buildModel),
SafeDiv
( safeDiv,
safeDivMod,
safeMod,
safeQuot,
safeQuotRem,
safeRem
),
SafeLinearArith
( safeAdd,
safeNeg,
safeSub
),
SimpleMergeable (mrgIte),
SizedBV
( sizedBVConcat,
sizedBVExt,
sizedBVSelect,
sizedBVSext,
sizedBVZext
),
Solvable (con, conView, isym, ssym),
SolvingFailure (Unsat),
SomeSymIntN,
SomeSymWordN,
SymEq ((./=), (.==)),
SymFP,
SymFPRoundingMode,
SymIEEEFPTraits (symFpIsNaN),
SymIntN32,
SymOrd (symCompare, (.<), (.<=), (.>), (.>=)),
SymWordN32,
ToCon (toCon),
ToSym (toSym),
TypedAnySymbol,
Union,
bitCastOrCanonical,
genSym,
genSymSimple,
mrgIf,
mrgSingle,
simpleMerge,
solve,
tryMerge,
z3,
pattern Con,
pattern SomeSymIntN,
pattern SomeSymWordN,
type (-->),
type (=->),
)
import Grisette.Internal.Core.Data.Class.SafeFromFP (SafeFromFP (safeFromFP))
import Grisette.Internal.SymPrim.BV
( IntN (IntN),
WordN (WordN),
)
import Grisette.Internal.SymPrim.FP (NotRepresentableFPError)
import Grisette.Internal.SymPrim.Prim.Model
( Model (Model),
SymbolSet (SymbolSet),
)
import Grisette.Internal.SymPrim.Prim.Term
( LinkedRep (wrapTerm),
PEvalApplyTerm (pevalApplyTerm),
PEvalBVTerm
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm
),
PEvalBitwiseTerm
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalXorBitsTerm
),
PEvalDivModIntegralTerm
( pevalDivIntegralTerm,
pevalModIntegralTerm,
pevalQuotIntegralTerm,
pevalRemIntegralTerm
),
PEvalNumTerm
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalMulNumTerm,
pevalNegNumTerm,
pevalSignumNumTerm
),
PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
PEvalRotateTerm
( pevalRotateLeftTerm,
pevalRotateRightTerm
),
PEvalShiftTerm
( pevalShiftLeftTerm,
pevalShiftRightTerm
),
SupportedPrim (pevalITETerm),
Term,
conTerm,
isymTerm,
pevalAndTerm,
pevalEqTerm,
pevalGeOrdTerm,
pevalGtOrdTerm,
pevalImplyTerm,
pevalNotTerm,
pevalOrTerm,
pevalSubNumTerm,
pevalXorTerm,
someTypedSymbol,
ssymTerm,
toModelValue,
)
import Grisette.SymPrim
( ModelSymPair ((:=)),
SymAlgReal,
SymBool (SymBool),
SymFP32,
SymIntN (SymIntN),
SymInteger (SymInteger),
SymWordN (SymWordN),
symSize,
symsSize,
(-->),
type (-~>),
type (=~>),
)
import Test.Framework (Test, TestName, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, assertFailure, (@=?), (@?=))
import Test.QuickCheck (Arbitrary, ioProperty)
newtype AEWrapper = AEWrapper ArithException deriving (Eq)
instance Show AEWrapper where
show (AEWrapper x) = show x
instance NFData AEWrapper where
rnf (AEWrapper x) = x `seq` ()
sameSafeDiv ::
forall c s.
( Show s,
Eq s,
Mergeable s,
NFData c,
Solvable c s
) =>
c ->
c ->
(s -> s -> ExceptT ArithException Union s) ->
(c -> c -> c) ->
Assertion
sameSafeDiv i j f cf = do
xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
case xc of
Left (AEWrapper e) -> f (con i :: s) (con j) @=? tryMerge (throwError e)
Right c -> f (con i :: s) (con j) @=? mrgSingle (con c)
sameSafeDivMod ::
forall c s.
( Show s,
Eq s,
Mergeable s,
NFData c,
Solvable c s
) =>
c ->
c ->
(s -> s -> ExceptT ArithException Union (s, s)) ->
(c -> c -> (c, c)) ->
Assertion
sameSafeDivMod i j f cf = do
xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left $ AEWrapper e
case xc of
Left (AEWrapper e) -> f (con i :: s) (con j) @=? tryMerge (throwError e)
Right (c1, c2) -> f (con i :: s) (con j) @=? mrgSingle (con c1, con c2)
safeDivisionBoundedOnlyTests ::
forall c s.
(LinkedRep c s, Bounded c, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
(s -> s -> ExceptT ArithException Union s) ->
(c -> c -> c) ->
(Term c -> Term c -> Term c) ->
[Test]
safeDivisionBoundedOnlyTests f cf pf =
[ testCase "on concrete min divided by minus one" $ do
sameSafeDiv minBound (-1) f cf,
testCase "on symbolic" $ do
f (ssym "a" :: s) (ssym "b")
@=? ( mrgIf
((ssym "b" :: s) .== con (0 :: c) :: SymBool)
(throwError DivideByZero)
( mrgIf
((ssym "b" :: s) .== con (-1) .&& (ssym "a" :: s) .== con (minBound :: c) :: SymBool)
(throwError Overflow)
(mrgSingle $ wrapTerm $ pf (ssymTerm "a") (ssymTerm "b"))
) ::
ExceptT ArithException Union s
)
]
safeDivisionUnboundedOnlyTests ::
forall c s.
(LinkedRep c s, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
(s -> s -> ExceptT ArithException Union s) ->
(Term c -> Term c -> Term c) ->
[Test]
safeDivisionUnboundedOnlyTests f pf =
[ testCase "on symbolic" $ do
f (ssym "a" :: s) (ssym "b")
@=? ( mrgIf
((ssym "b" :: s) .== con (0 :: c) :: SymBool)
(throwError DivideByZero)
(mrgSingle $ wrapTerm $ pf (ssymTerm "a") (ssymTerm "b")) ::
ExceptT ArithException Union s
)
]
safeDivisionGeneralTests ::
forall c c0 s.
( LinkedRep c s,
Arbitrary c0,
Show c0,
Solvable c s,
Eq s,
Num c,
Show s,
Mergeable s
) =>
(c0 -> c) ->
(s -> s -> ExceptT ArithException Union s) ->
(c -> c -> c) ->
[Test]
safeDivisionGeneralTests transform f cf =
[ testProperty "on concrete prop" $ \(i0 :: c0, j0 :: c0) ->
ioProperty $ do
let i = transform i0
let j = transform j0
sameSafeDiv i j f cf,
testProperty "on concrete divided by zero" $ \(i0 :: c0) ->
ioProperty $ do
let i = transform i0
sameSafeDiv i 0 f cf,
testCase "when divided by zero" $ do
f (ssym "a" :: s) (con 0)
@=? (tryMerge $ throwError DivideByZero :: ExceptT ArithException Union s)
]
safeDivisionBoundedTests ::
forall c c0 s.
(LinkedRep c s, Arbitrary c0, Show c0, Bounded c, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
TestName ->
(c0 -> c) ->
(s -> s -> ExceptT ArithException Union s) ->
(c -> c -> c) ->
(Term c -> Term c -> Term c) ->
Test
safeDivisionBoundedTests name transform f cf pf =
testGroup name $
safeDivisionGeneralTests transform f cf
++ safeDivisionBoundedOnlyTests f cf pf
safeDivisionUnboundedTests ::
forall c c0 s.
(LinkedRep c s, Arbitrary c0, Show c0, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
TestName ->
(c0 -> c) ->
(s -> s -> ExceptT ArithException Union s) ->
(c -> c -> c) ->
(Term c -> Term c -> Term c) ->
Test
safeDivisionUnboundedTests name transform f cf pf =
testGroup name $
safeDivisionGeneralTests transform f cf
++ safeDivisionUnboundedOnlyTests f pf
safeDivModBoundedOnlyTests ::
forall c s.
(LinkedRep c s, Bounded c, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
( s ->
s ->
ExceptT ArithException Union (s, s)
) ->
(c -> c -> (c, c)) ->
(Term c -> Term c -> Term c) ->
(Term c -> Term c -> Term c) ->
[Test]
safeDivModBoundedOnlyTests f cf pf1 pf2 =
[ testCase "on concrete min divided by minus one" $
sameSafeDivMod minBound (-1) f cf,
testCase "on symbolic" $ do
f (ssym "a" :: s) (ssym "b")
@=? ( mrgIf
((ssym "b" :: s) .== con (0 :: c) :: SymBool)
(throwError DivideByZero)
( mrgIf
((ssym "b" :: s) .== con (-1) .&& (ssym "a" :: s) .== con (minBound :: c) :: SymBool)
(throwError Overflow)
( mrgSingle
( wrapTerm $ pf1 (ssymTerm "a") (ssymTerm "b"),
wrapTerm $ pf2 (ssymTerm "a") (ssymTerm "b")
)
)
) ::
ExceptT ArithException Union (s, s)
)
]
safeDivModUnboundedOnlyTests ::
forall c s.
(LinkedRep c s, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
( s ->
s ->
ExceptT ArithException Union (s, s)
) ->
(Term c -> Term c -> Term c) ->
(Term c -> Term c -> Term c) ->
[Test]
safeDivModUnboundedOnlyTests f pf1 pf2 =
[ testCase "on symbolic" $ do
f (ssym "a" :: s) (ssym "b")
@=? ( mrgIf
((ssym "b" :: s) .== con (0 :: c) :: SymBool)
(throwError DivideByZero)
( mrgSingle
( wrapTerm $ pf1 (ssymTerm "a") (ssymTerm "b"),
wrapTerm $ pf2 (ssymTerm "a") (ssymTerm "b")
)
) ::
ExceptT ArithException Union (s, s)
)
]
safeDivModGeneralTests ::
forall c c0 s.
( LinkedRep c s,
Arbitrary c0,
Show c0,
Solvable c s,
Eq s,
Num c,
Show s,
Mergeable s
) =>
(c0 -> c) ->
( s ->
s ->
ExceptT ArithException Union (s, s)
) ->
(c -> c -> (c, c)) ->
[Test]
safeDivModGeneralTests transform f cf =
[ testProperty "on concrete" $ \(i0 :: c0, j0 :: c0) ->
ioProperty $ do
let i = transform i0
let j = transform j0
sameSafeDivMod i j f cf,
testProperty "on concrete divided by zero" $ \(i0 :: c0) ->
ioProperty $ do
let i = transform i0
sameSafeDivMod i 0 f cf,
testCase "when divided by zero" $ do
f (ssym "a" :: s) (con 0)
@=? (tryMerge $ throwError DivideByZero :: ExceptT ArithException Union (s, s))
]
safeDivModBoundedTests ::
forall c c0 s.
(LinkedRep c s, Arbitrary c0, Show c0, Bounded c, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
TestName ->
(c0 -> c) ->
( s ->
s ->
ExceptT ArithException Union (s, s)
) ->
(c -> c -> (c, c)) ->
(Term c -> Term c -> Term c) ->
(Term c -> Term c -> Term c) ->
Test
safeDivModBoundedTests name transform f cf pf1 pf2 =
testGroup name $
safeDivModGeneralTests transform f cf
++ safeDivModBoundedOnlyTests f cf pf1 pf2
safeDivModUnboundedTests ::
forall c c0 s.
(LinkedRep c s, Arbitrary c0, Show c0, Solvable c s, Eq s, Num c, Show s, Mergeable s, SymEq s) =>
TestName ->
(c0 -> c) ->
( s ->
s ->
ExceptT ArithException Union (s, s)
) ->
(c -> c -> (c, c)) ->
(Term c -> Term c -> Term c) ->
(Term c -> Term c -> Term c) ->
Test
safeDivModUnboundedTests name transform f cf pf1 pf2 =
testGroup name $
safeDivModGeneralTests transform f cf
++ safeDivModUnboundedOnlyTests f pf1 pf2
symPrimTests :: Test
symPrimTests =
testGroup
"SymPrim"
[ testGroup
"General SymPrim"
[ testGroup
"Solvable"
[ testCase "con" $ (con 1 :: SymInteger) @=? SymInteger (conTerm 1),
testCase "ssym" $ (ssym "a" :: SymInteger) @=? SymInteger (ssymTerm "a"),
testCase "isym" $ (isym "a" 1 :: SymInteger) @=? SymInteger (isymTerm "a" 1),
testCase "conView" $ do
conView (con 1 :: SymInteger) @=? Just 1
conView (ssym "a" :: SymInteger) @=? Nothing
case con 1 :: SymInteger of
Con 1 -> return ()
_ -> assertFailure "Bad match"
case ssym "a" :: SymInteger of
Con _ -> assertFailure "Bad match"
_ -> return ()
],
testGroup
"ITEOp"
[ testCase "symIte" $
symIte (ssym "a" :: SymBool) (ssym "b" :: SymInteger) (ssym "c")
@=? SymInteger (pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c"))
],
testCase "Mergeable" $ do
let SimpleStrategy s = rootStrategy :: MergingStrategy SymInteger
s (ssym "a") (ssym "b") (ssym "c")
@=? symIte (ssym "a" :: SymBool) (ssym "b" :: SymInteger) (ssym "c"),
testCase "SimpleMergeable" $
mrgIte (ssym "a" :: SymBool) (ssym "b") (ssym "c")
@=? symIte (ssym "a" :: SymBool) (ssym "b" :: SymInteger) (ssym "c"),
testCase "IsString" $ ("a" :: SymBool) @=? SymBool (ssymTerm "a"),
testGroup
"ToSym"
[ testCase "From self" $ toSym (ssym "a" :: SymBool) @=? (ssym "a" :: SymBool),
testCase "From concrete" $ toSym True @=? (con True :: SymBool)
],
testGroup
"ToCon"
[ testCase "To self" $ toCon (ssym "a" :: SymBool) @=? (Nothing :: Maybe Bool),
testCase "To concrete" $ toCon True @=? Just True
],
testCase "EvalSym" $ do
let m1 = emptyModel :: Model
let m2 = insertValue "a" (1 :: Integer) m1
let m3 = insertValue "b" True m2
evalSym False m3 (symIte ("c" :: SymBool) "a" ("a" + "a" :: SymInteger))
@=? symIte ("c" :: SymBool) 1 2
evalSym True m3 (symIte ("c" :: SymBool) "a" ("a" + "a" :: SymInteger)) @=? 2,
testCase "ExtractSym" $
extractSym (symIte ("c" :: SymBool) ("a" :: SymInteger) ("b" :: SymInteger))
@=? SymbolSet
( S.fromList
[ someTypedSymbol ("c" :: TypedAnySymbol Bool),
someTypedSymbol ("a" :: TypedAnySymbol Integer),
someTypedSymbol ("b" :: TypedAnySymbol Integer)
]
),
testCase "GenSym" $ do
(genSym () "a" :: Union SymBool) @=? mrgSingle (isym "a" 0)
(genSymSimple () "a" :: SymBool) @=? isym "a" 0
(genSym (ssym "a" :: SymBool) "a" :: Union SymBool) @=? mrgSingle (isym "a" 0)
(genSymSimple (ssym "a" :: SymBool) "a" :: SymBool) @=? isym "a" 0,
testCase "SymEq" $ do
(ssym "a" :: SymBool) .== ssym "b" @=? SymBool (pevalEqTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b"))
(ssym "a" :: SymBool) ./= ssym "b" @=? SymBool (pevalNotTerm $ pevalEqTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b"))
],
testGroup
"SymBool"
[ testGroup
"LogicalOp"
[ testCase ".||" $ ssym "a" .|| ssym "b" @=? SymBool (pevalOrTerm (ssymTerm "a") (ssymTerm "b")),
testCase ".|| short circuit" $ con True .|| undefined @=? (con True :: SymBool),
testCase ".&&" $ ssym "a" .&& ssym "b" @=? SymBool (pevalAndTerm (ssymTerm "a") (ssymTerm "b")),
testCase ".&& short circuit" $ con False .&& undefined @=? (con False :: SymBool),
testCase "symNot" $ symNot (ssym "a") @=? SymBool (pevalNotTerm (ssymTerm "a")),
testCase "symXor" $ symXor (ssym "a") (ssym "b") @=? SymBool (pevalXorTerm (ssymTerm "a") (ssymTerm "b")),
testCase "symImplies" $ symImplies (ssym "a") (ssym "b") @=? SymBool (pevalImplyTerm (ssymTerm "a") (ssymTerm "b")),
testCase "symImplies short circuit" $ symImplies (con False) (ssym "b") @=? (con True :: SymBool),
testCase "symIte short circuit" $ do
symIte (con True) (ssym "a") undefined @=? (ssym "a" :: SymBool)
symIte (con False) undefined (ssym "a") @=? (ssym "a" :: SymBool)
]
],
testGroup
"SymInteger"
[ testGroup
"Num"
[ testCase "fromInteger" $ (1 :: SymInteger) @=? SymInteger (conTerm 1),
testCase "(+)" $ (ssym "a" :: SymInteger) + ssym "b" @=? SymInteger (pevalAddNumTerm (ssymTerm "a") (ssymTerm "b")),
testCase "(-)" $ (ssym "a" :: SymInteger) - ssym "b" @=? SymInteger (pevalSubNumTerm (ssymTerm "a") (ssymTerm "b")),
testCase "(*)" $ (ssym "a" :: SymInteger) * ssym "b" @=? SymInteger (pevalMulNumTerm (ssymTerm "a") (ssymTerm "b")),
testCase "negate" $ negate (ssym "a" :: SymInteger) @=? SymInteger (pevalNegNumTerm (ssymTerm "a")),
testCase "abs" $ abs (ssym "a" :: SymInteger) @=? SymInteger (pevalAbsNumTerm (ssymTerm "a")),
testCase "signum" $ signum (ssym "a" :: SymInteger) @=? SymInteger (pevalSignumNumTerm (ssymTerm "a"))
],
testGroup
"SafeDiv"
[ safeDivisionUnboundedTests @Integer "safeDiv" id safeDiv div pevalDivIntegralTerm,
safeDivisionUnboundedTests @Integer "safeMod" id safeMod mod pevalModIntegralTerm,
safeDivModUnboundedTests @Integer "safeDivMod" id safeDivMod divMod pevalDivIntegralTerm pevalModIntegralTerm,
safeDivisionUnboundedTests @Integer "safeQuot" id safeQuot quot pevalQuotIntegralTerm,
safeDivisionUnboundedTests @Integer "safeRem" id safeRem rem pevalRemIntegralTerm,
safeDivModUnboundedTests @Integer "safeQuotRem" id safeQuotRem quotRem pevalQuotIntegralTerm pevalRemIntegralTerm
],
testGroup
"SafeLinearArith"
[ testProperty "safeAdd on concrete" $ \(i :: Integer, j :: Integer) ->
ioProperty $ do
safeAdd (con i :: SymInteger) (con j)
@=? (mrgSingle $ con $ i + j :: ExceptT ArithException Union SymInteger),
testCase "safeAdd on symbolic" $ do
safeAdd (ssym "a" :: SymInteger) (ssym "b")
@=? (mrgSingle $ SymInteger $ pevalAddNumTerm (ssymTerm "a") (ssymTerm "b") :: ExceptT ArithException Union SymInteger),
testProperty "safeNeg on concrete" $ \(i :: Integer) ->
ioProperty $ do
safeNeg (con i :: SymInteger)
@=? (mrgSingle $ con $ -i :: ExceptT ArithException Union SymInteger),
testCase "safeNeg on symbolic" $ do
safeNeg (ssym "a" :: SymInteger)
@=? (mrgSingle $ SymInteger $ pevalNegNumTerm (ssymTerm "a") :: ExceptT ArithException Union SymInteger),
testProperty "safeSub on concrete" $ \(i :: Integer, j :: Integer) ->
ioProperty $ do
safeSub (con i :: SymInteger) (con j)
@=? (mrgSingle $ con $ i - j :: ExceptT ArithException Union SymInteger),
testCase "safeSub on symbolic" $ do
safeSub (ssym "a" :: SymInteger) (ssym "b")
@=? (mrgSingle $ SymInteger $ pevalSubNumTerm (ssymTerm "a") (ssymTerm "b") :: ExceptT ArithException Union SymInteger)
],
testGroup
"SymOrd"
[ testProperty "SymOrd on concrete" $ \(i :: Integer, j :: Integer) -> ioProperty $ do
(con i :: SymInteger) .<= con j @=? (con (i <= j) :: SymBool)
(con i :: SymInteger) .< con j @=? (con (i < j) :: SymBool)
(con i :: SymInteger) .>= con j @=? (con (i >= j) :: SymBool)
(con i :: SymInteger) .> con j @=? (con (i > j) :: SymBool)
(con i :: SymInteger)
`symCompare` con j
@=? (i `symCompare` j :: Union Ordering),
testCase "SymOrd on symbolic" $ do
let a :: SymInteger = ssym "a"
let b :: SymInteger = ssym "b"
let at :: Term Integer = ssymTerm "a"
let bt :: Term Integer = ssymTerm "b"
a .<= b @=? SymBool (pevalLeOrdTerm at bt)
a .< b @=? SymBool (pevalLtOrdTerm at bt)
a .>= b @=? SymBool (pevalGeOrdTerm at bt)
a .> b @=? SymBool (pevalGtOrdTerm at bt)
(a `symCompare` ssym "b" :: Union Ordering)
@=? mrgIf (a .< b) (mrgSingle LT) (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT))
]
],
let au :: SymWordN 4 = ssym "a"
bu :: SymWordN 4 = ssym "b"
as :: SymIntN 4 = ssym "a"
bs :: SymIntN 4 = ssym "b"
aut :: Term (WordN 4) = ssymTerm "a"
but :: Term (WordN 4) = ssymTerm "b"
ast :: Term (IntN 4) = ssymTerm "a"
bst :: Term (IntN 4) = ssymTerm "b"
in testGroup
"Sym BV"
[ testGroup
"Num"
[ testCase "fromInteger" $ do
(1 :: SymWordN 4) @=? SymWordN (conTerm 1)
(1 :: SymIntN 4) @=? SymIntN (conTerm 1),
testCase "(+)" $ do
au + bu @=? SymWordN (pevalAddNumTerm aut but)
as + bs @=? SymIntN (pevalAddNumTerm ast bst),
testCase "(-)" $ do
au - bu @=? SymWordN (pevalSubNumTerm aut but)
as - bs @=? SymIntN (pevalSubNumTerm ast bst),
testCase "(*)" $ do
au * bu @=? SymWordN (pevalMulNumTerm aut but)
as * bs @=? SymIntN (pevalMulNumTerm ast bst),
testCase "negate" $ do
negate au @=? SymWordN (pevalNegNumTerm aut)
negate as @=? SymIntN (pevalNegNumTerm ast),
testCase "abs" $ do
abs au @=? SymWordN (pevalAbsNumTerm aut)
abs as @=? SymIntN (pevalAbsNumTerm ast),
testCase "signum" $ do
signum au @=? SymWordN (pevalSignumNumTerm aut)
signum as @=? SymIntN (pevalSignumNumTerm ast)
],
testGroup
"SafeDiv"
[ testGroup
"WordN"
[ safeDivisionUnboundedTests @(WordN 4) "safeDiv" WordN safeDiv div pevalDivIntegralTerm,
safeDivisionUnboundedTests @(WordN 4) "safeMod" WordN safeMod mod pevalModIntegralTerm,
safeDivModUnboundedTests @(WordN 4) "safeDivMod" WordN safeDivMod divMod pevalDivIntegralTerm pevalModIntegralTerm,
safeDivisionUnboundedTests @(WordN 4) "safeQuot" WordN safeQuot quot pevalQuotIntegralTerm,
safeDivisionUnboundedTests @(WordN 4) "safeRem" WordN safeRem rem pevalRemIntegralTerm,
safeDivModUnboundedTests @(WordN 4) "safeQuotRem" WordN safeQuotRem divMod pevalQuotIntegralTerm pevalRemIntegralTerm
],
testGroup
"IntN"
[ safeDivisionBoundedTests @(IntN 4) "safeDiv" IntN safeDiv div pevalDivIntegralTerm,
safeDivisionUnboundedTests @(IntN 4) "safeMod" IntN safeMod mod pevalModIntegralTerm,
safeDivModBoundedTests @(IntN 4) "safeDivMod" IntN safeDivMod divMod pevalDivIntegralTerm pevalModIntegralTerm,
safeDivisionBoundedTests @(IntN 4) "safeQuot" IntN safeQuot quot pevalQuotIntegralTerm,
safeDivisionUnboundedTests @(IntN 4) "safeRem" IntN safeRem rem pevalRemIntegralTerm,
safeDivModBoundedTests @(IntN 4) "safeQuotRem" IntN safeQuotRem quotRem pevalQuotIntegralTerm pevalRemIntegralTerm
]
],
testGroup
"SafeLinearArith"
[ testGroup
"IntN"
[ testProperty "safeAdd on concrete" $ \(i :: Int8, j :: Int8) ->
ioProperty $
let iint = fromIntegral i :: Integer
jint = fromIntegral j
in safeAdd (toSym i :: SymIntN 8) (toSym j)
@=? mrgIf
(iint + jint .< fromIntegral (i + j))
(throwError Underflow)
( mrgIf
(iint + jint .> fromIntegral (i + j))
(throwError Overflow)
(mrgSingle $ toSym $ i + j :: ExceptT ArithException Union (SymIntN 8))
),
testProperty "safeSub on concrete" $ \(i :: Int8, j :: Int8) ->
ioProperty $
let iint = fromIntegral i :: Integer
jint = fromIntegral j
in safeSub (toSym i :: SymIntN 8) (toSym j)
@=? mrgIf
(iint - jint .< fromIntegral (i - j))
(throwError Underflow)
( mrgIf
(iint - jint .> fromIntegral (i - j))
(throwError Overflow)
(mrgSingle $ toSym $ i - j :: ExceptT ArithException Union (SymIntN 8))
),
testProperty "safeNeg on concrete" $ \(i :: Int8) ->
ioProperty $
let iint = fromIntegral i :: Integer
in safeNeg (toSym i :: SymIntN 8)
@=? mrgIf
((-iint) .< fromIntegral (-i))
(throwError Underflow)
( mrgIf
((-iint) .> fromIntegral (-i))
(throwError Overflow)
(mrgSingle $ toSym $ -i :: ExceptT ArithException Union (SymIntN 8))
)
],
testGroup
"WordN"
[ testProperty "safeAdd on concrete" $ \(i :: Word8, j :: Word8) ->
ioProperty $
let iint = fromIntegral i :: Integer
jint = fromIntegral j
in safeAdd (toSym i :: SymWordN 8) (toSym j)
@=? mrgIf
(iint + jint .< fromIntegral (i + j))
(throwError Underflow)
( mrgIf
(iint + jint .> fromIntegral (i + j))
(throwError Overflow)
(mrgSingle $ toSym $ i + j :: ExceptT ArithException Union (SymWordN 8))
),
testProperty "safeSub on concrete" $ \(i :: Word8, j :: Word8) ->
ioProperty $
let iint = fromIntegral i :: Integer
jint = fromIntegral j
in safeSub (toSym i :: SymWordN 8) (toSym j)
@=? mrgIf
(iint - jint .< fromIntegral (i - j))
(throwError Underflow)
( mrgIf
(iint - jint .> fromIntegral (i - j))
(throwError Overflow)
(mrgSingle $ toSym $ i - j :: ExceptT ArithException Union (SymWordN 8))
),
testProperty "safeNeg on concrete" $ \(i :: Word8) ->
ioProperty $
let iint = fromIntegral i :: Integer
in safeNeg (toSym i :: SymWordN 8)
@=? mrgIf
((-iint) .< fromIntegral (-i))
(throwError Underflow)
( mrgIf
((-iint) .> fromIntegral (-i))
(throwError Overflow)
(mrgSingle $ toSym $ -i :: ExceptT ArithException Union (SymWordN 8))
)
]
],
testGroup
"SymOrd"
[ testProperty "SymOrd on concrete" $ \(i :: Integer, j :: Integer) -> ioProperty $ do
let iu :: WordN 4 = fromInteger i
let ju :: WordN 4 = fromInteger j
let is :: IntN 4 = fromInteger i
let js :: IntN 4 = fromInteger j
let normalizeu k = k - k `div` 16 * 16
let normalizes k = if normalizeu k >= 8 then normalizeu k - 16 else normalizeu k
(con iu :: SymWordN 4) .<= con ju @=? (con (normalizeu i <= normalizeu j) :: SymBool)
(con iu :: SymWordN 4) .< con ju @=? (con (normalizeu i < normalizeu j) :: SymBool)
(con iu :: SymWordN 4) .>= con ju @=? (con (normalizeu i >= normalizeu j) :: SymBool)
(con iu :: SymWordN 4) .> con ju @=? (con (normalizeu i > normalizeu j) :: SymBool)
(con iu :: SymWordN 4)
`symCompare` con ju
@=? (normalizeu i `symCompare` normalizeu j :: Union Ordering)
(con is :: SymIntN 4) .<= con js @=? (con (normalizes i <= normalizes j) :: SymBool)
(con is :: SymIntN 4) .< con js @=? (con (normalizes i < normalizes j) :: SymBool)
(con is :: SymIntN 4) .>= con js @=? (con (normalizes i >= normalizes j) :: SymBool)
(con is :: SymIntN 4) .> con js @=? (con (normalizes i > normalizes j) :: SymBool)
(con is :: SymIntN 4)
`symCompare` con js
@=? (normalizes i `symCompare` normalizes j :: Union Ordering),
testCase "SymOrd on symbolic" $ do
au .<= bu @=? SymBool (pevalLeOrdTerm aut but)
au .< bu @=? SymBool (pevalLtOrdTerm aut but)
au .>= bu @=? SymBool (pevalGeOrdTerm aut but)
au .> bu @=? SymBool (pevalGtOrdTerm aut but)
(au `symCompare` bu :: Union Ordering)
@=? mrgIf (au .< bu) (mrgSingle LT) (mrgIf (au .== bu) (mrgSingle EQ) (mrgSingle GT))
as .<= bs @=? SymBool (pevalLeOrdTerm ast bst)
as .< bs @=? SymBool (pevalLtOrdTerm ast bst)
as .>= bs @=? SymBool (pevalGeOrdTerm ast bst)
as .> bs @=? SymBool (pevalGtOrdTerm ast bst)
(as `symCompare` bs :: Union Ordering)
@=? mrgIf (as .< bs) (mrgSingle LT) (mrgIf (as .== bs) (mrgSingle EQ) (mrgSingle GT))
],
testGroup
"Bits"
[ testCase ".&." $ do
au .&. bu @=? SymWordN (pevalAndBitsTerm aut but)
as .&. bs @=? SymIntN (pevalAndBitsTerm ast bst),
testCase ".|." $ do
au .|. bu @=? SymWordN (pevalOrBitsTerm aut but)
as .|. bs @=? SymIntN (pevalOrBitsTerm ast bst),
testCase "xor" $ do
au `xor` bu @=? SymWordN (pevalXorBitsTerm aut but)
as `xor` bs @=? SymIntN (pevalXorBitsTerm ast bst),
testCase "complement" $ do
complement au @=? SymWordN (pevalComplementBitsTerm aut)
complement as @=? SymIntN (pevalComplementBitsTerm ast),
testCase "shift" $ do
shift au 1 @=? SymWordN (pevalShiftLeftTerm aut $ conTerm 1)
shift as 1 @=? SymIntN (pevalShiftLeftTerm ast $ conTerm 1)
shift au (-1) @=? SymWordN (pevalShiftRightTerm aut $ conTerm 1)
shift as (-1) @=? SymIntN (pevalShiftRightTerm ast $ conTerm 1),
testCase "rotate" $ do
rotate au 1 @=? SymWordN (pevalRotateLeftTerm aut $ conTerm 1)
rotate as 1 @=? SymIntN (pevalRotateLeftTerm ast $ conTerm 1)
rotate au (-1) @=? SymWordN (pevalRotateRightTerm aut $ conTerm 1)
rotate as (-1) @=? SymIntN (pevalRotateRightTerm ast $ conTerm 1),
testCase "bitSize" $ do
bitSizeMaybe au @=? Just 4
bitSizeMaybe as @=? Just 4,
testCase "isSigned" $ do
isSigned au @=? False
isSigned as @=? True,
testCase "testBit would only work on concrete ones" $ do
testBit (con 3 :: SymWordN 4) 1 @=? True
testBit (con 3 :: SymWordN 4) 2 @=? False
testBit (con 3 :: SymIntN 4) 1 @=? True
testBit (con 3 :: SymIntN 4) 2 @=? False,
testCase "bit would work" $ do
bit 1 @=? (con 2 :: SymWordN 4)
bit 1 @=? (con 2 :: SymIntN 4),
testCase "popCount would only work on concrete ones" $ do
popCount (con 3 :: SymWordN 4) @=? 2
popCount (con 3 :: SymWordN 4) @=? 2
popCount (con 3 :: SymIntN 4) @=? 2
popCount (con 3 :: SymIntN 4) @=? 2
],
testGroup
"sizedBVConcat"
[ testCase "sizedBVConcat" $
sizedBVConcat
(ssym "a" :: SymWordN 4)
(ssym "b" :: SymWordN 3)
@=? SymWordN
( pevalBVConcatTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 3))
)
],
testGroup
"sizedBVExt for Sym BV"
[ testCase "sizedBVZext" $ do
sizedBVZext (Proxy @6) au @=? SymWordN (pevalBVExtendTerm False (Proxy @6) aut)
sizedBVZext (Proxy @6) as @=? SymIntN (pevalBVExtendTerm False (Proxy @6) ast),
testCase "sizedBVSext" $ do
sizedBVSext (Proxy @6) au @=? SymWordN (pevalBVExtendTerm True (Proxy @6) aut)
sizedBVSext (Proxy @6) as @=? SymIntN (pevalBVExtendTerm True (Proxy @6) ast),
testCase "sizedBVExt" $ do
sizedBVExt (Proxy @6) au @=? SymWordN (pevalBVExtendTerm False (Proxy @6) aut)
sizedBVExt (Proxy @6) as @=? SymIntN (pevalBVExtendTerm True (Proxy @6) ast)
],
testGroup
"sizedBVSelect for Sym BV"
[ testCase "sizedBVSelect" $ do
sizedBVSelect (Proxy @2) (Proxy @1) au
@=? SymWordN (pevalBVSelectTerm (Proxy @2) (Proxy @1) aut)
sizedBVSelect (Proxy @2) (Proxy @1) as
@=? SymIntN (pevalBVSelectTerm (Proxy @2) (Proxy @1) ast)
],
testGroup
"conversion between Int8 and Sym BV"
[ testCase "toSym" $ do
toSym (0 :: Int8) @=? (con 0 :: SymIntN 8)
toSym (-127 :: Int8) @=? (con $ -127 :: SymIntN 8)
toSym (-128 :: Int8) @=? (con $ -128 :: SymIntN 8)
toSym (127 :: Int8) @=? (con 127 :: SymIntN 8),
testCase "toCon" $ do
toCon (con 0 :: SymIntN 8) @=? Just (0 :: Int8)
toCon (con $ -127 :: SymIntN 8) @=? Just (-127 :: Int8)
toCon (con $ -128 :: SymIntN 8) @=? Just (-128 :: Int8)
toCon (con 127 :: SymIntN 8) @=? Just (127 :: Int8)
],
testGroup
"conversion between Word8 and Sym BV"
[ testCase "toSym" $ do
toSym (0 :: Word8) @=? (con 0 :: SymWordN 8)
toSym (1 :: Word8) @=? (con 1 :: SymWordN 8)
toSym (255 :: Word8) @=? (con 255 :: SymWordN 8),
testCase "toCon" $ do
toCon (con 0 :: SymWordN 8) @=? Just (0 :: Word8)
toCon (con 1 :: SymWordN 8) @=? Just (1 :: Word8)
toCon (con 255 :: SymWordN 8) @=? Just (255 :: Word8)
]
],
testGroup
"SymFP"
[ testCase "bitCast consistent to SymWordN32" $ do
let x = "x" :: SymFP32
r <-
solve
z3
( symFpIsNaN x
.&& ( (bitCastOrCanonical x :: SymWordN32)
./= (con (bitCastOrCanonical (fpNaN :: FP32)))
)
)
case r of
Left Unsat -> return ()
_ -> fail $ show r,
testCase "bitCast consistent to SymIntN32" $ do
let x = "x" :: SymFP32
r <-
solve
z3
( symFpIsNaN x
.&& ( (bitCastOrCanonical x :: SymIntN32)
./= (con (bitCastOrCanonical (fpNaN :: FP32)))
)
)
case r of
Left Unsat -> return ()
_ -> fail $ show r,
testGroup "SafeFromFP" $ do
let safeFromFPComplianceTest ::
forall c s.
( Arbitrary c,
Show c,
Solvable c s,
SymEq s,
SafeFromFP
NotRepresentableFPError
s
(SymFP 4 4)
SymFPRoundingMode
(ExceptT NotRepresentableFPError Union)
) =>
Test
safeFromFPComplianceTest =
testProperty "safeFromFP" $
\(d :: c) (md :: FPRoundingMode) (v :: FP 4 4) -> ioProperty $ do
let s =
runExceptT $
safeFromFP
(con md :: SymFPRoundingMode)
(con v :: SymFP 4 4) ::
Union (Either NotRepresentableFPError s)
let f =
fromFPOr
(con d :: s)
(con md :: SymFPRoundingMode)
(con v :: SymFP 4 4)
let cond = simpleMerge $ do
s' <- s
case s' of
Left _ -> return $ f .== (con d)
Right r -> return $ r .== f
res <- solve z3 $ symNot cond
case res of
Left Unsat -> return ()
m -> error $ show m
[ safeFromFPComplianceTest @Integer @SymInteger,
safeFromFPComplianceTest @AlgReal @SymAlgReal,
safeFromFPComplianceTest @(WordN 3) @(SymWordN 3),
safeFromFPComplianceTest @(IntN 3) @(SymIntN 3)
]
],
testGroup
"SomeSym"
[ testGroup
"BV"
[ testCase "bv" $ do
(bv 12 21 :: SomeSymWordN) @?= SomeSymWordN (21 :: SymWordN 12)
(bv 12 21 :: SomeSymIntN) @?= SomeSymIntN (21 :: SymIntN 12)
]
],
testGroup
"TabularFun"
[ testCase "#" $
(ssym "a" :: SymInteger =~> SymInteger)
# ssym "b"
@=? SymInteger (pevalApplyTerm (ssymTerm "a" :: Term (Integer =-> Integer)) (ssymTerm "b")),
testCase "apply" $
apply
(ssym "f" :: SymInteger =~> SymInteger =~> SymInteger)
(ssym "a")
(ssym "b")
@=? SymInteger
( pevalApplyTerm
( pevalApplyTerm
(ssymTerm "f" :: Term (Integer =-> Integer =-> Integer))
(ssymTerm "a")
)
(ssymTerm "b")
)
],
testGroup
"GeneralFun"
[ testCase "evaluate" $ do
evalSym
False
(buildModel ("a" := (1 :: Integer), "b" := (2 :: Integer)))
(con ("a" --> "a" + "b") :: SymInteger -~> SymInteger)
@=? (con ("a" --> "a" + 2) :: SymInteger -~> SymInteger)
evalSym
False
(buildModel ("a" := (1 :: Integer), "b" := (2 :: Integer), "c" := (3 :: Integer)))
(con ("a" --> con ("b" --> "a" + "b" + "c")) :: SymInteger -~> SymInteger -~> SymInteger)
@=? con ("a" --> con ("b" --> "a" + "b" + 3) :: Integer --> Integer --> Integer),
testCase "#" $ do
let f :: SymInteger -~> SymInteger -~> SymInteger =
con ("a" --> con ("b" --> "a" + "b"))
f # ssym "x" @=? con ("b" --> "x" + "b"),
testCase "apply" $ do
let f :: SymInteger -~> SymInteger -~> SymInteger =
con ("a" --> con ("b" --> "a" + "b"))
apply f "x" "y" @=? "x" + "y"
],
testGroup
"Symbolic size"
[ testCase "symSize" $ do
symSize (ssym "a" :: SymInteger) @=? 1
symSize (con 1 :: SymInteger) @=? 1
symSize (con 1 + ssym "a" :: SymInteger) @=? 3
symSize (ssym "a" + ssym "a" :: SymInteger) @=? 2
symSize (-(ssym "a") :: SymInteger) @=? 2
symSize (symIte (ssym "a" :: SymBool) (ssym "b") (ssym "c") :: SymInteger) @=? 4,
testCase "symsSize" $ symsSize [ssym "a" :: SymInteger, ssym "a" + ssym "a"] @=? 2
],
let asymbol :: TypedAnySymbol Integer = "a"
bsymbol :: TypedAnySymbol Bool = "b"
csymbol :: TypedAnySymbol Integer = "c"
dsymbol :: TypedAnySymbol Bool = "d"
esymbol :: TypedAnySymbol (WordN 4) = "e"
fsymbol :: TypedAnySymbol (IntN 4) = "f"
gsymbol :: TypedAnySymbol (WordN 16) = "g"
hsymbol :: TypedAnySymbol (IntN 16) = "h"
va :: Integer = 1
vc :: Integer = 2
ve :: WordN 4 = 3
vf :: IntN 4 = 4
vg :: WordN 16 = 5
vh :: IntN 16 = 6
in testCase
"construting Model from ModelSymPair"
$ do
buildModel ("a" := va) @=? Model (M.singleton (someTypedSymbol asymbol) (toModelValue va))
buildModel ("a" := va, "b" := True)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc,
"d" := False
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc),
(someTypedSymbol dsymbol, toModelValue False)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc,
"d" := False,
"e" := ve
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc),
(someTypedSymbol dsymbol, toModelValue False),
(someTypedSymbol esymbol, toModelValue ve)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc,
"d" := False,
"e" := ve,
"f" := vf
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc),
(someTypedSymbol dsymbol, toModelValue False),
(someTypedSymbol esymbol, toModelValue ve),
(someTypedSymbol fsymbol, toModelValue vf)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc,
"d" := False,
"e" := ve,
"f" := vf,
"g" := vg
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc),
(someTypedSymbol dsymbol, toModelValue False),
(someTypedSymbol esymbol, toModelValue ve),
(someTypedSymbol fsymbol, toModelValue vf),
(someTypedSymbol gsymbol, toModelValue vg)
]
)
buildModel
( "a" := va,
"b" := True,
"c" := vc,
"d" := False,
"e" := ve,
"f" := vf,
"g" := vg,
"h" := vh
)
@=? Model
( M.fromList
[ (someTypedSymbol asymbol, toModelValue va),
(someTypedSymbol bsymbol, toModelValue True),
(someTypedSymbol csymbol, toModelValue vc),
(someTypedSymbol dsymbol, toModelValue False),
(someTypedSymbol esymbol, toModelValue ve),
(someTypedSymbol fsymbol, toModelValue vf),
(someTypedSymbol gsymbol, toModelValue vg),
(someTypedSymbol hsymbol, toModelValue vh)
]
)
]