{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module What4.Utils.ResolveBounds.BV
( resolveSymBV
, SearchStrategy(..)
, ResolvedSymBV(..)
) where
import Data.BitVector.Sized ( BV )
import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.NatRepr as PN
import qualified Prettyprinter as PP
import qualified What4.Expr.Builder as WEB
import qualified What4.Expr.GroundEval as WEG
import qualified What4.Interface as WI
import qualified What4.Protocol.Online as WPO
import qualified What4.Protocol.SMTWriter as WPS
import qualified What4.SatResult as WSat
import qualified What4.Utils.BVDomain.Arith as WUBA
data ResolvedSymBV w
= BVConcrete (BV w)
| BVSymbolic (WUBA.Domain w)
instance Show (ResolvedSymBV w) where
showsPrec :: Int -> ResolvedSymBV w -> ShowS
showsPrec Int
_p ResolvedSymBV w
res =
case ResolvedSymBV w
res of
BVConcrete BV w
bv ->
String -> ShowS
showString String
"BVConcrete " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 BV w
bv
BVSymbolic Domain w
d ->
let (Integer
lb, Integer
ub) = forall (w :: Nat). Domain w -> (Integer, Integer)
WUBA.ubounds Domain w
d in
String -> ShowS
showString String
"BVSymbolic ["
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Integer
lb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
", "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Integer
ub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]"
data SearchStrategy
= ExponentialSearch
| BinarySearch
instance PP.Pretty SearchStrategy where
pretty :: forall ann. SearchStrategy -> Doc ann
pretty SearchStrategy
ExponentialSearch = forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"exponential search"
pretty SearchStrategy
BinarySearch = forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"binary search"
resolveSymBV ::
forall w sym solver scope st fs
. ( 1 PN.<= w
, sym ~ WEB.ExprBuilder scope st fs
, WPO.OnlineSolver solver
)
=> sym
-> SearchStrategy
-> PN.NatRepr w
-> WPO.SolverProcess scope solver
-> WI.SymBV sym w
-> IO (ResolvedSymBV w)
resolveSymBV :: forall (w :: Nat) sym solver scope (st :: Type -> Type) fs.
(1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) =>
sym
-> SearchStrategy
-> NatRepr w
-> SolverProcess scope solver
-> SymBV sym w
-> IO (ResolvedSymBV w)
resolveSymBV sym
sym SearchStrategy
searchStrat NatRepr w
w SolverProcess scope solver
proc SymBV sym w
symBV =
case forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
WI.asBV SymBV sym w
symBV of
Just BV w
bv -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). BV w -> ResolvedSymBV w
BVConcrete BV w
bv
Maybe (BV w)
Nothing -> do
BV w
modelForBV <- forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$ do
SatResult (GroundEvalFn scope) ()
msat <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
WPO.checkAndGetModel SolverProcess scope solver
proc String
"resolveSymBV (check with initial assumptions)"
GroundEvalFn scope
model <- case SatResult (GroundEvalFn scope) ()
msat of
SatResult (GroundEvalFn scope) ()
WSat.Unknown -> forall a. IO a
failUnknown
WSat.Unsat{} -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"resolveSymBV: Initial assumptions are unsatisfiable"
WSat.Sat GroundEvalFn scope
model -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GroundEvalFn scope
model
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WEG.groundEval GroundEvalFn scope
model SymBV sym w
symBV
Bool
isSymbolic <- forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$ do
BoolExpr scope
block <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym w
symBV forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w BV w
modelForBV
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
block
SatResult () ()
msat <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
WPO.check SolverProcess scope solver
proc String
"resolveSymBV (check under assumption that model cannot happen)"
case SatResult () ()
msat of
SatResult () ()
WSat.Unknown -> forall a. IO a
failUnknown
WSat.Sat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
WSat.Unsat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
if Bool
isSymbolic
then
case SearchStrategy
searchStrat of
SearchStrategy
ExponentialSearch -> do
BV w
lowerBound <- BV w -> IO (BV w)
computeLowerBoundExponential BV w
modelForBV
BV w
upperBound <- BV w -> IO (BV w)
computeUpperBoundExponential BV w
modelForBV
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Domain w -> ResolvedSymBV w
BVSymbolic forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
WUBA.range NatRepr w
w
(forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
lowerBound) (forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
upperBound)
SearchStrategy
BinarySearch -> do
BV w
lowerBound <- BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
bvZero BV w
bvMaxUnsigned
BV w
upperBound <- BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
bvZero BV w
bvMaxUnsigned
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Domain w -> ResolvedSymBV w
BVSymbolic forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
WUBA.range NatRepr w
w
(forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
lowerBound) (forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
upperBound)
else forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). BV w -> ResolvedSymBV w
BVConcrete BV w
modelForBV
where
conn :: WPS.WriterConn scope solver
conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
WPO.solverConn SolverProcess scope solver
proc
failUnknown :: forall a. IO a
failUnknown :: forall a. IO a
failUnknown = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"resolveSymBV: Resolving value yielded UNKNOWN"
bvZero :: BV w
bvZero :: BV w
bvZero = forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w
bvOne :: BV w
bvOne :: BV w
bvOne = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr w
w
bvTwo :: BV w
bvTwo :: BV w
bvTwo = forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
2
bvMaxUnsigned :: BV w
bvMaxUnsigned :: BV w
bvMaxUnsigned = forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w
computeLowerBoundExponential :: BV w -> IO (BV w)
computeLowerBoundExponential :: BV w -> IO (BV w)
computeLowerBoundExponential BV w
start = BV w -> BV w -> IO (BV w)
go BV w
start BV w
bvOne
where
go :: BV w -> BV w -> IO (BV w)
go :: BV w -> BV w -> IO (BV w)
go BV w
previouslyTried BV w
diff
|
BV w
start forall (w :: Nat). BV w -> BV w -> Bool
`BV.ult` BV w
diff
= BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
bvZero BV w
previouslyTried
|
Bool
otherwise
= do let nextToTry :: BV w
nextToTry = forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w BV w
start BV w
diff
Bool
exceedsLB <- BV w -> IO Bool
checkExceedsLowerBound BV w
nextToTry
if |
Bool
exceedsLB
-> BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
nextToTry BV w
previouslyTried
|
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff forall a. Num a => a -> a -> a
* Integer
2 forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
bvMaxUnsigned
-> BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
bvZero BV w
nextToTry
|
Bool
otherwise
-> BV w -> BV w -> IO (BV w)
go BV w
nextToTry forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
diff BV w
bvTwo
computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
l BV w
r
|
BV w
l forall a. Eq a => a -> a -> Bool
== BV w
r
= forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BV w
l
|
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w BV w
r BV w
l forall a. Ord a => a -> a -> Bool
< BV w
bvTwo
= do Bool
lExceedsLB <- BV w -> IO Bool
checkExceedsLowerBound BV w
l
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if Bool
lExceedsLB then BV w
r else BV w
l
|
Bool
otherwise
= do let nextToTry :: BV w
nextToTry = forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w ((forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
l forall a. Num a => a -> a -> a
+ forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
r) forall a. Integral a => a -> a -> a
`div` Integer
2)
Bool
exceedsLB <- BV w -> IO Bool
checkExceedsLowerBound BV w
nextToTry
if Bool
exceedsLB
then BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
nextToTry BV w
r
else BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
l BV w
nextToTry
checkExceedsLowerBound :: BV w -> IO Bool
checkExceedsLowerBound :: BV w -> IO Bool
checkExceedsLowerBound BV w
bv = forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$ do
BoolExpr scope
leLowerBound <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUle sym
sym SymBV sym w
symBV forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w BV w
bv
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
leLowerBound
SatResult () ()
msat <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
WPO.check SolverProcess scope solver
proc String
"resolveSymBV (check if lower bound has been exceeded)"
case SatResult () ()
msat of
SatResult () ()
WSat.Unknown -> forall a. IO a
failUnknown
WSat.Sat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
WSat.Unsat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
computeUpperBoundExponential :: BV w -> IO (BV w)
computeUpperBoundExponential :: BV w -> IO (BV w)
computeUpperBoundExponential BV w
start = BV w -> BV w -> IO (BV w)
go BV w
start BV w
bvOne
where
go :: BV w -> BV w -> IO (BV w)
go :: BV w -> BV w -> IO (BV w)
go BV w
previouslyTried BV w
diff
|
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
start forall a. Num a => a -> a -> a
+ forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
bvMaxUnsigned
= BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
previouslyTried BV w
bvMaxUnsigned
| Bool
otherwise
= do let nextToTry :: BV w
nextToTry = forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
w BV w
start BV w
diff
Bool
exceedsUB <- BV w -> IO Bool
checkExceedsUpperBound BV w
nextToTry
if |
Bool
exceedsUB
-> BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
previouslyTried BV w
nextToTry
|
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff forall a. Num a => a -> a -> a
* Integer
2 forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
bvMaxUnsigned
-> BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
nextToTry BV w
bvMaxUnsigned
|
Bool
otherwise
-> BV w -> BV w -> IO (BV w)
go BV w
nextToTry forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
diff BV w
bvTwo
computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
l BV w
r
|
BV w
l forall a. Eq a => a -> a -> Bool
== BV w
r
= forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BV w
l
|
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w BV w
r BV w
l forall a. Ord a => a -> a -> Bool
< BV w
bvTwo
= do Bool
rExceedsUB <- BV w -> IO Bool
checkExceedsUpperBound BV w
r
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if Bool
rExceedsUB then BV w
l else BV w
r
|
Bool
otherwise
= do let nextToTry :: BV w
nextToTry = forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w ((forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
l forall a. Num a => a -> a -> a
+ forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
r) forall a. Integral a => a -> a -> a
`div` Integer
2)
Bool
exceedsUB <- BV w -> IO Bool
checkExceedsUpperBound BV w
nextToTry
if Bool
exceedsUB
then BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
l BV w
nextToTry
else BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
nextToTry BV w
r
checkExceedsUpperBound :: BV w -> IO Bool
checkExceedsUpperBound :: BV w -> IO Bool
checkExceedsUpperBound BV w
bv = forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$ do
BoolExpr scope
geUpperBound <- forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUge sym
sym SymBV sym w
symBV forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w BV w
bv
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
geUpperBound
SatResult () ()
msat <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
WPO.check SolverProcess scope solver
proc String
"resolveSymBV (check if upper bound has been exceeded)"
case SatResult () ()
msat of
SatResult () ()
WSat.Unknown -> forall a. IO a
failUnknown
WSat.Sat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
WSat.Unsat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True