GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-09-11 12:15:51 +03:00
Code Issues Projects Releases Wiki Activity

migration to bv-sized representation (#34)

Browse Source 
Update all `what4`-related packages to to concrete computation using the `bv-sized` library for fixed (but arbitrary) sized bitvector values.

Currently, the bitvector abstract domain computations are still being done directly on raw integers; we can revisit this in the future.

Co-authored-by: Ben Selfridge <benselfridge@000279.local>
Co-authored-by: Rob Dockins <rdockins@galois.com>
This commit is contained in:
Ben Selfridge 2020-06-04 15:07:57 -07:00 committed by GitHub
parent 89e85e14f9
commit 213b23099c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
27 changed files with 694 additions and 616 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitmodules vendored
View File

@ -7,6 +7,3 @@
[submodule "dependencies/blt"]
path = dependencies/blt
url = https://github.com/GaloisInc/blt
[submodule "dependencies/parameterized-utils"]
path = dependencies/parameterized-utils
url = https://github.com/GaloisInc/parameterized-utils

23
bv-sized-migration.md Normal file
View File

@ -0,0 +1,23 @@
This is a WIP migration guide for porting downstream libraries after the
what4/bv-sized change.
* Constants (no Num instance): "0" because "BV.zero w"
* All Data.Bits operations
First pass: resolving Integer ~ BV.BV w mismatch
* Basically, there's two scenarios -- one where you want to turn the Integer into a BV w, and one where you just want to convert.
* asUnsignedBV x ==> BV.asUnsigned <$> asBV x
* fromConcreteUnsignedBV x ==> BV.asUnsigned (fromConcreteBV x)
* bvLit sym w x ==> bvLit sym w (BV.mkBV w x)
* i <- [0..n] ==> i <- BV.enumFromToUnsigned (BV.zero w) (BV.mkBV w n)
* minSigned ==> BV.minSigned
* functions from parameterized-utils that return Integers ==> functions from bv-sized that return BVs
* Num operators ==> BV operators
* Bits operators ==> BV operators
* shifting/masking ==> BV concat/select/trunc/zext/sext
* bvLit sym w (intValue w) ==> bvLit sym w (BV.width w)
Second pass: resolving "no Num instance"
* 0 ==> BV.zero w
* 1 ==> BV.one w
* for anything else, you probably should use BV.mkBV w

2
cabal.project
View File

@ -13,5 +13,3 @@ optional-packages:
dependencies/abcBridge/
dependencies/aig/
dependencies/blt/
dependencies/parameterized-utils/

1
dependencies/parameterized-utils vendored

@ -1 +0,0 @@
Subproject commit b9260b8aeb30af2edc8b4fbc6bb18acfcc7f9889

119
what4-abc/src/What4/Solver/ABC.hs
View File

@ -48,6 +48,7 @@ import Control.Lens
import Control.Monad.Identity
import Control.Monad.ST
import Data.Bits
import qualified Data.BitVector.Sized as BV
import qualified Data.ABC as GIA
import qualified Data.ABC.GIA as GIA
import qualified Data.AIG.Operations as AIG
@ -87,6 +88,7 @@ import What4.Expr.GroundEval
import qualified What4.Expr.UnaryBV as UnaryBV
import What4.Expr.VarIdentification
import qualified What4.Expr.WeightedSum as WSum
import What4.Panic
import What4.ProgramLoc
import What4.Solver.Adapter
import What4.SatResult
@ -166,7 +168,7 @@ type family LitValue s (tp :: BaseType) where
-- | Newtype wrapper around names.
data NameType s (tp :: BaseType) where
B :: GIA.Lit s -> NameType s BaseBoolType
BV :: AIG.BV (GIA.Lit s) -> NameType s (BaseBVType n)
BV :: NatRepr n -> AIG.BV (GIA.Lit s) -> NameType s (BaseBVType n)
GroundNat :: Natural -> NameType s BaseNatType
GroundInt :: Integer -> NameType s BaseIntegerType
GroundRat :: Rational -> NameType s BaseRealType
@ -179,7 +181,8 @@ data VarBinding t s where
-> GIA.Lit s
-> VarBinding t s
BVBinding :: (1 <= w)
=> Nonce t (BaseBVType w)
=> NatRepr w
-> Nonce t (BaseBVType w)
-> AIG.BV (GIA.Lit s)
-> GIA.Lit s {- side condition -}
-> VarBinding t s
@ -212,8 +215,8 @@ eval _ (BoolExpr b _) =
eval _ (SemiRingLiteral SemiRingNatRepr n _) = return (GroundNat n)
eval _ (SemiRingLiteral SemiRingIntegerRepr n _) = return (GroundInt n)
eval _ (SemiRingLiteral SemiRingRealRepr r _) = return (GroundRat r)
eval ntk (SemiRingLiteral (SemiRingBVRepr _ w) v _) =
return $ BV $ AIG.bvFromInteger (gia ntk) (widthVal w) v
eval ntk (SemiRingLiteral (SemiRingBVRepr _ w) bv _) =
return $ BV w $ AIG.bvFromInteger (gia ntk) (widthVal w) (BV.asUnsigned bv)
eval _ (StringExpr s _) = return (GroundString s)
eval ntk (NonceAppExpr e) = do
@ -237,7 +240,7 @@ eval' ntk e = do
r <- eval ntk e
case r of
B l -> return l
BV v -> return v
BV _ v -> return v
GroundNat c -> return c
GroundInt c -> return c
GroundRat c -> return c
@ -333,9 +336,9 @@ bitblastExpr h ae = do
BaseBoolRepr ->
do c' <- eval' h c
B <$> AIG.lazyMux g c' (eval' h x) (eval' h y)
BaseBVRepr _ ->
BaseBVRepr w ->
do c' <- eval' h c
BV <$> AIG.iteM g c' (eval' h x) (eval' h y)
BV w <$> AIG.iteM g c' (eval' h x) (eval' h y)
BaseNatRepr -> natFail
BaseIntegerRepr -> intFail
BaseRealRepr -> realFail
@ -373,14 +376,14 @@ bitblastExpr h ae = do
ite p x y = do
c <- eval' h p
AIG.ite g c x y
BV <$> UnaryBV.sym_evaluate cns ite u
BVConcat _w xe ye -> do
BV w <$> UnaryBV.sym_evaluate cns ite u
BVConcat w xe ye -> do
x <- eval' h xe
y <- eval' h ye
return $ BV $ x AIG.++ y
return $ BV w $ x AIG.++ y
BVSelect idx n xe -> do
x <- eval' h xe
return $ BV $ AIG.sliceRev x (fromIntegral (natValue idx)) (fromIntegral (natValue n))
return $ BV n $ AIG.sliceRev x (fromIntegral (natValue idx)) (fromIntegral (natValue n))
NotPred xe -> B . AIG.not <$> eval' h xe
@ -396,17 +399,17 @@ bitblastExpr h ae = do
SemiRingSum s ->
case WSum.sumRepr s of
SemiRingBVRepr BVArithRepr w -> BV <$> WSum.evalM (AIG.add g) smul cnst s
SemiRingBVRepr BVArithRepr w -> BV w <$> WSum.evalM (AIG.add g) smul cnst s
where
smul c e =
-- NB, better constant folding if the constant is the second value
flip (AIG.mul g) (AIG.bvFromInteger g (widthVal w) c) =<< eval' h e
cnst c = pure (AIG.bvFromInteger g (widthVal w) c)
flip (AIG.mul g) (AIG.bvFromInteger g (widthVal w) (BV.asUnsigned c)) =<< eval' h e
cnst c = pure (AIG.bvFromInteger g (widthVal w) (BV.asUnsigned c))
SemiRingBVRepr BVBitsRepr w -> BV <$> WSum.evalM (AIG.zipWithM (AIG.lXor' g)) smul cnst s
SemiRingBVRepr BVBitsRepr w -> BV w <$> WSum.evalM (AIG.zipWithM (AIG.lXor' g)) smul cnst s
where
smul c e = AIG.zipWithM (AIG.lAnd' g) (AIG.bvFromInteger g (widthVal w) c) =<< eval' h e
cnst c = pure (AIG.bvFromInteger g (widthVal w) c)
smul c e = AIG.zipWithM (AIG.lAnd' g) (AIG.bvFromInteger g (widthVal w) (BV.asUnsigned c)) =<< eval' h e
cnst c = pure (AIG.bvFromInteger g (widthVal w) (BV.asUnsigned c))
SemiRingNatRepr -> natFail
SemiRingIntegerRepr -> intFail
@ -415,10 +418,10 @@ bitblastExpr h ae = do
SemiRingProd pd ->
case WSum.prodRepr pd of
SemiRingBVRepr BVArithRepr w ->
maybe (BV (AIG.bvFromInteger g (widthVal w) 1)) BV <$>
maybe (BV w (AIG.bvFromInteger g (widthVal w) 1)) (BV w) <$>
WSum.prodEvalM (AIG.mul g) (eval' h) pd
SemiRingBVRepr BVBitsRepr w ->
maybe (BV (AIG.bvFromInteger g (widthVal w) (maxUnsigned w))) BV <$>
maybe (BV w (AIG.bvFromInteger g (widthVal w) (maxUnsigned w))) (BV w) <$>
WSum.prodEvalM (AIG.zipWithM (AIG.lAnd' g)) (eval' h) pd
SemiRingNatRepr -> natFail
@ -428,42 +431,42 @@ bitblastExpr h ae = do
BVOrBits w bs ->
do bs' <- traverse (eval' h) (bvOrToList bs)
case bs' of
[] -> return (BV (AIG.bvFromInteger g (widthVal w) 0))
x:xs -> BV <$> foldM (AIG.zipWithM (AIG.lOr' g)) x xs
[] -> return (BV w (AIG.bvFromInteger g (widthVal w) 0))
x:xs -> BV w <$> foldM (AIG.zipWithM (AIG.lOr' g)) x xs
BVUdiv _w x y -> do
BV <$> join (AIG.uquot g <$> eval' h x <*> eval' h y)
BVUrem _w x y -> do
BV <$> join (AIG.urem g <$> eval' h x <*> eval' h y)
BVSdiv _w x y ->
BV <$> join (AIG.squot g <$> eval' h x <*> eval' h y)
BVSrem _w x y ->
BV <$> join (AIG.srem g <$> eval' h x <*> eval' h y)
BVUdiv w x y -> do
BV w <$> join (AIG.uquot g <$> eval' h x <*> eval' h y)
BVUrem w x y -> do
BV w <$> join (AIG.urem g <$> eval' h x <*> eval' h y)
BVSdiv w x y ->
BV w <$> join (AIG.squot g <$> eval' h x <*> eval' h y)
BVSrem w x y ->
BV w <$> join (AIG.srem g <$> eval' h x <*> eval' h y)
BVShl _w x y -> BV <$> join (AIG.shl g <$> eval' h x <*> eval' h y)
BVLshr _w x y -> BV <$> join (AIG.ushr g <$> eval' h x <*> eval' h y)
BVAshr _w x y -> BV <$> join (AIG.sshr g <$> eval' h x <*> eval' h y)
BVRol _w x y -> BV <$> join (AIG.rol g <$> eval' h x <*> eval' h y)
BVRor _w x y -> BV <$> join (AIG.ror g <$> eval' h x <*> eval' h y)
BVShl w x y -> BV w <$> join (AIG.shl g <$> eval' h x <*> eval' h y)
BVLshr w x y -> BV w <$> join (AIG.ushr g <$> eval' h x <*> eval' h y)
BVAshr w x y -> BV w <$> join (AIG.sshr g <$> eval' h x <*> eval' h y)
BVRol w x y -> BV w <$> join (AIG.rol g <$> eval' h x <*> eval' h y)
BVRor w x y -> BV w <$> join (AIG.ror g <$> eval' h x <*> eval' h y)
BVFill w xe -> BV . AIG.bvFromList . replicate (widthVal w) <$> eval' h xe
BVFill w xe -> BV w . AIG.bvFromList . replicate (widthVal w) <$> eval' h xe
BVPopcount _w xe -> do
BVPopcount w xe -> do
x <- eval' h xe
BV <$> AIG.popCount g x
BVCountLeadingZeros _w xe -> do
BV w <$> AIG.popCount g x
BVCountLeadingZeros w xe -> do
x <- eval' h xe
BV <$> AIG.countLeadingZeros g x
BVCountTrailingZeros _w xe -> do
BV w <$> AIG.countLeadingZeros g x
BVCountTrailingZeros w xe -> do
x <- eval' h xe
BV <$> AIG.countTrailingZeros g x
BV w <$> AIG.countTrailingZeros g x
BVZext w' xe -> do
x <- eval' h xe
return $ BV $ AIG.zext g x (widthVal w')
return $ BV w' $ AIG.zext g x (widthVal w')
BVSext w' xe -> do
x <- eval' h xe
return $ BV $ AIG.sext g x (widthVal w')
return $ BV w' $ AIG.sext g x (widthVal w')
------------------------------------------------------------------------
-- Floating point operations
@ -576,10 +579,15 @@ withNetwork m = do
GIA.SomeGraph h <- newNetwork
m h
asInteger :: Monad m => (l -> m Bool) -> AIG.BV l -> m Integer
asInteger f v = go 0 0
where n = AIG.length v
go r i | i == n = return r
data SizedBV = forall w . SizedBV (NatRepr w) (BV.BV w)
asBV :: Monad m => (l -> m Bool) -> AIG.BV l -> m SizedBV
asBV f v = do
x <- go 0 0
Some n <- return $ mkNatRepr (fromIntegral nInt)
return $ SizedBV n (BV.mkBV n x)
where nInt = AIG.length v
go r i | i == nInt = return r
go r i = do
b <- f (v `AIG.at` i)
let q = if b then 1 else 0
@ -596,7 +604,12 @@ evalNonce ntk n eval_fn fallback = do
mnm <- liftST $ H.lookup (nameCache ntk) n
case mnm of
Just (B l) -> return $ eval_fn l
Just (BV bv) -> asInteger (return . eval_fn) bv
Just (BV w bv) -> do
SizedBV w' bv' <- asBV (return . eval_fn) bv
case w `testEquality` w' of
Just Refl -> return bv'
Nothing -> panic "What4.Solver.ABC.evalNonce"
["Got back bitvector with wrong width"]
Just (GroundNat x) -> return x
Just (GroundInt x) -> return x
Just (GroundRat x) -> return x
@ -656,7 +669,7 @@ outputExpr h e = do
r <- eval h e
case r of
B l -> addOutput h l
BV v -> Fold.traverse_ (addOutput h) v
BV _ v -> Fold.traverse_ (addOutput h) v
GroundNat _ -> fail $ "Cannot bitblast nat values."
GroundInt _ -> fail $ "Cannot bitblast integer values."
GroundRat _ -> fail $ "Cannot bitblast real values."
@ -815,15 +828,15 @@ recordBinding ntk b = liftST $
BoolBinding n r ->
do H.insert (nameCache ntk) n (B r)
return GIA.true
BVBinding n r sidecond ->
do H.insert (nameCache ntk) n (BV r)
BVBinding w n r sidecond ->
do H.insert (nameCache ntk) n (BV w r)
return sidecond
deleteBinding :: Network t s -> VarBinding t s -> IO ()
deleteBinding ntk b = liftST $
case b of
BoolBinding n _ -> H.delete (nameCache ntk) n
BVBinding n _ _ -> H.delete (nameCache ntk) n
BVBinding _ n _ _ -> H.delete (nameCache ntk) n
freshBV :: AIG.IsAIG l g => g s -> NatRepr n -> IO (AIG.BV (l s))
freshBV g w = AIG.generateM_msb0 (widthVal w) (\_ -> GIA.newInput g)
@ -857,7 +870,7 @@ freshBinding ntk n l tp mbnds = do
case bnds of
BVD.BVDArith a -> arithBounds (A.arithDomainData a)
BVD.BVDBitwise b -> between g (B.bitbounds b) bv
return (BVBinding n bv cond)
return (BVBinding w n bv cond)
BaseNatRepr -> failAt l "Natural number variables are not supported by ABC."
BaseIntegerRepr -> failAt l "Integer variables are not supported by ABC."

1
what4-abc/what4-abc.cabal
View File

@ -21,6 +21,7 @@ library
aig,
abcBridge >= 0.11,
ansi-wl-pprint,
bv-sized >= 1.0.0,
containers,
what4 >= 0.4,
directory,

15
what4/src/What4/BaseTypes.hs
View File

@ -52,6 +52,7 @@ module What4.BaseTypes
, Unicode
-- * FloatPrecision data kind
, type FloatPrecision
, type FloatPrecisionBits
-- ** Constructors for kind FloatPrecision
, FloatingPointPrecision
-- ** FloatingPointPrecision aliases
@ -160,6 +161,10 @@ data FloatPrecision where
-> FloatPrecision
type FloatingPointPrecision = 'FloatingPointPrecision -- ^ @:: 'GHC.TypeNats.Nat' -> 'GHC.TypeNats.Nat' -> 'FloatPrecision'@.
-- | This computes the number of bits occupied by a floating-point format.
type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where
FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb
-- | Floating-point precision aliases
type Prec16 = FloatingPointPrecision 5 11
type Prec32 = FloatingPointPrecision 8 24
@ -173,14 +178,12 @@ type Prec128 = FloatingPointPrecision 15 113
-- | A runtime representation of a solver interface type. Parameter @bt@
-- has kind 'BaseType'.
data BaseTypeRepr (bt::BaseType) :: Type where
BaseBoolRepr :: BaseTypeRepr BaseBoolType
BaseBVRepr :: (1 <= w) => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)
BaseNatRepr :: BaseTypeRepr BaseNatType
BaseBoolRepr :: BaseTypeRepr BaseBoolType
BaseBVRepr :: (1 <= w) => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)
BaseNatRepr :: BaseTypeRepr BaseNatType
BaseIntegerRepr :: BaseTypeRepr BaseIntegerType
BaseRealRepr :: BaseTypeRepr BaseRealType
BaseFloatRepr
:: !(FloatPrecisionRepr fpp)
-> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr :: !(FloatPrecisionRepr fpp) -> BaseTypeRepr (BaseFloatType fpp)
BaseStringRepr :: StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseComplexRepr :: BaseTypeRepr BaseComplexType

15
what4/src/What4/Concrete.hs
View File

@ -43,8 +43,7 @@ module What4.Concrete
, fromConcreteInteger
, fromConcreteReal
, fromConcreteString
, fromConcreteUnsignedBV
, fromConcreteSignedBV
, fromConcreteBV
, fromConcreteComplex
) where
@ -55,6 +54,7 @@ import qualified Numeric as N
import Numeric.Natural
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Classes
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
@ -76,7 +76,7 @@ data ConcreteVal tp where
ConcreteBV ::
(1 <= w) =>
NatRepr w {- Width of the bitvector -} ->
Integer {- Unsigned value of the bitvector -} ->
BV.BV w {- Unsigned value of the bitvector -} ->
ConcreteVal (BaseBVType w)
ConcreteStruct :: Ctx.Assignment ConcreteVal ctx -> ConcreteVal (BaseStructType ctx)
ConcreteArray ::
@ -106,11 +106,8 @@ fromConcreteComplex (ConcreteComplex x) = x
fromConcreteString :: ConcreteVal (BaseStringType si) -> StringLiteral si
fromConcreteString (ConcreteString x) = x
fromConcreteUnsignedBV :: ConcreteVal (BaseBVType w) -> Integer
fromConcreteUnsignedBV (ConcreteBV _w x) = x
fromConcreteSignedBV :: ConcreteVal (BaseBVType w) -> Integer
fromConcreteSignedBV (ConcreteBV w x) = toSigned w x
fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV.BV w
fromConcreteBV (ConcreteBV _w x) = x
-- | Compute the type representative for a concrete value.
concreteType :: ConcreteVal tp -> BaseTypeRepr tp
@ -159,7 +156,7 @@ ppConcrete = \case
ConcreteInteger x -> PP.text (show x)
ConcreteReal x -> PP.text (show x)
ConcreteString x -> PP.text (show x)
ConcreteBV w x -> PP.text ("0x" ++ (N.showHex x (":[" ++ show w ++ "]")))
ConcreteBV w x -> PP.text ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]")))
ConcreteComplex (r :+ i) -> PP.text "complex(" PP.<> PP.text (show r) PP.<> PP.text ", " PP.<> PP.text (show i) PP.<> PP.text ")"
ConcreteStruct xs -> PP.text "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.text ")"
ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.text "constArray(" PP.<> ppConcrete def PP.<> PP.text ")")

364
what4/src/What4/Expr/Builder.hs
View File

@ -173,10 +173,10 @@ import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.ST
import Control.Monad.Trans.Writer.Strict (writer, runWriter)
import qualified Data.BitVector.Sized as BV
import Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import qualified Data.Binary.IEEE754 as IEEE754
import qualified Data.Bits as Bits
import Data.Foldable
import qualified Data.HashTable.Class as H (toList)
import qualified Data.HashTable.ST.Basic as H
@ -207,7 +207,6 @@ import Data.Text (Text)
import qualified Data.Text as Text
import Data.Word (Word64)
import GHC.Generics (Generic)
import qualified Numeric as N
import Numeric.Natural
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
@ -1013,10 +1012,8 @@ instance IsExpr (Expr t) where
exprType (AppExpr e) = appType (appExprApp e)
exprType (BoundVarExpr i) = bvarType i
asUnsignedBV (SemiRingLiteral (SR.SemiRingBVRepr _ _) i _) = Just i
asUnsignedBV _ = Nothing
asSignedBV x = toSigned (bvWidth x) <$> asUnsignedBV x
asBV (SemiRingLiteral (SR.SemiRingBVRepr _ _) i _) = Just i
asBV _ = Nothing
unsignedBVBounds x = Just $ BVD.ubounds $ exprAbsValue x
signedBVBounds x = Just $ BVD.sbounds (bvWidth x) $ exprAbsValue x
@ -1699,7 +1696,7 @@ exprAbsValue (SemiRingLiteral sr x _) =
SR.SemiRingNatRepr -> natSingleRange x
SR.SemiRingIntegerRepr -> singleRange x
SR.SemiRingRealRepr -> ravSingle x
SR.SemiRingBVRepr _ w -> BVD.singleton w x
SR.SemiRingBVRepr _ w -> BVD.singleton w (BV.asUnsigned x)
exprAbsValue (StringExpr l _) = stringAbsSingle l
exprAbsValue (BoolExpr b _) = Just b
@ -1857,19 +1854,19 @@ ppApp' a0 = do
ppEntry sm e = [ PrettyFunc "natMul" [stringPrettyArg (show sm), exprPrettyArg e ] ]
SR.SemiRingBVRepr SR.BVArithRepr w -> prettyApp "bvSum" (WSum.eval (++) ppEntry ppConstant s)
where ppConstant 0 = []
where ppConstant (BV.BV 0) = []
ppConstant c = [ stringPrettyArg (ppBV c) ]
ppEntry 1 e = [ exprPrettyArg e ]
ppEntry (BV.BV 1) e = [ exprPrettyArg e ]
ppEntry sm e = [ PrettyFunc "bvMul" [ stringPrettyArg (ppBV sm), exprPrettyArg e ] ]
ppBV x = "0x" ++ (N.showHex x []) ++ ":[" ++ show w ++ "]"
ppBV = BV.ppHex w
SR.SemiRingBVRepr SR.BVBitsRepr w -> prettyApp "bvXor" (WSum.eval (++) ppEntry ppConstant s)
where ppConstant 0 = []
where ppConstant (BV.BV 0) = []
ppConstant c = [ stringPrettyArg (ppBV c) ]
ppEntry sm e
| sm == maxUnsigned w = [ exprPrettyArg e ]
| sm == BV.maxUnsigned w = [ exprPrettyArg e ]
| otherwise = [ PrettyFunc "bvAnd" [ stringPrettyArg (ppBV sm), exprPrettyArg e ] ]
ppBV x = "0x" ++ (N.showHex x []) ++ ":[" ++ show w ++ "]"
ppBV = BV.ppHex w
SemiRingProd pd ->
case WSum.prodRepr pd of
@ -2615,7 +2612,7 @@ ppExpr' e0 o = do
| use_decimal = prettyApp (fromString (show (fromRational x :: Double))) []
| otherwise = prettyApp "divReal" [ showPrettyArg n, showPrettyArg d ]
SR.SemiRingBVRepr _ w ->
return $ stringPPExpr $ "0x" ++ (N.showHex x []) ++ ":[" ++ show w ++ "]"
return $ stringPPExpr $ BV.ppHex w x
getBindings (StringExpr x _) =
return $ stringPPExpr $ (show x)
@ -2888,7 +2885,7 @@ sbMakeExpr sym a = do
BaseNatRepr | Just c <- asSingleNatRange v -> natLit sym c
BaseIntegerRepr | Just c <- asSingleRange v -> intLit sym c
BaseRealRepr | Just c <- asSingleRange (ravRange v) -> realLit sym c
BaseBVRepr w | Just x <- BVD.asSingleton v -> bvLit sym w x
BaseBVRepr w | Just x <- BVD.asSingleton v -> bvLit sym w (BV.mkBV w x)
_ -> appExpr s pc a v
-- | Update the binding to point to the current variable.
@ -3091,7 +3088,7 @@ startCaching sb = do
writeIORef (curAllocator sb) s
bvBinDivOp :: (1 <= w)
=> (Integer -> Integer -> Integer)
=> (NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)
-> (NatRepr w -> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w))
-> ExprBuilder t st fs
-> BVExpr t w
@ -3099,26 +3096,10 @@ bvBinDivOp :: (1 <= w)
-> IO (BVExpr t w)
bvBinDivOp f c sb x y = do
let w = bvWidth x
case (asUnsignedBV x, asUnsignedBV y) of
(Just i, Just j) | j /= 0 -> bvLit sb w $ f i j
case (asBV x, asBV y) of
(Just i, Just j) | j /= BV.zero w -> bvLit sb w $ f w i j
_ -> sbMakeExpr sb $ c w x y
bvSignedBinDivOp :: (1 <= w)
=> (Integer -> Integer -> Integer)
-> (NatRepr w -> BVExpr t w
-> BVExpr t w
-> App (Expr t) (BaseBVType w))
-> ExprBuilder t st fs
-> BVExpr t w
-> BVExpr t w
-> IO (BVExpr t w)
bvSignedBinDivOp f c sym x y = do
let w = bvWidth x
case (asSignedBV x, asSignedBV y) of
(Just i, Just j) | j /= 0 -> bvLit sym w $ f i j
_ -> sbMakeExpr sym $ c w x y
asConcreteIndices :: IsExpr e
=> Ctx.Assignment e ctx
-> Maybe (Ctx.Assignment IndexLit ctx)
@ -3127,7 +3108,7 @@ asConcreteIndices = traverseFC f
f x =
case exprType x of
BaseNatRepr -> NatIndexLit . fromIntegral <$> asNat x
BaseBVRepr w -> BVIndexLit w <$> asUnsignedBV x
BaseBVRepr w -> BVIndexLit w <$> asBV x
_ -> Nothing
symbolicIndices :: forall sym ctx
@ -3196,9 +3177,9 @@ reduceApp sym a0 = do
SR.SemiRingRealRepr ->
maybe (realLit sym 1) return =<< WSum.prodEvalM (realMul sym) return pd
SR.SemiRingBVRepr SR.BVArithRepr w ->
maybe (bvLit sym w 1) return =<< WSum.prodEvalM (bvMul sym) return pd
maybe (bvLit sym w (BV.one w)) return =<< WSum.prodEvalM (bvMul sym) return pd
SR.SemiRingBVRepr SR.BVBitsRepr w ->
maybe (bvLit sym w (maxUnsigned w)) return =<< WSum.prodEvalM (bvAndBits sym) return pd
maybe (bvLit sym w (BV.maxUnsigned w)) return =<< WSum.prodEvalM (bvAndBits sym) return pd
SemiRingLe SR.OrderedSemiRingRealRepr x y -> realLe sym x y
SemiRingLe SR.OrderedSemiRingIntegerRepr x y -> intLe sym x y
@ -3228,7 +3209,7 @@ reduceApp sym a0 = do
BVOrBits w bs ->
case bvOrToList bs of
[] -> bvLit sym w 0
[] -> bvLit sym w (BV.zero w)
(x:xs) -> foldM (bvOrBits sym) x xs
BVTestBit i e -> testBitBV sym i e
@ -3590,10 +3571,12 @@ conjPred sym bm =
bvUnary :: (1 <= w) => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary sym u
| Just v <- UnaryBV.asConstant u =
bvLit sym (UnaryBV.width u) v
| otherwise =
sbMakeExpr sym (BVUnaryTerm u)
-- BGS: We probably don't need to re-truncate the result, but
-- until we refactor UnaryBV to use BV w instead of integer,
-- that'll have to wait.
| Just v <- UnaryBV.asConstant u = bvLit sym w (BV.mkBV w v)
| otherwise = sbMakeExpr sym (BVUnaryTerm u)
where w = UnaryBV.width u
asUnaryBV :: (?unaryThreshold :: Int)
=> ExprBuilder t st fs
@ -3602,7 +3585,7 @@ asUnaryBV :: (?unaryThreshold :: Int)
asUnaryBV sym e
| Just (BVUnaryTerm u) <- asApp e = Just u
| ?unaryThreshold == 0 = Nothing
| SemiRingLiteral (SR.SemiRingBVRepr _ w) v _ <- e = Just $ UnaryBV.constant sym w v
| SemiRingLiteral (SR.SemiRingBVRepr _ w) v _ <- e = Just $ UnaryBV.constant sym w (BV.asUnsigned v)
| otherwise = Nothing
-- | This create a unary bitvector representing if the size is not too large.
@ -4276,15 +4259,13 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= let wx = bvWidth xbv
wy = bvWidth ybv
-- Sign extend to largest bitvector and compare.
in case compareNat wx wy of
NatLT _ -> do
Just LeqProof <- return (testLeq (incNat wx) wy)
in case testNatCases wx wy of
NatCaseLT LeqProof -> do
x' <- bvSext sym wy xbv
bvEq sym x' ybv
NatEQ ->
NatCaseEQ ->
bvEq sym xbv ybv
NatGT _ -> do
Just LeqProof <- return (testLeq (incNat wy) wx)
NatCaseGT LeqProof -> do
y' <- bvSext sym wx ybv
bvEq sym xbv y'
@ -4294,15 +4275,13 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= let wx = bvWidth xbv
wy = bvWidth ybv
-- Zero extend to largest bitvector and compare.
in case compareNat wx wy of
NatLT _ -> do
Just LeqProof <- return (testLeq (incNat wx) wy)
in case testNatCases wx wy of
NatCaseLT LeqProof -> do
x' <- bvZext sym wy xbv
bvEq sym x' ybv
NatEQ ->
NatCaseEQ ->
bvEq sym xbv ybv
NatGT _ -> do
Just LeqProof <- return (testLeq (incNat wy) wx)
NatCaseGT LeqProof -> do
y' <- bvZext sym wx ybv
bvEq sym xbv y'
@ -4311,28 +4290,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= let w = bvWidth xbv in
if yi < minSigned w || yi > maxSigned w
then return (falsePred sym)
else bvEq sym xbv =<< bvLit sym w yi
else bvEq sym xbv =<< bvLit sym w (BV.mkBV w yi)
| Just xi <- asSemiRingLit SR.SemiRingIntegerRepr x
, Just (SBVToInteger ybv) <- asApp x
= let w = bvWidth ybv in
if xi < minSigned w || xi > maxSigned w
then return (falsePred sym)
else bvEq sym ybv =<< bvLit sym w xi
else bvEq sym ybv =<< bvLit sym w (BV.mkBV w xi)
| Just (BVToInteger xbv) <- asApp x
, Just yi <- asSemiRingLit SR.SemiRingIntegerRepr y
= let w = bvWidth xbv in
if yi < minUnsigned w || yi > maxUnsigned w
then return (falsePred sym)
else bvEq sym xbv =<< bvLit sym w yi
else bvEq sym xbv =<< bvLit sym w (BV.mkBV w yi)
| Just xi <- asSemiRingLit SR.SemiRingIntegerRepr x
, Just (BVToInteger ybv) <- asApp x
= let w = bvWidth ybv in
if xi < minUnsigned w || xi > maxUnsigned w
then return (falsePred sym)
else bvEq sym ybv =<< bvLit sym w xi
else bvEq sym ybv =<< bvLit sym w (BV.mkBV w xi)
| otherwise = semiRingEq sym SR.SemiRingIntegerRepr (intEq sym) x y
@ -4347,14 +4326,12 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= do let wx = bvWidth xbv
let wy = bvWidth ybv
-- Sign extend to largest bitvector and compare.
case compareNat wx wy of
NatLT _ -> do
Just LeqProof <- return (testLeq (incNat wx) wy)
case testNatCases wx wy of
NatCaseLT LeqProof -> do
x' <- bvSext sym wy xbv
bvSle sym x' ybv
NatEQ -> bvSle sym xbv ybv
NatGT _ -> do
Just LeqProof <- return (testLeq (incNat wy) wx)
NatCaseEQ -> bvSle sym xbv ybv
NatCaseGT LeqProof -> do
y' <- bvSext sym wx ybv
bvSle sym xbv y'
@ -4364,14 +4341,12 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= do let wx = bvWidth xbv
let wy = bvWidth ybv
-- Zero extend to largest bitvector and compare.
case compareNat wx wy of
NatLT _ -> do
Just LeqProof <- return (testLeq (incNat wx) wy)
case testNatCases wx wy of
NatCaseLT LeqProof -> do
x' <- bvZext sym wy xbv
bvUle sym x' ybv
NatEQ -> bvUle sym xbv ybv
NatGT _ -> do
Just LeqProof <- return (testLeq (incNat wy) wx)
NatCaseEQ -> bvUle sym xbv ybv
NatCaseGT LeqProof -> do
y' <- bvZext sym wx ybv
bvUle sym xbv y'
@ -4380,28 +4355,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= let w = bvWidth xbv in
if | yi < minSigned w -> return (falsePred sym)
| yi > maxSigned w -> return (truePred sym)
| otherwise -> join (bvSle sym <$> pure xbv <*> bvLit sym w yi)
| otherwise -> join (bvSle sym <$> pure xbv <*> bvLit sym w (BV.mkBV w yi))
| Just xi <- asSemiRingLit SR.SemiRingIntegerRepr x
, Just (SBVToInteger ybv) <- asApp x
= let w = bvWidth ybv in
if | xi < minSigned w -> return (truePred sym)
| xi > maxSigned w -> return (falsePred sym)
| otherwise -> join (bvSle sym <$> bvLit sym w xi <*> pure ybv)
| otherwise -> join (bvSle sym <$> bvLit sym w (BV.mkBV w xi) <*> pure ybv)
| Just (BVToInteger xbv) <- asApp x
, Just yi <- asSemiRingLit SR.SemiRingIntegerRepr y
= let w = bvWidth xbv in
if | yi < minUnsigned w -> return (falsePred sym)
| yi > maxUnsigned w -> return (truePred sym)
| otherwise -> join (bvUle sym <$> pure xbv <*> bvLit sym w yi)
| otherwise -> join (bvUle sym <$> pure xbv <*> bvLit sym w (BV.mkBV w yi))
| Just xi <- asSemiRingLit SR.SemiRingIntegerRepr x
, Just (BVToInteger ybv) <- asApp x
= let w = bvWidth ybv in
if | xi < minUnsigned w -> return (truePred sym)
| xi > maxUnsigned w -> return (falsePred sym)
| otherwise -> join (bvUle sym <$> bvLit sym w xi <*> pure ybv)
| otherwise -> join (bvUle sym <$> bvLit sym w (BV.mkBV w xi) <*> pure ybv)
{- FIXME? how important are these reductions?
@ -4488,25 +4463,20 @@ instance IsExprBuilder (ExprBuilder t st fs) where
---------------------------------------------------------------------
-- Bitvector operations
bvLit sym w i =
semiRingLit sym (SR.SemiRingBVRepr SR.BVArithRepr w) (toUnsigned w i)
bvLit sym w bv =
semiRingLit sym (SR.SemiRingBVRepr SR.BVArithRepr w) bv
bvConcat sym x y =
case (asUnsignedBV x, asUnsignedBV y) of
case (asBV x, asBV y) of
-- both values are constants, just compute the concatenation
(Just xv, Just yv) -> do
let shft :: Int
shft = fromIntegral (natValue (bvWidth y))
let w' = addNat (bvWidth x) (bvWidth y)
-- Work around to satisfy GHC typechecker.
case isPosNat w' of
Nothing -> fail $ "bvConcat given bad width."
Just LeqProof -> do
bvLit sym w' ((xv `Bits.shiftL` shft) Bits..|. yv)
LeqProof <- return (leqAddPos (bvWidth x) (bvWidth y))
bvLit sym w' (BV.concat (bvWidth x) (bvWidth y) xv yv)
-- reassociate to combine constants where possible
(Just _xv, _)
| Just (BVConcat _w a b) <- asApp y
, Just _av <- asUnsignedBV a
, Just _av <- asBV a
, Just Refl <- testEquality (addNat (bvWidth x) (addNat (bvWidth a) (bvWidth b)))
(addNat (addNat (bvWidth x) (bvWidth a)) (bvWidth b))
, Just LeqProof <- isPosNat (addNat (bvWidth x) (bvWidth a)) -> do
@ -4522,7 +4492,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvSelect sym idx2 (addNat n1 n2) a
-- always reassociate to the right
_ | Just (BVConcat _w a b) <- asApp x
, Just _bv <- asUnsignedBV b
, Just _bv <- asBV b
, Just Refl <- testEquality (addNat (bvWidth a) (addNat (bvWidth b) (bvWidth y)))
(addNat (addNat (bvWidth a) (bvWidth b)) (bvWidth y))
, Just LeqProof <- isPosNat (addNat (bvWidth b) (bvWidth y)) -> do
@ -4540,10 +4510,8 @@ instance IsExprBuilder (ExprBuilder t st fs) where
-- of expressions that result from the very verbose packing and unpacking
-- operations that arise from byte-oriented memory models.
bvSelect sb idx n x
| Just xv <- asUnsignedBV x = do
let mask = maxUnsigned n
let shft = fromIntegral (natValue idx)
bvLit sb n ((xv `Bits.shiftR` shft) Bits..&. mask)
| Just xv <- asBV x = do
bvLit sb n (BV.select idx n xv)
-- nested selects can be collapsed
| Just (BVSelect idx' _n' b) <- asApp x
@ -4557,35 +4525,35 @@ instance IsExprBuilder (ExprBuilder t st fs) where
return x
| Just (BVShl w a b) <- asApp x
, Just diff <- asUnsignedBV b
, Just (Some diffRepr) <- someNat diff
, Just diff <- asBV b
, Some diffRepr <- mkNatRepr (BV.asNatural diff)
, Just LeqProof <- testLeq diffRepr idx = do
Just LeqProof <- return $ testLeq (addNat (subNat idx diffRepr) n) w
bvSelect sb (subNat idx diffRepr) n a
| Just (BVShl _w _a b) <- asApp x
, Just diff <- asUnsignedBV b
, Just (Some diffRepr) <- someNat diff
, Just diff <- asBV b
, Some diffRepr <- mkNatRepr (BV.asNatural diff)
, Just LeqProof <- testLeq (addNat idx n) diffRepr =
bvLit sb n 0
bvLit sb n (BV.zero n)
| Just (BVAshr w a b) <- asApp x
, Just diff <- asUnsignedBV b
, Just (Some diffRepr) <- someNat diff
, Just diff <- asBV b
, Some diffRepr <- mkNatRepr (BV.asNatural diff)
, Just LeqProof <- testLeq (addNat (addNat idx diffRepr) n) w =
bvSelect sb (addNat idx diffRepr) n a
| Just (BVLshr w a b) <- asApp x
, Just diff <- asUnsignedBV b
, Just (Some diffRepr) <- someNat diff
, Just diff <- asBV b
, Some diffRepr <- mkNatRepr (BV.asNatural diff)
, Just LeqProof <- testLeq (addNat (addNat idx diffRepr) n) w =
bvSelect sb (addNat idx diffRepr) n a
| Just (BVLshr w _a b) <- asApp x
, Just diff <- asUnsignedBV b
, Just (Some diffRepr) <- someNat diff
, Just diff <- asBV b
, Some diffRepr <- mkNatRepr (BV.asNatural diff)
, Just LeqProof <- testLeq w (addNat idx diffRepr) =
bvLit sb n 0
bvLit sb n (BV.zero n)
-- select from a sign extension
| Just (BVSext w b) <- asApp x = do
@ -4611,7 +4579,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
let ext = subNat w (bvWidth b)
Just LeqProof <- return $ isPosNat w
Just LeqProof <- return $ isPosNat ext
hi <- bvLit sb ext 0
hi <- bvLit sb ext (BV.zero ext)
x' <- bvConcat sb hi b
-- Add dynamic check
Just LeqProof <- return $ testLeq (addNat idx n) (addNat ext (bvWidth b))
@ -4673,12 +4641,14 @@ instance IsExprBuilder (ExprBuilder t st fs) where
-- App node in the event that one of the coefficients has changed;
-- the writer monad tracks whether a change has occurred.
| Just (SemiRingSum s) <- asApp x
, SR.SemiRingBVRepr SR.BVArithRepr _w <- WSum.sumRepr s
, SR.SemiRingBVRepr SR.BVArithRepr w <- WSum.sumRepr s
, Just Refl <- testEquality idx (knownNat :: NatRepr 0) =
do let mask = maxUnsigned n
do let mask = case testStrictLeq n w of
Left LeqProof -> BV.zext w (BV.maxUnsigned n)
Right Refl -> BV.maxUnsigned n
let reduce i
| i Bits..&. mask == 0 = writer (0, Any True)
| otherwise = writer (i, Any False)
| i `BV.and` mask == BV.zero w = writer (BV.zero w, Any True)
| otherwise = writer (i, Any False)
let (s', Any changed) = runWriter $ WSum.traverseCoeffs reduce s
x' <- if changed then sbMakeExpr sb (SemiRingSum s') else return x
sbMakeExpr sb $ BVSelect idx n x'
@ -4727,9 +4697,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
fail $ "Illegal bit index."
-- Constant evaluation
| Just yc <- asUnsignedBV y
| Just yc <- asBV y
, i <= fromIntegral (maxBound :: Int)
= return $! backendPred sym (yc `Bits.testBit` fromIntegral i)
= return $! backendPred sym (BV.testBit' (fromIntegral i) yc)
| Just (BVZext _w y') <- asApp y
= if i >= natValue (bvWidth y') then
@ -4750,7 +4720,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
= return $! backendPred sym b
| Just (BaseIte _ _ c a b) <- asApp y
, isJust (asUnsignedBV a) || isJust (asUnsignedBV b) -- NB avoid losing sharing
, isJust (asBV a) || isJust (asBV b) -- NB avoid losing sharing
= do a' <- testBitBV sym i a
b' <- testBitBV sym i b
itePred sym c a' b'
@ -4775,8 +4745,8 @@ instance IsExprBuilder (ExprBuilder t st fs) where
| otherwise = sbMakeExpr sym $ BVTestBit i y
bvFill sym w p
| Just True <- asConstantPred p = bvLit sym w (maxUnsigned w)
| Just False <- asConstantPred p = bvLit sym w 0
| Just True <- asConstantPred p = bvLit sym w (BV.maxUnsigned w)
| Just False <- asConstantPred p = bvLit sym w (BV.zero w)
| otherwise = sbMakeExpr sym $ BVFill w p
bvIte sym c x y
@ -4857,9 +4827,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
-> sbMakeExpr sym $ BaseEq (BaseBVRepr (bvWidth x)) (min x y) (max x y)
bvSlt sym x y
| Just xc <- asSignedBV x
, Just yc <- asSignedBV y =
return $! backendPred sym (xc < yc)
| Just xc <- asBV x
, Just yc <- asBV y =
return $! backendPred sym (BV.slt (bvWidth x) xc yc)
| Just b <- BVD.slt (bvWidth x) (exprAbsValue x) (exprAbsValue y) =
return $! backendPred sym b
| x == y = return (falsePred sym)
@ -4874,9 +4844,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
-> sbMakeExpr sym $ BVSlt x y
bvUlt sym x y
| Just xc <- asUnsignedBV x
, Just yc <- asUnsignedBV y = do
return $! backendPred sym (xc < yc)
| Just xc <- asBV x
, Just yc <- asBV y = do
return $! backendPred sym (BV.ult xc yc)
| Just b <- BVD.ult (exprAbsValue x) (exprAbsValue y) =
return $! backendPred sym b
| x == y =
@ -4894,39 +4864,39 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvShl sym x y
-- shift by 0 is the identity function
| Just 0 <- asUnsignedBV y
| Just (BV.BV 0) <- asBV y
= pure x
-- shift by more than word width returns 0
| let (lo, _hi) = BVD.ubounds (exprAbsValue y)
, lo >= intValue (bvWidth x)
= bvLit sym (bvWidth x) 0
= bvLit sym (bvWidth x) (BV.zero (bvWidth x))
| Just i <- asUnsignedBV x, Just n <- asUnsignedBV y
= bvLit sym (bvWidth x) (Bits.shiftL i (fromIntegral n))
| Just xv <- asBV x, Just n <- asBV y
= bvLit sym (bvWidth x) (BV.shl (bvWidth x) xv (BV.asNatural n))
| otherwise
= sbMakeExpr sym $ BVShl (bvWidth x) x y
bvLshr sym x y
-- shift by 0 is the identity function
| Just 0 <- asUnsignedBV y
| Just (BV.BV 0) <- asBV y
= pure x
-- shift by more than word width returns 0
| let (lo, _hi) = BVD.ubounds (exprAbsValue y)
, lo >= intValue (bvWidth x)
= bvLit sym (bvWidth x) 0
= bvLit sym (bvWidth x) (BV.zero (bvWidth x))
| Just i <- asUnsignedBV x, Just n <- asUnsignedBV y
= bvLit sym (bvWidth x) $ Bits.shiftR i (fromIntegral n)
| Just xv <- asBV x, Just n <- asBV y
= bvLit sym (bvWidth x) $ BV.lshr (bvWidth x) xv (BV.asNatural n)
| otherwise
= sbMakeExpr sym $ BVLshr (bvWidth x) x y
bvAshr sym x y
-- shift by 0 is the identity function
| Just 0 <- asUnsignedBV y
| Just (BV.BV 0) <- asBV y
= pure x
-- shift by more than word width returns either 0 (if x is nonnegative)
@ -4935,18 +4905,18 @@ instance IsExprBuilder (ExprBuilder t st fs) where
, lo >= intValue (bvWidth x)
= bvFill sym (bvWidth x) =<< bvIsNeg sym x
| Just i <- asSignedBV x, Just n <- asUnsignedBV y
= bvLit sym (bvWidth x) (Bits.shiftR i (fromIntegral n))
| Just xv <- asBV x, Just n <- asBV y
= bvLit sym (bvWidth x) $ BV.ashr (bvWidth x) xv (BV.asNatural n)
| otherwise
= sbMakeExpr sym $ BVAshr (bvWidth x) x y
bvRol sym x y
| Just i <- asUnsignedBV x, Just n <- asUnsignedBV y
= bvLit sym (bvWidth x) $ rotateLeft (bvWidth x) i n
| Just xv <- asBV x, Just n <- asBV y
= bvLit sym (bvWidth x) $ BV.rotateL (bvWidth x) xv (BV.asNatural n)
| Just n <- asUnsignedBV y
, n `rem` intValue (bvWidth x) == 0
| Just n <- asBV y
, n `BV.urem` BV.width (bvWidth y) == BV.zero (bvWidth y)
= return x
| Just (BVRol w x' n) <- asApp x
@ -4955,7 +4925,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvRol sym x' z
| Just (BVRol w x' n) <- asApp x
= do wbv <- bvLit sym w (intValue w)
= do wbv <- bvLit sym w (BV.width w)
n' <- bvUrem sym n wbv
y' <- bvUrem sym y wbv
z <- bvAdd sym n' y'
@ -4967,7 +4937,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvRor sym x' z
| Just (BVRor w x' n) <- asApp x
= do wbv <- bvLit sym w (intValue w)
= do wbv <- bvLit sym w (BV.width w)
y' <- bvUrem sym y wbv
n' <- bvUrem sym n wbv
z <- bvAdd sym n' =<< bvSub sym wbv y'
@ -4978,11 +4948,11 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym $ BVRol w x y
bvRor sym x y
| Just i <- asUnsignedBV x, Just n <- asUnsignedBV y
= bvLit sym (bvWidth x) $ rotateRight (bvWidth x) i n
| Just xv <- asBV x, Just n <- asBV y
= bvLit sym (bvWidth x) $ BV.rotateR (bvWidth x) xv (BV.asNatural n)
| Just n <- asUnsignedBV y
, n `rem` intValue (bvWidth x) == 0
| Just n <- asBV y
, n `BV.urem` BV.width (bvWidth y) == BV.zero (bvWidth y)
= return x
| Just (BVRor w x' n) <- asApp x
@ -4991,7 +4961,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvRor sym x' z
| Just (BVRor w x' n) <- asApp x
= do wbv <- bvLit sym w (intValue w)
= do wbv <- bvLit sym w (BV.width w)
n' <- bvUrem sym n wbv
y' <- bvUrem sym y wbv
z <- bvAdd sym n' y'
@ -5003,7 +4973,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
bvRol sym x' z
| Just (BVRol w x' n) <- asApp x
= do wbv <- bvLit sym w (intValue w)
= do wbv <- bvLit sym w (BV.width w)
n' <- bvUrem sym n wbv
y' <- bvUrem sym y wbv
z <- bvAdd sym n' =<< bvSub sym wbv y'
@ -5014,10 +4984,10 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym $ BVRor w x y
bvZext sym w x
| Just i <- asUnsignedBV x = do
| Just xv <- asBV x = do
-- Add dynamic check for GHC typechecker.
Just LeqProof <- return $ isPosNat w
bvLit sym w i
bvLit sym w (BV.zext w xv)
-- Concatenate unsign extension.
| Just (BVZext _ y) <- asApp x = do
@ -5037,10 +5007,10 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym $ BVZext w x
bvSext sym w x
| Just i <- asSignedBV x = do
| Just xv <- asBV x = do
-- Add dynamic check for GHC typechecker.
Just LeqProof <- return $ isPosNat w
bvLit sym w i
bvLit sym w (BV.sext (bvWidth x) w xv)
-- Concatenate sign extension.
| Just (BVSext _ y) <- asApp x = do
@ -5060,7 +5030,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym (BVSext w x)
bvXorBits sym x y
| x == y = bvLit sym (bvWidth x) 0 -- special case: x `xor` x = 0
| x == y = bvLit sym (bvWidth x) (BV.zero (bvWidth x)) -- special case: x `xor` x = 0
| otherwise
= let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)
in semiRingAdd sym sr x y
@ -5083,22 +5053,22 @@ instance IsExprBuilder (ExprBuilder t st fs) where
-- XOR by the all-1 constant of the bitwise semiring.
-- This is equivalant to negation
bvNotBits sym x
| Just i <- asUnsignedBV x
= bvLit sym (bvWidth x) $ i `Bits.xor` (maxUnsigned (bvWidth x))
| Just xv <- asBV x
= bvLit sym (bvWidth x) $ xv `BV.xor` (BV.maxUnsigned (bvWidth x))
| otherwise
= let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x))
in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (maxUnsigned (bvWidth x))
in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x))
bvOrBits sym x y =
case (asUnsignedBV x, asUnsignedBV y) of
(Just xi, Just yi) -> bvLit sym (bvWidth x) (xi Bits..|. yi)
(Just xi , _)
| xi == 0 -> return y
| xi == maxUnsigned (bvWidth x) -> return x
(_, Just yi)
| yi == 0 -> return x
| yi == maxUnsigned (bvWidth x) -> return y
case (asBV x, asBV y) of
(Just xv, Just yv) -> bvLit sym (bvWidth x) (xv `BV.or` yv)
(Just xv , _)
| xv == BV.zero (bvWidth x) -> return y
| xv == BV.maxUnsigned (bvWidth x) -> return x
(_, Just yv)
| yv == BV.zero (bvWidth y) -> return x
| yv == BV.maxUnsigned (bvWidth x) -> return y
_
| x == y
@ -5134,7 +5104,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
where sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)
bvNeg sym x
| Just i <- asSignedBV x = bvLit sym (bvWidth x) (-i)
| Just xv <- asBV x = bvLit sym (bvWidth x) (BV.negate (bvWidth x) xv)
| otherwise =
do ut <- CFG.getOpt (sbUnaryThreshold sym)
let ?unaryThreshold = fromInteger ut
@ -5142,16 +5112,16 @@ instance IsExprBuilder (ExprBuilder t st fs) where
(do ux <- asUnaryBV sym x
Just (UnaryBV.neg sym ux))
(do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)
scalarMul sym sr (toUnsigned (bvWidth x) (-1)) x)
scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x)
bvIsNonzero sym x
| Just (BaseIte _ _ p t f) <- asApp x
, isJust (asUnsignedBV t) || isJust (asUnsignedBV f) -- NB, avoid losing possible sharing
, isJust (asBV t) || isJust (asBV f) -- NB, avoid losing possible sharing
= do t' <- bvIsNonzero sym t
f' <- bvIsNonzero sym f
itePred sym p t' f'
| Just (BVConcat _ a b) <- asApp x
, isJust (asUnsignedBV a) || isJust (asUnsignedBV b) -- NB, avoid losing possible sharing
, isJust (asBV a) || isJust (asBV b) -- NB, avoid losing possible sharing
= do pa <- bvIsNonzero sym a
pb <- bvIsNonzero sym b
orPred sym pa pb
@ -5168,28 +5138,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where
ubv
| otherwise = do
let w = bvWidth x
zro <- bvLit sym w 0
zro <- bvLit sym w (BV.zero w)
notPred sym =<< bvEq sym x zro
bvUdiv = bvBinDivOp quot BVUdiv
bvUdiv = bvBinDivOp (const BV.uquot) BVUdiv
bvUrem sym x y
| Just True <- BVD.ult (exprAbsValue x) (exprAbsValue y) = return x
| otherwise = bvBinDivOp rem BVUrem sym x y
bvSdiv = bvSignedBinDivOp quot BVSdiv
bvSrem = bvSignedBinDivOp rem BVSrem
| otherwise = bvBinDivOp (const BV.urem) BVUrem sym x y
bvSdiv = bvBinDivOp BV.squot BVSdiv
bvSrem = bvBinDivOp BV.srem BVSrem
bvPopcount sym x
| Just i <- asUnsignedBV x = bvLit sym w (toInteger (Bits.popCount i))
| Just xv <- asBV x = bvLit sym w (BV.popCount xv)
| otherwise = sbMakeExpr sym $ BVPopcount w x
where w = bvWidth x
bvCountTrailingZeros sym x
| Just i <- asUnsignedBV x = bvLit sym w (ctz w i)
| Just xv <- asBV x = bvLit sym w (BV.ctz w xv)
| otherwise = sbMakeExpr sym $ BVCountTrailingZeros w x
where w = bvWidth x
bvCountLeadingZeros sym x
| Just i <- asUnsignedBV x = bvLit sym w (clz w i)
| Just xv <- asBV x = bvLit sym w (BV.clz w xv)
| otherwise = sbMakeExpr sym $ BVCountLeadingZeros w x
where w = bvWidth x
@ -5492,13 +5462,13 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym (RealToInteger x)
bvToNat sym x
| Just i <- asUnsignedBV x =
natLit sym (fromInteger i)
| Just xv <- asBV x =
natLit sym (BV.asNatural xv)
| otherwise = sbMakeExpr sym (BVToNat x)
bvToInteger sym x
| Just i <- asUnsignedBV x =
intLit sym i
| Just xv <- asBV x =
intLit sym (BV.asUnsigned xv)
-- bvToInteger (integerToBv x w) == mod x (2^w)
| Just (IntegerToBV xi w) <- asApp x =
intMod sym xi =<< intLit sym (2^natValue w)
@ -5506,8 +5476,8 @@ instance IsExprBuilder (ExprBuilder t st fs) where
sbMakeExpr sym (BVToInteger x)
sbvToInteger sym x
| Just i <- asSignedBV x =
intLit sym i
| Just xv <- asBV x =
intLit sym (BV.asSigned (bvWidth x) xv)
-- sbvToInteger (integerToBv x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)
| Just (IntegerToBV xi w) <- asApp x =
do halfmod <- intLit sym (2 ^ (natValue w - 1))
@ -5520,28 +5490,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where
predToBV sym p w
| Just b <- asConstantPred p =
if b then bvLit sym w 1 else bvLit sym w 0
if b then bvLit sym w (BV.one w) else bvLit sym w (BV.zero w)
| otherwise =
case compareNat w (knownNat @1) of
NatEQ -> sbMakeExpr sym (BVFill (knownNat @1) p)
NatGT _ -> bvZext sym w =<< sbMakeExpr sym (BVFill (knownNat @1) p)
NatLT _ -> fail "impossible case in predToBV"
case testNatCases w (knownNat @1) of
NatCaseEQ -> sbMakeExpr sym (BVFill (knownNat @1) p)
NatCaseGT LeqProof -> bvZext sym w =<< sbMakeExpr sym (BVFill (knownNat @1) p)
NatCaseLT LeqProof -> fail "impossible case in predToBV"
integerToBV sym xr w
| SemiRingLiteral SR.SemiRingIntegerRepr i _ <- xr =
bvLit sym w i
bvLit sym w (BV.mkBV w i)
| Just (BVToInteger r) <- asApp xr =
case compareNat (bvWidth r) w of
NatLT _ -> bvZext sym w r
NatEQ -> return r
NatGT _ -> bvTrunc sym w r
case testNatCases (bvWidth r) w of
NatCaseLT LeqProof -> bvZext sym w r
NatCaseEQ -> return r
NatCaseGT LeqProof -> bvTrunc sym w r
| Just (SBVToInteger r) <- asApp xr =
case compareNat (bvWidth r) w of
NatLT _ -> bvSext sym w r
NatEQ -> return r
NatGT _ -> bvTrunc sym w r
case testNatCases (bvWidth r) w of
NatCaseLT LeqProof -> bvSext sym w r
NatCaseEQ -> return r
NatCaseGT LeqProof -> bvTrunc sym w r
| otherwise =
sbMakeExpr sym (IntegerToBV xr w)
@ -6003,13 +5973,13 @@ instance IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpret
iFloatLit sym fi x = iRealToFloat sym fi RNE =<< realLit sym x
iFloatLitSingle sym x =
iFloatFromBinary sym SingleFloatRepr
=<< (bvLit sym knownNat $ toInteger $ IEEE754.floatToWord x)
=<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)
iFloatLitDouble sym x =
iFloatFromBinary sym DoubleFloatRepr
=<< (bvLit sym knownNat $ toInteger $ IEEE754.doubleToWord x)
=<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)
iFloatLitLongDouble sym x =
iFloatFromBinary sym X86_80FloatRepr
=<< (bvLit sym knownNat $ fp80ToBits x)
=<< (bvLit sym knownNat $ BV.mkBV knownNat $ fp80ToBits x)
iFloatNeg = floatUninterpArithUnOp "uninterpreted_float_neg"
iFloatAbs = floatUninterpArithUnOp "uninterpreted_float_abs"
@ -6159,13 +6129,13 @@ instance IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) wher
iFloatLit sym = floatLit sym . floatInfoToPrecisionRepr
iFloatLitSingle sym x =
floatFromBinary sym knownRepr
=<< (bvLit sym knownNat $ toInteger $ IEEE754.floatToWord x)
=<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)
iFloatLitDouble sym x =
floatFromBinary sym knownRepr
=<< (bvLit sym knownNat $ toInteger $ IEEE754.doubleToWord x)
=<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)
iFloatLitLongDouble sym (X86_80Val e s) = do
el <- bvLit sym (knownNat @16) $ toInteger e
sl <- bvLit sym (knownNat @64) $ toInteger s
el <- bvLit sym (knownNat @16) $ BV.word16 e
sl <- bvLit sym (knownNat @64) $ BV.word64 s
fl <- bvConcat sym el sl
floatFromBinary sym knownRepr fl
-- n.b. This may not be valid semantically for operations

111
what4/src/What4/Expr/GroundEval.hs
View File

@ -18,6 +18,7 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module What4.Expr.GroundEval
@ -41,11 +42,10 @@ module What4.Expr.GroundEval
import Control.Monad.Fail( MonadFail )
#endif
import Control.Exception
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.List (foldl')
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as Map
@ -66,7 +66,7 @@ import qualified What4.Expr.StringSeq as SSeq
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.UnaryBV as UnaryBV
import What4.Utils.Arithmetic ( roundAway, clz, ctz, rotateLeft, rotateRight )
import What4.Utils.Arithmetic ( roundAway )
import What4.Utils.Complex
import What4.Utils.StringLiteral
@ -76,8 +76,8 @@ type family GroundValue (tp :: BaseType) where
GroundValue BaseNatType = Natural
GroundValue BaseIntegerType = Integer
GroundValue BaseRealType = Rational
GroundValue (BaseBVType w) = Integer
GroundValue (BaseFloatType fpp) = Integer
GroundValue (BaseBVType w) = BV.BV w
GroundValue (BaseFloatType fpp) = BV.BV (FloatPrecisionBits fpp)
GroundValue BaseComplexType = Complex Rational
GroundValue (BaseStringType si) = StringLiteral si
GroundValue (BaseArrayType idx b) = GroundArray idx b
@ -129,14 +129,14 @@ defaultValueForType tp =
case tp of
BaseBoolRepr -> False
BaseNatRepr -> 0
BaseBVRepr _ -> 0
BaseBVRepr w -> BV.zero w
BaseIntegerRepr -> 0
BaseRealRepr -> 0
BaseComplexRepr -> 0 :+ 0
BaseStringRepr si -> stringLitEmpty si
BaseArrayRepr _ b -> ArrayConcrete (defaultValueForType b) Map.empty
BaseStructRepr ctx -> fmapFC (GVW . defaultValueForType) ctx
BaseFloatRepr _ -> 0
BaseFloatRepr (FloatingPointPrecisionRepr eb sb) -> BV.zero (addNat eb sb)
{-# INLINABLE evalGroundExpr #-}
-- | Helper function for evaluating @Expr@ expressions in a model.
@ -263,12 +263,11 @@ evalGroundApp f0 a0 = do
foldl' (&&) <$> pol t <*> mapM pol ts
RealIsInteger x -> (\xv -> denominator xv == 1) <$> f x
BVTestBit i x -> assert (i <= fromIntegral (maxBound :: Int)) $
(`testBit` (fromIntegral i)) <$> f x
BVSlt x y -> (<) <$> (toSigned w <$> f x)
<*> (toSigned w <$> f y)
BVTestBit i x ->
BV.testBit' i <$> f x
BVSlt x y -> BV.slt w <$> f x <*> f y
where w = bvWidth x
BVUlt x y -> (<) <$> f x <*> f y
BVUlt x y -> BV.ult <$> f x <*> f y
NatDiv x y -> g <$> f x <*> f y
where g _ 0 = 0
@ -309,12 +308,12 @@ evalGroundApp f0 a0 = do
where smul sm e = (sm *) <$> f e
SR.SemiRingBVRepr SR.BVArithRepr w -> WSum.evalM sadd smul pure s
where
smul sm e = toUnsigned w . (sm *) <$> f e
sadd x y = pure (toUnsigned w (x + y))
smul sm e = BV.mul w sm <$> f e
sadd x y = pure (BV.add w x y)
SR.SemiRingBVRepr SR.BVBitsRepr _w -> WSum.evalM sadd smul pure s
where
smul sm e = (sm .&.) <$> f e
sadd x y = pure (x `xor` y)
smul sm e = BV.and sm <$> f e
sadd x y = pure (BV.xor x y)
SemiRingProd pd ->
case WSum.prodRepr pd of
@ -322,9 +321,9 @@ evalGroundApp f0 a0 = do
SR.SemiRingIntegerRepr -> fromMaybe 1 <$> WSum.prodEvalM (\x y -> pure (x*y)) f pd
SR.SemiRingRealRepr -> fromMaybe 1 <$> WSum.prodEvalM (\x y -> pure (x*y)) f pd
SR.SemiRingBVRepr SR.BVArithRepr w ->
fromMaybe 1 <$> WSum.prodEvalM (\x y -> pure (toUnsigned w (x*y))) f pd
fromMaybe (BV.one w) <$> WSum.prodEvalM (\x y -> pure (BV.mul w x y)) f pd
SR.SemiRingBVRepr SR.BVBitsRepr w ->
fromMaybe (maxUnsigned w) <$> WSum.prodEvalM (\x y -> pure (x .&. y)) f pd
fromMaybe (BV.maxUnsigned w) <$> WSum.prodEvalM (\x y -> pure (BV.and x y)) f pd
RealDiv x y -> do
xv <- f x
@ -356,55 +355,49 @@ evalGroundApp f0 a0 = do
------------------------------------------------------------------------
-- Bitvector Operations
BVOrBits _w bs -> foldl' (.|.) 0 <$> traverse f (bvOrToList bs)
BVUnaryTerm u -> do
UnaryBV.evaluate f u
BVConcat w x y -> cat <$> f x <*> f y
where w2 = bvWidth y
cat a b = toUnsigned w $ a `shiftL` (fromIntegral (natValue w2)) .|. b
BVSelect idx n x -> sel <$> f x
where sel a = toUnsigned n (a `shiftR` shft)
shft = fromIntegral (natValue (bvWidth x) - natValue idx - natValue n)
BVUdiv w x y -> toUnsigned w <$> (myDiv <$> f x <*> f y)
where myDiv _ 0 = 0
myDiv u v = u `div` v
BVUrem w x y -> toUnsigned w <$> (myRem <$> f x <*> f y)
where myRem u 0 = u
myRem u v = u `rem` v
BVSdiv w x y -> toUnsigned w <$> (myDiv <$> f x <*> f y)
where myDiv _ 0 = 0
myDiv u v = toSigned w u `div` toSigned w v
BVSrem w x y -> toUnsigned w <$> (myRem <$> f x <*> f y)
where myRem u 0 = u
myRem u v = toSigned w u `rem` toSigned w v
BVShl w x y -> toUnsigned w <$> (shiftL <$> f x <*> (fromInteger <$> f y))
BVLshr w x y -> lift $
toUnsigned w <$> (shiftR <$> f0 x <*> (fromInteger <$> f0 y))
BVAshr w x y -> lift $
toUnsigned w <$> (shiftR <$> (toSigned w <$> f0 x) <*> (fromInteger <$> f0 y))
BVOrBits w bs -> foldl' BV.or (BV.zero w) <$> traverse f (bvOrToList bs)
BVUnaryTerm u ->
BV.mkBV (UnaryBV.width u) <$> UnaryBV.evaluate f u
BVConcat _w x y -> BV.concat (bvWidth x) (bvWidth y) <$> f x <*> f y
BVSelect idx n x -> BV.select idx n <$> f x
BVUdiv w x y -> myDiv <$> f x <*> f y
where myDiv _ (BV.BV 0) = BV.zero w
myDiv u v = BV.uquot u v
BVUrem _w x y -> myRem <$> f x <*> f y
where myRem u (BV.BV 0) = u
myRem u v = BV.urem u v
BVSdiv w x y -> myDiv <$> f x <*> f y
where myDiv _ (BV.BV 0) = BV.zero w
myDiv u v = BV.sdiv w u v
BVSrem w x y -> myRem <$> f x <*> f y
where myRem u (BV.BV 0) = u
myRem u v = BV.srem w u v
BVShl w x y -> BV.shl w <$> f x <*> (BV.asNatural <$> f y)
BVLshr w x y -> BV.lshr w <$> f x <*> (BV.asNatural <$> f y)
BVAshr w x y -> BV.ashr w <$> f x <*> (BV.asNatural <$> f y)
BVRol w x y -> BV.rotateL w <$> f x <*> (BV.asNatural <$> f y)
BVRor w x y -> BV.rotateR w <$> f x <*> (BV.asNatural <$> f y)
BVRol w x y -> lift $ (rotateLeft w <$> f0 x <*> f0 y)
BVRor w x y -> lift $ (rotateRight w <$> f0 x <*> f0 y)
BVZext _ x -> lift $ f0 x
BVSext w x -> lift $ do
BVZext w x -> BV.zext w <$> f x
-- BGS: This check can be proven to GHC
BVSext w x ->
case isPosNat w of
Just LeqProof -> (toUnsigned w . toSigned (bvWidth x)) <$> f0 x
Just LeqProof -> BV.sext (bvWidth x) w <$> f x
Nothing -> error "BVSext given bad width"
BVFill w p ->
do b <- f p
return $! if b then maxUnsigned w else 0
return $! if b then BV.maxUnsigned w else BV.zero w
BVPopcount _w x ->
toInteger . popCount <$> f x
BV.popCount <$> f x
BVCountLeadingZeros w x ->
clz w <$> f x
BV.clz w <$> f x
BVCountTrailingZeros w x ->
ctz w <$> f x
BV.ctz w <$> f x
------------------------------------------------------------------------
-- Bitvector Operations
-- Floating point Operations
FloatPZero{} -> MaybeT $ return Nothing
FloatNZero{} -> MaybeT $ return Nothing
FloatNaN{} -> MaybeT $ return Nothing
@ -499,9 +492,9 @@ evalGroundApp f0 a0 = do
NatToInteger x -> toInteger <$> f x
IntegerToReal x -> toRational <$> f x
BVToNat x -> fromInteger <$> f x
BVToInteger x -> f x
SBVToInteger x -> toSigned (bvWidth x) <$> f x
BVToNat x -> BV.asNatural <$> f x
BVToInteger x -> BV.asUnsigned <$> f x
SBVToInteger x -> BV.asSigned (bvWidth x) <$> f x
RoundReal x -> roundAway <$> f x
FloorReal x -> floor <$> f x
@ -510,7 +503,7 @@ evalGroundApp f0 a0 = do
RealToInteger x -> floor <$> f x
IntegerToNat x -> fromInteger . max 0 <$> f x
IntegerToBV x w -> toUnsigned w <$> f x
IntegerToBV x w -> BV.mkBV w <$> f x
------------------------------------------------------------------------
-- Complex operations.

13
what4/src/What4/Expr/MATLAB.hs
View File

@ -37,6 +37,7 @@ module What4.Expr.MATLAB
) where
import Control.Monad (join)
import qualified Data.BitVector.Sized as BV
import Data.Kind (Type)
import Data.Hashable
import Data.Parameterized.Classes
@ -70,12 +71,12 @@ clampedIntAdd sym x y = do
r' <- bvAdd sym x' y'
-- Check is result is greater than or equal to max value.
too_high <- bvSgt sym r' =<< bvLit sym w' (maxSigned w)
max_int <- bvLit sym w (maxSigned w)
too_high <- bvSgt sym r' =<< bvLit sym w' (BV.maxSigned w')
max_int <- bvLit sym w (BV.maxSigned w)
-- Check is result is less than min value.
too_low <- bvSlt sym r' =<< bvLit sym w' (minSigned w)
min_int <- bvLit sym w (minSigned w)
too_low <- bvSlt sym r' =<< bvLit sym w' (BV.minSigned w')
min_int <- bvLit sym w (BV.minSigned w)
-- Clamp integer range.
r <- bvTrunc sym w r'
@ -104,7 +105,7 @@ clampedIntMul :: (IsExprBuilder sym, 1 <= w)
clampedIntMul sym x y = do
let w = bvWidth x
(hi,lo) <- signedWideMultiplyBV sym x y
zro <- bvLit sym w 0
zro <- bvLit sym w (BV.zero w)
ones <- maxUnsignedBV sym w
ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo)
<*> bvEq sym hi zro
@ -176,7 +177,7 @@ clampedUIntSub sym x y = do
sym
no_underflow
(bvSub sym x y) -- Perform subtraction if y >= x
(bvLit sym w 0) -- Otherwise return min int
(bvLit sym w (BV.zero w)) -- Otherwise return min int
clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
=> sym

9
what4/src/What4/Expr/WeightedSum.hs
View File

@ -70,6 +70,7 @@ module What4.Expr.WeightedSum
import Control.Lens
import Control.Monad.State
import qualified Data.BitVector.Sized as BV
import Data.Hashable
import Data.Kind
import Data.List (foldl')
@ -121,8 +122,8 @@ abstractTerm sr c e =
SR.SemiRingRealRepr -> SRAbsRealAdd (AD.ravScalarMul c (AD.getAbsValue e))
SR.SemiRingBVRepr fv _w ->
case fv of
SR.BVArithRepr -> SRAbsBVAdd (A.scale c (BVD.asArithDomain (AD.getAbsValue e)))
SR.BVBitsRepr -> SRAbsBVXor (X.and_scalar c (BVD.asXorDomain (AD.getAbsValue e)))
SR.BVArithRepr -> SRAbsBVAdd (A.scale (BV.asUnsigned c) (BVD.asArithDomain (AD.getAbsValue e)))
SR.BVBitsRepr -> SRAbsBVXor (X.and_scalar (BV.asUnsigned c) (BVD.asXorDomain (AD.getAbsValue e)))
abstractVal :: AD.HasAbsValue f => SR.SemiRingRepr sr -> f (SR.SemiRingBase sr) -> SRAbsValue sr
abstractVal sr e =
@ -144,8 +145,8 @@ abstractScalar sr c =
SR.SemiRingRealRepr -> SRAbsRealAdd (AD.ravSingle c)
SR.SemiRingBVRepr fv w ->
case fv of
SR.BVArithRepr -> SRAbsBVAdd (A.singleton w c)
SR.BVBitsRepr -> SRAbsBVXor (X.singleton w c)
SR.BVArithRepr -> SRAbsBVAdd (A.singleton w (BV.asUnsigned c))
SR.BVBitsRepr -> SRAbsBVXor (X.singleton w (BV.asUnsigned c))
fromSRAbsValue ::
SRAbsValue sr -> AD.AbstractValue (SR.SemiRingBase sr)

3
what4/src/What4/IndexLit.hs
View File

@ -4,6 +4,7 @@
module What4.IndexLit where
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Classes
import Numeric.Natural
@ -16,7 +17,7 @@ import What4.BaseTypes
-- arrays.
data IndexLit idx where
NatIndexLit :: !Natural -> IndexLit BaseNatType
BVIndexLit :: (1 <= w) => !(NatRepr w) -> !Integer -> IndexLit (BaseBVType w)
BVIndexLit :: (1 <= w) => !(NatRepr w) -> !(BV.BV w) -> IndexLit (BaseBVType w)
instance Eq (IndexLit tp) where
x == y = isJust (testEquality x y)

219
what4/src/What4/Interface.hs
View File

@ -160,7 +160,7 @@ import Control.Exception (assert)
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.Coerce (coerce)
import Data.Foldable
import Data.Hashable
@ -296,18 +296,16 @@ class HasAbsValue e => IsExpr e where
asComplex :: e BaseComplexType -> Maybe (Complex Rational)
asComplex _ = Nothing
-- | Return the unsigned value if this is a constant bitvector.
asUnsignedBV :: e (BaseBVType w) -> Maybe Integer
asUnsignedBV _ = Nothing
-- | Return a bitvector if this is a constant bitvector.
asBV :: e (BaseBVType w) -> Maybe (BV.BV w)
asBV _ = Nothing
-- | Return the signed value if this is a constant bitvector.
asSignedBV :: (1 <= w) => e (BaseBVType w) -> Maybe Integer
asSignedBV _ = Nothing
-- | If we have bounds information about the term, return unsigned upper and lower bounds
-- | If we have bounds information about the term, return unsigned
-- upper and lower bounds as integers
unsignedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
-- | If we have bounds information about the term, return signed upper and lower bounds
-- | If we have bounds information about the term, return signed
-- upper and lower bounds as integers
signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)
@ -636,7 +634,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
-- Bitvector operations
-- | Create a bitvector with the given width and value.
bvLit :: (1 <= w) => sym -> NatRepr w -> Integer -> IO (SymBV sym w)
bvLit :: (1 <= w) => sym -> NatRepr w -> BV.BV w -> IO (SymBV sym w)
-- | Concatenate two bitvectors.
bvConcat :: (1 <= u, 1 <= v)
@ -735,7 +733,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
-- | Return true if bitvector is negative.
bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) 0
bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) (BV.zero (bvWidth x))
-- | If-then-else applied to bitvectors.
bvIte :: (1 <= w)
@ -802,7 +800,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
bvIsNonzero :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym x = do
let w = bvWidth x
zro <- bvLit sym w 0
zro <- bvLit sym w (BV.zero w)
notPred sym =<< bvEq sym x zro
-- | Left shift. The shift amount is treated as an unsigned value.
@ -895,9 +893,9 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
-- of the original term and bvFill terms. It has the nice property that we
-- do not introduce any additional subterm sharing.
do let w = bvWidth v
let mask = bit (fromIntegral i)
let mask = BV.bit' w i
pbits <- bvFill sym w p
vbits <- bvAndBits sym v =<< bvLit sym w (complement mask)
vbits <- bvAndBits sym v =<< bvLit sym w (BV.complement w mask)
bvXorBits sym vbits =<< bvAndBits sym pbits =<< bvLit sym w mask
-- | @bvFill sym w p@ returns a bitvector @w@-bits long where every bit
@ -911,24 +909,24 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
-- | Return the bitvector of the desired width with all 0 bits;
-- this is the minimum unsigned integer.
minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minUnsignedBV sym w = bvLit sym w 0
minUnsignedBV sym w = bvLit sym w (BV.zero w)
-- | Return the bitvector of the desired width with all bits set;
-- this is the maximum unsigned integer.
maxUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym w = bvLit sym w (maxUnsigned w)
maxUnsignedBV sym w = bvLit sym w (BV.maxUnsigned w)
-- | Return the bitvector representing the largest 2's complement
-- signed integer of the given width. This consists of all bits
-- set except the MSB.
maxSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym w = bvLit sym w (maxSigned w)
maxSignedBV sym w = bvLit sym w (BV.maxSigned w)
-- | Return the bitvector representing the smallest 2's complement
-- signed integer of the given width. This consists of all 0 bits
-- except the MSB, which is set.
minSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym w = bvLit sym w (minSigned w)
minSignedBV sym w = bvLit sym w (BV.minSigned w)
-- | Return the number of 1 bits in the input.
bvPopcount :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
@ -1022,8 +1020,8 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
SymBV sym w ->
IO (SymBV sym (w+w))
carrylessMultiply sym x0 y0
| Just _ <- asUnsignedBV x0
, Nothing <- asUnsignedBV y0
| Just _ <- BV.asUnsigned <$> asBV x0
, Nothing <- BV.asUnsigned <$> asBV y0
= go y0 x0
| otherwise
= go x0 y0
@ -1032,16 +1030,22 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
go x y =
do let w = bvWidth x
let w2 = addNat w w
Just LeqProof <- return (testLeq (knownNat @1) w2)
Just LeqProof <- return (testLeq (addNat w (knownNat @1)) w2)
z <- bvLit sym w2 0
-- 1 <= w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
-- 1 <= w implies 1 <= w + w
LeqProof <- return (leqAdd one_leq_w w)
-- w <= w
w_leq_w@LeqProof <- return (leqProof w w)
-- w <= w, 1 <= w implies w + 1 <= w + w
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
z <- bvLit sym w2 (BV.zero w2)
x' <- bvZext sym w2 x
xs <- sequence [ do p <- testBitBV sym i y
xs <- sequence [ do p <- testBitBV sym (BV.asNatural i) y
iteM bvIte sym
p
(bvShl sym x' =<< bvLit sym w2 (toInteger i))
(bvShl sym x' =<< bvLit sym w2 i)
(return z)
| i <- [ 0 .. natValue w - 1 ]
| i <- BV.enumFromToUnsigned (BV.zero w2) (BV.mkBV w2 (intValue w - 1))
]
foldM (bvXorBits sym) z xs
@ -1057,16 +1061,19 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
unsignedWideMultiplyBV sym x y = do
let w = bvWidth x
let dbl_w = addNat w w
-- Add dynamic check to assert w' is positive to work around
-- Haskell typechecker limitation.
Just LeqProof <- return (isPosNat dbl_w)
-- Add dynamic check to assert w+1 <= 2*w.
Just LeqProof <- return (testLeq (incNat w) dbl_w)
-- 1 <= w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
-- 1 <= w implies 1 <= w + w
LeqProof <- return (leqAdd one_leq_w w)
-- w <= w
w_leq_w@LeqProof <- return (leqProof w w)
-- w <= w, 1 <= w implies w + 1 <= w + w
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvZext sym dbl_w x
y' <- bvZext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
n <- bvLit sym dbl_w (intValue w)
n <- bvLit sym dbl_w (BV.zext dbl_w (BV.width w))
hi <- bvTrunc sym w =<< bvLshr sym s n
return (hi, lo)
@ -1080,18 +1087,21 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
mulUnsignedOF sym x y =
do let w = bvWidth x
let dbl_w = addNat w w
-- Add dynamic check to assert w' is positive to work around
-- Haskell typechecker limitation.
Just LeqProof <- return (isPosNat dbl_w)
-- Add dynamic check to assert w+1 <= 2*w.
Just LeqProof <- return (testLeq (incNat w) dbl_w)
-- 1 <= w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
-- 1 <= w implies 1 <= w + w
LeqProof <- return (leqAdd one_leq_w w)
-- w <= w
w_leq_w@LeqProof <- return (leqProof w w)
-- w <= w, 1 <= w implies w + 1 <= w + w
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvZext sym dbl_w x
y' <- bvZext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
-- overflow if the result is greater than the max representable value in w bits
ov <- bvUgt sym s =<< bvLit sym dbl_w (maxUnsigned w)
ov <- bvUgt sym s =<< bvLit sym dbl_w (BV.zext dbl_w (BV.maxUnsigned w))
return (ov, lo)
@ -1107,16 +1117,19 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
signedWideMultiplyBV sym x y = do
let w = bvWidth x
let dbl_w = addNat w w
-- Add dynamic check to assert dbl_w is positive to work around
-- Haskell typechecker limitation.
Just LeqProof <- return (isPosNat dbl_w)
-- Add dynamic check to assert w+1 <= 2*w.
Just LeqProof <- return (testLeq (incNat w) dbl_w)
-- 1 <= w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
-- 1 <= w implies 1 <= w + w
LeqProof <- return (leqAdd one_leq_w w)
-- w <= w
w_leq_w@LeqProof <- return (leqProof w w)
-- w <= w, 1 <= w implies w + 1 <= w + w
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvSext sym dbl_w x
y' <- bvSext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
n <- bvLit sym dbl_w (fromIntegral (widthVal w))
n <- bvLit sym dbl_w (BV.zext dbl_w (BV.width w))
hi <- bvTrunc sym w =<< bvLshr sym s n
return (hi, lo)
@ -1130,19 +1143,22 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
mulSignedOF sym x y =
do let w = bvWidth x
let dbl_w = addNat w w
-- Add dynamic check to assert dbl_w is positive to work around
-- Haskell typechecker limitation.
Just LeqProof <- return (isPosNat dbl_w)
-- Add dynamic check to assert w+1 <= 2*w.
Just LeqProof <- return (testLeq (incNat w) dbl_w)
-- 1 <= w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
-- 1 <= w implies 1 <= w + w
LeqProof <- return (leqAdd one_leq_w w)
-- w <= w
w_leq_w@LeqProof <- return (leqProof w w)
-- w <= w, 1 <= w implies w + 1 <= w + w
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvSext sym dbl_w x
y' <- bvSext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
-- overflow if greater or less than max representable values
ov1 <- bvSlt sym s =<< bvLit sym dbl_w (minSigned w)
ov2 <- bvSgt sym s =<< bvLit sym dbl_w (maxSigned w)
ov1 <- bvSlt sym s =<< bvLit sym dbl_w (BV.sext w dbl_w (BV.minSigned w))
ov2 <- bvSgt sym s =<< bvLit sym dbl_w (BV.sext w dbl_w (BV.maxSigned w))
ov <- orPred sym ov1 ov2
return (ov, lo)
@ -1395,18 +1411,20 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
clampedIntToSBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToSBV sym i w
| Just v <- asInteger i = do
bvLit sym w $ signedClamp w v
bvLit sym w $ BV.signedClamp w v
| otherwise = do
-- Handle case where i < minSigned w
let min_val = minSigned w
min_val_bv = BV.minSigned w
min_sym <- intLit sym min_val
is_lt <- intLt sym i min_sym
iteM bvIte sym is_lt (bvLit sym w min_val) $ do
iteM bvIte sym is_lt (bvLit sym w min_val_bv) $ do
-- Handle case where i > maxSigned w
let max_val = maxSigned w
max_val_bv = BV.maxSigned w
max_sym <- intLit sym max_val
is_gt <- intLt sym max_sym i
iteM bvIte sym is_gt (bvLit sym w max_val) $ do
iteM bvIte sym is_gt (bvLit sym w max_val_bv) $ do
-- Do unclamped conversion.
integerToBV sym i w
@ -1416,17 +1434,18 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
clampedIntToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToBV sym i w
| Just v <- asInteger i = do
bvLit sym w $ unsignedClamp w v
bvLit sym w $ BV.unsignedClamp w v
| otherwise = do
-- Handle case where i < 0
min_sym <- intLit sym 0
is_lt <- intLt sym i min_sym
iteM bvIte sym is_lt (bvLit sym w 0) $ do
iteM bvIte sym is_lt (bvLit sym w (BV.zero w)) $ do
-- Handle case where i > maxUnsigned w
let max_val = maxUnsigned w
max_val_bv = BV.maxUnsigned w
max_sym <- intLit sym max_val
is_gt <- intLt sym max_sym i
iteM bvIte sym is_gt (bvLit sym w max_val) $
iteM bvIte sym is_gt (bvLit sym w max_val_bv) $
-- Do unclamped conversion.
integerToBV sym i w
@ -1437,76 +1456,60 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
-- the given width. If the resulting width is smaller, this clamps
-- the value to min-int or max-int when necessary.
intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intSetWidth sym e w = do
let e_width = bvWidth e
case w `compareNat` e_width of
intSetWidth sym e n = do
let m = bvWidth e
case n `testNatCases` m of
-- Truncate when the width of e is larger than w.
NatLT _ -> do
-- Add dynamic check due to limitation in GHC typechecker.
Just LeqProof <- return (testLeq (incNat w) e_width)
NatCaseLT LeqProof -> do
-- Check if e underflows
does_underflow <- bvSlt sym e =<< bvLit sym e_width (minSigned w)
iteM bvIte sym does_underflow (bvLit sym w (minSigned w)) $ do
does_underflow <- bvSlt sym e =<< bvLit sym m (BV.sext n m (BV.minSigned n))
iteM bvIte sym does_underflow (bvLit sym n (BV.minSigned n)) $ do
-- Check if e overflows target signed representation.
does_overflow <- bvSgt sym e =<< bvLit sym e_width (maxSigned w)
iteM bvIte sym does_overflow (bvLit sym w (maxSigned w)) $ do
does_overflow <- bvSgt sym e =<< bvLit sym m (BV.mkBV m (maxSigned n))
iteM bvIte sym does_overflow (bvLit sym n (BV.maxSigned n)) $ do
-- Just do truncation.
bvTrunc sym w e
NatEQ -> return e
NatGT _ -> do
-- Add dynamic check due to limitation in GHC typechecker.
Just LeqProof <- return (testLeq (incNat e_width) w)
bvSext sym w e
bvTrunc sym n e
NatCaseEQ -> return e
NatCaseGT LeqProof -> bvSext sym n e
-- | Convert an unsigned bitvector to the nearest unsigned bitvector with
-- the given width (clamp on overflow).
uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym e w = do
let e_width = bvWidth e
case w `compareNat` e_width of
NatLT _ -> do
-- Add dynamic check due to limitation in GHC typechecker.
Just LeqProof <- return (testLeq (incNat w) e_width)
-- Check if e overflows target unsigned representation.
does_overflow <- bvUgt sym e =<< bvLit sym e_width (maxUnsigned w)
iteM bvIte sym does_overflow (bvLit sym w (maxUnsigned w)) $ do
-- Just do truncation.
bvTrunc sym w e
NatEQ -> return e
NatGT _ -> do
-- Add dynamic check due to limitation in GHC typechecker.
Just LeqProof <- return (testLeq (incNat e_width) w)
bvZext sym w e
uintSetWidth sym e n = do
let m = bvWidth e
case n `testNatCases` m of
NatCaseLT LeqProof -> do
does_overflow <- bvUgt sym e =<< bvLit sym m (BV.mkBV m (maxUnsigned n))
iteM bvIte sym does_overflow (bvLit sym n (BV.maxUnsigned n)) $ bvTrunc sym n e
NatCaseEQ -> return e
NatCaseGT LeqProof -> bvZext sym n e
-- | Convert an signed bitvector to the nearest unsigned bitvector with
-- the given width (clamp on overflow).
intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intToUInt sym e w = do
p <- bvIsNeg sym e
iteM bvIte sym p (bvLit sym w 0) (uintSetWidth sym e w)
iteM bvIte sym p (bvLit sym w (BV.zero w)) (uintSetWidth sym e w)
-- | Convert an unsigned bitvector to the nearest signed bitvector with
-- the given width (clamp on overflow).
uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintToInt sym e w = do
let n = bvWidth e
case w `compareNat` n of
NatLT _ -> do
-- Get maximum signed w-bit number.
max_val <- bvLit sym n ((2^(widthVal w-1))-1)
uintToInt sym e n = do
let m = bvWidth e
case n `testNatCases` m of
NatCaseLT LeqProof -> do
-- Get maximum signed n-bit number.
max_val <- bvLit sym m (BV.sext n m (BV.maxSigned n))
-- Check if expression is less than maximum.
p <- bvUle sym e max_val
Just LeqProof <- return (testLeq (incNat w) n)
-- Select appropriate number then truncate.
bvTrunc sym w =<< bvIte sym p e max_val
NatEQ -> do
max_val <- maxSignedBV sym w
bvTrunc sym n =<< bvIte sym p e max_val
NatCaseEQ -> do
max_val <- maxSignedBV sym n
p <- bvUle sym e max_val
bvIte sym p e max_val
NatGT _ -> do
-- Add dynamic check to ensure GHC typechecks.
Just LeqProof <- return (testLeq (incNat n) w)
bvZext sym w e
NatCaseGT LeqProof -> do
bvZext sym n e
----------------------------------------------------------------------
-- String operations
@ -2492,7 +2495,7 @@ baseIsConcrete x =
BaseBoolRepr -> isJust $ asConstantPred x
BaseNatRepr -> isJust $ asNat x
BaseIntegerRepr -> isJust $ asInteger x
BaseBVRepr _ -> isJust $ asUnsignedBV x
BaseBVRepr _ -> isJust $ asBV x
BaseRealRepr -> isJust $ asRational x
BaseFloatRepr _ -> False
BaseStringRepr{} -> isJust $ asString x
@ -2515,7 +2518,7 @@ baseDefaultValue sym bt =
BaseBoolRepr -> return $! falsePred sym
BaseNatRepr -> natLit sym 0
BaseIntegerRepr -> intLit sym 0
BaseBVRepr w -> bvLit sym w 0
BaseBVRepr w -> bvLit sym w (BV.zero w)
BaseRealRepr -> return $! realZero sym
BaseFloatRepr fpp -> floatPZero sym fpp
BaseComplexRepr -> mkComplexLit sym (0 :+ 0)
@ -2692,7 +2695,7 @@ asConcrete x =
BaseRealRepr -> ConcreteReal <$> asRational x
BaseStringRepr _si -> ConcreteString <$> asString x
BaseComplexRepr -> ConcreteComplex <$> asComplex x
BaseBVRepr w -> ConcreteBV w <$> asUnsignedBV x
BaseBVRepr w -> ConcreteBV w <$> asBV x
BaseFloatRepr _ -> Nothing
BaseStructRepr _ -> Nothing -- FIXME?
BaseArrayRepr _ _ -> Nothing -- FIXME?

121
what4/src/What4/Protocol/SMTLib2.hs
View File

@ -14,6 +14,7 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
@ -84,7 +85,8 @@ import Control.Applicative
import Control.Exception
import Control.Monad.State.Strict
import qualified Data.Attoparsec.Text as AT
import Data.Bits (bit, setBit, shiftL, shiftR, (.&.))
import qualified Data.BitVector.Sized as BV
import qualified Data.Bits as Bits
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import Data.Char (digitToInt, isPrint, isAscii)
@ -96,6 +98,7 @@ import qualified Data.Map.Strict as Map
import Data.Monoid
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Pair
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Ratio
@ -198,8 +201,8 @@ byteStringTerm bs = SMT2.T ("\"" <> BS.foldr f "\"" bs)
| isPrint c = Builder.singleton c <> x
| otherwise = "\\x" <> h1 <> h2 <> x
where
h1 = Builder.fromString (showHex (w `shiftR` 4) "")
h2 = Builder.fromString (showHex (w .&. 0xF) "")
h1 = Builder.fromString (showHex (w `Bits.shiftR` 4) "")
h2 = Builder.fromString (showHex (w Bits..&. 0xF) "")
c :: Char
c = toEnum (fromEnum w)
@ -445,7 +448,9 @@ instance SupportTermOps Term where
x .> y = SMT2.gt [x,y]
x .>= y = SMT2.ge [x,y]
bvTerm w u = SMT2.bvdecimal u (natValue w)
bvTerm w u = case isZeroOrGT1 w of
Left Refl -> error "Cannot construct BV term with 0 width"
Right LeqProof -> SMT2.bvdecimal w u
bvNeg = SMT2.bvneg
bvAdd x y = SMT2.bvadd x [y]
@ -685,47 +690,79 @@ parseRealSolverValue (SApp ["/", x , y]) = do
<*> parseRealSolverValue y
parseRealSolverValue s = fail $ "Could not parse solver value: " ++ show s
parseBvSolverValue :: MonadFail m => Int -> SExp -> m Integer
parseBvSolverValue _ s
| (n, _) <- parseBVLitHelper s = return n
| otherwise = fail $ "Could not parse solver value: " ++ show s
parseBvSolverValue :: MonadFail m => NatRepr w -> SExp -> m (BV.BV w)
parseBvSolverValue w s
| Pair w' bv <- parseBVLitHelper s = case w' `testEquality` w of
Just Refl -> return bv
Nothing -> fail $ "Solver value parsed with width " ++
show w' ++ ", but should have width " ++ show w
parseBVLitHelper :: SExp -> (Integer, Int)
natBV :: Natural
-- ^ width
-> Integer
-- ^ BV value
-> Pair NatRepr BV.BV
natBV wNatural x = case mkNatRepr wNatural of
Some w -> Pair w (BV.mkBV w x)
-- | Parse an s-expression and return a bitvector and its width
parseBVLitHelper :: SExp -> Pair NatRepr BV.BV
parseBVLitHelper (SAtom (Text.unpack -> ('#' : 'b' : n_str))) | [(n, "")] <- readBin n_str =
(n, length n_str)
natBV (fromIntegral (length n_str)) n
parseBVLitHelper (SAtom (Text.unpack -> ('#' : 'x' : n_str))) | [(n, "")] <- readHex n_str =
(n, length n_str * 4)
natBV (fromIntegral (length n_str * 4)) n
parseBVLitHelper (SApp ["_", SAtom (Text.unpack -> ('b' : 'v' : n_str)), SAtom (Text.unpack -> w_str)])
| [(n, "")] <- readDec n_str, [(w, "")] <- readDec w_str = (n, w)
parseBVLitHelper _ = (0, 0)
| [(n, "")] <- readDec n_str, [(w, "")] <- readDec w_str = natBV w n
-- BGS: Is this correct?
parseBVLitHelper _ = natBV 0 0
parseStringSolverValue :: MonadFail m => SExp -> m ByteString
parseStringSolverValue (SString t) | Just bs <- unescapeText t = return bs
parseStringSolverValue x = fail ("Could not parse string solver value:\n " ++ show x)
parseFloatSolverValue :: MonadFail m => SExp -> m Integer
parseFloatSolverValue (SApp ["fp", sign_s, exponent_s, significant_s])
| (sign_n, 1) <- parseBVLitHelper sign_s
, (exponent_n, eb) <- parseBVLitHelper exponent_s
, 2 <= eb
, (significant_n, sb) <- parseBVLitHelper significant_s
, 1 <= sb
= return $ (((sign_n `shiftL` eb) + exponent_n) `shiftL` sb) + significant_n
parseFloatSolverValue
parseFloatSolverValue :: MonadFail m => FloatPrecisionRepr fpp
-> SExp
-> m (BV.BV (FloatPrecisionBits fpp))
parseFloatSolverValue (FloatingPointPrecisionRepr eb sb) s = do
ParsedFloatResult sgn eb' expt sb' sig <- parseFloatLitHelper s
case (eb `testEquality` eb',
sb `testEquality` ((knownNat @1) `addNat` sb')) of
(Just Refl, Just Refl) -> do
-- eb' + 1 ~ 1 + eb'
Refl <- return $ plusComm eb' (knownNat @1)
-- (eb' + 1) + sb' ~ eb' + (1 + sb')
Refl <- return $ plusAssoc eb' (knownNat @1) sb'
return bv
where bv = BV.concat (addNat (knownNat @1) eb) sb' (BV.concat knownNat eb sgn expt) sig
_ -> fail $ "Unexpected float precision: " <> show eb' <> ", " <> show sb'
data ParsedFloatResult = forall eb sb . ParsedFloatResult
(BV.BV 1) -- ^ sign
(NatRepr eb) -- ^ exponent width
(BV.BV eb) -- ^ exponent
(NatRepr sb) -- ^ significand bit width
(BV.BV sb) -- ^ significand bit
parseFloatLitHelper :: MonadFail m => SExp -> m ParsedFloatResult
parseFloatLitHelper (SApp ["fp", sign_s, expt_s, scand_s])
| Pair sign_w sign <- parseBVLitHelper sign_s
, Just Refl <- sign_w `testEquality` (knownNat @1)
, Pair eb expt <- parseBVLitHelper expt_s
, Pair sb scand <- parseBVLitHelper scand_s
= return $ ParsedFloatResult sign eb expt sb scand
parseFloatLitHelper
s@(SApp ["_", SAtom (Text.unpack -> nm), SAtom (Text.unpack -> eb_s), SAtom (Text.unpack -> sb_s)])
| [(eb, "")] <- readDec eb_s, [(sb, "")] <- readDec sb_s = case nm of
"+oo" -> return $ ones eb `shiftL` (sb - 1)
"-oo" -> return $ setBit (ones eb `shiftL` (sb - 1)) (eb + sb - 1)
"+zero" -> return 0
"-zero" -> return $ bit (eb + sb - 1)
"NaN" -> return $ ones (eb + sb - 1)
_ -> fail $ "Could not parse float solver value: " ++ show s
parseFloatSolverValue s =
fail $ "Could not parse float solver value: " ++ show s
ones :: Int -> Integer
ones n = foldl setBit 0 ([0..(n - 1)] :: [Int])
| [(eb_n, "")] <- readDec eb_s, [(sb_n, "")] <- readDec sb_s
, Some eb <- mkNatRepr eb_n
, Some sb <- mkNatRepr (sb_n-1)
= case nm of
"+oo" -> return $ ParsedFloatResult (BV.zero knownNat) eb (BV.maxUnsigned eb) sb (BV.zero sb)
"-oo" -> return $ ParsedFloatResult (BV.one knownNat) eb (BV.maxUnsigned eb) sb (BV.zero sb)
"+zero" -> return $ ParsedFloatResult (BV.zero knownNat) eb (BV.zero eb) sb (BV.zero sb)
"-zero" -> return $ ParsedFloatResult (BV.one knownNat) eb (BV.zero eb) sb (BV.zero sb)
"NaN" -> return $ ParsedFloatResult (BV.zero knownNat) eb (BV.maxUnsigned eb) sb (BV.maxUnsigned sb)
_ -> fail $ "Could not parse float solver value: " ++ show s
parseFloatLitHelper s = fail $ "Could not parse float solver value: " ++ show s
parseBvArraySolverValue :: (MonadFail m,
1 <= w,
@ -735,14 +772,14 @@ parseBvArraySolverValue :: (MonadFail m,
-> SExp
-> m (Maybe (GroundArray (Ctx.SingleCtx (BaseBVType w)) (BaseBVType v)))
parseBvArraySolverValue _ v (SApp [SApp ["as", "const", _], c]) = do
c' <- parseBvSolverValue (widthVal v) c
c' <- parseBvSolverValue v c
return . Just $ ArrayConcrete c' Map.empty
parseBvArraySolverValue w v (SApp ["store", arr, idx, val]) = do
arr' <- parseBvArraySolverValue w v arr
case arr' of
Just (ArrayConcrete base m) -> do
idx' <- B.BVIndexLit w <$> parseBvSolverValue (widthVal w) idx
val' <- parseBvSolverValue (widthVal v) val
idx' <- B.BVIndexLit w <$> parseBvSolverValue w idx
val' <- parseBvSolverValue v val
return . Just $ ArrayConcrete base (Map.insert (Ctx.empty Ctx.:> idx') val' m)
_ -> return Nothing
parseBvArraySolverValue _ _ _ = return Nothing
@ -900,11 +937,15 @@ smtLibEvalFuns s = SMTEvalFunctions
}
where
evalBool tm = parseBoolSolverValue =<< runGetValue s tm
evalBV w tm = parseBvSolverValue w =<< runGetValue s tm
evalReal tm = parseRealSolverValue =<< runGetValue s tm
evalFloat tm = parseFloatSolverValue =<< runGetValue s tm
evalStr tm = parseStringSolverValue =<< runGetValue s tm
evalBV :: NatRepr w -> Term -> IO (BV.BV w)
evalBV w tm = parseBvSolverValue w =<< runGetValue s tm
evalFloat :: FloatPrecisionRepr fpp -> Term -> IO (BV.BV (FloatPrecisionBits fpp))
evalFloat fpp tm = parseFloatSolverValue fpp =<< runGetValue s tm
evalBvArray :: SMTEvalBVArrayFn (Writer a) w v
evalBvArray w v tm = parseBvArraySolverValue w v =<< runGetValue s tm

47
what4/src/What4/Protocol/SMTLib2/Syntax.hs
View File

@ -8,11 +8,15 @@ so that clients can generate new values that are not exposed through
this interface.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module What4.Protocol.SMTLib2.Syntax
( -- * Commands
Command(..)
@ -137,8 +141,9 @@ module What4.Protocol.SMTLib2.Syntax
, store
) where
import Data.Bits hiding (xor)
import qualified Data.BitVector.Sized as BV
import Data.Char (intToDigit)
import Data.Parameterized.NatRepr
import Data.String
import Data.Text (Text, cons)
import Data.Text.Lazy.Builder (Builder)
@ -503,22 +508,21 @@ bit0 = T "#b0"
bit1 :: Term
bit1 = T "#b1"
-- | @bvbinary x w@ constructs a bitvector term with width @w@ equal to @x `mod` 2^w@.
-- | @bvbinary w x@ constructs a bitvector term with width @w@ equal
-- to @x `mod` 2^w@.
--
-- The width @w@ must be positive.
--
-- The literal uses a binary notation.
bvbinary :: Integer -> Natural -> Term
bvbinary u w0
| w0 > fromIntegral (maxBound :: Int) = error $ "Integer width is too large."
| w0 == 0 = error $ "bvbinary width must be positive."
| otherwise = T $ "#b" <> go (fromIntegral w0)
where go :: Int -> Builder
bvbinary :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvbinary w0 u
| otherwise = T $ "#b" <> go (natValue w0)
where go :: Natural -> Builder
go 0 = mempty
go w =
let i = w - 1
b :: Builder
b = if u `testBit` i then "1" else "0"
b = if BV.testBit' i u then "1" else "0"
in b <> go i
-- | @bvdecimal x w@ constructs a bitvector term with width @w@ equal to @x `mod` 2^w@.
@ -526,29 +530,30 @@ bvbinary u w0
-- The width @w@ must be positive.
--
-- The literal uses a decimal notation.
bvdecimal :: Integer -> Natural -> Term
bvdecimal u w
| w == 0 = error "bvdecimal expects positive width"
| otherwise = T $ mconcat [ "(_ bv", Builder.decimal d, " ", Builder.decimal w, ")"]
where d = u .&. (2^w - 1)
bvdecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvdecimal w u = T $ mconcat [ "(_ bv"
, Builder.decimal d
, " "
, Builder.decimal (natValue w)
, ")"]
where d = BV.asUnsigned u
-- | @bvhexadecimal x w@ constructs a bitvector term with width @w@ equal to @x `mod` 2^w@.
--
-- The width @w@ must be a positive multiple of 4.
--
-- The literal uses hex notation.
bvhexadecimal :: Integer -> Natural -> Term
bvhexadecimal u w0
| w0 == 0 = error $ "bvhexadecimal width must be positive."
| w0 > fromIntegral (maxBound :: Int) = error $ "Integer width is too large."
| otherwise = T $ "#x" <> go (fromIntegral w0)
where go :: Int -> Builder
bvhexadecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvhexadecimal w0 u
| otherwise = T $ "#x" <> go (natValue w0)
where go :: Natural -> Builder
go 0 = mempty
go w | w < 4 = error "bvhexadecimal width must be a multiple of 4."
go w =
let i = w - 4
charBits = BV.asUnsigned (BV.select' i (knownNat @4) u)
c :: Char
c = intToDigit $ fromInteger $ (u `shiftR` i) .&. 0xf
c = intToDigit $ fromInteger charBits
in Builder.singleton c <> go i
-- | @concat x y@ returns the bitvector with the bits of @x@ followed by the bits of @y@.

96
what4/src/What4/Protocol/SMTWriter.hs
View File

@ -102,8 +102,9 @@ import Control.Monad.Reader
import Control.Monad.ST
import Control.Monad.State.Strict
import Control.Monad.Trans.Maybe
import qualified Data.Bits as Bits
import qualified Data.BitVector.Sized as BV
import Data.ByteString (ByteString)
import Data.Bits (shiftL)
import Data.IORef
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
@ -331,7 +332,7 @@ class Num v => SupportTermOps v where
intDivisible :: v -> Natural -> v
-- | Create expression from bitvector.
bvTerm :: NatRepr w -> Integer -> v
bvTerm :: NatRepr w -> BV.BV w -> v
bvNeg :: v -> v
bvAdd :: v -> v -> v
bvSub :: v -> v -> v
@ -369,12 +370,12 @@ class Num v => SupportTermOps v where
-- | @bvTestBit w i x@ returns predicate that holds if bit @i@
-- in @x@ is set to true. @w@ should be the number of bits in @x@.
bvTestBit :: NatRepr w -> Natural -> v -> v
bvTestBit w i x = (bvExtract w i 1 x .== bvTerm w1 1)
bvTestBit w i x = (bvExtract w i 1 x .== bvTerm w1 (BV.one w1))
where w1 :: NatRepr 1
w1 = knownNat
bvSumExpr :: NatRepr w -> [v] -> v
bvSumExpr w [] = bvTerm w 0
bvSumExpr w [] = bvTerm w (BV.zero w)
bvSumExpr _ (h:r) = foldl bvAdd h r
floatPZero :: FloatPrecisionRepr fpp -> v
@ -1215,15 +1216,15 @@ addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDArith rng)) = assertRange (BV
where
assertRange Nothing = return ()
assertRange (Just (lo, sz)) =
addSideCondition "bv_range" $ bvULe (bvSub t (bvTerm w lo)) (bvTerm w sz)
addSideCondition "bv_range" $ bvULe (bvSub t (bvTerm w (BV.mkBV w lo))) (bvTerm w (BV.mkBV w sz))
addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDBitwise rng)) = assertBitRange (BVD.bitbounds rng)
where
assertBitRange (lo, hi) = do
when (lo > 0) $
addSideCondition "bv_bitrange" $ (bvOr (bvTerm w lo) t) .== t
addSideCondition "bv_bitrange" $ (bvOr (bvTerm w (BV.mkBV w lo)) t) .== t
when (hi < maxUnsigned w) $
addSideCondition "bv_bitrange" $ (bvOr t (bvTerm w hi)) .== (bvTerm w hi)
addSideCondition "bv_bitrange" $ (bvOr t (bvTerm w (BV.mkBV w hi))) .== (bvTerm w (BV.mkBV w hi))
addPartialSideCond _ t (Char8TypeMap) (Just (StringAbs len)) =
do case natRangeLow len of
@ -1899,7 +1900,7 @@ appSMTExpr ae = do
BVTestBit n xe -> do
x <- mkBaseExpr xe
let this_bit = bvExtract (bvWidth xe) n 1 x
one = bvTerm (knownNat :: NatRepr 1) 1
one = bvTerm (knownNat :: NatRepr 1) (BV.one knownNat)
freshBoundTerm BoolTypeMap $ this_bit .== one
BVSlt xe ye -> do
x <- mkBaseExpr xe
@ -1982,13 +1983,13 @@ appSMTExpr ae = do
case WSum.prodRepr pd of
SR.SemiRingBVRepr SR.BVArithRepr w ->
do pd' <- WSum.prodEvalM (\a b -> pure (bvMul a b)) mkBaseExpr pd
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w 1)
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w (BV.one w))
(freshBoundTerm (BVTypeMap w))
pd'
SR.SemiRingBVRepr SR.BVBitsRepr w ->
do pd' <- WSum.prodEvalM (\a b -> pure (bvAnd a b)) mkBaseExpr pd
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w (maxUnsigned w))
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w (BV.maxUnsigned w))
(freshBoundTerm (BVTypeMap w))
pd'
sr ->
@ -2037,10 +2038,10 @@ appSMTExpr ae = do
SR.SemiRingBVRepr SR.BVArithRepr w ->
let smul c e
| c == 1 = (:[]) <$> mkBaseExpr e
| c == -1 = (:[]) . bvNeg <$> mkBaseExpr e
| c == BV.one w = (:[]) <$> mkBaseExpr e
| c == BV.maxUnsigned w = (:[]) . bvNeg <$> mkBaseExpr e
| otherwise = (:[]) <$> (bvMul (bvTerm w c)) <$> mkBaseExpr e
cnst 0 = []
cnst (BV.BV 0) = []
cnst x = [bvTerm w x]
add x y = pure (y ++ x) -- reversed for efficiency when grouped to the left
in
@ -2049,12 +2050,12 @@ appSMTExpr ae = do
SR.SemiRingBVRepr SR.BVBitsRepr w ->
let smul c e
| c == maxUnsigned w = (:[]) <$> mkBaseExpr e
| otherwise = (:[]) <$> (bvAnd (bvTerm w c)) <$> mkBaseExpr e
cnst 0 = []
| c == BV.maxUnsigned w = (:[]) <$> mkBaseExpr e
| otherwise = (:[]) <$> (bvAnd (bvTerm w c)) <$> mkBaseExpr e
cnst (BV.BV 0) = []
cnst x = [bvTerm w x]
add x y = pure (y ++ x) -- reversed for efficiency when grouped to the left
xorsum [] = bvTerm w 0
xorsum [] = bvTerm w (BV.zero w)
xorsum xs = foldr1 bvXor xs
in
freshBoundTerm (BVTypeMap w) . xorsum
@ -2117,6 +2118,8 @@ appSMTExpr ae = do
------------------------------------------
-- Bitvector operations
-- BGS: If UnaryBV is ported to BV, a lot of the unnecessary masks
-- here will go away
BVUnaryTerm t -> do
let w = UnaryBV.width t
let entries = UnaryBV.unsignedRanges t
@ -2128,12 +2131,12 @@ appSMTExpr ae = do
-- q is equivalent to v being less than or equal to the result
-- of this term (denoted by nm)
q <- mkBaseExpr pr
addSideCondition "unary term" $ q .== nm_s `bvULe` (bvTerm w l)
addSideCondition "unary term" $ q .== nm_s `bvULe` (bvTerm w u)
addSideCondition "unary term" $ q .== nm_s `bvULe` bvTerm w (BV.mkBV w l)
addSideCondition "unary term" $ q .== nm_s `bvULe` bvTerm w (BV.mkBV w u)
case entries of
(_, l, _):_ | l > 0 -> do
addSideCondition "unary term" $ bvTerm w l `bvULe` nm_s
addSideCondition "unary term" $ bvTerm w (BV.mkBV w l) `bvULe` nm_s
_ ->
return ()
return nm
@ -2142,7 +2145,7 @@ appSMTExpr ae = do
do bs' <- traverse mkBaseExpr (bvOrToList bs)
freshBoundTerm (BVTypeMap w) $!
case bs' of
[] -> bvTerm w 0
[] -> bvTerm w (BV.zero w)
x:xs -> foldl bvOr x xs
BVConcat w xe ye -> do
@ -2193,7 +2196,7 @@ appSMTExpr ae = do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
let w' = bvTerm w (intValue w)
let w' = bvTerm w (BV.width w)
y' <- asBase <$> (freshBoundTerm (BVTypeMap w) $ bvURem y w')
let lo = bvLshr x (bvSub w' y')
@ -2205,7 +2208,7 @@ appSMTExpr ae = do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
let w' = bvTerm w (intValue w)
let w' = bvTerm w (BV.width w)
y' <- asBase <$> (freshBoundTerm (BVTypeMap w) $ bvURem y w')
let lo = bvLshr x y'
@ -2219,7 +2222,7 @@ appSMTExpr ae = do
let n = intValue w' - intValue w
case someNat n of
Just (Some w2) | Just LeqProof <- isPosNat w' -> do
let zeros = bvTerm w2 0
let zeros = bvTerm w2 (BV.zero w2)
freshBoundTerm (BVTypeMap w') $ bvConcat zeros x
_ -> fail "invalid zero extension"
@ -2229,40 +2232,44 @@ appSMTExpr ae = do
let n = intValue w' - intValue w
case someNat n of
Just (Some w2) | Just LeqProof <- isPosNat w' -> do
let zeros = bvTerm w2 0
let ones = bvTerm w2 (maxUnsigned w2)
let zeros = bvTerm w2 (BV.zero w2)
let ones = bvTerm w2 (BV.maxUnsigned w2)
let sgn = bvTestBit w (natValue w - 1) x
freshBoundTerm (BVTypeMap w') $ bvConcat (ite sgn ones zeros) x
_ -> fail "invalid sign extension"
BVFill w xe ->
do x <- mkBaseExpr xe
let zeros = bvTerm w 0
let ones = bvTerm w (maxUnsigned w)
let zeros = bvTerm w (BV.zero w)
let ones = bvTerm w (BV.maxUnsigned w)
freshBoundTerm (BVTypeMap w) $ ite x ones zeros
BVPopcount w xe ->
do x <- mkBaseExpr xe
let zs = [ ite (bvTestBit w idx x) (bvTerm w 1) (bvTerm w 0)
let zs = [ ite (bvTestBit w idx x) (bvTerm w (BV.one w)) (bvTerm w (BV.zero w))
| idx <- [ 0 .. natValue w - 1 ]
]
freshBoundTerm (BVTypeMap w) $! bvSumExpr w zs
-- BGS: The mkBV call here shouldn't be necessary, but it is
-- unless we use a NatRepr as the index
BVCountLeadingZeros w xe ->
do x <- mkBaseExpr xe
freshBoundTerm (BVTypeMap w) $! go 0 x
where
go !idx x
| idx < natValue w = ite (bvTestBit w (natValue w - idx - 1) x) (bvTerm w (toInteger idx)) (go (idx+1) x)
| otherwise = bvTerm w (intValue w)
| idx < natValue w = ite (bvTestBit w (natValue w - idx - 1) x) (bvTerm w (BV.mkBV w (toInteger idx))) (go (idx+1) x)
| otherwise = bvTerm w (BV.width w)
-- BGS: The mkBV call here shouldn't be necessary, but it is
-- unless we use a NatRepr as the index
BVCountTrailingZeros w xe ->
do x <- mkBaseExpr xe
freshBoundTerm (BVTypeMap w) $! go 0 x
where
go !idx x
| idx < natValue w = ite (bvTestBit w idx x) (bvTerm w (toInteger idx)) (go (idx+1) x)
| otherwise = bvTerm w (intValue w)
| idx < natValue w = ite (bvTestBit w idx x) (bvTerm w (BV.mkBV w (toInteger idx))) (go (idx+1) x)
| otherwise = bvTerm w (BV.width w)
------------------------------------------
-- String operations
@ -2441,10 +2448,13 @@ appSMTExpr ae = do
addSideCondition "float_binary" $
floatFromBinary fpp val .== xe
-- qnan: 0b0 0b1..1 0b10..0
let qnan = bvTerm (addNat eb sb) $ shiftL
-- BGS: I tried using bv-sized primitives for this and it would
-- have required a lot of proofs. Probable worth revisiting this.
let qnan = bvTerm (addNat eb sb) $
BV.mkBV (addNat eb sb) $
Bits.shiftL
(2 ^ (natValue eb + 1) - 1)
(fromIntegral (natValue sb - 2))
-- return (ite (fp.isNaN xe) qnan val)
freshBoundTerm (BVTypeMap $ addNat eb sb) $ ite (floatIsNaN xe) qnan val
FloatFromBinary fpp x -> do
xe <- mkBaseExpr x
@ -2854,17 +2864,19 @@ data SMTEvalFunctions h
= SMTEvalFunctions { smtEvalBool :: Term h -> IO Bool
-- ^ Given a SMT term for a Boolean value, this should
-- whether the term is assigned true or false.
, smtEvalBV :: Int -> Term h -> IO Integer
, smtEvalBV :: forall w . NatRepr w -> Term h -> IO (BV.BV w)
-- ^ Given a bitwidth, and a SMT term for a bitvector
-- with that bitwidth, this should return an unsigned
-- integer with the value of that bitvector.
, smtEvalReal :: Term h -> IO Rational
-- ^ Given a SMT term for real value, this should
-- return a rational value for that term.
, smtEvalFloat :: Term h -> IO Integer
-- ^ Given a SMT term for a floating-point value,
-- this returns an unsigned integer with the bits
-- of the IEEE-754 representation.
, smtEvalFloat :: forall fpp . FloatPrecisionRepr fpp -> Term h -> IO (BV.BV (FloatPrecisionBits fpp))
-- ^ Given floating point format, and an SMT
-- term for a floating-point value in that
-- format, this returns an unsigned integer
-- with the bits of the IEEE-754
-- representation.
, smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper h)
-- ^ If 'Just', a function to read arrays whose domain
-- and codomain are both bitvectors. If 'Nothing',
@ -2918,9 +2930,9 @@ getSolverVal :: forall h t tp
-> Term h
-> IO (GroundValue tp)
getSolverVal _ smtFns BoolTypeMap tm = smtEvalBool smtFns tm
getSolverVal _ smtFns (BVTypeMap w) tm = smtEvalBV smtFns (widthVal w) tm
getSolverVal _ smtFns (BVTypeMap w) tm = smtEvalBV smtFns w tm
getSolverVal _ smtFns RealTypeMap tm = smtEvalReal smtFns tm
getSolverVal _ smtFns (FloatTypeMap _) tm = smtEvalFloat smtFns tm
getSolverVal _ smtFns (FloatTypeMap fpp) tm = smtEvalFloat smtFns fpp tm
getSolverVal _ smtFns Char8TypeMap tm = Char8Literal <$> smtEvalString smtFns tm
getSolverVal _ smtFns NatTypeMap tm = do
r <- smtEvalReal smtFns tm

14
what4/src/What4/SWord.hs
View File

@ -107,6 +107,7 @@ import Numeric.Natural
import GHC.TypeNats
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.NatRepr
import Data.Parameterized.Some(Some(..))
@ -136,13 +137,13 @@ instance Show (SWord sym) where
bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsSignedInteger ZBV = Just 0
bvAsSignedInteger (DBV (bv :: SymBV sym w)) =
W.asSignedBV bv
BV.asSigned (W.bvWidth bv) <$> W.asBV bv
-- | Return the unsigned value if this is a constant bitvector
bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsUnsignedInteger ZBV = Just 0
bvAsUnsignedInteger (DBV (bv :: SymBV sym w)) =
W.asUnsignedBV bv
BV.asUnsigned <$> W.asBV bv
unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
@ -194,7 +195,7 @@ bvLit _ w _
bvLit sym w dat
| Just (Some rw) <- someNat w
, Just LeqProof <- isPosNat rw
= DBV <$> W.bvLit sym rw dat
= DBV <$> W.bvLit sym rw (BV.mkBV rw dat)
| otherwise
= panic "bvLit" ["size of bitvector is < 0 or >= maxInt", show w]
@ -362,7 +363,8 @@ w_bvLg2 sym x = go 0
size :: Integer
size = intValue w
lit :: Integer -> IO (SymBV sym w)
lit n = W.bvLit sym w n
-- BGS: This change could lead to some inefficency
lit n = W.bvLit sym w (BV.mkBV w n)
go :: Integer -> IO (SymBV sym w)
go i | i < size = do
x' <- lit (2 ^ i)
@ -673,7 +675,7 @@ reduceShift wop sym (DBV x) (DBV y) =
-- Truncation is OK because the value will always fit after
-- clamping.
NatLT _diff ->
do wx <- W.bvLit sym (W.bvWidth y) (intValue (W.bvWidth x))
do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
y' <- W.bvTrunc sym (W.bvWidth x) =<< bvMax sym y wx
DBV <$> wop sym x y'
@ -698,7 +700,7 @@ reduceRotate wop sym (DBV x) (DBV y) =
-- Truncation is OK because the value will always
-- fit after modulo reduction
NatLT _diff ->
do wx <- W.bvLit sym (W.bvWidth y) (intValue (W.bvWidth x))
do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
y' <- W.bvTrunc sym (W.bvWidth x) =<< W.bvUrem sym y wx
DBV <$> wop sym x y'

21
what4/src/What4/SemiRing.hs
View File

@ -74,12 +74,11 @@ module What4.SemiRing
) where
import GHC.TypeNats
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.Kind
import Data.Hashable
import Data.Parameterized.Classes
import Data.Parameterized.TH.GADT
import Data.Parameterized.NatRepr
import Numeric.Natural
import What4.BaseTypes
@ -144,7 +143,7 @@ type family Coefficient (sr :: SemiRing) :: Type where
Coefficient SemiRingNat = Natural
Coefficient SemiRingInteger = Integer
Coefficient SemiRingReal = Rational
Coefficient (SemiRingBV fv w) = Integer
Coefficient (SemiRingBV fv w) = BV.BV w
-- | The 'Occurrence' family counts how many times a term occurs in a
-- product. For most semirings, this is just a natural number
@ -216,29 +215,29 @@ zero :: SemiRingRepr sr -> Coefficient sr
zero SemiRingNatRepr = 0 :: Natural
zero SemiRingIntegerRepr = 0 :: Integer
zero SemiRingRealRepr = 0 :: Rational
zero (SemiRingBVRepr BVArithRepr _) = 0 :: Integer
zero (SemiRingBVRepr BVBitsRepr _) = 0 :: Integer
zero (SemiRingBVRepr BVArithRepr w) = BV.zero w
zero (SemiRingBVRepr BVBitsRepr w) = BV.zero w
one :: SemiRingRepr sr -> Coefficient sr
one SemiRingNatRepr = 1 :: Natural
one SemiRingIntegerRepr = 1 :: Integer
one SemiRingRealRepr = 1 :: Rational
one (SemiRingBVRepr BVArithRepr _) = 1 :: Integer
one (SemiRingBVRepr BVBitsRepr w) = maxUnsigned w :: Integer
one (SemiRingBVRepr BVArithRepr w) = BV.mkBV w 1
one (SemiRingBVRepr BVBitsRepr w) = BV.maxUnsigned w
add :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
add SemiRingNatRepr = (+)
add SemiRingIntegerRepr = (+)
add SemiRingRealRepr = (+)
add (SemiRingBVRepr BVArithRepr w) = \x y -> toUnsigned w (x + y)
add (SemiRingBVRepr BVBitsRepr _) = xor
add (SemiRingBVRepr BVArithRepr w) = BV.add w
add (SemiRingBVRepr BVBitsRepr _) = BV.xor
mul :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
mul SemiRingNatRepr = (*)
mul SemiRingIntegerRepr = (*)
mul SemiRingRealRepr = (*)
mul (SemiRingBVRepr BVArithRepr w) = \x y -> toUnsigned w (x * y)
mul (SemiRingBVRepr BVBitsRepr _) = (.&.)
mul (SemiRingBVRepr BVArithRepr w) = BV.mul w
mul (SemiRingBVRepr BVBitsRepr _) = BV.and
eq :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
eq SemiRingNatRepr = (==)

24
what4/src/What4/Solver/Boolector.hs
View File

@ -12,8 +12,10 @@
------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module What4.Solver.Boolector
( Boolector(..)
, boolectorPath
@ -31,12 +33,15 @@ import Control.Lens(folded)
import Control.Monad
import Control.Monad.Identity
import Data.Bits ( (.|.) )
import qualified Data.BitVector.Sized as BV
import qualified Data.ByteString.UTF8 as UTF8
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Parameterized.Some ( Some(..) )
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import Numeric.Natural
import System.Exit
import qualified System.IO.Streams as Streams
import System.Process
@ -159,11 +164,15 @@ boolectorBoolValue "1" = return True
boolectorBoolValue "0" = return False
boolectorBoolValue s = fail $ "Could not parse " ++ s ++ " as a Boolean."
boolectorBVValue :: MonadFail m => Int -> String -> m Integer
boolectorBVValue w0 s0 = go 0 0 s0
where go w r [] = do
when (w /= w0) $ fail "Unexpected number of bits in output."
return r
boolectorBVValue :: forall m w . MonadFail m => NatRepr w -> String -> m (BV.BV w)
boolectorBVValue w0 s0 = do
(wNatural, x) <- go 0 0 s0
Some w <- return $ mkNatRepr wNatural
case w0 `testEquality` w of
Just Refl -> return $ BV.mkBV w0 x
Nothing -> fail "Unexpected number of bits in output."
where go :: Natural -> Integer -> String -> m (Natural, Integer)
go w r [] = return (w, r)
go w r ('1':s) = go (w+1) (2 * r + 1) s
go w r ('0':s) = go (w+1) (2 * r) s
go _ _ _ = fail $ "Could not parse " ++ s0 ++ " as a bitvector."
@ -192,9 +201,10 @@ parseBoolectorOutput c out_lines =
let mdl_lines = filter (/= "") mdl_lines0
m <- Map.fromList <$> mapM parseBoolectorOutputLine mdl_lines
let evalBool tm = lookupBoolectorVar m boolectorBoolValue $ Builder.toLazyText $ SMT2.renderTerm tm
let evalBV w tm = lookupBoolectorVar m (boolectorBVValue w) $ Builder.toLazyText $ SMT2.renderTerm tm
let evalBV :: NatRepr w -> SMT2.Term -> IO (BV.BV w)
evalBV w tm = lookupBoolectorVar m (boolectorBVValue w) $ Builder.toLazyText $ SMT2.renderTerm tm
let evalReal _ = fail "Boolector does not support real variables."
let evalFloat _ = fail "Boolector does not support floats."
let evalFloat _ _ = fail "Boolector does not support floats."
let evalStr _ = fail "Boolector does not support strings."
let evalFns = SMTEvalFunctions { smtEvalBool = evalBool
, smtEvalBV = evalBV

4
what4/src/What4/Solver/DReal.hs
View File

@ -137,7 +137,7 @@ getAvgBindings c m = do
evalStr _ = fail "dReal does not support strings."
evalReal tm = do
return $ maybe 0 drealAvgBinding $ Map.lookup (Builder.toLazyText (SMT2.renderTerm tm)) m
evalFloat _ = fail "dReal does not support floats."
evalFloat _ _ = fail "dReal does not support floats."
let evalFns = SMTWriter.SMTEvalFunctions { SMTWriter.smtEvalBool = evalBool
, SMTWriter.smtEvalBV = evalBV
, SMTWriter.smtEvalReal = evalReal
@ -159,7 +159,7 @@ getMaybeEval proj c m = do
case proj =<< Map.lookup (Builder.toLazyText (SMT2.renderTerm tm)) m of
Just v -> return v
Nothing -> throwIO (userError "unbound")
evalFloat _ = fail "dReal does not support floats."
evalFloat _ _ = fail "dReal does not support floats."
let evalFns = SMTWriter.SMTEvalFunctions { SMTWriter.smtEvalBool = evalBool
, SMTWriter.smtEvalBV = evalBV
, SMTWriter.smtEvalReal = evalReal

11
what4/src/What4/Solver/Yices.hs
View File

@ -75,6 +75,7 @@ import Control.Monad
import Control.Monad.Identity
import qualified Data.Attoparsec.Text as Atto
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.IORef
import Data.Foldable (toList)
@ -232,7 +233,7 @@ instance SupportTermOps (YicesTerm s) where
(.>=) = bin_app ">="
bvTerm w u = term_app "mk-bv" [width_term w, decimal_term d]
where d = toUnsigned w u
where d = BV.asUnsigned u
bvNeg x = term_app "bv-neg" [x]
bvAdd = bin_app "bv-add"
@ -558,7 +559,7 @@ instance SMTReadWriter (Connection s) where
SMTEvalFunctions { smtEvalBool = yicesEvalBool conn resp
, smtEvalBV = \w -> yicesEvalBV w conn resp
, smtEvalReal = yicesEvalReal conn resp
, smtEvalFloat = \_ -> fail "Yices does not support floats."
, smtEvalFloat = \_ _ -> fail "Yices does not support floats."
, smtEvalBvArray = Nothing
, smtEvalString = \_ -> fail "Yices does not support strings."
}
@ -861,17 +862,17 @@ yicesBV w =
readBit w (Text.unpack digits)
-- | Send eval command and get result back.
yicesEvalBV :: Int -> Eval s t Integer
yicesEvalBV :: NatRepr w -> Eval s t (BV.BV w)
yicesEvalBV w conn resp tm =
do eval conn tm
mb <- tryJust filterAsync (Streams.parseFromStream (skipSpaceOrNewline *> yicesBV w) resp)
mb <- tryJust filterAsync (Streams.parseFromStream (skipSpaceOrNewline *> yicesBV (widthVal w)) resp)
case mb of
Left (SomeException ex) ->
fail $ unlines
[ "Could not parse bitvector value returned by yices: "
, displayException ex
]
Right b -> pure b
Right b -> pure (BV.mkBV w b)
readBit :: MonadFail m => Int -> String -> m Integer
readBit w0 = go 0 0

31
what4/test/ExprBuilderSMTLib2.hs
View File

@ -17,6 +17,7 @@ import Test.Tasty.HUnit
import Control.Exception (bracket, try, finally, SomeException)
import Control.Monad (void)
import qualified Data.BitVector.Sized as BV
import qualified Data.ByteString as BS
import qualified Data.Binary.IEEE754 as IEEE754
import Data.Foldable
@ -252,8 +253,8 @@ testFloatSat0 = testCase "Sat float formula" $ withZ3 $ \sym s -> do
p1 <- floatEq sym y e1
p2 <- andPred sym p0 p1
withModel s p2 $ \groundEval -> do
(@?=) (toInteger $ IEEE754.floatToWord 2.5) =<< groundEval x
y_val <- IEEE754.wordToFloat . fromInteger <$> groundEval y
(@?=) (BV.word32 $ IEEE754.floatToWord 2.5) =<< groundEval x
y_val <- IEEE754.wordToFloat . fromInteger . BV.asUnsigned <$> groundEval y
assertBool ("expected y = +infinity, actual y = " ++ show y_val) $
isInfinite y_val && 0 < y_val
@ -267,7 +268,7 @@ testFloatSat1 = testCase "Sat float formula" $ withZ3 $ \sym s -> do
p1 <- floatLe sym x e1
p2 <- andPred sym p0 p1
withModel s p2 $ \groundEval -> do
x_val <- IEEE754.wordToFloat . fromInteger <$> groundEval x
x_val <- IEEE754.wordToFloat . fromInteger . BV.asUnsigned <$> groundEval x
assertBool ("expected x in [0.5, 1.5], actual x = " ++ show x_val) $
0.5 <= x_val && x_val <= 1.5
@ -334,9 +335,9 @@ testBVSelectShl :: TestTree
testBVSelectShl = testCase "select shl simplification" $
withSym FloatIEEERepr $ \sym -> do
x <- freshConstant sym (userSymbol' "x") knownRepr
e0 <- bvLit sym (knownNat @64) 0
e0 <- bvLit sym (knownNat @64) (BV.zero knownNat)
e1 <- bvConcat sym e0 x
e2 <- bvShl sym e1 =<< bvLit sym knownRepr 64
e2 <- bvShl sym e1 =<< bvLit sym knownRepr (BV.mkBV knownNat 64)
e3 <- bvSelect sym (knownNat @64) (knownNat @64) e2
e3 @?= x
@ -344,8 +345,8 @@ testBVSelectLshr :: TestTree
testBVSelectLshr = testCase "select lshr simplification" $
withSym FloatIEEERepr $ \sym -> do
x <- freshConstant sym (userSymbol' "x") knownRepr
e0 <- bvConcat sym x =<< bvLit sym (knownNat @64) 0
e1 <- bvLshr sym e0 =<< bvLit sym knownRepr 64
e0 <- bvConcat sym x =<< bvLit sym (knownNat @64) (BV.zero knownNat)
e1 <- bvLshr sym e0 =<< bvLit sym knownRepr (BV.mkBV knownNat 64)
e2 <- bvSelect sym (knownNat @0) (knownNat @64) e1
e2 @?= x
@ -367,7 +368,7 @@ testUninterpretedFunctionScope = testCase "uninterpreted function scope" $
testBVIteNesting :: TestTree
testBVIteNesting = testCase "nested bitvector ites" $ withZ3 $ \sym s -> do
bv0 <- bvLit sym (knownNat @32) 0
bv0 <- bvLit sym (knownNat @32) (BV.zero knownNat)
let setSymBit bv idx = do
c1 <- freshConstant sym (userSymbol' ("c1_" ++ show idx)) knownRepr
c2 <- freshConstant sym (userSymbol' ("c2_" ++ show idx)) knownRepr
@ -389,11 +390,11 @@ testRotate1 :: TestTree
testRotate1 = testCase "rotate test1" $ withOnlineZ3 $ \sym s -> do
bv <- freshConstant sym (userSymbol' "bv") (BaseBVRepr (knownNat @32))
bv1 <- bvRol sym bv =<< bvLit sym knownNat 8
bv2 <- bvRol sym bv1 =<< bvLit sym knownNat 16
bv3 <- bvRol sym bv2 =<< bvLit sym knownNat 8
bv4 <- bvRor sym bv2 =<< bvLit sym knownNat 24
bv5 <- bvRor sym bv2 =<< bvLit sym knownNat 28
bv1 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 8)
bv2 <- bvRol sym bv1 =<< bvLit sym knownNat (BV.mkBV knownNat 16)
bv3 <- bvRol sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 8)
bv4 <- bvRor sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 24)
bv5 <- bvRor sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 28)
res <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv3
isUnsat res @? "unsat1"
@ -411,7 +412,7 @@ testRotate2 = testCase "rotate test2" $ withOnlineZ3 $ \sym s -> do
bv1 <- bvRol sym bv amt
bv2 <- bvRor sym bv1 amt
bv3 <- bvRol sym bv =<< bvLit sym knownNat 20
bv3 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 20)
bv == bv2 @? "syntactic equality"
@ -428,7 +429,7 @@ testRotate3 = testCase "rotate test3" $ withOnlineZ3 $ \sym s -> do
bv1 <- bvRol sym bv amt
bv2 <- bvRor sym bv1 amt
bv3 <- bvRol sym bv =<< bvLit sym knownNat 3
bv3 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 3)
-- Note, because 7 is not a power of two, this simplification doesn't quite
-- work out... it would probably be significant work to make it do so.

17
what4/test/ExprsTest.hs
View File

@ -19,6 +19,7 @@ verify the correctness of those.
import Control.Monad.IO.Class ( liftIO )
import Data.Bits
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Nonce
import GenWhat4Expr
import Hedgehog
@ -72,13 +73,13 @@ testBvIsNeg = testGroup "bvIsNeg"
testCase "-1.32 bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) ((-1) .&. allbits32)
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat ((-1) .&. allbits32))
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool True) @=? r
, testCase "-1 bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) (-1)
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat (-1))
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool True) @=? r
@ -86,39 +87,39 @@ testBvIsNeg = testGroup "bvIsNeg"
, testCase "0xffffffff bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) allbits32
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat allbits32)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool True) @=? r
, testCase "0x80000000 bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) 0x80000000
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat 0x80000000)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool True) @=? r
, testCase "0x7fffffff !bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) 0x7fffffff
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat 0x7fffffff)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool False) @=? r
, testCase "0 !bvIsNeg.32" $ do
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) 0
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.zero knownNat)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool False) @=? r
, testProperty "bvIsNeg.32" $ property $ do
i <- forAll $ Gen.integral $ Range.linear (-10) (-1)
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) i
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat i)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool True) === r
, testProperty "!bvIsNeg.32" $ property $ do
i <- forAll $ Gen.integral $ Range.linear 0 10
r <- liftIO $ withTestSolver $ \sym -> do
v <- bvLit sym (knownRepr :: NatRepr 32) i
v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat i)
asConcrete <$> bvIsNeg sym v
Just (ConcreteBool False) === r
]

