{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

{-|
Module           : What4.Utils.ResolveBounds.BV
Description      : Resolve the lower and upper bounds of a SymBV
Copyright        : (c) Galois, Inc 2021
License          : BSD3
Maintainer       : Ryan Scott <rscott@galois.com>

A utility for using an 'WPO.OnlineSolver' to query if a 'WI.SymBV' is concrete
or symbolic, and if it is symbolic, what the lower and upper bounds are.
-}
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

-- | The results of an 'WPO.OnlineSolver' trying to resolve a 'WI.SymBV' as
-- concrete.
data ResolvedSymBV w
  = BVConcrete (BV w)
    -- ^ A concrete bitvector, including its value as a 'BV'.
  | BVSymbolic (WUBA.Domain w)
    -- ^ A symbolic 'SymBV', including its lower and upper bounds as a
    --   'WUBA.Domain'.

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 " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> BV w -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 BV w
bv
      BVSymbolic Domain w
d  ->
        let (Integer
lb, Integer
ub) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
WUBA.ubounds Domain w
d in
          String -> ShowS
showString String
"BVSymbolic ["
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Integer
lb
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
", "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Integer
ub
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]"

-- | The strategy to use to search for lower and upper bounds in
-- 'resolveSymBV'.
data SearchStrategy
  = ExponentialSearch
    -- ^ After making an initial guess for a bound, increase (for upper bounds)
    --   or decrease (for lower bounds) the initial guess by an exponentially
    --   increasing amount (1, 2, 4, 8, ...) until the bound has been exceeded.
    --   At that point, back off from exponential search and use binary search
    --   until the bound has been determined.
    --
    --   For many use cases, this is a reasonable default.
  | BinarySearch
    -- ^ Use binary search to found each bound, using @0@ as the leftmost
    --   bounds of the search and 'BV.maxUnsigned' as the rightmost bounds of
    --   the search.

  -- Some possibilities for additional search strategies include:
  --
  -- - Using Z3's minimize/maximize commands. See
  --   https://github.com/GaloisInc/what4/issues/188
  --
  -- - A custom, user-specified strategy that uses callback(s) to guide the
  --   search at each iteration.

instance PP.Pretty SearchStrategy where
  pretty :: forall ann. SearchStrategy -> Doc ann
pretty SearchStrategy
ExponentialSearch = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"exponential search"
  pretty SearchStrategy
BinarySearch      = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"binary search"

-- | Use an 'WPO.OnlineSolver' to attempt to resolve a 'WI.SymBV' as concrete.
-- If it cannot, return the lower and upper bounds. This is primarly intended
-- for compound expressions whose bounds cannot trivially be determined by
-- using 'WI.signedBVBounds' or 'WI.unsignedBVBounds'.
resolveSymBV ::
     forall w sym solver scope st fs
   . ( 1 PN.<= w
     , sym ~ WEB.ExprBuilder scope st fs
     , WPO.OnlineSolver solver
     )
  => sym
  -> SearchStrategy
     -- ^ The strategy to use when searching for lower and upper bounds. For
     --   many use cases, 'ExponentialSearch' is a reasonable default.
  -> PN.NatRepr w
     -- ^ The bitvector width
  -> WPO.SolverProcess scope solver
     -- ^ The online solver process to use to search for lower and upper
     --   bounds.
  -> WI.SymBV sym w
     -- ^ The bitvector to resolve.
  -> 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 =
  -- First check, if the SymBV can be trivially resolved as concrete. If so,
  -- this can avoid the need to call out to the solver at all.
  case Expr scope (BaseBVType w) -> Maybe (BV w)
