grisette-0.13.0.1: 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 Data.Data (Proxy (Proxy))
import Grisette (IntN, SupportedPrim, WordN)
import Grisette.Internal.SymPrim.Prim.Term
( PEvalBitwiseTerm
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalXorBitsTerm
),
PEvalRotateTerm
( pevalRotateLeftTerm,
pevalRotateRightTerm
),
PEvalShiftTerm
( pevalShiftLeftTerm,
pevalShiftRightTerm
),
Term,
andBitsTerm,
bvConcatTerm,
bvExtendTerm,
bvSelectTerm,
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)) (ssymTerm "b")
@?= shiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b"),
testCase "shift symbolic by concrete" $ do
pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@?= bvConcatTerm
(bvSelectTerm (Proxy @0) (Proxy @2) (ssymTerm "a" :: Term (WordN 4)))
(conTerm 0 :: Term (WordN 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" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
@?= bvExtendTerm
True
(Proxy @4)
( bvSelectTerm
(Proxy @3)
(Proxy @1)
(ssymTerm "a" :: Term (IntN 4))
)
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
@?= bvExtendTerm
True
(Proxy @4)
( bvSelectTerm
(Proxy @3)
(Proxy @1)
(ssymTerm "a" :: Term (IntN 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)) (ssymTerm "b")
@?= shiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b"),
testCase "shift symbolic by concrete" $ do
pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
@?= bvConcatTerm
(conTerm 0 :: Term (WordN 2))
(bvSelectTerm (Proxy @2) (Proxy @2) (ssymTerm "a" :: Term (WordN 4)))
pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 2)
@?= bvExtendTerm
True
(Proxy @4)
(bvSelectTerm (Proxy @2) (Proxy @2) (ssymTerm "a" :: Term (IntN 4))),
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, SupportedPrim a) =>
a ->
a ->
Property
concreteSmallRotateRightCorrect _ b | b < 0 = discard
concreteSmallRotateRightCorrect a b = ioProperty $ do
pevalRotateRightTerm (conTerm a) (conTerm b)
@?= conTerm (rotateR a (fromIntegral b))