11
what4/test/GenWhat4Expr.hs
View File

@ -37,6 +37,7 @@ 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 )
@ -508,7 +509,7 @@ genBV8TestExpr = let ret8 = return . TE_BV8 in
Gen.recursive Gen.choice
[
do n <- genBV8val
ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> bvLit sym knownRepr n
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
@ -549,7 +550,7 @@ genBV16TestExpr = let ret16 = return . TE_BV16 in
Gen.recursive Gen.choice
[
do n <- genBV16val
ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> bvLit sym knownRepr n
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
@ -592,7 +593,7 @@ genBV32TestExpr = let ret32 = return . TE_BV32 in
Gen.recursive Gen.choice
[
do n <- genBV32val
ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> bvLit sym knownRepr n
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
@ -636,7 +637,7 @@ genBV64TestExpr = let ret64 = return . TE_BV64 in
Gen.recursive Gen.choice
[
do n <- genBV64val
ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> bvLit sym knownRepr n
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
@ -765,7 +766,7 @@ bvExprs bvTerm conTE projTE teSubCon expr width toWord =
then conTE $ teSubCon
(pdesc t <> " +1")
(testval t + 1)
(\sym -> do lit1 <- bvLit sym knownRepr 1
(\sym -> do lit1 <- bvLit sym knownRepr (BV.one knownNat)
orig <- expr t sym
bvAdd sym orig lit1)

9
what4/test/IteExprs.hs
View File

@ -19,6 +19,7 @@ those.
-}
import Control.Monad.IO.Class ( liftIO )
import qualified Data.BitVector.Sized as BV
import Data.List ( isInfixOf )
import Data.Parameterized.Nonce
import GenWhat4Expr
@ -99,13 +100,13 @@ calcBVIte :: ITETestCond -> CalcReturn (BaseBVType 16)
calcBVIte itc =
withTestSolver $ \sym -> do
let w = knownRepr :: NatRepr 16
l <- bvLit sym w 12890
r <- bvLit sym w 8293
l <- bvLit sym w (BV.mkBV w 12890)
r <- bvLit sym w (BV.mkBV w 8293)
c <- cond itc sym
i <- baseTypeIte sym c l r
let e = case expect itc of
Then -> 12890
Else -> 8293
Then -> BV.mkBV w 12890
Else -> BV.mkBV w 8293
return (asConcrete i, ConcreteBV w e, desc itc, show c)
-- | Given a function that returns a condition, generate ITE's of

6
what4/what4.cabal
View File

@ -22,6 +22,7 @@ library
ansi-wl-pprint,
bimap >= 0.2,
bifunctors >= 5,
bv-sized >= 1.0.0,
bytestring,
deriving-compat >= 0.5,
containers >= 0.5.0.0,
@ -38,7 +39,7 @@ library
lens,
mtl,
panic >= 0.3,
parameterized-utils >= 1.0.8 && < 2.2,
parameterized-utils >= 2.1 && < 2.2,
process,
QuickCheck >= 2.14 && < 2.15,
scientific,
@ -144,6 +145,7 @@ test-suite expr-builder-smtlib2
build-depends:
base,
bv-sized,
bytestring,
containers,
data-binary-ieee754,
@ -167,6 +169,7 @@ test-suite exprs_tests
GenWhat4Expr
build-depends: base
, bv-sized
, hedgehog >= 1.0.2
, parameterized-utils
, tasty >= 0.10
@ -187,6 +190,7 @@ test-suite iteexprs_tests
GenWhat4Expr
build-depends: base
, bv-sized
, hedgehog >= 1.0.2
, parameterized-utils
, tasty >= 0.10