From 4ebfdf0c5160695edd9aa2efb4aaba61dca5f67c Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Sun, 9 Feb 2025 19:43:58 -0800 Subject: [PATCH] :sparkles: Add more rewrites --- .../Prim/Internal/Instances/PEvalShiftTerm.hs | 142 ++++++++++++++---- .../Internal/SymPrim/Prim/Internal/Term.hs | 83 ++++++++-- test/Grisette/Backend/TermRewritingTests.hs | 115 ++++++++++++-- 3 files changed, 285 insertions(+), 55 deletions(-) diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs index efbb2a91..56297e22 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalShiftTerm.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -23,11 +24,13 @@ where import Data.Bits (Bits (isSigned, shiftR, zeroBits), FiniteBits (finiteBitSize)) import Data.Proxy (Proxy (Proxy)) -import GHC.TypeLits (KnownNat, type (<=)) +import Data.Typeable ((:~:) (Refl)) +import GHC.TypeLits (KnownNat, type (+), type (<=)) import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift)) import Grisette.Internal.SymPrim.BV (IntN, WordN) import Grisette.Internal.SymPrim.Prim.Internal.Term - ( PEvalShiftTerm + ( PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm), + PEvalShiftTerm ( pevalShiftLeftTerm, pevalShiftRightTerm, withSbvShiftTermConstraint @@ -39,18 +42,37 @@ import Grisette.Internal.SymPrim.Prim.Internal.Term conTerm, shiftLeftTerm, shiftRightTerm, + unsafePevalBVSelectTerm, pattern ConTerm, pattern SupportedTerm, ) import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce) +import Grisette.Internal.Utils.Parameterized + ( LeqProof (LeqProof), + NatRepr, + SomePositiveNatRepr (SomePositiveNatRepr), + mkPositiveNatRepr, + natRepr, + subNat, + unsafeAxiom, + unsafeLeqProof, + ) -- | Partial evaluation of symbolic shift left term for finite bits types. pevalFiniteBitsSymShiftShiftLeftTerm :: - forall a. - (Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) => - Term a -> - Term a -> - Term a + forall bv n. + ( forall m. (KnownNat m, 1 <= m) => Integral (bv m), + forall m. (KnownNat m, 1 <= m) => SymShift (bv m), + forall m. (KnownNat m, 1 <= m) => FiniteBits (bv m), + forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m), + forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), + PEvalBVTerm bv, + KnownNat n, + 1 <= n + ) => + Term (bv n) -> + Term (bv n) -> + Term (bv n) pevalFiniteBitsSymShiftShiftLeftTerm t@SupportedTerm n = unaryUnfoldOnce (`doPevalFiniteBitsSymShiftShiftLeftTerm` n) @@ -58,11 +80,19 @@ pevalFiniteBitsSymShiftShiftLeftTerm t@SupportedTerm n = t doPevalFiniteBitsSymShiftShiftLeftTerm :: - forall a. - (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => - Term a -> - Term a -> - Maybe (Term a) + forall bv n. + ( forall m. (KnownNat m, 1 <= m) => Integral (bv m), + forall m. (KnownNat m, 1 <= m) => SymShift (bv m), + forall m. (KnownNat m, 1 <= m) => FiniteBits (bv m), + forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m), + forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), + PEvalBVTerm bv, + KnownNat n, + 1 <= n + ) => + Term (bv n) -> + Term (bv n) -> + Maybe (Term (bv n)) doPevalFiniteBitsSymShiftShiftLeftTerm (ConTerm a) (ConTerm n) | n >= 0 = if (fromIntegral n :: Integer) >= fromIntegral (finiteBitSize n) @@ -73,17 +103,45 @@ doPevalFiniteBitsSymShiftShiftLeftTerm x (ConTerm 0) = Just x -- doPevalShiftLeftTerm (ShiftLeftTerm _ x (ConTerm n)) (ConTerm n1) -- | n >= 0 && n1 >= 0 = Just $ pevalShiftLeftTerm x (conTerm $ n + n1) doPevalFiniteBitsSymShiftShiftLeftTerm _ (ConTerm n) - | n >= 0 && (fromIntegral n :: Integer) >= fromIntegral (finiteBitSize n) = + | n > 0 && (fromIntegral n :: Integer) >= fromIntegral (finiteBitSize n) = Just $ conTerm zeroBits +doPevalFiniteBitsSymShiftShiftLeftTerm x (ConTerm shiftAmount) + | shiftAmount > 0 = + case (namount, nremaining) of + ( SomePositiveNatRepr (_ :: NatRepr amount), + SomePositiveNatRepr (nremaining :: NatRepr remaining) + ) -> + case ( unsafeLeqProof @remaining @n, + unsafeAxiom @(remaining + amount) @n + ) of + (LeqProof, Refl) -> + Just $ + pevalBVConcatTerm + (unsafePevalBVSelectTerm nn (natRepr @0) nremaining x) + (conTerm zeroBits :: Term (bv amount)) + where + nn = natRepr @n + namount = mkPositiveNatRepr $ fromIntegral shiftAmount + nremaining = + mkPositiveNatRepr $ + fromIntegral (finiteBitSize shiftAmount) - fromIntegral shiftAmount doPevalFiniteBitsSymShiftShiftLeftTerm _ _ = Nothing -- | Partial evaluation of symbolic shift right term for finite bits types. pevalFiniteBitsSymShiftShiftRightTerm :: - forall a. - (Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) => - Term a -> - Term a -> - Term a + forall bv n. + ( forall m. (KnownNat m, 1 <= m) => Integral (bv m), + forall m. (KnownNat m, 1 <= m) => SymShift (bv m), + forall m. (KnownNat m, 1 <= m) => FiniteBits (bv m), + forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m), + forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), + PEvalBVTerm bv, + KnownNat n, + 1 <= n + ) => + Term (bv n) -> + Term (bv n) -> + Term (bv n) pevalFiniteBitsSymShiftShiftRightTerm t@SupportedTerm n = unaryUnfoldOnce (`doPevalFiniteBitsSymShiftShiftRightTerm` n) @@ -91,11 +149,19 @@ pevalFiniteBitsSymShiftShiftRightTerm t@SupportedTerm n = t doPevalFiniteBitsSymShiftShiftRightTerm :: - forall a. - (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => - Term a -> - Term a -> - Maybe (Term a) + forall bv n. + ( forall m. (KnownNat m, 1 <= m) => Integral (bv m), + forall m. (KnownNat m, 1 <= m) => SymShift (bv m), + forall m. (KnownNat m, 1 <= m) => FiniteBits (bv m), + forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m), + forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), + PEvalBVTerm bv, + KnownNat n, + 1 <= n + ) => + Term (bv n) -> + Term (bv n) -> + Maybe (Term (bv n)) doPevalFiniteBitsSymShiftShiftRightTerm (ConTerm a) (ConTerm n) | n >= 0 && not (isSigned a) = if (fromIntegral n :: Integer) >= fromIntegral (finiteBitSize n) @@ -107,10 +173,34 @@ doPevalFiniteBitsSymShiftShiftRightTerm (ConTerm a) (ConTerm n) doPevalFiniteBitsSymShiftShiftRightTerm x (ConTerm 0) = Just x -- doPevalFiniteBitsSymShiftShiftRightTerm (ShiftRightTerm _ x (ConTerm n)) (ConTerm n1) -- | n >= 0 && n1 >= 0 = Just $ pevalFiniteBitsSymShiftShiftRightTerm x (conTerm $ n + n1) -doPevalFiniteBitsSymShiftShiftRightTerm _ (ConTerm n) - | not (isSigned n) - && (fromIntegral n :: Integer) >= fromIntegral (finiteBitSize n) = +doPevalFiniteBitsSymShiftShiftRightTerm x (ConTerm shiftAmount) + | not (isSigned shiftAmount) + && (fromIntegral shiftAmount :: Integer) >= fromIntegral (finiteBitSize shiftAmount) = Just $ conTerm zeroBits + | isSigned shiftAmount + && (fromIntegral shiftAmount :: Integer) >= fromIntegral (finiteBitSize shiftAmount) = + Just $ pevalBVExtendTerm True nn $ unsafePevalBVSelectTerm nn nnp1 none x + where + nn = natRepr @n + none = natRepr @1 + nnp1 = subNat nn none +doPevalFiniteBitsSymShiftShiftRightTerm x (ConTerm shiftAmount) + | shiftAmount > 0 = + case (namount, nremaining) of + ( SomePositiveNatRepr namount, + SomePositiveNatRepr (nremaining :: NatRepr remaining) + ) -> + case unsafeLeqProof @remaining @n of + LeqProof -> + Just $ + pevalBVExtendTerm (isSigned shiftAmount) nn $ + unsafePevalBVSelectTerm nn namount nremaining x + where + nn = natRepr @n + namount = mkPositiveNatRepr $ fromIntegral shiftAmount + nremaining = + mkPositiveNatRepr $ + fromIntegral (finiteBitSize shiftAmount) - fromIntegral shiftAmount doPevalFiniteBitsSymShiftShiftRightTerm _ _ = Nothing instance (KnownNat n, 1 <= n) => PEvalShiftTerm (IntN n) where diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs index 91338941..1d626a61 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs @@ -271,6 +271,7 @@ module Grisette.Internal.SymPrim.Prim.Internal.Term unsafePevalBVConcatTerm, unsafePevalBVExtendTerm, unsafePevalBVSelectTerm, + boolToBVTerm, -- * num pevalDefaultAddNumTerm, @@ -328,7 +329,10 @@ import qualified Control.Monad.Writer.Lazy as Lazy import qualified Control.Monad.Writer.Strict as Strict import Data.Atomics (atomicModifyIORefCAS_) import qualified Data.Binary as Binary -import Data.Bits (Bits (complement, isSigned, xor, zeroBits, (.&.), (.|.)), FiniteBits (countLeadingZeros)) +import Data.Bits + ( Bits (complement, isSigned, xor, zeroBits, (.&.), (.|.)), + FiniteBits (countLeadingZeros), + ) import Data.Bytes.Serial (Serial (deserialize, serialize)) import Data.Coerce (coerce) import qualified Data.HashMap.Strict as HM @@ -5751,7 +5755,8 @@ leOrdTerm = unsafeInCurThread2 curThreadLeOrdTerm -- | Construct and internalizing a 'AndBitsTerm'. andBitsTerm :: (PEvalBitwiseTerm a) => Term a -> Term a -> Term a -andBitsTerm = unsafeInCurThread2 curThreadAndBitsTerm +andBitsTerm a b = + unsafeInCurThread2 curThreadAndBitsTerm a b {-# NOINLINE andBitsTerm #-} -- | Construct and internalizing a 'OrBitsTerm'. @@ -6863,25 +6868,25 @@ pevalITEBVTerm cond (AndBitsTerm a b) (AndBitsTerm c d) | b == c = Just $ andBitsTerm b $ pevalITETerm cond a d | b == d = Just $ andBitsTerm b $ pevalITETerm cond a c pevalITEBVTerm cond (AndBitsTerm a b) c - | a == c = Just $ andBitsTerm c $ orBitsTerm (expandCond $ pevalNotTerm cond) b - | b == c = Just $ andBitsTerm c $ orBitsTerm (expandCond $ pevalNotTerm cond) a + | a == c = Just $ andBitsTerm c $ pevalOrBitsTerm (boolToBVTerm $ pevalNotTerm cond) b + | b == c = Just $ andBitsTerm c $ pevalOrBitsTerm (boolToBVTerm $ pevalNotTerm cond) a pevalITEBVTerm cond a (AndBitsTerm b c) - | a == b = Just $ andBitsTerm a $ orBitsTerm (expandCond cond) c - | a == c = Just $ andBitsTerm a $ orBitsTerm (expandCond cond) b + | a == b = Just $ andBitsTerm a $ pevalOrBitsTerm (boolToBVTerm cond) c + | a == c = Just $ andBitsTerm a $ pevalOrBitsTerm (boolToBVTerm cond) b pevalITEBVTerm cond (OrBitsTerm a b) (OrBitsTerm c d) | a == c = Just $ orBitsTerm a $ pevalITETerm cond b d | a == d = Just $ orBitsTerm a $ pevalITETerm cond b c | b == c = Just $ orBitsTerm b $ pevalITETerm cond a d | b == d = Just $ orBitsTerm b $ pevalITETerm cond a c pevalITEBVTerm cond (OrBitsTerm a b) c - | a == c = Just $ orBitsTerm c $ andBitsTerm (expandCond cond) b - | b == c = Just $ orBitsTerm c $ andBitsTerm (expandCond cond) a + | a == c = Just $ orBitsTerm c $ pevalAndBitsTerm (boolToBVTerm cond) b + | b == c = Just $ orBitsTerm c $ pevalAndBitsTerm (boolToBVTerm cond) a pevalITEBVTerm cond a (OrBitsTerm b c) - | a == b = Just $ orBitsTerm a $ andBitsTerm (expandCond $ pevalNotTerm cond) c - | a == c = Just $ orBitsTerm a $ andBitsTerm (expandCond $ pevalNotTerm cond) b + | a == b = Just $ orBitsTerm a $ pevalAndBitsTerm (boolToBVTerm $ pevalNotTerm cond) c + | a == c = Just $ orBitsTerm a $ pevalAndBitsTerm (boolToBVTerm $ pevalNotTerm cond) b pevalITEBVTerm _ _ _ = Nothing -expandCond :: +boolToBVTerm :: forall bv n. ( PEvalBVTerm bv, KnownNat n, @@ -6889,7 +6894,7 @@ expandCond :: forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m) ) => Term Bool -> Term (bv n) -expandCond cond = +boolToBVTerm cond = let bv = case cond of NotTerm c -> iteTerm c (conTerm 0) (conTerm 1) @@ -7264,10 +7269,34 @@ pevalDefaultAndBitsTerm = binaryUnfoldOnce doPevalAndBitsTerm andBitsTerm acok = ac .&. (ac + 1) == 0 doPevalAndBitsTerm a b@(ConTerm _) = doPevalAndBitsTerm b a doPevalAndBitsTerm a b | a == b = Just a - doPevalAndBitsTerm (ITETerm cond a@(ConTerm _) b@(ConTerm _)) c = - Just $ pevalITETerm cond (pevalAndBitsTerm a c) (pevalAndBitsTerm b c) - doPevalAndBitsTerm a (ITETerm cond b@(ConTerm _) c@(ConTerm _)) = - Just $ pevalITETerm cond (pevalAndBitsTerm a b) (pevalAndBitsTerm a c) + doPevalAndBitsTerm (ITETerm cond a@(ConTerm av) b@(ConTerm bv)) c + | av `elem` [0, -1] || bv `elem` [0, -1] = + Just $ pevalITETerm cond (pevalAndBitsTerm a c) (pevalAndBitsTerm b c) + doPevalAndBitsTerm a (ITETerm cond b@(ConTerm bv) c@(ConTerm cv)) + | bv `elem` [0, -1] || cv `elem` [0, -1] = + Just $ pevalITETerm cond (pevalAndBitsTerm a b) (pevalAndBitsTerm a c) + doPevalAndBitsTerm (ITETerm cond a@(ConTerm v) b) c + | v == 0 = Just $ pevalITETerm cond a (pevalAndBitsTerm b c) + doPevalAndBitsTerm (ITETerm cond a b@(ConTerm v)) c + | v == 0 = Just $ pevalITETerm cond (pevalAndBitsTerm a c) b + doPevalAndBitsTerm a (ITETerm cond b@(ConTerm v) c) + | v == 0 = Just $ pevalITETerm cond b (pevalAndBitsTerm a c) + doPevalAndBitsTerm a (ITETerm cond b c@(ConTerm v)) + | v == 0 = Just $ pevalITETerm cond (pevalAndBitsTerm a b) c + doPevalAndBitsTerm (BVExtendTerm True pl (ITETerm cond at@(ConTerm a) bt@(ConTerm b))) c + | a `elem` [0, -1] && b `elem` [0, -1] = + Just $ + pevalITETerm + cond + (pevalAndBitsTerm (pevalBVExtendTerm True pl at) c) + (pevalAndBitsTerm (pevalBVExtendTerm True pl bt) c) + doPevalAndBitsTerm a (BVExtendTerm True pl (ITETerm cond bt@(ConTerm b) ct@(ConTerm c))) + | b `elem` [0, -1] && c `elem` [0, -1] = + Just $ + pevalITETerm + cond + (pevalAndBitsTerm a (pevalBVExtendTerm True pl bt)) + (pevalAndBitsTerm a (pevalBVExtendTerm True pl ct)) doPevalAndBitsTerm a b = bitOpOnConcat @bv @m pevalDefaultAndBitsTerm a b pevalDefaultOrBitsTerm :: @@ -7322,6 +7351,28 @@ pevalDefaultOrBitsTerm = binaryUnfoldOnce doPevalOrBitsTerm orBitsTerm Just $ pevalITETerm cond (pevalOrBitsTerm a c) (pevalOrBitsTerm b c) doPevalOrBitsTerm a (ITETerm cond b@(ConTerm _) c@(ConTerm _)) = Just $ pevalITETerm cond (pevalOrBitsTerm a b) (pevalOrBitsTerm a c) + doPevalOrBitsTerm (ITETerm cond a@(ConTerm v) b) c + | v == -1 = Just $ pevalITETerm cond a (pevalOrBitsTerm b c) + doPevalOrBitsTerm (ITETerm cond a b@(ConTerm v)) c + | v == -1 = Just $ pevalITETerm cond (pevalOrBitsTerm a c) b + doPevalOrBitsTerm a (ITETerm cond b@(ConTerm v) c) + | v == -1 = Just $ pevalITETerm cond b (pevalOrBitsTerm a c) + doPevalOrBitsTerm a (ITETerm cond b c@(ConTerm v)) + | v == -1 = Just $ pevalITETerm cond (pevalOrBitsTerm a b) c + doPevalOrBitsTerm (BVExtendTerm True pl (ITETerm cond at@(ConTerm a) bt@(ConTerm b))) c + | a `elem` [0, -1] && b `elem` [0, -1] = + Just $ + pevalITETerm + cond + (pevalOrBitsTerm (pevalBVExtendTerm True pl at) c) + (pevalOrBitsTerm (pevalBVExtendTerm True pl bt) c) + doPevalOrBitsTerm a (BVExtendTerm True pl (ITETerm cond bt@(ConTerm b) ct@(ConTerm c))) + | b `elem` [0, -1] && c `elem` [0, -1] = + Just $ + pevalITETerm + cond + (pevalOrBitsTerm a (pevalBVExtendTerm True pl bt)) + (pevalOrBitsTerm a (pevalBVExtendTerm True pl ct)) doPevalOrBitsTerm a b = bitOpOnConcat @bv @m pevalDefaultOrBitsTerm a b pevalDefaultXorBitsTerm :: diff --git a/test/Grisette/Backend/TermRewritingTests.hs b/test/Grisette/Backend/TermRewritingTests.hs index 00d09dca..bea25926 100644 --- a/test/Grisette/Backend/TermRewritingTests.hs +++ b/test/Grisette/Backend/TermRewritingTests.hs @@ -100,6 +100,7 @@ import Grisette.Backend.TermRewritingGen orSpec, quotIntegralSpec, remIntegralSpec, + shiftLeftSpec, shiftRightSpec, signumNumSpec, toFPSpec, @@ -129,8 +130,8 @@ import Grisette.Internal.SymPrim.Prim.Term PEvalBitCastTerm, PEvalBitwiseTerm (pevalAndBitsTerm, pevalOrBitsTerm), PEvalIEEEFPConvertibleTerm, + PEvalShiftTerm, SupportedNonFuncPrim, - SupportedPrim (pevalITETerm), Term, andBitsTerm, bvConcatTerm, @@ -268,6 +269,7 @@ divisionTest name f = 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) => Num (bv n), forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n), Typeable bv, @@ -275,7 +277,7 @@ bvConcatTest :: ) => Test bvConcatTest = - testGroup (show (typeRep @bv) <> " concat") $ + testGroup (show (typeRep @bv) <> "_concat") $ ( do (opName, opSpec, termOp) <- [ ("and", andBitsSpec, andBitsTerm), @@ -496,8 +498,8 @@ bvConcatTest = ) ++ ( do trueBranch <- [True, False] - (opName, op, spec) <- - [("and", pevalAndBitsTerm, andBitsSpec), ("or", pevalOrBitsTerm, orBitsSpec)] + (opName, spec) <- + [("and", andBitsSpec), ("or", orBitsSpec)] let iteName = "ite(cond,const,const)" let name = opName @@ -515,17 +517,104 @@ bvConcatTest = let s = symSpec "a" :: FixedSizedBVWithBoolSpec bv 4 let lhs = if trueBranch then ite else s let rhs = if trueBranch then s else ite - let sterm = ssymTerm "a" :: Term (bv 4) - let transform = if trueBranch then (`op` sterm) else op sterm - let iteExpected = - pevalITETerm - (ssymTerm "cond" :: Term Bool) - (transform $ conTerm a) - (transform $ conTerm b) - let resSpec@(FixedSizedBVWithBoolSpec _ r) = spec lhs rhs - r @?= iteExpected + 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.