grisette-0.5.0.0: test/Grisette/SymPrim/Prim/BitsTests.hs
{-# LANGUAGE BinaryLiterals #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Grisette.SymPrim.Prim.BitsTests (bitsTests) where
import Data.Bits (Bits (rotateL, rotateR), FiniteBits)
import Grisette
( IntN,
SymRotate,
WordN,
)
import Grisette.Internal.SymPrim.Prim.Term
( PEvalBitwiseTerm
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalXorBitsTerm
),
PEvalRotateTerm
( pevalRotateLeftTerm,
pevalRotateRightTerm
),
PEvalShiftTerm
( pevalShiftLeftTerm,
pevalShiftRightTerm
),
Term,
andBitsTerm,
complementBitsTerm,
conTerm,
orBitsTerm,
rotateLeftTerm,
rotateRightTerm,
shiftLeftTerm,
shiftRightTerm,
ssymTerm,
xorBitsTerm,
)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit ((@=?))
import Test.QuickCheck (Property, discard, ioProperty)
bitsTests :: Test
bitsTests =
testGroup
"Bits"
[ testGroup
"AndBits"
[ testCase "On both concrete" $ do
pevalAndBitsTerm
(conTerm 3 :: Term (WordN 4))
(conTerm 5)
@=? conTerm 1,
testCase "On zeroBits" $ do
pevalAndBitsTerm
(conTerm 0 :: Term (WordN 4))
(ssymTerm "a")
@=? conTerm 0
pevalAndBitsTerm
(ssymTerm "a")
(conTerm 0 :: Term (WordN 4))
@=? conTerm 0,
testCase "On all one bits" $ do
pevalAndBitsTerm
(conTerm 15 :: Term (WordN 4))
(ssymTerm "a")
@=? ssymTerm "a"
pevalAndBitsTerm
(ssymTerm "a")
(conTerm 15 :: Term (WordN 4))
@=? ssymTerm "a",
testCase "On symbolic" $ do
pevalAndBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b")
@=? andBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
],
testGroup
"OrBits"
[ testCase "On both concrete" $ do
pevalOrBitsTerm
(conTerm 3 :: Term (WordN 4))
(conTerm 5)
@=? conTerm 7,
testCase "On zeroBits" $ do
pevalOrBitsTerm
(conTerm 0 :: Term (WordN 4))
(ssymTerm "a")
@=? ssymTerm "a"
pevalOrBitsTerm
(ssymTerm "a")
(conTerm 0 :: Term (WordN 4))
@=? ssymTerm "a",
testCase "On all one bits" $ do
pevalOrBitsTerm
(conTerm 15 :: Term (WordN 4))
(ssymTerm "a")
@=? conTerm 15
pevalOrBitsTerm
(ssymTerm "a")
(conTerm 15 :: Term (WordN 4))
@=? conTerm 15,
testCase "On symbolic" $ do
pevalOrBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b")
@=? orBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
],
testGroup
"XorBits"
[ testCase "On both concrete" $ do
pevalXorBitsTerm
(conTerm 3 :: Term (WordN 4))
(conTerm 5)
@=? conTerm 6,
testCase "On zeroBits" $ do
pevalXorBitsTerm
(conTerm 0 :: Term (WordN 4))
(ssymTerm "a")
@=? ssymTerm "a"
pevalXorBitsTerm
(ssymTerm "a")
(conTerm 0 :: Term (WordN 4))
@=? ssymTerm "a",
testCase "On all one bits" $ do
pevalXorBitsTerm
(conTerm 15 :: Term (WordN 4))
(ssymTerm "a")
@=? pevalComplementBitsTerm (ssymTerm "a")
pevalXorBitsTerm
(ssymTerm "a")
(conTerm 15 :: Term (WordN 4))
@=? pevalComplementBitsTerm (ssymTerm "a"),
testCase "On single complement" $ do
pevalXorBitsTerm
(pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b")
@=? pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"))
pevalXorBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(pevalComplementBitsTerm $ ssymTerm "b")
@=? pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b")),
testCase "On both complement" $ do
pevalXorBitsTerm
(pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
(pevalComplementBitsTerm $ ssymTerm "b")
@=? pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"),
testCase "On symbolic" $ do
pevalXorBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b")
@=? xorBitsTerm
(ssymTerm "a" :: Term (WordN 4))
(ssymTerm "b" :: Term (WordN 4))
],
testGroup
"ComplementBits"
[ testCase "On concrete" $ do
pevalComplementBitsTerm (conTerm 5 :: Term (WordN 4)) @=? conTerm 10,
testCase "On complement" $ do
pevalComplementBitsTerm (pevalComplementBitsTerm (ssymTerm "a") :: Term (WordN 4)) @=? ssymTerm "a",
testCase "On symbolic" $ do
pevalComplementBitsTerm (ssymTerm "a" :: Term (WordN 4))
@=? complementBitsTerm (ssymTerm "a" :: Term (WordN 4))
],
testGroup
"ShiftLeft"
[ testCase "On concrete" $ do
pevalShiftLeftTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @=? conTerm 12
pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @=? conTerm 12,
testCase "shift 0" $ do
pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
testCase "shift greater or equal to left bitsize" $ do
pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @=? conTerm 0
pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4) @=? conTerm 0
pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @=? conTerm 0
pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5) @=? conTerm 0,
testCase "shift negative amount is undefined on for IntN" $ do
pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
@=? shiftLeftTerm (conTerm 15) (conTerm $ -1)
pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
@=? shiftLeftTerm (conTerm 15) (conTerm $ -8),
testCase "shift symbolic" $ do
pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@=? shiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
testCase "Regression: shift by very large number" $ do
pevalShiftLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm 0
pevalShiftLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm 0
],
testGroup
"ShiftRight"
[ testCase "On concrete, should perform arithmetic shifting on IntN" $ do
pevalShiftRightTerm (conTerm 7 :: Term (IntN 4)) (conTerm 2) @=? conTerm 1
pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @=? conTerm 15,
testCase "On concrete, should perform logical shifting on WordN" $ do
pevalShiftRightTerm (conTerm 7 :: Term (WordN 4)) (conTerm 2) @=? conTerm 1
pevalShiftRightTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @=? conTerm 3,
testCase "shift 0" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
testCase "shift greater or equal to left bitsize on WordN" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @=? conTerm 0
pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @=? conTerm 0,
testCase "shift greater or equal to left bitsize on IntN will not be reduced" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
@=? shiftRightTerm (ssymTerm "a") (conTerm 5)
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
@=? shiftRightTerm (ssymTerm "a") (conTerm 4),
testCase "shift negative amount is undefined on for IntN" $ do
pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
@=? shiftRightTerm (conTerm 15) (conTerm $ -1)
pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
@=? shiftRightTerm (conTerm 15) (conTerm $ -8),
testCase "shift symbolic" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@=? shiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
testCase "Regression: shift by very large number" $ do
pevalShiftRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm 0
pevalShiftRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm 0
],
testGroup
"RotateLeft"
[ testCase "On concrete" $ do
pevalRotateLeftTerm (conTerm 0b10100101 :: Term (WordN 8)) (conTerm 2) @=? conTerm 0b10010110
pevalRotateLeftTerm (conTerm 0b10100101 :: Term (IntN 8)) (conTerm 2) @=? conTerm 0b10010110,
testCase "rotate 0" $ do
pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
testCase "rotate bitsize" $ do
pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
@=? ssymTerm "a"
pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
@=? ssymTerm "a",
testCase "rotate greater than left bitsize" $ do
pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
@=? rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
@=? rotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
testCase "rotate negative amount is undefined on for IntN" $ do
pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
@=? rotateLeftTerm (conTerm 15) (conTerm $ -1)
pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
@=? rotateLeftTerm (conTerm 15) (conTerm $ -8),
testCase "rotate symbolic" $ do
pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@=? rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
testCase "Regression: rotate by very large number" $ do
pevalRotateLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm (rotateR 15 1)
pevalRotateLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm (rotateR 15 1)
],
testGroup
"RotateRight"
[ testProperty "On concrete WordN 1" $
concreteSmallRotateRightCorrect @(WordN 1),
testProperty "On concrete WordN 2" $
concreteSmallRotateRightCorrect @(WordN 2),
testProperty "On concrete WordN 3" $
concreteSmallRotateRightCorrect @(WordN 3),
testProperty "On concrete WordN 4" $
concreteSmallRotateRightCorrect @(WordN 4),
testProperty "On concrete WordN 8" $
concreteSmallRotateRightCorrect @(WordN 8),
testProperty "On concrete IntN 1" $
concreteSmallRotateRightCorrect @(IntN 1),
testProperty "On concrete IntN 2" $
concreteSmallRotateRightCorrect @(IntN 2),
testProperty "On concrete IntN 3" $
concreteSmallRotateRightCorrect @(IntN 3),
testProperty "On concrete IntN 4" $
concreteSmallRotateRightCorrect @(IntN 4),
testProperty "On concrete IntN 8" $
concreteSmallRotateRightCorrect @(IntN 8),
testCase "rotate 0" $ do
pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @=? ssymTerm "a"
pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @=? ssymTerm "a",
testCase "rotate bitsize" $ do
pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
@=? ssymTerm "a"
pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
@=? ssymTerm "a",
testCase "rotate greater than left bitsize" $ do
pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
@=? rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
@=? rotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
testCase "rotate negative amount is undefined on for IntN" $ do
pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
@=? rotateRightTerm (conTerm 15) (conTerm $ -1)
pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
@=? rotateRightTerm (conTerm 15) (conTerm $ -8),
testCase "rotate symbolic" $ do
pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@=? rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
testCase "Regression: rotate by very large number" $ do
pevalRotateRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @=? conTerm (rotateL 15 1)
pevalRotateRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @=? conTerm (rotateL 15 1)
]
]
concreteSmallRotateRightCorrect ::
(PEvalRotateTerm a, Integral a, FiniteBits a, SymRotate a) =>
a ->
a ->
Property
concreteSmallRotateRightCorrect _ b | b < 0 = discard
concreteSmallRotateRightCorrect a b = ioProperty $ do
pevalRotateRightTerm (conTerm a) (conTerm b)
@=? conTerm (rotateR a (fromIntegral b))