{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-| Module : GenWhat4Expr Copyright : (c) Galois Inc, 2020 License : BSD3 Maintainer : kquick@galois.com This module provides Hedgehog generators for What4 expression values that have associated Haskell counterparts; the Haskell value predicts the What4 value on evaluation. The What4 expression is often generated from a Haskell value evaluation, so the "distance" between the tests and the implementation might be seen as fairly small. However, there is a lot of simplification and subterm-elimination that is attempted in What4 expressions; this testing can verify the expected *functional* behavior of the expressions as various simplifications and implementation adjustments are made. Because these are generated expressions, they don't tend to shrink as much one would expect (e.g. @(5 + 1)@ will not be shrunk to @6@) because that requires domain-specific expression evaluation. When failures occur, it can be helpful to temporarily edit out portions of these generators to attempt simplification. -} module GenWhat4Expr where import Data.Bits import qualified Data.BitVector.Sized as BV import Data.Word import GHC.Natural import GHC.TypeNats ( KnownNat ) import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Internal.Gen as IGen import qualified Hedgehog.Range as Range import Test.Tasty.HUnit import What4.Interface -- | A convenience class to extract the description string and haskell -- value (and type) for any type of TestExpr. class IsTestExpr x where type HaskellTy x desc :: x -> String testval :: x -> HaskellTy x -- n.b. cannot ad What4BTy, because the target (SymExpr) is a type -- synonym for a type family and type family instances cannot -- specify a type synonym as a target. -- -- data What4BTy x :: BaseType -- -> Type -- type What4BTy x :: Type -> Type -- testexpr :: forall sym. (IsExprBuilder sym) => x -> sym -> IO (What4BTy x sym) pdesc :: IsTestExpr x => x -> String pdesc s = "(" <> desc s <> ")" ---------------------------------------------------------------------- -- Somewhat awkward, but when using Gen.subtermN for Gen.recursive, -- each of the subterms is required to have the same type as the -- result of the recursive term. This is fine for uniform values -- (e.g. simply-typed lambda calculi) but for a DSL like the What4 -- IsExprBuilder this means that even though there are separate -- generators here for each subtype the results must be wrapped in a -- common type that can hold all the 't' results from 'SymExpr sym -- t'... the 'TestExpr' type here. There's a lot of expectation of -- which value is present when unwrapping (this is just test code), -- and there various uses of Hedgehog 'Gen.filter' to ensure the right -- value is returned even in the face of shrinking: when shrinking a -- recursive term (e.g. "natEq x y") the result is a 'Pred sym', but -- shrinking will try to eliminate the 'natEq' wrapper and end up -- trying to return 'x' or 'y', which is a 'SymNat sym' instead. data TestExpr = TE_Bool PredTestExpr | TE_Int IntTestExpr | TE_BV8 BV8TestExpr | TE_BV16 BV16TestExpr | TE_BV32 BV32TestExpr | TE_BV64 BV64TestExpr isBoolTestExpr, isIntTestExpr, isBV8TestExpr, isBV16TestExpr, isBV32TestExpr, isBV64TestExpr :: TestExpr -> Bool isBoolTestExpr = \case TE_Bool _ -> True _ -> False isIntTestExpr = \case TE_Int _ -> True _ -> False isBV8TestExpr = \case TE_BV8 _ -> True _ -> False isBV16TestExpr = \case TE_BV16 _ -> True _ -> False isBV32TestExpr = \case TE_BV32 _ -> True _ -> False isBV64TestExpr = \case TE_BV64 _ -> True _ -> False ---------------------------------------------------------------------- data PredTestExpr = PredTest { preddsc :: String , predval :: Bool , predexp :: forall sym. (IsExprBuilder sym) => sym -> IO (Pred sym) } instance IsTestExpr PredTestExpr where type HaskellTy PredTestExpr = Bool desc = preddsc testval = predval genBoolCond :: (HasCallStack, Monad m) => GenT m TestExpr genBoolCond = Gen.recursive Gen.choice [ return $ TE_Bool $ PredTest "true" True $ return . truePred , return $ TE_Bool $ PredTest "false" False $ return . falsePred ] $ let boolTerm = IGen.filterT isBoolTestExpr genBoolCond intTerm = IGen.filterT isIntTestExpr genIntTestExpr bv8Term = IGen.filterT isBV8TestExpr genBV8TestExpr bv16Term = IGen.filterT isBV16TestExpr genBV16TestExpr bv32Term = IGen.filterT isBV32TestExpr genBV32TestExpr bv64Term = IGen.filterT isBV64TestExpr genBV64TestExpr subBoolTerm2 gen = Gen.subterm2 boolTerm boolTerm (\(TE_Bool x) (TE_Bool y) -> TE_Bool $ gen x y) subBoolTerm3 gen = Gen.subterm3 boolTerm boolTerm boolTerm (\(TE_Bool x) (TE_Bool y) (TE_Bool z) -> TE_Bool $ gen x y z) subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\(TE_Int x) (TE_Int y) -> TE_Bool $ gen x y) -- subBV16Terms2 gen = Gen.subterm2 bv16Term bv16Term (\(TE_BV16 x) (TE_BV16 y) -> TE_Bool $ gen x y) -- subBV8Terms2 gen = Gen.subterm2 bv8Term bv8Term (\(TE_BV8 x) (TE_BV8 y) -> TE_Bool $ gen x y) in [ Gen.subterm genBoolCond (\(TE_Bool itc) -> TE_Bool $ PredTest ("not " <> pdesc itc) (not $ testval itc) (\sym -> notPred sym =<< predexp itc sym)) , subBoolTerm2 (\x y -> PredTest ("and " <> pdesc x <> " " <> pdesc y) (testval x && testval y) (\sym -> do x' <- predexp x sym y' <- predexp y sym andPred sym x' y' )) , subBoolTerm2 (\x y -> PredTest ("or " <> pdesc x <> " " <> pdesc y) (testval x || testval y) (\sym -> do x' <- predexp x sym y' <- predexp y sym orPred sym x' y' )) , subBoolTerm2 (\x y -> PredTest ("eq " <> pdesc x <> " " <> pdesc y) (testval x == testval y) (\sym -> do x' <- predexp x sym y' <- predexp y sym eqPred sym x' y' )) , subBoolTerm2 (\x y -> PredTest ("xor " <> pdesc x <> " " <> pdesc y) (testval x `xor` testval y) (\sym -> do x' <- predexp x sym y' <- predexp y sym xorPred sym x' y' )) , subBoolTerm3 (\c x y -> PredTest ("ite " <> pdesc c <> " " <> pdesc x <> " " <> pdesc y) (if testval c then testval x else testval y) (\sym -> do c' <- predexp c sym x' <- predexp x sym y' <- predexp y sym itePred sym c' x' y' )) , subIntTerms2 (\x y -> PredTest ("intEq " <> pdesc x <> " " <> pdesc y) (testval x == testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intEq sym x' y' )) , subIntTerms2 (\x y -> PredTest (pdesc x <> " int.<= " <> pdesc y) (testval x <= testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intLe sym x' y' )) , subIntTerms2 (\x y -> PredTest (pdesc x <> " int.< " <> pdesc y) (testval x < testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intLt sym x' y' )) , Gen.subterm2 intTerm bv16Term -- Note [natTerm]: natTerm is used as the index into -- bv16term. This is somewhat inefficient, but saves the -- administrative overhead of another TestExpr member. However, -- the NatExpr could be greater than the bit range, so mod the -- result if necessary. Also note that the testBitBV uses an -- actual Natural, not a What4 Nat, so the natval is used and the -- natexpr is ignored. (\(TE_Int i) (TE_BV16 v) -> TE_Bool $ -- KWQ: bvsized let ival = fromInteger (testval i `mod` 16) in PredTest (pdesc v <> "[" <> show ival <> "]") (testBit (testval v) (fromEnum ival)) (\sym -> testBitBV sym ival =<< bvexpr v sym)) ] ++ bvPredExprs bv8Term (\(TE_BV8 x) -> x) bv8expr 8 ++ bvPredExprs bv16Term (\(TE_BV16 x) -> x) bvexpr 16 ++ bvPredExprs bv32Term (\(TE_BV32 x) -> x) bv32expr 32 ++ bvPredExprs bv64Term (\(TE_BV64 x) -> x) bv64expr 64 bvPredExprs :: ( Monad m , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , 1 <= w ) => GenT m TestExpr -> (TestExpr -> bvtestexpr) -> (bvtestexpr -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w))) -> Natural -> [GenT m TestExpr] bvPredExprs bvTerm projTE expr width = let subBVTerms2 gen = Gen.subterm2 bvTerm bvTerm (\x y -> TE_Bool $ gen (projTE x) (projTE y)) mask = (.&.) (2^width - 1) uBV v = if v >= 0 then v else 2^width + v sBV v = let norm = if v >= 0 then v else mask (v - 2^width) in if norm >= (2^(width-1)) then norm - 2^width else norm pfx o = "bv" <> show width <> "." <> o in [ subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvEq", pdesc y]) (uBV (testval x) == uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvEq sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvNe", pdesc y]) (uBV (testval x) /= uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvNe sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvUlt", pdesc y]) (uBV (testval x) < uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvUlt sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvUle", pdesc y]) (uBV (testval x) <= uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvUle sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvUge", pdesc y]) (uBV (testval x) >= uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvUge sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvUgt", pdesc y]) (uBV (testval x) > uBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvUgt sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvSlt", pdesc y]) (sBV (testval x) < sBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvSlt sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvSle", pdesc y]) (sBV (testval x) <= sBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvSle sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvSge", pdesc y]) (sBV (testval x) >= sBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvSge sym x' y' )) , subBVTerms2 (\x y -> PredTest (unwords [pdesc x, pfx "bvSgt", pdesc y]) (sBV (testval x) > sBV (testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvSgt sym x' y' )) , Gen.subterm bvTerm (\vt -> TE_Bool $ let v = projTE vt in PredTest (pfx "isneg? " <> pdesc v) (mask (testval v) < 0 || mask (testval v) >= 2^(width-1)) (\sym -> bvIsNeg sym =<< expr v sym)) , Gen.subterm bvTerm (\vt -> TE_Bool $ let v = projTE vt in PredTest (pfx "isNonZero? " <> pdesc v) (testval v /= 0) (\sym -> bvIsNonzero sym =<< expr v sym)) ] ---------------------------------------------------------------------- data IntTestExpr = IntTestExpr { intdesc :: String , intval :: Integer , intexpr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymInteger sym) } instance IsTestExpr IntTestExpr where type HaskellTy IntTestExpr = Integer desc = intdesc testval = intval genIntTestExpr :: Monad m => GenT m TestExpr genIntTestExpr = Gen.recursive Gen.choice [ do n <- Gen.integral $ Range.constant (-3) 3 -- keep the range small, or will never see dup values for natEq return $ TE_Int $ IntTestExpr (show n) n $ \sym -> intLit sym n ] $ let intTerm = IGen.filterT isIntTestExpr genIntTestExpr intTermNZ = IGen.filterT isIntNZTestExpr genIntTestExpr isIntNZTestExpr = \case TE_Int n -> testval n /= 0 _ -> False subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\(TE_Int x) (TE_Int y) -> TE_Int $ gen x y) subIntTerms2nz gen = Gen.subterm2 intTerm intTermNZ (\(TE_Int x) (TE_Int y) -> TE_Int $ gen x y) in [ subIntTerms2 (\x y -> IntTestExpr (pdesc x <> " int.+ " <> pdesc y) (testval x + testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intAdd sym x' y' )) , subIntTerms2 (\x y -> IntTestExpr (pdesc x <> " int.- " <> pdesc y) (testval x - testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intSub sym x' y' )) , subIntTerms2 (\x y -> IntTestExpr (pdesc x <> " int.* " <> pdesc y) (testval x * testval y) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intMul sym x' y' )) , subIntTerms2nz -- nz on 2nd to avoid divide-by-zero (\x y -> IntTestExpr (pdesc x <> " int./ " <> pdesc y) (if testval y >= 0 then testval x `div` testval y else negate (testval x `div` negate (testval y))) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intDiv sym x' y' )) , subIntTerms2nz -- nz on 2nd to avoid divide-by-zero (\x y -> IntTestExpr (pdesc x <> " int.mod " <> pdesc y) (testval x `mod` abs (testval y)) (\sym -> do x' <- intexpr x sym y' <- intexpr y sym intMod sym x' y' )) , Gen.subterm3 (IGen.filterT isBoolTestExpr genBoolCond) intTerm intTerm (\(TE_Bool c) (TE_Int x) (TE_Int y) -> TE_Int $ IntTestExpr (pdesc c <> " int.? " <> pdesc x <> " : " <> pdesc y) (if testval c then testval x else testval y) (\sym -> do c' <- predexp c sym x' <- intexpr x sym y' <- intexpr y sym intIte sym c' x' y' )) ] ---------------------------------------------------------------------- -- TBD: genIntTestExpr :: Monad m => GenT m TestExpr ---------------------------------------------------------------------- allbits8, allbits16, allbits32, allbits64 :: Integer allbits8 = (2 :: Integer) ^ (8 :: Integer) - 1 allbits16 = (2 :: Integer) ^ (16 :: Integer) - 1 allbits32 = (2 :: Integer) ^ (32 :: Integer) - 1 allbits64 = (2 :: Integer) ^ (64 :: Integer) - 1 genBV8val :: Monad m => GenT m Integer genBV8val = Gen.choice [ -- keep the range small, or will never see dup values Gen.integral $ Range.constantFrom 0 (-10) 10 , Gen.integral $ Range.constant (128-1) (128+1) , Gen.integral $ Range.constant (allbits8-2) allbits8 ] data BV8TestExpr = BV8TestExpr { bv8desc :: String , bv8val :: Integer , bv8expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 8) } instance IsTestExpr BV8TestExpr where type HaskellTy BV8TestExpr = Integer desc = bv8desc testval = bv8val genBV8TestExpr :: Monad m => GenT m TestExpr genBV8TestExpr = let ret8 = return . TE_BV8 in Gen.recursive Gen.choice [ do n <- genBV8val ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n) , ret8 $ BV8TestExpr ("0`8") 0 $ \sym -> minUnsignedBV sym knownRepr , let n = allbits8 in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> maxUnsignedBV sym knownRepr , let n = allbits8 `shiftR` 1 in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> maxSignedBV sym knownRepr , let n = allbits8 `xor` (allbits8 `shiftR` 1) in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> minSignedBV sym knownRepr ] $ bvTGExprs (tgen8 bvTermGens) ++ bvTGMixedExprs bvTermGens 8 genBV16val :: Monad m => GenT m Integer genBV16val = Gen.choice [ -- keep the range small, or will never see dup values Gen.integral $ Range.constantFrom 0 (-10) 10 , Gen.integral $ Range.constant (allbits8-1) (allbits8+2) , Gen.integral $ Range.constant ((-1) * (allbits8+2)) ((-1) * (allbits8-1)) , Gen.integral $ Range.constant (allbits16-2) allbits16 ] data BV16TestExpr = BV16TestExpr { bvdesc :: String , bvval :: Integer , bvexpr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 16) } instance IsTestExpr BV16TestExpr where type HaskellTy BV16TestExpr = Integer desc = bvdesc testval = bvval genBV16TestExpr :: Monad m => GenT m TestExpr genBV16TestExpr = let ret16 = return . TE_BV16 in Gen.recursive Gen.choice [ do n <- genBV16val ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n) , ret16 $ BV16TestExpr ("0`16") 0 $ \sym -> minUnsignedBV sym knownRepr , let n = allbits16 in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> maxUnsignedBV sym knownRepr , let n = allbits16 `shiftR` 1 in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> maxSignedBV sym knownRepr , let n = allbits16 `xor` (allbits16 `shiftR` 1) in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> minSignedBV sym knownRepr ] $ bvTGExprs (tgen16 bvTermGens) ++ bvTGMixedExprs bvTermGens 16 genBV32val :: Monad m => GenT m Integer genBV32val = Gen.choice [ -- keep the range small, or will never see dup values Gen.integral $ Range.constantFrom 0 (-10) 10 , Gen.integral $ Range.constant (allbits8-1) (allbits8+2) , Gen.integral $ Range.constant (allbits16-1) (allbits16+2) , Gen.integral $ Range.constant ((-1) * (allbits16+2)) ((-1) * (allbits16-1)) , Gen.integral $ Range.constant (allbits32-2) allbits32 ] data BV32TestExpr = BV32TestExpr { bv32desc :: String , bv32val :: Integer , bv32expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 32) } instance IsTestExpr BV32TestExpr where type HaskellTy BV32TestExpr = Integer desc = bv32desc testval = bv32val genBV32TestExpr :: Monad m => GenT m TestExpr genBV32TestExpr = let ret32 = return . TE_BV32 in Gen.recursive Gen.choice [ do n <- genBV32val ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n) , ret32 $ BV32TestExpr ("0`32") 0 $ \sym -> minUnsignedBV sym knownRepr , let n = allbits32 in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> maxUnsignedBV sym knownRepr , let n = allbits32 `shiftR` 1 in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> maxSignedBV sym knownRepr , let n = allbits32 `xor` (allbits32 `shiftR` 1) in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> minSignedBV sym knownRepr ] $ bvTGExprs (tgen32 bvTermGens) ++ bvTGMixedExprs bvTermGens 32 genBV64val :: Monad m => GenT m Integer genBV64val = Gen.choice [ -- keep the range small, or will never see dup values Gen.integral $ Range.constantFrom 0 (-10) 10 , Gen.integral $ Range.constant (allbits8-1) (allbits8+2) , Gen.integral $ Range.constant (allbits16-1) (allbits16+2) , Gen.integral $ Range.constant (allbits32-1) (allbits32+2) , Gen.integral $ Range.constant ((-1) * (allbits32+2)) ((-1) * (allbits32-1)) , Gen.integral $ Range.constant (allbits64-2) allbits64 ] data BV64TestExpr = BV64TestExpr { bv64desc :: String , bv64val :: Integer , bv64expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 64) } instance IsTestExpr BV64TestExpr where type HaskellTy BV64TestExpr = Integer desc = bv64desc testval = bv64val genBV64TestExpr :: Monad m => GenT m TestExpr genBV64TestExpr = let ret64 = return . TE_BV64 in Gen.recursive Gen.choice [ do n <- genBV64val ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n) , ret64 $ BV64TestExpr ("0`64") 0 $ \sym -> minUnsignedBV sym knownRepr , let n = allbits64 in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> maxUnsignedBV sym knownRepr , let n = allbits64 `shiftR` 1 in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> maxSignedBV sym knownRepr , let n = allbits64 `xor` (allbits64 `shiftR` 1) in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> minSignedBV sym knownRepr ] $ bvTGExprs (tgen64 bvTermGens) ++ bvTGMixedExprs bvTermGens 64 -- | For a particular bitwidth, the BVTermGen structure provides the -- various definitions of term generators, constructors and -- projectors, What4 expression extractors, and width designations. data BVTermGen m bvtestexpr w word = BVTermGen { genTerm :: GenT m TestExpr , conBVT :: bvtestexpr -> TestExpr , projBVT :: TestExpr -> bvtestexpr , subBVTCon :: String -> Integer -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w)) -> bvtestexpr , symExpr :: bvtestexpr -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w)) , bitWidth :: Natural , toBVWord :: (Integer -> word) } -- | This combines the information about BVTermGen for all of the -- standard widths data BVTermsGen m = BVTermsGen { tgen8 :: BVTermGen m BV8TestExpr 8 Word8 , tgen16 :: BVTermGen m BV16TestExpr 16 Word16 , tgen32 :: BVTermGen m BV32TestExpr 32 Word32 , tgen64 :: BVTermGen m BV64TestExpr 64 Word64 } bvTermGens :: Monad m => BVTermsGen m bvTermGens = let g8 = BVTermGen (IGen.filterT isBV8TestExpr genBV8TestExpr) TE_BV8 (\(TE_BV8 x) -> x) BV8TestExpr bv8expr 8 fromIntegral g16 = BVTermGen (IGen.filterT isBV16TestExpr genBV16TestExpr) TE_BV16 (\(TE_BV16 x) -> x) BV16TestExpr bvexpr 16 fromIntegral g32 = BVTermGen (IGen.filterT isBV32TestExpr genBV32TestExpr) TE_BV32 (\(TE_BV32 x) -> x) BV32TestExpr bv32expr 32 fromIntegral g64 = BVTermGen (IGen.filterT isBV64TestExpr genBV64TestExpr) TE_BV64 (\(TE_BV64 x) -> x) BV64TestExpr bv64expr 64 fromIntegral -- n.b. toEnum . fromEnum doesn't work for very large -- Word64 values (-1, -2, high-bit set?), so use -- fromIntegral instead (probably faster?) in BVTermsGen g8 g16 g32 g64 bvTGExprs :: ( Monad m , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , 1 <= w , KnownNat w , Integral word , FiniteBits word ) => BVTermGen m bvtestexpr w word -> [GenT m TestExpr] bvTGExprs gt = bvExprs (genTerm gt) (conBVT gt) (projBVT gt) (subBVTCon gt) (symExpr gt) (bitWidth gt) (toBVWord gt) bvExprs :: ( Monad m , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , 1 <= w , KnownNat w , Integral word , Bits word , FiniteBits word ) => GenT m TestExpr -> (bvtestexpr -> TestExpr) -> (TestExpr -> bvtestexpr) -> (String -> Integer -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w)) -> bvtestexpr) -> (bvtestexpr -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w))) -> Natural -> (HaskellTy bvtestexpr -> word) -> [GenT m TestExpr] bvExprs bvTerm conTE projTE teSubCon expr width toWord = let subBVTerms1 gen = Gen.subterm bvTerm (conTE . gen . projTE) subBVTerms2 gen = Gen.subterm2 bvTerm bvTerm (\x y -> conTE $ gen (projTE x) (projTE y)) subBVTerms2nz gen = Gen.subterm2 bvTerm bvTermNZ (\x y -> conTE $ gen (projTE x) (projTE y)) bvTermNZ = do t <- projTE <$> bvTerm -- adjust 0 to +1 to avoid divide-by-zero. A -- Gen.filterT tends to lead to non-termination -- here return $ if testval t == 0 then conTE $ teSubCon (pdesc t <> " +1") (testval t + 1) (\sym -> do lit1 <- bvLit sym knownRepr (BV.one knownNat) orig <- expr t sym bvAdd sym orig lit1) else conTE t mask = (.&.) (2^width - 1) uBV v = if v >= 0 then v else 2^width + v sBV v = let norm = if v >= 0 then v else mask (v - 2^width) in if norm >= (2^(width-1)) then norm - 2^width else norm pfx o = "bv" <> show width <> "." <> o in [ subBVTerms1 (\x -> teSubCon (pfx "neg " <> pdesc x) (mask ((-1) * testval x)) (\sym -> bvNeg sym =<< expr x sym)) , subBVTerms1 (\x -> teSubCon (pfx "not " <> pdesc x) (mask (complement $ testval x)) (\sym -> bvNotBits sym =<< expr x sym)) , subBVTerms2 (\x y -> teSubCon (pdesc x <> " " <> pfx "+ " <> pdesc y) (mask (testval x + testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvAdd sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "-", pdesc y]) (mask (testval x - testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvSub sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "*", pdesc y]) (mask (testval x * testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvMul sym x' y')) , subBVTerms2nz (\x y -> teSubCon (unwords [pdesc x, pfx "u/", pdesc y]) (mask (uBV (testval x) `quot` uBV (testval y))) (\sym -> do x' <- expr x sym y' <- expr y sym bvUdiv sym x' y')) , subBVTerms2nz (\x y -> teSubCon (unwords [pdesc x, pfx "urem", pdesc y]) (mask (uBV (testval x) `rem` uBV (testval y))) (\sym -> do x' <- expr x sym y' <- expr y sym bvUrem sym x' y')) , subBVTerms2nz (\x y -> teSubCon (unwords [pdesc x, pfx "s/", pdesc y]) (let x' = sBV $ testval x y' = sBV $ testval y in mask (x' `quot` y')) (\sym -> do x' <- expr x sym y' <- expr y sym bvSdiv sym x' y')) , subBVTerms2nz (\x y -> teSubCon (unwords [pdesc x, pfx "srem", pdesc y]) (let x' = sBV $ testval x y' = sBV $ testval y in mask (x' `rem` y')) (\sym -> do x' <- expr x sym y' <- expr y sym bvSrem sym x' y')) , Gen.subterm3 (IGen.filterT isBoolTestExpr genBoolCond) bvTerm bvTerm (\(TE_Bool c) lt rt -> conTE $ let l = projTE lt r = projTE rt in teSubCon (unwords [pdesc c, pfx "?", pdesc l, ":", pdesc r]) (if testval c then testval l else testval r) (\sym -> do c' <- predexp c sym l' <- expr l sym r' <- expr r sym bvIte sym c' l' r')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "rol", pdesc y]) (let x' = toWord $ uBV $ testval x y' = fromEnum $ uBV $ testval y in mask (toInteger (x' `rotateL` y'))) (\sym -> do x' <- expr x sym y' <- expr y sym bvRol sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "ror", pdesc y]) (let x' = toWord $ uBV $ testval x y' = fromEnum $ uBV $ testval y in mask (toInteger (x' `rotateR` y'))) (\sym -> do x' <- expr x sym y' <- expr y sym bvRor sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "&", pdesc y]) (mask (testval x .&. testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvAndBits sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "|", pdesc y]) (mask (testval x .|. testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvOrBits sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "xor", pdesc y]) (mask (testval x `xor` testval y)) (\sym -> do x' <- expr x sym y' <- expr y sym bvXorBits sym x' y')) , let intTerm = IGen.filterT isIntTestExpr genIntTestExpr boolTerm = IGen.filterT isBoolTestExpr genBoolCond in Gen.subterm3 bvTerm intTerm boolTerm $ -- see Note [natTerm] \bvt (TE_Int n) (TE_Bool b) -> let bv = projTE bvt nval = fromInteger (testval n `mod` toInteger width) ival = fromIntegral nval :: Int in conTE $ teSubCon (pdesc bv <> "[" <> show nval <> "]" <> pfx ":=" <> pdesc b) (if testval b then setBit (testval bv) ival else clearBit (testval bv) ival) (\sym -> do bv' <- expr bv sym b' <- predexp b sym bvSet sym bv' nval b') , let boolTerm = IGen.filterT isBoolTestExpr genBoolCond in Gen.subterm boolTerm $ \(TE_Bool b) -> -- technically bvFill also takes a NatRepr for the output -- width, but due to the arrangement of these expression -- generators, it will just generate the size specified for -- the current width conTE $ teSubCon (pfx "=" <> pdesc b <> "..") (if testval b then mask (-1) else mask 0) (\sym -> bvFill sym knownRepr =<< predexp b sym) , subBVTerms1 (\x -> teSubCon (pfx "bvPopCount " <> pdesc x) (fromIntegral $ popCount $ mask $ testval x) (\sym -> bvPopcount sym =<< expr x sym)) , subBVTerms1 (\x -> teSubCon (pfx "bvCountLeadingZeros " <> pdesc x) (fromIntegral $ countLeadingZeros $ toWord $ uBV $ mask $ testval x) (\sym -> bvCountLeadingZeros sym =<< expr x sym)) , subBVTerms1 (\x -> teSubCon (pfx "bvCountTrailingZeros " <> pdesc x) (fromIntegral $ countTrailingZeros $ toWord $ uBV $ mask $ testval x) (\sym -> bvCountTrailingZeros sym =<< expr x sym)) -- TBD: carrylessMultiply , subBVTerms1 (\x -> teSubCon (pfx "bvSelect @0[" <> pdesc x <> "]") (mask (testval x)) (\sym -> do x' <- expr x sym bvSelect sym (knownRepr :: NatRepr 0) knownRepr x')) -- TODO: bvTrunc doesn't allow the no-op/same-size operation -- , subBVTerms1 -- (\x -> teSubCon -- (pfx "bvTrunc " <> pdesc x) -- (mask (testval x)) -- (\sym -> do x' <- expr x sym -- bvTrunc sym knownRepr x')) -- TODO: bvZext doesn't allow the no-op/same-size operation -- , subBVTerms1 -- (\x -> teSubCon -- (pfx "bvZext " <> pdesc x) -- (mask (testval x)) -- (\sym -> do x' <- expr x sym -- bvZext sym knownRepr x')) -- TODO: bvSext doesn't allow the no-op/same-size operation -- , subBVTerms1 -- (\x -> teSubCon -- (pfx "bvSext " <> pdesc x) -- (mask (testval x)) -- (\sym -> do x' <- expr x sym -- bvSext sym knownRepr x')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "<<", pdesc y]) (mask (uBV (testval x) `shiftL` (fromEnum $ min (toInteger width) $ uBV $ testval y))) (\sym -> do x' <- expr x sym y' <- expr y sym bvShl sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "lsr", pdesc y]) (let s = fromEnum $ min (toInteger width) $ uBV $ testval y in mask (uBV (testval x) `shiftR` s)) (\sym -> do x' <- expr x sym y' <- expr y sym bvLshr sym x' y')) , subBVTerms2 (\x y -> teSubCon (unwords [pdesc x, pfx "asr", pdesc y]) (let s = fromEnum $ min (toInteger width) $ uBV $ testval y in mask (sBV (testval x) `shiftR` s)) (\sym -> do x' <- expr x sym y' <- expr y sym bvAshr sym x' y')) ] bvTGMixedExprs :: Monad m => BVTermsGen m -> Natural -> [GenT m TestExpr] bvTGMixedExprs termGens tgtWidth = case tgtWidth of 8 -> bvTGMixedExprs_Double (tgen8 termGens) (tgen16 termGens) ++ bvTGMixedExprs_Quadruple (tgen8 termGens) (tgen32 termGens) 16 -> bvTGMixedExprs_Half (tgen16 termGens) (tgen8 termGens) ++ bvTGMixedExprs_Double (tgen16 termGens) (tgen32 termGens) ++ bvTGMixedExprs_Quadruple (tgen16 termGens) (tgen64 termGens) 32 -> bvTGMixedExprs_Half (tgen32 termGens) (tgen16 termGens) ++ bvTGMixedExprs_QuarterHalf (tgen32 termGens) (tgen16 termGens) (tgen8 termGens) ++ bvTGMixedExprs_Double (tgen32 termGens) (tgen64 termGens) 64 -> bvTGMixedExprs_Half (tgen64 termGens) (tgen32 termGens) ++ bvTGMixedExprs_QuarterHalf (tgen64 termGens) (tgen32 termGens) (tgen16 termGens) _ -> error $ "Unsupported width for mixed BV expressions: " <> show tgtWidth bvTGMixedExprs_Half :: ( Monad m , 1 <= w , w + 1 <= w + w , KnownNat (w + w) , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , HaskellTy bvtestexpr_h ~ Integer , IsTestExpr bvtestexpr_h ) => BVTermGen m bvtestexpr (w + w) word -> BVTermGen m bvtestexpr_h w word_h -> [GenT m TestExpr] bvTGMixedExprs_Half thisTG halfTG = let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o halfWidth = bitWidth halfTG halfMask = (.&.) (2^halfWidth - 1) width = bitWidth thisTG mask = (.&.) (2^width - 1) halfHiBit = (.&.) (2^(halfWidth - 1)) in -- output size must match the size of thisTG [ Gen.subterm2 (genTerm halfTG) (genTerm halfTG) $ (\gen x y -> conBVT thisTG $ gen (projBVT halfTG x) (projBVT halfTG y)) $ (\x y -> subBVTCon thisTG (pfx "bvConcat " <> pdesc x <> " " <> pdesc y) (let x' = halfMask (testval x) y' = halfMask (testval y) in (x' `shiftL` (fromEnum halfWidth)) .|. y') (\sym -> do x' <- symExpr halfTG x sym y' <- symExpr halfTG y sym bvConcat sym x' y')) , Gen.subterm (genTerm halfTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvZext " <> pdesc (projBVT halfTG x)) (let x' = testval (projBVT halfTG x) in (halfMask x')) (\sym -> do x' <- symExpr halfTG (projBVT halfTG x) sym bvZext sym knownRepr x')) , Gen.subterm (genTerm halfTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSext " <> pdesc (projBVT halfTG x)) (let x' = halfMask $ testval (projBVT halfTG x) hiBits = mask (-1) `xor` halfMask (-1) in if halfHiBit x' == 0 then x' else (hiBits .|. x')) (\sym -> do x' <- symExpr halfTG (projBVT halfTG x) sym bvSext sym knownRepr x')) ] bvTGMixedExprs_QuarterHalf :: ( Monad m , 1 <= w , 1 <= w + w , 1 <= w + w + w + w , (w + (w + w)) ~ ((w + w) + w) , 1 <= ((w + w) + w) , (w + 1) <= w + w + w + w , KnownNat (w + w + w + w) , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , HaskellTy bvtestexpr_h ~ Integer , IsTestExpr bvtestexpr_h , HaskellTy bvtestexpr_q ~ Integer , IsTestExpr bvtestexpr_q ) => BVTermGen m bvtestexpr (w + w + w + w) word -> BVTermGen m bvtestexpr_h (w + w) word_h -> BVTermGen m bvtestexpr_q w word_q -> [GenT m TestExpr] bvTGMixedExprs_QuarterHalf thisTG halfTG quarterTG = let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o halfWidth = bitWidth halfTG halfMask = (.&.) (2^halfWidth - 1) quarterWidth = bitWidth quarterTG quarterMask = (.&.) (2^quarterWidth - 1) quarterHiBit = (.&.) (2^(quarterWidth - 1)) width = bitWidth thisTG mask = (.&.) (2^width - 1) in [ Gen.subterm3 (genTerm quarterTG) (genTerm halfTG) (genTerm quarterTG) $ (\gen x y z -> conBVT thisTG $ gen (projBVT quarterTG x) (projBVT halfTG y) (projBVT quarterTG z)) $ (\x y z -> subBVTCon thisTG (pfx "bvConcat " <> pdesc x <> " " <> pfx "bvConcat " <> pdesc y <> " " <> pdesc z) (let x' = quarterMask (testval x) y' = halfMask (testval y) z' = quarterMask (testval z) s1 = fromEnum halfWidth s2 = fromEnum quarterWidth in ((((x' `shiftL` s1) .|. y') `shiftL` s2) .|. z')) (\sym -> do x' <- symExpr quarterTG x sym y' <- symExpr halfTG y sym z' <- symExpr quarterTG z sym xy <- bvConcat sym x' y' bvConcat sym xy z')) -- already did bvZext and bvSext with half-size in -- bvTGMixedExprs_Half, so just test extensions from quarter size -- here. , Gen.subterm (genTerm quarterTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvZext " <> pdesc (projBVT quarterTG x)) (let x' = testval (projBVT quarterTG x) in (quarterMask x')) (\sym -> do x' <- symExpr quarterTG (projBVT quarterTG x) sym bvZext sym knownRepr x')) , Gen.subterm (genTerm quarterTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSext " <> pdesc (projBVT quarterTG x)) (let x' = quarterMask $ testval (projBVT quarterTG x) hiBits = mask (-1) `xor` quarterMask (-1) in if quarterHiBit x' == 0 then x' else (hiBits .|. x')) (\sym -> do x' <- symExpr quarterTG (projBVT quarterTG x) sym bvSext sym knownRepr x')) ] bvTGMixedExprs_Double :: ( Monad m , 1 <= w , 0 + w <= w + w , 1 + w <= w + w -- bvSelect --v , w + 1 <= w + w -- bvTrunc ---^ , 2 + w <= w + w , 7 + w <= w + w , KnownNat w , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , HaskellTy bvtestexpr_d ~ Integer , IsTestExpr bvtestexpr_d ) => BVTermGen m bvtestexpr w word -> BVTermGen m bvtestexpr_d (w + w) word_d -> [GenT m TestExpr] bvTGMixedExprs_Double thisTG dblTG = let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o mask = (.&.) (2^(bitWidth thisTG) - 1) in [ -- The bvSelect offset and size are NatReprs, so the type must -- be known at compile time, thus these values cannot be -- generated via hedgehog property generation functions. The -- size must be the size of the current conBVT result, and -- bvSelect requres that offset + size < width of input -- value. There are a few hard-coded offsets used here that -- should be valid for all input BV sizes >= 16 and output BV -- sizes >= 8: -- -- 0, 1, 2, 7 Gen.subterm (genTerm dblTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @0[" <> pdesc (projBVT dblTG x) <> "]") (mask ((testval (projBVT dblTG x)) `shiftR` 0)) (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym bvSelect sym (knownRepr :: NatRepr 0) knownRepr x')) , Gen.subterm (genTerm dblTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @1[" <> pdesc (projBVT dblTG x) <> "]") (mask ((testval (projBVT dblTG x)) `shiftR` 1)) (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym bvSelect sym (knownRepr :: NatRepr 1) knownRepr x')) , Gen.subterm (genTerm dblTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @2[" <> pdesc (projBVT dblTG x) <> "]") (mask ((testval (projBVT dblTG x)) `shiftR` 2)) (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym bvSelect sym (knownRepr :: NatRepr 2) knownRepr x')) , Gen.subterm (genTerm dblTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @7[" <> pdesc (projBVT dblTG x) <> "]") (mask ((testval (projBVT dblTG x)) `shiftR` 7)) (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym bvSelect sym (knownRepr :: NatRepr 7) knownRepr x')) , Gen.subterm (genTerm dblTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvTrunc " <> pdesc (projBVT dblTG x)) (mask (testval (projBVT dblTG x))) (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym bvTrunc sym knownRepr x')) ] bvTGMixedExprs_Quadruple :: ( Monad m , 1 <= w , 0 + w <= w + w + w + w , 1 + w <= w + w + w + w -- bvSelect --v , w + 1 <= w + w + w + w -- bvTrunc ---^ , 2 + w <= w + w + w + w , 7 + w <= w + w + w + w , 12 + w <= w + w + w + w , 19 + w <= w + w + w + w , KnownNat w , HaskellTy bvtestexpr ~ Integer , IsTestExpr bvtestexpr , HaskellTy bvtestexpr_d ~ Integer , IsTestExpr bvtestexpr_d ) => BVTermGen m bvtestexpr w word -> BVTermGen m bvtestexpr_d (w + w + w + w) word_d -> [GenT m TestExpr] bvTGMixedExprs_Quadruple thisTG quadTG = let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o mask = (.&.) (2^(bitWidth thisTG) - 1) in [ -- The bvSelect offset and size are NatReprs, so the type must -- be known at compile time, thus these values cannot be -- generated via hedgehog property generation functions. The -- size must be the size of the current conBVT result, and there -- are a few hard-coded offsets used here that should be valid -- for all BV sizes >= 32: -- -- 0, 1, 2, 7, 12, 19 Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @0[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 0)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 0) knownRepr x')) , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @1[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 1)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 1) knownRepr x')) , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @2[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 2)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 2) knownRepr x')) , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @7[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 7)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 7) knownRepr x')) , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @12[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 12)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 12) knownRepr x')) , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvSelect @19[" <> pdesc (projBVT quadTG x) <> "]") (mask ((testval (projBVT quadTG x)) `shiftR` 19)) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvSelect sym (knownRepr :: NatRepr 19) knownRepr x')) -- bvTrunc output size must match the size of thisTG , Gen.subterm (genTerm quadTG) (\x -> conBVT thisTG $ subBVTCon thisTG (pfx "bvTrunc " <> pdesc (projBVT quadTG x)) (mask (testval (projBVT quadTG x))) (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym bvTrunc sym knownRepr x')) ] -- TBD: BV operations returning a (Pred,BV) pair will need another TestExpr -- representation: addUnsignedOF, addSignedOF, subUnsignedOF, -- subSignedOF, mulUnsignedOF, mulSignedOF -- TBD: BV operations returning a (BV,BV) pair will need another -- TestExpr representation: unsignedWideMultiplyBV, signedWideMultiplyBV -- TBD: struct operations -- TBD: array operations -- TBD: Lossless conversions -- TBD: Lossless combinators -- TBD: Lossy conversions -- TBD: Lossy (non-injective) combinators -- TBD: Bitvector operations (intSetWidth, uintSetWidth, intToUInt) -- TBD: string operations -- TBD: real operations -- TBD: IEEE-754 floating-point operations -- TBD: Cplx operations -- TBD: misc functions in Interface.hs