forall (w :: Nat). Expr scope (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
WI.asBV SymBV sym w
Expr scope (BaseBVType w)
symBV of
    Just BV w
bv -> ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
-> ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a b. (a -> b) -> a -> b
$ BV w -> ResolvedSymBV w
forall (w :: Nat). BV w -> ResolvedSymBV w
BVConcrete BV w
bv
    -- Otherwise, we need to consult the solver.
    Maybe (BV w)
Nothing -> do
      -- First, ask for a particular model of the SymBV...
      BV w
modelForBV <- SolverProcess scope solver -> IO (BV w) -> IO (BV w)
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 (IO (BV w) -> IO (BV w)) -> IO (BV w) -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ do
        SatResult (GroundEvalFn scope) ()
msat <- SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
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   -> IO (GroundEvalFn scope)
forall a. IO a
failUnknown
          WSat.Unsat{}   -> String -> IO (GroundEvalFn scope)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"resolveSymBV: Initial assumptions are unsatisfiable"
          WSat.Sat GroundEvalFn scope
model -> GroundEvalFn scope -> IO (GroundEvalFn scope)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GroundEvalFn scope
model
        GroundEvalFn scope
-> forall (tp :: BaseType). Expr scope tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WEG.groundEval GroundEvalFn scope
model SymBV sym w
Expr scope (BaseBVType w)
symBV
      -- ...next, check if this is the only possible model for this SymBV. We
      -- do this by adding a blocking clause that assumes the SymBV is /not/
      -- equal to the model we found in the previous step. If this is
      -- unsatisfiable, the SymBV can only be equal to that model, so we can
      -- conclude it is concrete. If it is satisfiable, on the other hand, the
      -- SymBV can be multiple values, so it is truly symbolic.
      Bool
isSymbolic <- SolverProcess scope solver -> IO Bool -> IO Bool
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 (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
        BoolExpr scope
block <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym (BoolExpr scope -> IO (BoolExpr scope))
-> IO (BoolExpr scope) -> IO (BoolExpr scope)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
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 (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
-> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
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
        WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
block
        SatResult () ()
msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
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 -> IO Bool
forall a. IO a
failUnknown
          WSat.Sat{}   -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True  -- Truly symbolic
          WSat.Unsat{} -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False -- Concrete
      if Bool
isSymbolic
        then
          -- If we have a truly symbolic SymBV, search for its lower and upper
          -- bounds, using the model from the previous step as a starting point
          -- for the search.
          case SearchStrategy
searchStrat of
            SearchStrategy
ExponentialSearch -> do
              -- Use the model from the previous step as the initial guess for
              -- each bound
              BV w
lowerBound <- BV w -> IO (BV w)
computeLowerBoundExponential BV w
modelForBV
              BV w
upperBound <- BV w -> IO (BV w)
computeUpperBoundExponential BV w
modelForBV
              ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
-> ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a b. (a -> b) -> a -> b
$ Domain w -> ResolvedSymBV w
forall (w :: Nat). Domain w -> ResolvedSymBV w
BVSymbolic (Domain w -> ResolvedSymBV w) -> Domain w -> ResolvedSymBV w
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
WUBA.range NatRepr w
w
                (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
lowerBound) (BV w -> Integer
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
              ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
-> ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a b. (a -> b) -> a -> b
$ Domain w -> ResolvedSymBV w
forall (w :: Nat). Domain w -> ResolvedSymBV w
BVSymbolic (Domain w -> ResolvedSymBV w) -> Domain w -> ResolvedSymBV w
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
WUBA.range NatRepr w
w
                (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
lowerBound) (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
upperBound)
        else ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ResolvedSymBV w -> IO (ResolvedSymBV w))
-> ResolvedSymBV w -> IO (ResolvedSymBV w)
forall a b. (a -> b) -> a -> b
$ BV w -> ResolvedSymBV w
forall (w :: Nat). BV w -> ResolvedSymBV w
BVConcrete BV w
modelForBV
  where
    conn :: WPS.WriterConn scope solver
    conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
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 = String -> IO a
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"resolveSymBV: Resolving value yielded UNKNOWN"

    bvZero :: BV w
    bvZero :: BV w
bvZero = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w

    bvOne :: BV w
    bvOne :: BV w
bvOne = NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr w
w

    bvTwo :: BV w
    bvTwo :: BV w
bvTwo = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
2

    bvMaxUnsigned :: BV w
    bvMaxUnsigned :: BV w
bvMaxUnsigned = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w

    -- The general strategy for finding a bound is that we start searching
    -- from a particular value known to be within bounds. At each step, we
    -- change this value by exponentially increasing amount, then check if we
    -- have exceeded the bound by using the solver. If so, we then fall back to
    -- binary search to determine an exact bound. If we are within bounds, we
    -- repeat the process.
    --
    -- As an example, let's suppose we having a symbolic value with bounds of
    -- [0, 12], and we start searching for the upper bound at the value 1:
    --
    -- * In the first step, we add 1 to the starting value to get 2. We check
    --   if two has exceeded the upper bound using the solver. This is not the
    --   case, so we continue.
    -- * In the second step, we add 2 to the starting value. The result, 3,
    --   is within bounds.
    -- * We continue like this in the third and fourth steps, except that
    --   we add 4 and 8 to the starting value to get 5 and 9, respectively.
    -- * In the fifth step, we add 16 to the starting value. The result, 17,
    --   has exceeded the upper bound. We will now fall back to binary search,
    --   using the previous result (9) as the leftmost bounds of the search and
    --   the current result (17) as the rightmost bounds of the search.
    -- * Eventually, binary search discovers that 12 is the upper bound.
    --
    -- Note that at each step, we must also check to make sure that the amount
    -- to increase the starting value by does not cause a numeric overflow. If
    -- this would be the case, we fall back to binary search, using
    -- BV.maxUnsigned as the rightmost bounds of the search.
    --
    -- The process for finding a lower bound is quite similar, except that we
    -- /subtract/ an exponentially increasing amount from the starting value
    -- each time rather than adding it.

    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
          | -- If the diff is larger than the starting value, then subtracting
            -- the diff from the starting value would cause underflow. Instead,
            -- just fall back to binary search, using 0 as the leftmost bounds
            -- of the search.
            BV w
start BV w -> BV w -> Bool
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

          | -- Otherwise, check if (start - diff) exceeds the lower bound for
            -- the symBV.
            Bool
otherwise
          = do let nextToTry :: BV w
nextToTry = NatRepr w -> BV w -> BV w -> BV w
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 |  -- If we have exceeded the lower bound, fall back to
                     -- binary search.
                     Bool
exceedsLB
                  -> BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
nextToTry BV w
previouslyTried
                  |  -- Make sure that (diff * 2) doesn't overflow. If it
                     -- would, fall back to binary search.
                     BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV w -> Integer
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
                  |  -- Otherwise, keep exponentially searching.
                     Bool
otherwise
                  -> BV w -> BV w -> IO (BV w)
go BV w
nextToTry (BV w -> IO (BV w)) -> BV w -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
diff BV w
bvTwo

    -- Search for the upper bound of the SymBV. This function assumes the
    -- following invariants:
    --
    -- * l <= r
    --
    -- * The lower bound of the SymBV is somewhere within the range [l, r].
    computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
    computeLowerBoundBinary :: BV w -> BV w -> IO (BV w)
computeLowerBoundBinary BV w
l BV w
r
      | -- If the leftmost and rightmost bounds are the same, we are done.
        BV w
l BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
r
      = BV w -> IO (BV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BV w
l

      | -- If the leftmost and rightmost bounds of the search are 1 apart, we
        -- only have two possible choices for the lower bound. Consult the
        -- solver to determine which one is the lower bound.
        NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w BV w
r BV w
l BV w -> BV w -> Bool
forall a. Ord a => a -> a -> Bool
< BV w
bvTwo
      = do Bool
lExceedsLB <- BV w -> IO Bool
checkExceedsLowerBound BV w
l
           BV w -> IO (BV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> IO (BV w)) -> BV w -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ if Bool
lExceedsLB then BV w
r else BV w
l

      | -- Otherwise, keep binary searching.
        Bool
otherwise
      = do let nextToTry :: BV w
nextToTry = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w ((BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
r) Integer -> Integer -> Integer
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 = SolverProcess scope solver -> IO Bool -> IO Bool
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 (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
      BoolExpr scope
leLowerBound <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
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 (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
-> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
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
      WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
leLowerBound
      SatResult () ()
msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
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 -> IO Bool
forall a. IO a
failUnknown
        WSat.Sat{}   -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
        WSat.Unsat{} -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True -- symBV cannot be <= this value,
                                  -- so the value must be strictly
                                  -- less than the lower bound.

    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
          | -- Make sure that adding the diff to the starting value will not
            -- result in overflow. If it would, just fall back to binary
            -- search, using BV.maxUnsigned as the rightmost bounds of the
            -- search.
            BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
start Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV w -> Integer
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 = NatRepr w -> BV w -> BV w -> BV w
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 |  -- If we have exceeded the upper bound, fall back to
                     -- binary search.
                     Bool
exceedsUB
                  -> BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
previouslyTried BV w
nextToTry
                  |  -- Make sure that (diff * 2) doesn't overflow. If it
                     -- would, fall back to binary search.
                     BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
diff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV w -> Integer
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
                  |  -- Otherwise, keep exponentially searching.
                     Bool
otherwise
                  -> BV w -> BV w -> IO (BV w)
go BV w
nextToTry (BV w -> IO (BV w)) -> BV w -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
w BV w
diff BV w
bvTwo

    -- Search for the upper bound of the SymBV. This function assumes the
    -- following invariants:
    --
    -- * l <= r
    --
    -- * The upper bound of the SymBV is somewhere within the range [l, r].
    computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
    computeUpperBoundBinary :: BV w -> BV w -> IO (BV w)
computeUpperBoundBinary BV w
l BV w
r
      | -- If the leftmost and rightmost bounds are the same, we are done.
        BV w
l BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
r
      = BV w -> IO (BV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BV w
l

      | -- If the leftmost and rightmost bounds of the search are 1 apart, we
        -- only have two possible choices for the upper bound. Consult the
        -- solver to determine which one is the upper bound.
        NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.sub NatRepr w
w BV w
r BV w
l BV w -> BV w -> Bool
forall a. Ord a => a -> a -> Bool
< BV w
bvTwo
      = do Bool
rExceedsUB <- BV w -> IO Bool
checkExceedsUpperBound BV w
r
           BV w -> IO (BV w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV w -> IO (BV w)) -> BV w -> IO (BV w)
forall a b. (a -> b) -> a -> b
$ if Bool
rExceedsUB then BV w
l else BV w
r

      | -- Otherwise, keep binary searching.
        Bool
otherwise
      = do let nextToTry :: BV w
nextToTry = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w ((BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
r) Integer -> Integer -> Integer
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 = SolverProcess scope solver -> IO Bool -> IO Bool
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 (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
      BoolExpr scope
geUpperBound <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
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 (Expr scope (BaseBVType w) -> IO (BoolExpr scope))
-> IO (Expr scope (BaseBVType w)) -> IO (BoolExpr scope)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
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
      WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume WriterConn scope solver
conn BoolExpr scope
geUpperBound
      SatResult () ()
msat <- SolverProcess scope solver -> String -> IO (SatResult () ())
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 -> IO Bool
forall a. IO a
failUnknown
        WSat.Sat{}   -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
        WSat.Unsat{} -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True -- symBV cannot be >= this upper bound,
                                  -- so the value must be strictly
                                  -- greater than the upper bound.