grisette-0.13.0.1: test/Grisette/SymPrim/SomeBVTests.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Use /=" #-}
{-# HLINT ignore "Use ==" #-}

module Grisette.SymPrim.SomeBVTests (someBVTests) where

import Control.DeepSeq (NFData, force)
import Control.Exception (ArithException (Overflow), catch, evaluate)
import Control.Monad.Except (ExceptT)
import Data.Bits
  ( Bits
      ( clearBit,
        complement,
        complementBit,
        setBit,
        shiftL,
        unsafeShiftL,
        xor,
        (.&.),
        (.|.)
      ),
    FiniteBits (finiteBitSize),
  )
import Data.Proxy (Proxy (Proxy))
import Data.Serialize (decode, encode)
import Grisette
  ( AsKey (AsKey),
    AsKey1 (AsKey1),
    BV (bv, bvConcat, bvExt, bvSelect, bvSext, bvZext),
    ITEOp (symIte),
    LogicalOp (symNot),
    Mergeable (rootStrategy),
    SafeLinearArith (safeAdd, safeSub),
    SignConversion (toSigned, toUnsigned),
    Solvable (con, isym, ssym),
    SomeBV (SomeBVLit),
    SomeWordN,
    SymEq ((./=), (.==)),
    genSym,
    genSymSimple,
    mrgIf,
    mrgReturn,
    mrgSingle,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union (Union))
import Grisette.Internal.Core.Data.UnionBase
  ( UnionBase (UnionSingle),
    ifWithLeftMost,
  )
import Grisette.Internal.SymPrim.BV (IntN)
import Grisette.Internal.SymPrim.SomeBV
  ( SomeBV (SomeBV),
    SomeBVException (BitwidthMismatch),
    SomeIntN,
    SomeSymIntN,
    arbitraryBV,
    binSomeBV,
    binSomeBVR1,
    binSomeBVR2,
    binSomeBVSafe,
    binSomeBVSafeR1,
    conBV,
    conBVView,
    isymBV,
    ssymBV,
    unarySomeBV,
    unarySomeBVR1,
    pattern ConBV,
    pattern SomeIntN,
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN)
import Grisette.Lib.Control.Monad.Except (mrgThrowError)
import Grisette.Lib.Data.Functor (mrgFmap)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (assertBool, (@?=))
import Test.QuickCheck
  ( Arbitrary (arbitrary),
    Gen,
    NonNegative (getNonNegative),
    forAll,
    ioProperty,
  )

testFuncMatch ::
  (Eq r, Show r) =>
  String ->
  (SomeIntN -> SomeIntN -> r) ->
  SomeIntN ->
  SomeIntN ->
  r ->
  Test
testFuncMatch name f a b r = testCase name $ do
  let actual = f a b
  let expected = r
  actual @?= expected

testFuncMatchLit ::
  String ->
  (SomeIntN -> SomeIntN -> SomeIntN) ->
  SomeIntN ->
  SomeIntN ->
  SomeIntN ->
  Test
testFuncMatchLit name f a b r = testCase name $ do
  let SomeBVLit actual = f a b
  let SomeBVLit expected = r
  actual @?= expected

testSymFuncMatch ::
  String ->
  (SomeSymIntN -> SomeSymIntN -> SomeSymIntN) ->
  SomeSymIntN ->
  SomeSymIntN ->
  SomeSymIntN ->
  Test
testSymFuncMatch name f a b r = testCase name $ do
  let actual = f a b
  let expected = r
  AsKey actual @?= AsKey expected

testSymFuncMatchLit ::
  String ->
  (SomeSymIntN -> SomeSymIntN -> SomeSymIntN) ->
  SomeSymIntN ->
  SomeSymIntN ->
  SomeSymIntN ->
  Test
testSymFuncMatchLit name f a b r = testCase name $ do
  let SomeBVLit actual = f a b
  let SomeBVLit expected = r
  AsKey actual @?= AsKey expected

testFuncMisMatch ::
  (NFData r, Show r, Eq r) =>
  (SomeIntN -> SomeIntN -> r) ->
  SomeIntN ->
  SomeIntN ->
  r ->
  Test
testFuncMisMatch f a b r = testCase "bit width mismatch" $ do
  actual <-
    evaluate (force $ f a b)
      `catch` \(_ :: SomeBVException) -> return r
  let expected = r
  actual @?= expected

testSafeFuncMatchException ::
  (Eq r, Show r, Mergeable r) =>
  ( SomeIntN ->
    SomeIntN ->
    ExceptT (Either SomeBVException ArithException) Union r
  ) ->
  SomeIntN ->
  SomeIntN ->
  ArithException ->
  Test
testSafeFuncMatchException f a b e = testCase "bit width match" $ do
  let actual = f a b
  let expected = mrgThrowError (Right e)
  actual @?= expected

testSafeFuncMatch ::
  (Eq r, Show r, Mergeable r) =>
  String ->
  ( SomeIntN ->
    SomeIntN ->
    ExceptT (Either SomeBVException ArithException) Union r
  ) ->
  SomeIntN ->
  SomeIntN ->
  r ->
  Test
testSafeFuncMatch name f a b r = testCase name $ do
  let actual = f a b
  let expected = mrgSingle r
  actual @?= expected

testSafeFuncMatchLit ::
  String ->
  ( SomeIntN ->
    SomeIntN ->
    Either (Either SomeBVException ArithException) SomeIntN
  ) ->
  SomeIntN ->
  SomeIntN ->
  SomeIntN ->
  Test
testSafeFuncMatchLit name f a b r = testCase name $ do
  let Right (SomeBVLit actual) = f a b
  let Right (SomeBVLit expected) = mrgSingle r
  actual @?= expected

testSafeFuncMisMatch ::
  (Eq r, Show r, Mergeable r) =>
  ( SomeIntN ->
    SomeIntN ->
    ExceptT (Either SomeBVException ArithException) Union r
  ) ->
  SomeIntN ->
  SomeIntN ->
  Test
testSafeFuncMisMatch f a b = testCase "bit width mismatch" $ do
  let actual = f a b
  let expected = mrgThrowError (Left BitwidthMismatch)
  actual @?= expected

someBVTests :: Test
someBVTests =
  testGroup
    "SomeBV"
    [ testGroup
        "Helpers"
        [ testCase "conBV" $ do
            let actual = conBV (bv 4 5)
            let expected = bv 4 5 :: SomeSymIntN
            AsKey actual @?= AsKey expected,
          testGroup
            "conBVView"
            [ testCase "is concrete" $ do
                let value = bv 4 5 :: SomeSymIntN
                let actual = conBVView value
                let expected = Just (bv 4 5)
                actual @?= expected
                case value of
                  ConBV v -> v @?= bv 4 5
                  _ -> fail "is concrete",
              testCase "is not concrete" $ do
                let value = ssymBV 4 "a" :: SomeSymIntN
                let actual = conBVView value
                let expected = Nothing
                actual @?= expected
                case value of
                  ConBV _ -> fail "is not concrete"
                  _ -> return ()
            ],
          testCase "ssymBV" $ AsKey (ssymBV 4 "a") @?= AsKey (SomeBV (ssym "a" :: SymIntN 4)),
          testCase "isymBV" $
            AsKey (isymBV 4 "a" 1) @?= AsKey (SomeBV (isym "a" 1 :: SymIntN 4)),
          testGroup
            "unarySomeBV"
            [ testCase "SomeBV" $ do
                let actual =
                      unarySomeBV @IntN @SomeIntN
                        (SomeIntN . negate)
                        undefined
                        (bv 4 5 :: SomeIntN)
                let expected = bv 4 (-5)
                actual @?= expected,
              testCase "SomeBVLit" $ do
                let SomeBVLit actual =
                      unarySomeBV @IntN @SomeIntN
                        undefined
                        (SomeBVLit . negate)
                        (5 :: SomeIntN)
                let SomeBVLit expected = SomeBVLit $ -5
                actual @?= expected
            ],
          testGroup
            "unarySomeBVR1"
            [ testCase "SomeBV" $ do
                let actual = unarySomeBVR1 negate undefined (bv 4 5 :: SomeIntN)
                let expected = bv 4 (-5)
                actual @?= expected,
              testCase "SomeBVLit" $ do
                let SomeBVLit actual =
                      unarySomeBVR1 undefined negate (SomeBVLit 5 :: SomeIntN)
                let SomeBVLit expected = SomeBVLit $ -5
                actual @?= expected
            ],
          testGroup
            "binSomeBV"
            [ testFuncMatch @SomeIntN
                "SomeBV/SomeBV"
                (binSomeBV (\l r -> SomeIntN $ l + r) undefined)
                (bv 4 5)
                (bv 4 2)
                (bv 4 7),
              testFuncMatch @SomeIntN
                "SomeBV/SomeBVLit"
                (binSomeBV (\l r -> SomeIntN $ l + r) undefined)
                (bv 4 5)
                2
                (bv 4 7),
              testFuncMatch @SomeIntN
                "SomeBVLit/SomeBV"
                (binSomeBV (\l r -> SomeIntN $ l + r) undefined)
                5
                (bv 4 2)
                (bv 4 7),
              testFuncMatchLit
                "SomeBVLit/SomeBVLit"
                (binSomeBV undefined (\l r -> SomeBVLit $ l + r))
                5
                2
                7,
              testSymFuncMatch
                "SomeBV/SomeBV"
                (binSomeBV (\l r -> SomeBV $ l + r) undefined)
                (ssymBV 4 "a")
                (ssymBV 4 "b")
                ((ssymBV 4 "a") + (ssymBV 4 "b")),
              testSymFuncMatch
                "SomeBV/SomeBVCondLit"
                (binSomeBV (\l r -> SomeBV $ l + r) undefined)
                (ssymBV 4 "a")
                (symIte "b" 5 6)
                ((ssymBV 4 "a") + symIte "b" (bv 4 5) (bv 4 6)),
              testSymFuncMatchLit
                "SomeBVCondLit/SomeBVCondLit"
                (binSomeBV undefined (\l r -> SomeBVLit $ l + r))
                (symIte "a" 5 6)
                (symIte "b" 5 6)
                (symIte "a" (symIte "b" 10 11) (symIte "b" 11 12)),
              testSymFuncMatchLit
                "SomeBVLit/SomeBVCondLit"
                (binSomeBV undefined (\l r -> SomeBVLit $ l + r))
                5
                (symIte "b" 5 6)
                (symIte "b" 10 11),
              testFuncMisMatch @SomeIntN
                (binSomeBV (\l r -> SomeIntN $ l + r) undefined)
                (bv 4 5)
                (bv 5 4)
                (bv 3 0)
            ],
          testGroup
            "binSomeBVR1"
            [ testFuncMatch
                "SomeBV/SomeBV"
                (binSomeBVR1 (+) undefined)
                (bv 4 5)
                (bv 4 2)
                (bv 4 7),
              testFuncMisMatch
                (binSomeBVR1 (+) undefined)
                (bv 4 5)
                (bv 5 4)
                (bv 3 0)
            ],
          testGroup
            "binSomeBVR2"
            [ testFuncMatch
                "SomeBV/SomeBV"
                (binSomeBVR2 (\l r -> (l + r, l - r)) undefined)
                (bv 4 5)
                (bv 4 2)
                (bv 4 7, bv 4 3),
              testFuncMisMatch
                (binSomeBVR2 (\l r -> (l + r, l - r)) undefined)
                (bv 4 5)
                (bv 5 4)
                (bv 3 0, bv 6 1)
            ],
          testGroup "binSomeBVSafe" $ do
            let func l r = mrgFmap SomeIntN $ safeAdd l r
            [ testSafeFuncMatch @SomeIntN
                "SomeBV/SomeBV"
                (binSomeBVSafe func undefined)
                (bv 4 5)
                (bv 4 2)
                (bv 4 7),
              testSafeFuncMatch @SomeIntN
                "SomeBV/SomeBVInt"
                (binSomeBVSafe func undefined)
                (bv 4 5)
                2
                (bv 4 7),
              testSafeFuncMatchLit
                "SomeBVInt/SomeBVInt"
                ( binSomeBVSafe
                    undefined
                    (\l r -> mrgReturn $ SomeBVLit $ l + r)
                )
                5
                2
                7,
              testSafeFuncMatchException @SomeIntN
                (binSomeBVSafe func undefined)
                (bv 4 5)
                (bv 4 5)
                Overflow,
              testSafeFuncMisMatch @SomeIntN
                (binSomeBVSafe func undefined)
                (bv 4 5)
                (bv 5 4)
              ],
          testGroup
            "binSomeBVSafeR1"
            [ testSafeFuncMatch
                "SomeBV/SomeBV"
                (binSomeBVSafeR1 safeAdd undefined)
                (bv 4 5)
                (bv 4 2)
                (bv 4 7),
              testSafeFuncMatchException
                (binSomeBVSafeR1 safeAdd undefined)
                (bv 4 5)
                (bv 4 5)
                Overflow,
              testSafeFuncMisMatch
                (binSomeBVSafeR1 safeAdd undefined)
                (bv 4 5)
                (bv 5 4)
            ],
          testGroup "binSomeBVSafeR2" $ do
            let func l r = do
                  a <- safeAdd l r
                  b <- safeSub l r
                  mrgSingle (a, b)
            [ testSafeFuncMatch
                "SomeBV/SomeBV"
                func
                (bv 4 5)
                (bv 4 2)
                (bv 4 7, bv 4 3),
              testSafeFuncMatchException
                func
                (bv 4 5)
                (bv 4 5)
                Overflow,
              testSafeFuncMisMatch func (bv 4 5) (bv 5 4)
              ]
        ],
      testGroup
        "BV"
        [ testCase "bvConcat" $ do
            bvConcat (bv 8 0x14 :: SomeIntN) (bv 4 2) @?= bv 12 0x142,
          testCase "bvZext" $ do
            bvZext 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0x08,
          testCase "bvSext" $ do
            bvSext 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0xF8,
          testCase "bvExt" $ do
            bvExt 8 (bv 4 0x8 :: SomeIntN) @?= bv 8 0xF8
            bvExt 8 (bv 4 0x8 :: SomeWordN) @?= bv 8 0x08,
          testCase "bvSelect" $ do
            bvSelect 1 4 (bv 8 0x17 :: SomeIntN) @?= bv 4 0xB,
          testCase "bv" $ bv 8 0x14 @?= (SomeIntN (0x14 :: IntN 8))
        ],
      testGroup
        "Mergeable"
        [ testGroup "SomeIntN" $ do
            (name, l, r, merged) <-
              [ ( "same bitwidth",
                  bv 4 3,
                  bv 4 5,
                  ifWithLeftMost
                    True
                    "cond"
                    (UnionSingle $ bv 4 3)
                    (UnionSingle $ bv 4 5)
                ),
                ( "same bitwidth, should invert",
                  bv 4 5,
                  bv 4 2,
                  ifWithLeftMost
                    True
                    (symNot "cond")
                    (UnionSingle $ bv 4 2)
                    (UnionSingle $ bv 4 5)
                ),
                ( "different bitwidth",
                  bv 4 5,
                  bv 5 4,
                  ifWithLeftMost
                    True
                    "cond"
                    (UnionSingle $ bv 4 5)
                    (UnionSingle $ bv 5 4)
                ),
                ( "different bitwidth, should invert",
                  bv 5 4,
                  bv 4 5,
                  ifWithLeftMost
                    True
                    (symNot "cond")
                    (UnionSingle $ bv 4 5)
                    (UnionSingle $ bv 5 4)
                )
              ]
            return $ testCase name $ do
              let actual =
                    mrgIf "cond" (return l) (return r) :: Union SomeIntN
              let expected = Union (Just rootStrategy) merged
              AsKey actual @?= AsKey expected,
          testGroup "SomeSymIntN" $ do
            (name, l, r, merged) <-
              [ ( "same bitwidth",
                  ssymBV 4 "a",
                  ssymBV 4 "b",
                  (UnionSingle $ AsKey $ symIte "cond" (ssymBV 4 "a") (ssymBV 4 "b"))
                ),
                ( "different bitwidth",
                  ssymBV 4 "a",
                  ssymBV 5 "b",
                  ifWithLeftMost
                    True
                    "cond"
                    (UnionSingle $ AsKey $ ssymBV 4 "a")
                    (UnionSingle $ AsKey $ ssymBV 5 "b")
                ),
                ( "different bitwidth, should invert",
                  ssymBV 5 "b",
                  ssymBV 4 "a",
                  ifWithLeftMost
                    True
                    (symNot "cond")
                    (UnionSingle $ AsKey $ ssymBV 4 "a")
                    (UnionSingle $ AsKey $ ssymBV 5 "b")
                )
              ]
            return $ testCase name $ do
              let actual =
                    mrgIf
                      "cond"
                      (return $ AsKey l)
                      (return $ AsKey r) ::
                      Union (AsKey SomeSymIntN)
              let expected = Union (Just rootStrategy) merged
              AsKey1 actual @?= AsKey1 expected
        ],
      testGroup
        "GenSym"
        [ testCase "Proxy n" $ do
            let actual = genSym (Proxy :: Proxy 4) "a" :: Union (AsKey SomeSymIntN)
            let expected = mrgSingle $ AsKey $ isymBV 4 "a" 0
            AsKey1 actual @?= AsKey1 expected,
          testCase "SomeBV" $ do
            let actual =
                  genSym (bv 4 1 :: SomeSymIntN) "a" :: Union (AsKey SomeSymIntN)
            let expected = mrgSingle $ AsKey $ isymBV 4 "a" 0
            AsKey1 actual @?= AsKey1 expected,
          testCase "Int" $ do
            let actual =
                  genSym (4 :: Int) "a" :: Union (AsKey SomeSymIntN)
            let expected = mrgSingle $ AsKey $ isymBV 4 "a" 0
            AsKey1 actual @?= AsKey1 expected
        ],
      testGroup
        "GenSymSimple"
        [ testCase "Proxy n" $ do
            let actual = genSymSimple (Proxy :: Proxy 4) "a" :: SomeSymIntN
            let expected = isymBV 4 "a" 0
            AsKey actual @?= AsKey expected,
          testCase "SomeBV" $ do
            let actual =
                  genSymSimple (bv 4 1 :: SomeSymIntN) "a" :: SomeSymIntN
            let expected = isymBV 4 "a" 0
            AsKey actual @?= AsKey expected,
          testCase "Int" $ do
            let actual = genSymSimple (4 :: Int) "a" :: SomeSymIntN
            let expected = isymBV 4 "a" 0
            AsKey actual @?= AsKey expected
        ],
      testProperty "arbitraryBV" $
        forAll (arbitraryBV 4) $
          \(bv :: SomeIntN) -> ioProperty $ finiteBitSize bv @?= 4,
      testGroup
        "Eq"
        [ testCase "same bitwidth equal" $ do
            let a = bv 4 5 :: SomeIntN
            let b = bv 4 5 :: SomeIntN
            assertBool "SomeBV with same bitwidth should compare the value" $
              a == b
            assertBool "SomeBV with same bitwidth should compare the value" $
              not $
                a /= b,
          testProperty "==/SomeBV/SomeBVLit" $ \(a :: Integer) (b :: Integer) ->
            let ai = fromIntegral a :: SomeWordN
                bi = fromIntegral b :: SomeWordN
                ab = bv 4 a :: SomeWordN
                bb = bv 4 b :: SomeWordN
             in (ai == bb) == (ab == bb)
                  && (ab == bi) == (ab == bb)
                  && ai == ab,
          testProperty "/=/SomeBV/SomeBVLit" $ \(a :: Integer) (b :: Integer) ->
            let ai = fromIntegral a :: SomeWordN
                bi = fromIntegral b :: SomeWordN
                ab = bv 4 a :: SomeWordN
                bb = bv 4 b :: SomeWordN
             in (ai /= bb) == (ab /= bb)
                  && (ab /= bi) == (ab /= bb)
                  && not (ai /= ab),
          testCase "same bitwidth not equal" $ do
            let a = bv 4 4 :: SomeIntN
            let b = bv 4 5 :: SomeIntN
            assertBool "SomeBV with same bitwidth should compare the value" $
              not $
                a == b
            assertBool "SomeBV with same bitwidth should compare the value" $
              a /= b,
          testCase "different bitwidth" $ do
            let a = bv 3 5 :: SomeIntN
            let b = bv 4 5 :: SomeIntN
            assertBool "SomeBV with different bit width are not equal" $
              not $
                a == b
            assertBool "SomeBV with different bit width are not equal" $ a /= b
        ],
      testGroup
        "SymEq"
        [ testCase "same bitwidth" $ do
            let a = ssymBV 4 "a" :: SomeSymIntN
            let b = ssymBV 4 "b" :: SomeSymIntN
            AsKey (a .== b) @?= AsKey (("a" :: SymIntN 4) .== "b")
            AsKey (a ./= b) @?= AsKey (("a" :: SymIntN 4) ./= "b"),
          testCase "different bitwidth" $ do
            let a = ssymBV 4 "a" :: SomeSymIntN
            let b = ssymBV 3 "b" :: SomeSymIntN
            AsKey (a .== b) @?= AsKey (con False)
            AsKey (a ./= b) @?= AsKey (con True)
        ],
      testGroup
        "Num"
        [ testGroup
            "SomeIntN"
            [ binOpLitTest @SomeIntN (+) "+",
              binOpLitTest @SomeIntN (-) "-",
              unaryOpLitTest @SomeIntN negate "negate"
            ],
          testGroup
            "SomeWordN"
            [ binOpLitTest @SomeWordN (+) "+",
              binOpLitTest @SomeWordN (-) "-",
              unaryOpLitTest @SomeWordN negate "negate"
            ]
        ],
      testGroup
        "SignConversion"
        [ testGroup
            "SomeIntN"
            [unaryOpLitTest @SomeIntN toUnsigned "toUnsigned"],
          testGroup
            "SomeWordN"
            [unaryOpLitTest @SomeWordN toSigned "toSigned"]
        ],
      testGroup
        "Bits"
        [ testGroup
            "SomeIntN"
            [ binOpLitTest @SomeIntN (.&.) ".&.",
              binOpLitTest @SomeIntN (.|.) ".|.",
              binOpLitTest @SomeIntN xor "xor",
              unaryOpLitTest @SomeIntN complement "complement",
              binIntOpLitTest @SomeIntN
                (getNonNegative <$> arbitrary)
                setBit
                "setBit",
              binIntOpLitTest @SomeIntN
                (getNonNegative <$> arbitrary)
                clearBit
                "clearBit",
              binIntOpLitTest @SomeIntN
                (getNonNegative <$> arbitrary)
                complementBit
                "complementBit",
              binIntOpLitTest @SomeIntN
                (getNonNegative <$> arbitrary)
                shiftL
                "shiftL",
              binIntOpLitTest @SomeIntN
                (getNonNegative <$> arbitrary)
                unsafeShiftL
                "unsafeShiftL"
            ],
          testGroup
            "SomeWordN"
            [ binOpLitTest @SomeWordN (.&.) ".&.",
              binOpLitTest @SomeWordN (.|.) ".|.",
              binOpLitTest @SomeWordN xor "xor",
              unaryOpLitTest @SomeWordN complement "complement",
              binIntOpLitTest @SomeWordN
                (getNonNegative <$> arbitrary)
                setBit
                "setBit",
              binIntOpLitTest @SomeWordN
                (getNonNegative <$> arbitrary)
                clearBit
                "clearBit",
              binIntOpLitTest @SomeWordN
                (getNonNegative <$> arbitrary)
                complementBit
                "complementBit",
              binIntOpLitTest @SomeWordN
                (getNonNegative <$> arbitrary)
                shiftL
                "shiftL",
              binIntOpLitTest @SomeWordN
                (getNonNegative <$> arbitrary)
                unsafeShiftL
                "unsafeShiftL"
            ]
        ],
      testProperty "Serialize" $ forAll (arbitraryBV 8) $ \(v :: SomeWordN) ->
        Right v == decode (encode v)
    ]

binOpLitTest ::
  forall bv r. (Num bv, Eq r, BV bv) => (bv -> bv -> r) -> String -> Test
binOpLitTest f name =
  testProperty (name ++ "/SomeBV/SomeBVLit") $ \(a :: Integer) (b :: Integer) ->
    let ai = fromIntegral a :: bv
        bi = fromIntegral b :: bv
        ab = bv 4 a :: bv
        bb = bv 4 b :: bv
     in (f ai bb) == (f ab bb)
          && (f ab bi) == (f ab bb)
          && (f ai bi) == (f ab bb)

binIntOpLitTest ::
  forall bv.
  (Num bv, Eq bv, BV bv) =>
  Gen Int ->
  (bv -> Int -> bv) ->
  String ->
  Test
binIntOpLitTest gen f name =
  testProperty (name ++ "/SomeBV/SomeBVLit") $ \(a :: Integer) -> forAll gen $
    \(b :: Int) ->
      let ai = fromIntegral a :: bv
          ab = bv 4 a :: bv
       in (f ai b) == (f ab b)
            && (f ab b) == (f ab b)
            && (f ai b) == (f ab b)

unaryOpLitTest ::
  forall bv r. (Num bv, Eq r, BV bv) => (bv -> r) -> String -> Test
unaryOpLitTest f name =
  testProperty (name ++ "/SomeBV/SomeBVLit") $ \(a :: Integer) ->
    let ai = fromIntegral a :: bv
        ab = bv 4 a :: bv
     in f ai == f ab