grisette-0.13.0.1: test/Grisette/Backend/TermRewritingTests.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Backend.TermRewritingTests
( termRewritingTests,
validateSpec,
bitwuzlaConfig,
)
where
import Data.Foldable (traverse_)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette
( AlgReal,
BitCast (bitCast),
GrisetteSMTConfig,
IEEEFPConstants
( fpMaxNormalized,
fpMaxSubnormal,
fpMinNormalized,
fpMinSubnormal,
fpNaN,
fpNegativeInfinite,
fpNegativeZero,
fpPositiveInfinite,
fpPositiveZero
),
IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
ITEOp (symIte),
IntN,
LinkedRep,
LogicalOp (symNot, true),
Solvable (con),
SymBool (SymBool),
SymFP,
SymIEEEFPTraits (symFpIsNaN),
SymRep (SymType),
WordN,
bitwuzla,
fpIsNaN,
solve,
z3,
)
import Grisette.Backend.TermRewritingGen
( BoolOnlySpec (BoolOnlySpec),
BoolWithFixedSizedBVSpec (BoolWithFixedSizedBVSpec),
BoolWithLIASpec,
DifferentSizeBVSpec,
FPRoundingModeBoolOpSpec,
FPRoundingModeSpec,
FixedSizedBVWithBoolSpec (FixedSizedBVWithBoolSpec),
GeneralSpec,
IEEEFPBoolOpSpec (IEEEFPBoolOpSpec),
IEEEFPSpec,
LIAWithBoolSpec,
NRAWithBoolSpec,
TermRewritingSpec
( conSpec,
counterExample,
norewriteVer,
rewriteVer,
same,
symSpec,
wrap
),
absNumSpec,
addNumSpec,
andBitsSpec,
andSpec,
bitCastOrSpec,
bitCastSpec,
bvconcatSpec,
bvextendSpec,
bvselectSpec,
complementBitsSpec,
divIntegralSpec,
eqvSpec,
fpBinaryOpSpec,
fpFMASpec,
fpRoundingBinarySpec,
fpRoundingUnaryOpSpec,
fpTraitSpec,
fromFPOrSpec,
iteSpec,
leOrdSpec,
modIntegralSpec,
mulNumSpec,
negNumSpec,
notSpec,
orBitsSpec,
orSpec,
quotIntegralSpec,
remIntegralSpec,
shiftLeftSpec,
shiftRightSpec,
signumNumSpec,
toFPSpec,
xorBitsSpec,
)
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((./=), (.==)))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
( SymIEEEFPTraits (symFpIsPositiveInfinite),
)
import Grisette.Internal.SymPrim.FP
( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
FP,
FP32,
FPRoundingMode,
ValidFP,
nextFP,
prevFP,
)
import Grisette.Internal.SymPrim.Prim.Term
( FPBinaryOp (FPMaximum, FPMaximumNumber, FPMinimum, FPMinimumNumber, FPRem),
FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),
FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),
FPTrait (FPIsPositive),
PEvalBVTerm,
PEvalBitCastOrTerm,
PEvalBitCastTerm,
PEvalBitwiseTerm (pevalAndBitsTerm, pevalOrBitsTerm),
PEvalIEEEFPConvertibleTerm,
PEvalShiftTerm,
SupportedNonFuncPrim,
Term,
andBitsTerm,
andTerm,
bvConcatTerm,
bvExtendTerm,
complementBitsTerm,
conTerm,
eqTerm,
fpTraitTerm,
iteTerm,
notTerm,
orBitsTerm,
orTerm,
pformatTerm,
ssymTerm,
xorBitsTerm,
)
import Grisette.Internal.SymPrim.SymFP (SymFP32)
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,
elements,
forAll,
ioProperty,
mapSize,
vectorOf,
withMaxSuccess,
(==>),
)
import Type.Reflection (Typeable, typeRep)
validateSpec' ::
(TermRewritingSpec a av) =>
GrisetteSMTConfig ->
SymBool ->
a ->
Assertion
validateSpec' config precond a = do
r <- solve config (precond .&& SymBool (counterExample a))
rs <- solve config (precond .&& SymBool (same a))
case (r, rs) of
(Left _, Right _) -> do
return ()
(Left _, Left err) -> do
print err
assertFailure $
"Bad rewriting with unsolvable formula: "
++ pformatTerm (norewriteVer a)
++ " was rewritten to "
++ pformatTerm (rewriteVer a)
++ " under precondition"
++ show precond
++ " corresponding same formula:"
++ pformatTerm (same a)
(Right m, _) -> do
assertFailure $
"With model"
++ show m
++ "Bad rewriting: "
++ pformatTerm (norewriteVer a)
++ " was rewritten to "
++ pformatTerm (rewriteVer a)
++ " under precondition"
++ show precond
++ " corresponding cex formula:"
++ pformatTerm (counterExample a)
++ "\n"
++ show (norewriteVer a)
++ "\n"
++ show (rewriteVer a)
++ "\n"
++ show (counterExample a)
validateSpec ::
(TermRewritingSpec a av) =>
GrisetteSMTConfig ->
a ->
Assertion
validateSpec config = validateSpec' config true
bitwuzlaConfig :: IO (Maybe GrisetteSMTConfig)
bitwuzlaConfig = do
v <-
solve bitwuzla $
(("x" :: SymFP32) ./= "x")
.&& symNot (symFpIsPositiveInfinite (con $ -4.7e-38 :: SymFP32))
.&& ( symIte
"bool"
(con fpPositiveInfinite :: SymFP32)
(con fpNegativeInfinite)
.== "m"
)
case v of
Left _ -> return Nothing
Right _ -> return $ Just bitwuzla
onlyWhenBitwuzlaIsAvailable :: (GrisetteSMTConfig -> IO ()) -> IO ()
onlyWhenBitwuzlaIsAvailable action = do
config <- bitwuzlaConfig
case config of
Just config -> action config
Nothing ->
putStrLn $
"bitwuzla isn't available in the system, or the dependent sbv"
<> " library does not work well with it. This test is marked as "
<> " success."
unboundedConfig = z3
divisionTest ::
forall a b.
(TermRewritingSpec a b, Enum b, Num b) =>
TestName ->
(a -> a -> a) ->
Test
divisionTest name f =
testGroup
name
[ testCase "on concrete" $ do
traverse_
( \(x :: b, y :: b) -> do
validateSpec @a unboundedConfig $ f (conSpec x) (conSpec y)
)
[(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
testCase "on single concrete" $ do
traverse_
( \x -> do
validateSpec @a unboundedConfig $ f (conSpec x) (symSpec "a")
validateSpec @a unboundedConfig $ f (symSpec "a") (conSpec x)
)
[-3 .. 3]
]
bvConcatTest ::
forall bv.
( forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (bv n),
forall n. (KnownNat n, 1 <= n) => PEvalShiftTerm (bv n),
forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n),
Typeable bv,
PEvalBVTerm bv
) =>
Test
bvConcatTest =
testGroup (show (typeRep @bv) <> "_concat") $
( do
(opName, opSpec, termOp) <-
[ ("and", andBitsSpec, andBitsTerm),
("or", orBitsSpec, orBitsTerm),
("xor", xorBitsSpec, xorBitsTerm)
]
[ testCase (opName <> "(const,concat)") $ do
let lhs = conSpec 0x39 :: FixedSizedBVWithBoolSpec bv 8
let rhs =
bvconcatSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
let spec = opSpec lhs rhs
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
testCase (opName <> "(concat,concat)") $ do
let lhs =
bvconcatSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
let rhs =
bvconcatSpec
(symSpec "c" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "d" :: FixedSizedBVWithBoolSpec bv 4)
let spec@(FixedSizedBVWithBoolSpec _ r) = opSpec lhs rhs
let expected =
( bvConcatTerm
(termOp (ssymTerm "a" :: Term (bv 4)) (ssymTerm "c"))
(termOp (ssymTerm "b" :: Term (bv 4)) (ssymTerm "d"))
)
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
]
)
++ [ testCase "complement(concat)" $ do
let lhs =
bvconcatSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
let spec@(FixedSizedBVWithBoolSpec _ r) = complementBitsSpec lhs
let expected =
bvConcatTerm
(complementBitsTerm (ssymTerm "a" :: Term (bv 4)))
(complementBitsTerm (ssymTerm "b" :: Term (bv 4)))
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
testCase "complement(sext)" $ do
let spec@(FixedSizedBVWithBoolSpec _ r) =
complementBitsSpec
( bvextendSpec
True
(Proxy :: Proxy 8)
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
) ::
FixedSizedBVWithBoolSpec bv 8
let expected =
bvExtendTerm
True
(Proxy :: Proxy 8)
(complementBitsTerm (ssymTerm "a" :: Term (bv 4)))
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
testCase "and(leading_zero_then_all_one, b)" $ do
let spec =
andBitsSpec
(conSpec 0x1f)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
testCase "and(leading_one_then_all_zero, b)" $ do
let spec =
andBitsSpec
(conSpec 0xf8)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
testCase "or(leading_zero_then_all_one, b)" $ do
let spec =
orBitsSpec
(conSpec 0x1f)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
testCase "or(leading_one_then_all_zero, b)" $ do
let spec =
orBitsSpec
(conSpec 0xf8)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
testCase "select(sext)with_part_base" $ do
let spec =
bvselectSpec
(Proxy @2)
(Proxy @4)
( bvextendSpec
True
(Proxy @8)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4) ::
FixedSizedBVWithBoolSpec bv 8
) ::
FixedSizedBVWithBoolSpec bv 4
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
testCase "ite(cond,concat(a,b),concat(c,d))" $ do
let spec@(FixedSizedBVWithBoolSpec _ r) =
iteSpec
(symSpec "cond" :: BoolWithFixedSizedBVSpec bv 4)
( bvconcatSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
)
( bvconcatSpec
(symSpec "c" :: FixedSizedBVWithBoolSpec bv 4)
(symSpec "d" :: FixedSizedBVWithBoolSpec bv 4)
)
let expected =
bvConcatTerm
( iteTerm
(ssymTerm "cond" :: Term Bool)
(ssymTerm "a" :: Term (bv 4))
(ssymTerm "c" :: Term (bv 4))
)
( iteTerm
(ssymTerm "cond" :: Term Bool)
(ssymTerm "b" :: Term (bv 4))
(ssymTerm "d" :: Term (bv 4))
)
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
]
++ ( do
pos <- [True, False]
cvalue <- [0 :: Int, -1]
value <- [0 :: Int, -1]
let con = conSpec (fromIntegral value) :: FixedSizedBVWithBoolSpec bv 4
let sym = symSpec "b"
let t = if pos then con else sym
let f = if pos then sym else con
let spec =
iteSpec
( eqvSpec
(symSpec "c" :: FixedSizedBVWithBoolSpec bv 1)
(conSpec $ fromIntegral cvalue) ::
BoolWithFixedSizedBVSpec bv 1
)
t
f
let ts = if pos then show value else "sym"
let fs = if pos then "sym" else show value
return
$ testCase
( "ite(bv1="
<> show cvalue
<> ","
<> ts
<> ","
<> fs
<> ")"
)
$ validateSpec unboundedConfig spec
)
++ ( do
let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1
let condTerm = ssymTerm "cond" :: Term Bool
(opName, op, opSpec) <-
[ ("and", andBitsTerm, andBitsSpec),
("or", orBitsTerm, orBitsSpec),
("xor", xorBitsTerm, xorBitsSpec),
("ite", iteTerm condTerm, iteSpec cond)
]
let name = opName <> "(sext,sext)"
let spec@(FixedSizedBVWithBoolSpec _ r) =
opSpec
( bvextendSpec
True
(Proxy :: Proxy 8)
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
)
( bvextendSpec
True
(Proxy :: Proxy 8)
(symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
)
let expected =
bvExtendTerm
True
(Proxy :: Proxy 8)
( op
(ssymTerm "a" :: Term (bv 4))
(ssymTerm "b" :: Term (bv 4))
)
return $ testCase name $ do
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
)
++ ( do
let a = symSpec "a" :: FixedSizedBVWithBoolSpec bv 4
let b = symSpec "b" :: FixedSizedBVWithBoolSpec bv 4
let c = symSpec "c" :: FixedSizedBVWithBoolSpec bv 4
let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1
(lhs, rhs, lhsName, rhsName) <-
[ (andBitsSpec a b, a, "(& a b)", "a"),
(andBitsSpec a b, b, "(& a b)", "b"),
(a, andBitsSpec a b, "a", "(& a b)"),
(b, andBitsSpec a b, "b", "(& a b)"),
(orBitsSpec a b, a, "(| a b)", "a"),
(orBitsSpec a b, b, "(| a b)", "b"),
(a, orBitsSpec a b, "a", "(| a b)"),
(b, orBitsSpec a b, "b", "(| a b)"),
(andBitsSpec a b, andBitsSpec a c, "(& a b)", "(& a c)"),
(andBitsSpec a b, andBitsSpec c a, "(& a b)", "(& c a)"),
(andBitsSpec a b, andBitsSpec b c, "(& a b)", "(& b c)"),
(andBitsSpec a b, andBitsSpec c b, "(& a b)", "(& c b)"),
(orBitsSpec a b, orBitsSpec a c, "(| a b)", "(| a c)"),
(orBitsSpec a b, orBitsSpec c a, "(| a b)", "(| c a)"),
(orBitsSpec a b, orBitsSpec b c, "(| a b)", "(| b c)"),
(orBitsSpec a b, orBitsSpec c b, "(| a b)", "(| c b)")
]
let spec = iteSpec cond lhs rhs
return $
testCase ("ite(cond," <> lhsName <> "," <> rhsName <> ")") $
validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec
)
++ ( do
trueBranch <- [True, False]
(opName, spec) <-
[("and", andBitsSpec), ("or", orBitsSpec)]
let iteName = "ite(cond,const,const)"
let name =
opName
<> "("
<> (if trueBranch then iteName else "a")
<> ","
<> (if trueBranch then "b" else iteName)
<> ")"
return $ testProperty name $ \a b -> ioProperty $ do
let ite =
iteSpec
(symSpec "cond" :: BoolWithFixedSizedBVSpec bv 4)
(conSpec a :: FixedSizedBVWithBoolSpec bv 4)
(conSpec b :: FixedSizedBVWithBoolSpec bv 4)
let s = symSpec "a" :: FixedSizedBVWithBoolSpec bv 4
let lhs = if trueBranch then ite else s
let rhs = if trueBranch then s else ite
let resSpec = spec lhs rhs
validateSpec unboundedConfig resSpec
)
++ ( do
a <- [0, 1, 4, 7, 8, 9, 16]
(opName, opSpec) <-
[ ("shr", shiftRightSpec),
("shl", shiftLeftSpec)
]
return $ testCase (opName <> "(bv8," <> show a <> ")") $ do
let spec =
opSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 8)
(conSpec a)
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
)
++ ( do
trueBranch <- [True, False]
innerTrueBranch <- [True, False]
let l = symSpec "l" :: FixedSizedBVWithBoolSpec bv 8
let r = symSpec "r" :: FixedSizedBVWithBoolSpec bv 8
let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 8
(absorbing, absorbingTerm, absorbingValueName, opName, opSpec, opTerm) <-
[ ( conSpec 0 :: FixedSizedBVWithBoolSpec bv 8,
conTerm 0 :: Term (bv 8),
"0",
"and",
andBitsSpec,
andBitsTerm
),
( conSpec $ -1 :: FixedSizedBVWithBoolSpec bv 8,
conTerm $ -1 :: Term (bv 8),
"-1",
"or",
orBitsSpec,
orBitsTerm
)
]
let condTerm = ssymTerm "cond" :: Term Bool
let lTerm = ssymTerm "l" :: Term (bv 8)
let rTerm = ssymTerm "r" :: Term (bv 8)
let (lhsName, lhs, lhsResultTerm)
| trueBranch && innerTrueBranch = ("ite(cond," <> absorbingValueName <> ",l)", iteSpec cond absorbing l, absorbingTerm)
| trueBranch && not innerTrueBranch = ("ite(cond,l," <> absorbingValueName <> ")", iteSpec cond l absorbing, opTerm lTerm rTerm)
| otherwise = ("l", l, if innerTrueBranch then absorbingTerm else opTerm lTerm rTerm)
let (rhsName, rhs, rhsResultTerm)
| trueBranch = ("r", r, if innerTrueBranch then opTerm lTerm rTerm else absorbingTerm)
| innerTrueBranch = ("ite(cond," <> absorbingValueName <> ",r)", iteSpec cond absorbing r, opTerm lTerm rTerm)
| otherwise = ("ite(cond,r," <> absorbingValueName <> ")", iteSpec cond r absorbing, absorbingTerm)
let spec@(FixedSizedBVWithBoolSpec _ rspec) = opSpec lhs rhs
return $ testCase (opName <> "(" <> lhsName <> "," <> rhsName <> ")") $ do
rspec @?= iteTerm condTerm lhsResultTerm rhsResultTerm
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
)
++ ( do
innerTrueBranch <- [0 :: Int, -1]
let innerFalseBranch = -1 - innerTrueBranch
lhsIsExtend <- [True, False]
let extendName =
"sext(ite(cond,"
<> show innerTrueBranch
<> ","
<> show innerFalseBranch
<> "))"
(opName, opSpec, opTerm) <-
[ ("and", andBitsSpec, pevalAndBitsTerm),
("or", orBitsSpec, pevalOrBitsTerm)
]
let name =
opName
<> if lhsIsExtend then "(" <> extendName <> ",c)" else "(c," <> extendName <> ")"
return $
testCase name $
do
let extend =
bvextendSpec
True
(Proxy :: Proxy 8)
( iteSpec
(symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1)
(conSpec $ fromIntegral innerTrueBranch :: FixedSizedBVWithBoolSpec bv 4)
(conSpec $ fromIntegral innerFalseBranch :: FixedSizedBVWithBoolSpec bv 4)
) ::
FixedSizedBVWithBoolSpec bv 8
let single = symSpec "c" :: FixedSizedBVWithBoolSpec bv 8
let spec@(FixedSizedBVWithBoolSpec _ r) =
if lhsIsExtend
then opSpec extend single
else opSpec single extend
let expected =
iteTerm
(ssymTerm "cond" :: Term Bool)
(opTerm (conTerm $ fromIntegral innerTrueBranch) (ssymTerm "c"))
(opTerm (conTerm $ fromIntegral innerFalseBranch) (ssymTerm "c"))
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
)
bv1Test ::
forall bv.
( SupportedNonFuncPrim (bv 1),
Num (bv 1),
Typeable bv,
PEvalBitwiseTerm (bv 1)
) =>
Test
bv1Test =
testGroup (show (typeRep @bv) <> " 1") $
( do
(opName, op, v, bvop) <-
[ ("||", orSpec, 0, andBitsTerm),
("||", orSpec, 1, orBitsTerm),
("&&", andSpec, 0, orBitsTerm),
("&&", andSpec, 1, andBitsTerm)
]
let isV = "==" <> show v
let name = "(a" <> isV <> ")" <> opName <> "(b" <> isV <> ")"
let spec@(BoolWithFixedSizedBVSpec _ r) =
op
(eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (conSpec v))
(eqvSpec (symSpec "b" :: FixedSizedBVWithBoolSpec bv 1) (conSpec v))
let expected =
eqTerm
( bvop
(ssymTerm "a" :: Term (bv 1))
(ssymTerm "b")
)
(conTerm v)
return $ testCase name $ do
r @?= expected
validateSpec @(BoolWithFixedSizedBVSpec bv 1) unboundedConfig spec
)
++ ( do
cond <- [0 :: bv 1, 1]
t <- [0 :: bv 1, 1]
let f = 1 - t
let name = "ite(a==" <> show cond <> "," <> show t <> "," <> show f <> ")"
let spec@(FixedSizedBVWithBoolSpec _ r) =
iteSpec
( eqvSpec
(symSpec "a" :: FixedSizedBVWithBoolSpec bv 1)
(conSpec cond) ::
BoolWithFixedSizedBVSpec bv 1
)
(conSpec t)
(conSpec f)
let aTerm = ssymTerm "a" :: Term (bv 1)
let expected =
if t == cond
then aTerm
else complementBitsTerm aTerm
return $ testCase name $ do
r @?= expected
validateSpec @(FixedSizedBVWithBoolSpec bv 1) unboundedConfig spec
)
++ [ testCase "(a==b)==(a==c)" $ do
let spec@(BoolWithFixedSizedBVSpec _ r) =
eqvSpec
(eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (symSpec "b") :: BoolWithFixedSizedBVSpec bv 1)
(eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (symSpec "c"))
validateSpec @(BoolWithFixedSizedBVSpec bv 1)
unboundedConfig
spec
r @?= eqTerm (ssymTerm "b" :: Term (bv 1)) (ssymTerm "c")
]
termRewritingTests :: Test
termRewritingTests =
testGroup
"TermRewriting"
[ bv1Test @WordN,
bv1Test @IntN,
bvConcatTest @WordN,
bvConcatTest @IntN,
testGroup
"Bool only"
[ testProperty "Bool only random test" $
mapSize (`min` 10) $
ioProperty . \(x :: BoolOnlySpec) -> do
validateSpec unboundedConfig x,
testCase "Regression nested ite with (ite a (ite b c d) e) with b is true" $ do
validateSpec @BoolOnlySpec
unboundedConfig
( iteSpec
(symSpec "a" :: BoolOnlySpec)
( iteSpec
(orSpec (notSpec (andSpec (symSpec "b1") (symSpec "b2"))) (symSpec "b2") :: BoolOnlySpec)
(symSpec "c")
(symSpec "d")
)
(symSpec "e")
),
testCase "Regression for pevalImpliesTerm _ false should be false" $ do
validateSpec @BoolOnlySpec
unboundedConfig
( iteSpec
(symSpec "fbool" :: BoolOnlySpec)
( notSpec
( orSpec
(orSpec (notSpec (andSpec (symSpec "gbool" :: BoolOnlySpec) (symSpec "fbool" :: BoolOnlySpec))) (symSpec "gbool" :: BoolOnlySpec))
(orSpec (symSpec "abool" :: BoolOnlySpec) (notSpec (andSpec (symSpec "gbool" :: BoolOnlySpec) (symSpec "bbool" :: BoolOnlySpec))))
)
)
(symSpec "xxx" :: BoolOnlySpec)
),
testCase "And absortion" $ do
let spec@(BoolOnlySpec _ r) =
andSpec
(orSpec (symSpec "c") (orSpec (symSpec "b") (symSpec "a")))
(andSpec (symSpec "a") (andSpec (symSpec "d") (symSpec "e")))
validateSpec @BoolOnlySpec
unboundedConfig
spec
r @?= andTerm (ssymTerm "a") (andTerm (ssymTerm "d") (ssymTerm "e")),
testCase "Or absorption" $ do
let spec@(BoolOnlySpec _ r) =
orSpec
(andSpec (symSpec "c") (andSpec (symSpec "b") (symSpec "a")))
(orSpec (symSpec "a") (orSpec (symSpec "d") (symSpec "e")))
validateSpec @BoolOnlySpec
unboundedConfig
spec
r @?= orTerm (ssymTerm "a") (orTerm (ssymTerm "d") (ssymTerm "e")),
testCase "(a==b)==(a==c)" $ do
let spec@(BoolOnlySpec _ r) =
eqvSpec
(eqvSpec (symSpec "a" :: BoolOnlySpec) (symSpec "b") :: BoolOnlySpec)
(eqvSpec (symSpec "a" :: BoolOnlySpec) (symSpec "c"))
validateSpec @BoolOnlySpec
unboundedConfig
spec
r @?= eqTerm (ssymTerm "b" :: Term Bool) (ssymTerm "c")
],
testGroup
"LIA"
[ testProperty "LIA random test" $
mapSize (`min` 10) $
ioProperty . \(x :: LIAWithBoolSpec) -> do
validateSpec unboundedConfig x,
testCase "Regression nested ite with (ite a b (ite c d e)) with c implies a" $ do
validateSpec @LIAWithBoolSpec
unboundedConfig
( iteSpec
(notSpec (eqvSpec (symSpec "v" :: LIAWithBoolSpec) (conSpec 1 :: LIAWithBoolSpec) :: BoolWithLIASpec))
(symSpec "b")
( iteSpec
(eqvSpec (symSpec "v" :: LIAWithBoolSpec) (conSpec 2 :: LIAWithBoolSpec) :: BoolWithLIASpec)
(symSpec "d")
(symSpec "d")
)
)
],
testGroup
"NRA"
[ testProperty "NRA random test" $
mapSize (`min` 5) $
ioProperty . \(x :: NRAWithBoolSpec) ->
validateSpec unboundedConfig x
],
testGroup
"Different sized signed BV"
[ testProperty "Random test" $
withMaxSuccess 1000 . mapSize (`min` 5) $
ioProperty . \(x :: (DifferentSizeBVSpec IntN 4)) -> do
validateSpec unboundedConfig x
],
testGroup
"Fixed sized signed BV"
[ testProperty "Random test on IntN 1" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 1)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 2" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 2)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 4" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 4)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 63" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 63)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 64" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 64)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 65" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 65)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on IntN 128" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 128)) -> do
validateSpec unboundedConfig x
],
testGroup
"Different sized unsigned BV"
[ testProperty "random test" $
withMaxSuccess 1000 . mapSize (`min` 5) $
ioProperty . \(x :: (DifferentSizeBVSpec WordN 4)) -> do
validateSpec unboundedConfig x
],
testGroup
"Fixed sized unsigned BV"
[ testProperty "Random test on WordN 1" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 1)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 2" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 2)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 4" $
withMaxSuccess 200 . mapSize (`min` 5) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 4)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 63" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 63)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 64" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 64)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 65" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 65)) -> do
validateSpec unboundedConfig x,
testProperty "Random test on WordN 128" $
withMaxSuccess 200 . mapSize (`min` 1) $
ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 128)) -> do
validateSpec unboundedConfig x
],
testCase "Regression: shift twice and the sum of shift amount overflows" $ do
validateSpec @(FixedSizedBVWithBoolSpec IntN 4)
unboundedConfig
( shiftRightSpec
(shiftRightSpec (symSpec "fint") (conSpec 0x5))
(conSpec 0x5)
),
testGroup
"Regression for abs on unsigned BV"
[ testCase "abs on negate" $
validateSpec @(FixedSizedBVWithBoolSpec WordN 4)
unboundedConfig
(absNumSpec (negNumSpec (symSpec "a"))),
testCase "abs on times negate" $
validateSpec @(FixedSizedBVWithBoolSpec WordN 4)
unboundedConfig
(absNumSpec (mulNumSpec (symSpec "a") (negNumSpec (symSpec "b"))))
],
testGroup
"mulNumSpec on integer"
[ testCase "times on both concrete" $ do
traverse_
(\(x, y) -> validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (conSpec y))
[(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
testCase "times on single concrete" $ do
traverse_
( \x -> do
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "a") (conSpec x)
)
[-3 .. 3],
testCase "Two times with two concrete combined" $ do
traverse_
( \(x, y) -> do
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (conSpec y) (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (symSpec "a") (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (conSpec y)
)
[(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
testCase "Two times with one concrete" $ do
traverse_
( \x -> do
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (symSpec "b") (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "b") $ mulNumSpec (symSpec "a") (conSpec x)
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "b") $ mulNumSpec (conSpec x) (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (symSpec "b")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (symSpec "b")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (symSpec "b")) (conSpec x)
)
[-3 .. 3],
testCase "times and add with two concretes combined" $ do
traverse_
( \(x, y) -> do
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ addNumSpec (conSpec y) (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ addNumSpec (symSpec "a") (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (addNumSpec (conSpec x) (symSpec "a")) (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (addNumSpec (symSpec "a") (conSpec x)) (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (conSpec x) $ mulNumSpec (conSpec y) (symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (conSpec x) $ mulNumSpec (symSpec "a") (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (conSpec y)
validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (conSpec y)
)
[(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
testCase "times concrete with negNumSpec symbolic" $ do
traverse_
( \x -> do
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (negNumSpec $ symSpec "a")
validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (negNumSpec $ symSpec "a") (conSpec x)
)
[-3 .. 3]
],
testGroup
"divisions on integer"
[ divisionTest @(GeneralSpec Integer) "div" divIntegralSpec,
divisionTest @(GeneralSpec Integer) "mod" modIntegralSpec,
divisionTest @(GeneralSpec Integer) "quot" quotIntegralSpec,
divisionTest @(GeneralSpec Integer) "rem" remIntegralSpec
],
testGroup
"divisions on signed bv"
[ divisionTest @(GeneralSpec (IntN 4)) "div" divIntegralSpec,
divisionTest @(GeneralSpec (IntN 4)) "mod" modIntegralSpec,
divisionTest @(GeneralSpec (IntN 4)) "quot" quotIntegralSpec,
divisionTest @(GeneralSpec (IntN 4)) "rem" remIntegralSpec
],
testGroup
"divisions on unsigned bv"
[ divisionTest @(GeneralSpec (WordN 4)) "div" divIntegralSpec,
divisionTest @(GeneralSpec (WordN 4)) "mod" modIntegralSpec,
divisionTest @(GeneralSpec (WordN 4)) "quot" quotIntegralSpec,
divisionTest @(GeneralSpec (WordN 4)) "rem" remIntegralSpec
],
testGroup
"FP"
[ testCase "0.0 == -0.0" $
onlyWhenBitwuzlaIsAvailable
( `validateSpec`
( eqvSpec
(conSpec 0.0 :: IEEEFPSpec 5 11)
(conSpec $ -0.0) ::
IEEEFPBoolOpSpec 5 11
)
),
testCase "-0.0 <= -0.0" $
onlyWhenBitwuzlaIsAvailable
( `validateSpec`
( leOrdSpec
(conSpec 0.0 :: IEEEFPSpec 5 11)
(conSpec $ -0.0) ::
IEEEFPBoolOpSpec 5 11
)
),
testCase "is_pos(nan)" $
onlyWhenBitwuzlaIsAvailable
( `validateSpec`
( fpTraitSpec
FPIsPositive
(conSpec fpNaN :: IEEEFPSpec 5 11) ::
IEEEFPBoolOpSpec 5 11
)
),
testCase "is_pos(+inf)" $
onlyWhenBitwuzlaIsAvailable
( `validateSpec`
( fpTraitSpec
FPIsPositive
( iteSpec
(symSpec "bool" :: BoolOnlySpec)
(conSpec fpNegativeInfinite)
(conSpec fpPositiveInfinite) ::
IEEEFPSpec 5 11
) ::
IEEEFPBoolOpSpec 5 11
)
),
testCase "regression 2" $
onlyWhenBitwuzlaIsAvailable
( `validateSpec`
( eqvSpec
(signumNumSpec (conSpec (1.175e-38) :: IEEEFPSpec 5 11))
(symSpec "b") ::
IEEEFPBoolOpSpec 5 11
)
),
testCase "test sbv bug mitigation sbv#702" $
onlyWhenBitwuzlaIsAvailable
( flip validateSpec $
IEEEFPBoolOpSpec
( fpTraitTerm
FPIsPositive
( iteTerm
(ssymTerm "bool")
(conTerm fpNegativeInfinite :: Term FP32)
(conTerm fpPositiveInfinite :: Term FP32)
)
)
(notTerm $ ssymTerm "bool")
),
testProperty "FP32BoolOp" $
withMaxSuccess 1000 . mapSize (`min` 10) $
ioProperty . \(x :: IEEEFPBoolOpSpec 5 11) ->
onlyWhenBitwuzlaIsAvailable (`validateSpec` x),
testProperty "FPRoundingModeBoolOpSpec" $
mapSize (`min` 10) $
ioProperty . \(x :: FPRoundingModeBoolOpSpec) ->
onlyWhenBitwuzlaIsAvailable (`validateSpec` x),
testGroup "fpBinaryOp" $ do
op <-
[FPMaximum, FPMinimum, FPMaximumNumber, FPMinimumNumber, FPRem]
return $ testCase (show op) $ do
let lst =
[ conSpec fpNegativeInfinite,
conSpec fpPositiveInfinite,
conSpec fpNaN,
conSpec fpPositiveZero,
conSpec fpNegativeZero,
conSpec 1,
conSpec (-1),
symSpec "a",
symSpec "b"
]
let ps =
[ fpBinaryOpSpec op l r :: IEEEFPSpec 4 4
| l <- lst,
r <- lst
]
traverse_ (validateSpec z3) ps,
testGroup "RoundingOp" $ do
let rdgen =
elements
[ conSpec rna :: FPRoundingModeSpec,
conSpec rne,
conSpec rtz,
conSpec rtp,
conSpec rtn
]
let vgen =
elements
[ conSpec fpNegativeInfinite :: IEEEFPSpec 4 4,
conSpec fpPositiveInfinite,
conSpec fpNaN,
conSpec fpPositiveZero,
conSpec fpNegativeZero,
conSpec 120,
conSpec 60,
conSpec 1,
conSpec 2,
conSpec 3,
conSpec 4,
conSpec (-1),
conSpec (-2),
conSpec (-3),
conSpec (-4),
conSpec 1.5625e-2,
conSpec 2.4e2,
conSpec 1.953125e-3,
conSpec 1.3671875e-2,
symSpec "a",
symSpec "b"
]
[ testGroup "fpRoundingUnaryOp" $ do
op <- [FPSqrt, FPRoundToIntegral]
return $
testProperty (show op) $
forAll rdgen $ \rd ->
forAll vgen $ \v ->
ioProperty $
validateSpec z3 $
fpRoundingUnaryOpSpec op rd v,
testGroup "fpRoundingBinaryOp" $ do
op <- [FPAdd, FPSub, FPMul, FPDiv]
return $
testProperty (show op) $
forAll rdgen $ \rd ->
forAll (vectorOf 2 vgen) $ \[l, r] ->
ioProperty $
validateSpec z3 $
fpRoundingBinarySpec op rd l r,
testProperty "fma" $
forAll rdgen $ \rd ->
forAll (vectorOf 3 vgen) $ \[x, y, z] ->
ioProperty $
validateSpec z3 $
fpFMASpec rd x y z
]
],
testGroup "bitCast" $ do
let bitCastCase ::
forall a b.
( Arbitrary a,
PEvalBitCastTerm a b,
SupportedNonFuncPrim a,
SupportedNonFuncPrim b
) =>
Test
bitCastCase = testProperty
(show (typeRep @a) <> " -> " <> show (typeRep @b))
$ \x ->
withMaxSuccess 10 . ioProperty $
validateSpec
z3
( bitCastSpec (conSpec x :: GeneralSpec a) ::
GeneralSpec b
)
let fromFPCase ::
forall a b.
( Arbitrary a,
Arbitrary b,
PEvalBitCastOrTerm a b,
RealFloat a,
SupportedNonFuncPrim a,
SupportedNonFuncPrim b
) =>
Test
fromFPCase = testProperty
(show (typeRep @a) <> " -> " <> show (typeRep @b))
$ \d x ->
withMaxSuccess 10 . (not (isNaN x) ==>) . ioProperty $
validateSpec
z3
( bitCastOrSpec
(conSpec d :: GeneralSpec b)
(conSpec x :: GeneralSpec a)
)
let toFPCase ::
forall a b.
( Arbitrary a,
PEvalBitCastTerm a b,
RealFloat b,
SupportedNonFuncPrim a,
SupportedNonFuncPrim b
) =>
Test
toFPCase = testProperty
(show (typeRep @a) <> " -> " <> show (typeRep @b))
$ \x ->
withMaxSuccess 10
. (not (isNaN (bitCast x :: b)) ==>)
. ioProperty
$ validateSpec
z3
( bitCastSpec (conSpec x :: GeneralSpec a) ::
GeneralSpec b
)
[ bitCastCase @(IntN 4) @(WordN 4),
bitCastCase @(WordN 4) @(IntN 4),
bitCastCase @(IntN 1) @Bool,
bitCastCase @(WordN 1) @Bool,
bitCastCase @Bool @(IntN 1),
bitCastCase @Bool @(WordN 1),
fromFPCase @(FP 3 5) @(IntN 8),
fromFPCase @(FP 3 5) @(WordN 8),
toFPCase @(IntN 8) @(FP 3 5),
toFPCase @(WordN 8) @(FP 3 5)
],
testGroup "FPConvertible" $ do
let fromFPAssertion ::
forall eb sb spec b.
( ValidFP eb sb,
PEvalIEEEFPConvertibleTerm b,
TermRewritingSpec spec b
) =>
b ->
FPRoundingMode ->
FP eb sb ->
IO ()
fromFPAssertion d rd x
| fpIsNaN x = return ()
| otherwise =
validateSpec'
z3
( con x
.== p
.&& symNot (symFpIsNaN p)
)
( fromFPOrSpec
(conSpec d :: spec)
(conSpec rd :: GeneralSpec FPRoundingMode)
( wrap (ssymTerm "p") (conTerm x) ::
GeneralSpec (FP eb sb)
) ::
spec
)
where
p = "p" :: SymFP eb sb
fromFPAssertionDirect ::
forall eb sb spec b.
( ValidFP eb sb,
PEvalIEEEFPConvertibleTerm b,
TermRewritingSpec spec b
) =>
b ->
FPRoundingMode ->
FP eb sb ->
IO ()
fromFPAssertionDirect d rd x =
validateSpec
z3
( fromFPOrSpec
(conSpec d :: spec)
(conSpec rd :: GeneralSpec FPRoundingMode)
(conSpec x :: GeneralSpec (FP eb sb))
)
fromFPCase ::
forall eb sb spec b.
( ValidFP eb sb,
Arbitrary b,
PEvalIEEEFPConvertibleTerm b,
TermRewritingSpec spec b
) =>
Bool ->
Test
fromFPCase direct = testProperty
(show (typeRep @(FP eb sb)) <> " -> " <> show (typeRep @b))
$ \(d :: b) rd (x :: FP eb sb) ->
withMaxSuccess 10 . ioProperty $
( if direct
then fromFPAssertionDirect @eb @sb @spec
else fromFPAssertion @eb @sb @spec
)
d
rd
x
toFPAssertion ::
forall eb sb b bs.
( ValidFP eb sb,
PEvalIEEEFPConvertibleTerm b,
LinkedRep b bs,
Solvable b bs,
SupportedNonFuncPrim b,
SymEq bs
) =>
FPRoundingMode ->
b ->
IO ()
toFPAssertion rd x =
validateSpec'
z3
((con x :: SymType b) .== "p")
( toFPSpec
(conSpec rd :: GeneralSpec FPRoundingMode)
(wrap (ssymTerm "p") (conTerm x) :: GeneralSpec b) ::
IEEEFPSpec eb sb
)
toFPAssertionFP ::
forall eb sb eb0 sb0.
( ValidFP eb sb,
ValidFP eb0 sb0
) =>
FPRoundingMode ->
FP eb0 sb0 ->
IO ()
toFPAssertionFP _ x | fpIsNaN x = return ()
toFPAssertionFP rd x =
validateSpec'
z3
( con x
.== p
.&& symNot (symFpIsNaN p)
)
( toFPSpec
(conSpec rd :: GeneralSpec FPRoundingMode)
( wrap (ssymTerm "p") (conTerm x) ::
GeneralSpec (FP eb0 sb0)
) ::
IEEEFPSpec eb sb
)
where
p = "p" :: SymFP eb0 sb0
toFPCase ::
forall eb sb b bs.
( ValidFP eb sb,
Arbitrary b,
PEvalIEEEFPConvertibleTerm b,
SupportedNonFuncPrim b,
LinkedRep b bs,
Solvable b bs,
SymEq bs
) =>
Test
toFPCase = testProperty
(show (typeRep @b) <> " -> " <> show (typeRep @(FP eb sb)))
$ \rd (x :: b) ->
withMaxSuccess 10 . ioProperty $
toFPAssertion @eb @sb rd x
toFPCaseFP ::
forall eb sb eb0 sb0.
( ValidFP eb sb,
ValidFP eb0 sb0
) =>
Test
toFPCaseFP = testProperty
( show (typeRep @(FP eb0 sb0))
<> " -> "
<> show (typeRep @(FP eb sb))
)
$ \rd (x :: b) ->
withMaxSuccess 10 . ioProperty $
toFPAssertionFP @eb @sb @eb0 @sb0 rd x
specialFps :: (ValidFP eb sb) => [FP eb sb]
specialFps =
[ fpPositiveZero,
fpNegativeZero,
fpPositiveInfinite,
fpNegativeInfinite,
fpNaN,
fpMaxNormalized,
fpMinNormalized,
fpMaxSubnormal,
fpMinSubnormal
]
boundFps ::
(ConvertibleBound bv, KnownNat n, 1 <= n, ValidFP eb sb) =>
bv n ->
FPRoundingMode ->
[FP eb sb]
boundFps n mode =
[ convertibleLowerBound n mode,
convertibleUpperBound n mode
]
fps ::
(ConvertibleBound bv, KnownNat n, 1 <= n, ValidFP eb sb) =>
bv n ->
FPRoundingMode ->
[FP eb sb]
fps n mode =
specialFps
++ boundFps n mode
++ (nextFP <$> boundFps n mode)
++ (prevFP <$> boundFps n mode)
boundedFromFPCase ::
forall bv n eb sb.
( ConvertibleBound bv,
KnownNat n,
1 <= n,
ValidFP eb sb,
PEvalIEEEFPConvertibleTerm (bv n),
SupportedNonFuncPrim (bv n),
Num (bv n),
Typeable bv
) =>
FPRoundingMode ->
Test
boundedFromFPCase mode =
testCase (show (typeRep @bv) ++ "/" ++ show mode) $
mapM_
( fromFPAssertion @eb @sb @(GeneralSpec (bv n))
123
mode
)
(fps (undefined :: (bv n)) mode)
boundedFromFPTestGroup ::
forall n eb sb.
( KnownNat n,
1 <= n,
ValidFP eb sb
) =>
Test
boundedFromFPTestGroup =
testGroup
( show (typeRep @(FP eb sb))
++ " -> "
++ show (typeRep @(IntN n))
++ "/"
++ show (typeRep @(WordN n))
)
$ do
mode <- [rna, rne, rtz, rtp, rtn]
[ boundedFromFPCase @IntN @n @eb @sb mode,
boundedFromFPCase @WordN @n @eb @sb mode
]
[ -- z3 is buggy with the indirect encoding
-- https://github.com/Z3Prover/z3/issues/7321
fromFPCase @4 @4 @(GeneralSpec AlgReal) True,
toFPCase @4 @4 @AlgReal,
testCase "FP 4 4 -> Integer" $ do
sequence_ $
(fromFPAssertionDirect @4 @4 @(GeneralSpec Integer) 0)
<$> [rna, rne, rtz, rtp, rtn]
<*> (specialFps ++ ((/ 4) . fromIntegral <$> [-7 .. 7])),
toFPCase @4 @4 @Integer,
fromFPCase @4 @4 @(IEEEFPSpec 3 3) False,
toFPCaseFP @4 @4 @3 @3,
fromFPCase @4 @4 @(IEEEFPSpec 5 5) False,
toFPCaseFP @4 @4 @5 @5,
toFPCase @4 @4 @(WordN 8),
toFPCase @4 @4 @(IntN 8),
boundedFromFPTestGroup @32 @4 @4,
boundedFromFPTestGroup @12 @4 @16,
boundedFromFPTestGroup @12 @4 @12,
boundedFromFPTestGroup @12 @4 @11,
boundedFromFPTestGroup @12 @4 @10,
boundedFromFPTestGroup @12 @4 @9,
boundedFromFPTestGroup @12 @4 @2,
boundedFromFPTestGroup @10 @4 @16,
boundedFromFPTestGroup @10 @4 @10,
boundedFromFPTestGroup @10 @4 @9,
boundedFromFPTestGroup @10 @4 @8,
boundedFromFPTestGroup @10 @4 @7,
boundedFromFPTestGroup @10 @4 @2,
boundedFromFPTestGroup @9 @4 @16,
boundedFromFPTestGroup @9 @4 @9,
boundedFromFPTestGroup @9 @4 @8,
boundedFromFPTestGroup @9 @4 @7,
boundedFromFPTestGroup @9 @4 @6,
boundedFromFPTestGroup @9 @4 @2,
boundedFromFPTestGroup @8 @4 @16,
boundedFromFPTestGroup @8 @4 @8,
boundedFromFPTestGroup @8 @4 @7,
boundedFromFPTestGroup @8 @4 @6,
boundedFromFPTestGroup @8 @4 @5,
boundedFromFPTestGroup @8 @4 @2,
boundedFromFPTestGroup @7 @4 @16,
boundedFromFPTestGroup @7 @4 @7,
boundedFromFPTestGroup @7 @4 @6,
boundedFromFPTestGroup @7 @4 @5,
boundedFromFPTestGroup @7 @4 @4,
boundedFromFPTestGroup @7 @4 @2,
boundedFromFPTestGroup @5 @4 @16,
boundedFromFPTestGroup @5 @4 @5,
boundedFromFPTestGroup @5 @4 @4,
boundedFromFPTestGroup @5 @4 @3,
boundedFromFPTestGroup @5 @4 @2
]
]