-- TODO(#1406): Move the definitions of the deprecated imports into this module,
-- and remove the exports from MemModel.
{-# OPTIONS_GHC -Wno-warnings-deprecations #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Manipulating C-style null-terminated strings
module Lang.Crucible.LLVM.MemModel.Strings
  ( Mem.loadString
  , Mem.loadMaybeString
  , Mem.strLen
  , loadConcretelyNullTerminatedString
  , loadSymbolicString
  , storeString
  -- * Low-level string loading primitives
  -- ** 'ByteChecker'
  , ControlFlow(..)
  , ByteChecker(..)
  , fullyConcreteNullTerminatedString
  , concretelyNullTerminatedString
  , nullTerminatedString
  , withMaxChars
  -- ** 'ByteLoader'
  , ByteLoader(..)
  , llvmByteLoader
  -- ** 'loadBytes'
  , loadBytes
  ) where

import           Data.Bifunctor (Bifunctor(bimap, first))
import           Control.Monad.IO.Class (MonadIO, liftIO)
import qualified Data.BitVector.Sized as BV
import           Data.Functor ((<&>))
import qualified Data.Parameterized.NatRepr as DPN
import           Data.Word (Word8)
import qualified Data.Vector as Vec
import qualified GHC.Stack as GHC
import qualified Lang.Crucible.Backend as LCB
import qualified Lang.Crucible.Backend.Online as LCBO
import qualified Lang.Crucible.Simulator as LCS
import qualified Lang.Crucible.LLVM.DataLayout as CLD
import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.LLVM.MemModel as Mem
import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial
import qualified What4.Expr.Builder as WEB
import qualified What4.Interface as WI
import qualified What4.Protocol.Online as WPO
import qualified What4.SatResult as WS

-- | Load a null-terminated string (with a concrete null terminator) from memory.
--
-- The string must contain a concrete null terminator. If a maximum number of
-- characters is provided, no more than that number of characters will be read.
-- In either case, 'loadConcretelyNullTerminatedString' will stop reading if it
-- encounters a (concretely) null terminator.
--
-- Note that the loaded string may actually be smaller than the returned list if
-- any of the symbolic bytes are equal to 0.
loadConcretelyNullTerminatedString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  IO [WI.SymBV sym 8]
loadConcretelyNullTerminatedString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [SymBV sym 8]
loadConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
limit =
  let loader :: ByteLoader IO sym bak wptr
loader = MemImpl sym -> ByteLoader IO sym bak wptr
forall sym bak (wptr :: Natural) (m :: Type -> Type).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
MemImpl sym -> ByteLoader m sym bak wptr
llvmByteLoader MemImpl sym
mem in
  case Maybe Int
limit of
    Maybe Int
Nothing -> bak
-> MemImpl sym
-> ([SymBV sym 8] -> [SymBV sym 8])
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker
     IO sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
-> IO [SymBV sym 8]
forall (m :: Type -> Type) a b sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
bak
-> MemImpl sym
-> a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
loadBytes bak
bak MemImpl sym
mem [SymBV sym 8] -> [SymBV sym 8]
forall a. a -> a
id LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker
  IO sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
concretelyNullTerminatedString
    Just Int
l ->
      let byteChecker :: ByteChecker
  IO sym bak ([SymBV sym 8] -> [SymBV sym 8], Int) [SymBV sym 8]
byteChecker = Int
-> (([SymBV sym 8] -> [SymBV sym 8]) -> IO [SymBV sym 8])
-> ByteChecker
     IO sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
-> ByteChecker
     IO sym bak ([SymBV sym 8] -> [SymBV sym 8], Int) [SymBV sym 8]
forall sym bak (m :: Type -> Type) a b.
(HasCallStack, IsSymBackend sym bak, Functor m) =>
Int
-> (a -> m b)
-> ByteChecker m sym bak a b
-> ByteChecker m sym bak (a, Int) b
withMaxChars Int
l (\[SymBV sym 8] -> [SymBV sym 8]
f -> [SymBV sym 8] -> IO [SymBV sym 8]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([SymBV sym 8] -> [SymBV sym 8]
f [])) ByteChecker
  IO sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
concretelyNullTerminatedString in
      bak
-> MemImpl sym
-> ([SymBV sym 8] -> [SymBV sym 8], Int)
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker
     IO sym bak ([SymBV sym 8] -> [SymBV sym 8], Int) [SymBV sym 8]
-> IO [SymBV sym 8]
forall (m :: Type -> Type) a b sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
bak
-> MemImpl sym
-> a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
loadBytes bak
bak MemImpl sym
mem ([SymBV sym 8] -> [SymBV sym 8]
forall a. a -> a
id, Int
0) LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker
  IO sym bak ([SymBV sym 8] -> [SymBV sym 8], Int) [SymBV sym 8]
byteChecker

-- | Load a null-terminated string from memory.
--
-- Consults an SMT solver to check if any of the loaded bytes are known to be
-- null (0). If a maximum number of characters is provided, no more than that
-- number of charcters will be read. In either case, 'loadSymbolicString' will
-- stop reading if it encounters a null terminator.
--
-- Note that the loaded string may actually be smaller than the returned list if
-- any of the symbolic bytes are equal to 0.
loadSymbolicString ::
  ( LCB.IsSymBackend sym bak
  , sym ~ WEB.ExprBuilder scope st fs
  , bak ~ LCBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  IO [WI.SymBV sym 8]
loadSymbolicString :: forall sym bak scope (st :: Type -> Type) fs solver
       (wptr :: Natural).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver,
 HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts::MemOptions,
 HasCallStack) =>
bak
-> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [SymBV sym 8]
loadSymbolicString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
limit =
  let loader :: ByteLoader IO sym bak wptr
loader = MemImpl sym -> ByteLoader IO sym bak wptr
forall sym bak (wptr :: Natural) (m :: Type -> Type).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
MemImpl sym -> ByteLoader m sym bak wptr
llvmByteLoader MemImpl sym
mem in
  case Maybe Int
limit of
    Maybe Int
Nothing -> bak
-> MemImpl sym
-> ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker
     IO
     sym
     bak
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
     [Expr scope (BaseBVType 8)]
-> IO [Expr scope (BaseBVType 8)]
forall (m :: Type -> Type) a b sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
bak
-> MemImpl sym
-> a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
loadBytes bak
bak MemImpl sym
mem [Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)]
forall a. a -> a
id LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker
  IO
  sym
  bak
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
  [Expr scope (BaseBVType 8)]
ByteChecker
  IO sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall (m :: Type -> Type) sym bak scope (st :: Type -> Type) fs
       solver.
(MonadIO m, HasCallStack, IsSymBackend sym bak,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
nullTerminatedString
    Just Int
l ->
      let byteChecker :: ByteChecker
  IO
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)], Int)
  [Expr scope (BaseBVType 8)]
byteChecker = Int
-> (([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
    -> IO [Expr scope (BaseBVType 8)])
-> ByteChecker
     IO
     (ExprBuilder scope st fs)
     (OnlineBackend solver scope st fs)
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
     [Expr scope (BaseBVType 8)]
-> ByteChecker
     IO
     (ExprBuilder scope st fs)
     (OnlineBackend solver scope st fs)
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)], Int)
     [Expr scope (BaseBVType 8)]
forall sym bak (m :: Type -> Type) a b.
(HasCallStack, IsSymBackend sym bak, Functor m) =>
Int
-> (a -> m b)
-> ByteChecker m sym bak a b
-> ByteChecker m sym bak (a, Int) b
withMaxChars Int
l (\[Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)]
f -> [Expr scope (BaseBVType 8)] -> IO [Expr scope (BaseBVType 8)]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)]
f [])) ByteChecker
  IO
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
  [Expr scope (BaseBVType 8)]
ByteChecker
  IO
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  ([SymBV (ExprBuilder scope st fs) 8]
   -> [SymBV (ExprBuilder scope st fs) 8])
  [SymBV (ExprBuilder scope st fs) 8]
forall (m :: Type -> Type) sym bak scope (st :: Type -> Type) fs
       solver.
(MonadIO m, HasCallStack, IsSymBackend sym bak,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
nullTerminatedString in
      bak
-> MemImpl sym
-> ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)],
    Int)
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker
     IO
     sym
     bak
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)], Int)
     [Expr scope (BaseBVType 8)]
-> IO [Expr scope (BaseBVType 8)]
forall (m :: Type -> Type) a b sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
bak
-> MemImpl sym
-> a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
loadBytes bak
bak MemImpl sym
mem ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)]
forall a. a -> a
id, Int
0) LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker
  IO
  sym
  bak
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)], Int)
  [Expr scope (BaseBVType 8)]
ByteChecker
  IO
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)], Int)
  [Expr scope (BaseBVType 8)]
byteChecker

-- | Store a string to memory, adding a null terminator at the end.
storeString ::
  forall sym bak w.
  ( LCB.IsSymBackend sym bak
  , WI.IsExpr (WI.SymExpr sym)
  , LCLM.HasPtrWidth w
  , LCLM.HasLLVMAnn sym
  , ?memOpts :: LCLM.MemOptions
  ) =>
  bak ->
  LCLM.MemImpl sym ->
  -- | Pointer to write string to
  LCLM.LLVMPtr sym w ->
  -- | The bytes of the string to write (null terminator not included)
  Vec.Vector (WI.SymBV sym 8) ->
  IO (LCLM.MemImpl sym)
storeString :: forall sym bak (w :: Natural).
(IsSymBackend sym bak, IsExpr (SymExpr sym), HasPtrWidth w,
 HasLLVMAnn sym, ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Vector (SymBV sym 8)
-> IO (MemImpl sym)
storeString bak
bak MemImpl sym
mem LLVMPtr sym w
ptr Vector (SymBV sym 8)
bytesBvs = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymNat sym
zeroNat <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
WI.natLit sym
sym Natural
0
  let bytes :: Vector (LLVMVal sym)
bytes = (SymBV sym 8 -> LLVMVal sym)
-> Vector (SymBV sym 8) -> Vector (LLVMVal sym)
forall a b. (a -> b) -> Vector a -> Vector b
Vec.map (SymNat sym -> SymBV sym 8 -> LLVMVal sym
forall (w :: Natural) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
Mem.LLVMValInt SymNat sym
zeroNat) Vector (SymBV sym 8)
bytesBvs
  LLVMVal sym
zeroByte <- SymNat sym -> SymBV sym 8 -> LLVMVal sym
forall (w :: Natural) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
Mem.LLVMValInt SymNat sym
zeroNat (SymBV sym 8 -> LLVMVal sym)
-> IO (SymBV sym 8) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 8 -> IO (SymBV sym 8)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @8)
  let nullTerminatedBytes :: Vector (LLVMVal sym)
nullTerminatedBytes = Vector (LLVMVal sym) -> LLVMVal sym -> Vector (LLVMVal sym)
forall a. Vector a -> a -> Vector a
Vec.snoc Vector (LLVMVal sym)
bytes LLVMVal sym
zeroByte
  let val :: LLVMVal sym
val = StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
Mem.LLVMValArray (Bytes -> StorageType
Mem.bitvectorType Bytes
1) Vector (LLVMVal sym)
nullTerminatedBytes
  let storTy :: StorageType
storTy = forall sym. IsExpr (SymExpr sym) => LLVMVal sym -> StorageType
Mem.llvmValStorableType @sym LLVMVal sym
val
  bak
-> MemImpl sym
-> LLVMPtr sym w
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
Mem.storeRaw bak
bak MemImpl sym
mem LLVMPtr sym w
ptr StorageType
storTy Alignment
CLD.noAlignment LLVMVal sym
val

---------------------------------------------------------------------
-- * Low-level string loading primitives

---------------------------------------------------------------------
-- ** 'ByteChecker'

-- | Whether to stop or keep going
--
-- Like Rust's @std::ops::ControlFlow@.
data ControlFlow a b
  = Continue a
  | Break b
  deriving (forall a b. (a -> b) -> ControlFlow a a -> ControlFlow a b)
-> (forall a b. a -> ControlFlow a b -> ControlFlow a a)
-> Functor (ControlFlow a)
forall a b. a -> ControlFlow a b -> ControlFlow a a
forall a b. (a -> b) -> ControlFlow a a -> ControlFlow a b
forall a a b. a -> ControlFlow a b -> ControlFlow a a
forall a a b. (a -> b) -> ControlFlow a a -> ControlFlow a b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> ControlFlow a a -> ControlFlow a b
fmap :: forall a b. (a -> b) -> ControlFlow a a -> ControlFlow a b
$c<$ :: forall a a b. a -> ControlFlow a b -> ControlFlow a a
<$ :: forall a b. a -> ControlFlow a b -> ControlFlow a a
Functor

-- NB: 'first' is used in this module
instance Bifunctor ControlFlow where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> ControlFlow a c -> ControlFlow b d
bimap a -> b
l c -> d
r =
    \case
      Continue a
x -> b -> ControlFlow b d
forall a b. a -> ControlFlow a b
Continue (a -> b
l a
x)
      Break c
x -> d -> ControlFlow b d
forall a b. b -> ControlFlow a b
Break (c -> d
r c
x)

-- | Compute a result from a symbolic byte, and check if the load should
-- continue to the next byte.
--
-- Used to:
--
-- * Check if the byte is concrete ('fullyConcreteNullTerminatedString')
-- * Check if the byte is concretely a null terminator
--   ('concretelyNullTerminatedString')
-- * Check if a byte is known by a solver to be a null terminator ('nullTerminatedString')
-- * Check if we have surpassed a length limit ('withMaxChars')
--
-- Note that it is relatively common for @a@ to be a function @[b] -> [b]@. This
-- is used to build up a snoc-list.
newtype ByteChecker m sym bak a b
  = ByteChecker { forall (m :: Type -> Type) sym bak a b.
ByteChecker m sym bak a b
-> bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b)
runByteChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }

-- Helper, not exported
ptrToBv8 ::
  LCB.IsSymBackend sym bak =>
  bak ->
  Mem.LLVMPtr sym 8 ->
  IO (WI.SymBV sym 8)
ptrToBv8 :: forall sym bak.
IsSymBackend sym bak =>
bak -> LLVMPtr sym 8 -> IO (SymBV sym 8)
ptrToBv8 bak
bak LLVMPtr sym 8
bytePtr = do
  let err :: SimErrorReason
err = String -> String -> SimErrorReason
LCS.AssertFailureSimError String
"Found pointer instead of byte when loading string" String
""
  bak -> SimErrorReason -> LLVMPtr sym 8 -> IO (SymBV sym 8)
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> SimErrorReason -> LLVMPtr sym w -> IO (SymBV sym w)
Partial.ptrToBv bak
bak SimErrorReason
err LLVMPtr sym 8
bytePtr

-- | 'ByteChecker' for loading concrete strings.
--
-- Currently unused internally, but analogous with
-- 'Lang.Crucible.LLVM.MemModel.loadString'. In fact, it would be good to define
-- that function in terms of this one. However, this is blocked on TODO(#1406).
fullyConcreteNullTerminatedString ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]
fullyConcreteNullTerminatedString :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]
fullyConcreteNullTerminatedString =
  (bak
 -> ([Word8] -> [Word8])
 -> LLVMPtr sym 8
 -> m (ControlFlow ([Word8] -> [Word8]) [Word8]))
-> ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> ByteChecker m sym bak a b
ByteChecker ((bak
  -> ([Word8] -> [Word8])
  -> LLVMPtr sym 8
  -> m (ControlFlow ([Word8] -> [Word8]) [Word8]))
 -> ByteChecker m sym bak ([Word8] -> [Word8]) [Word8])
-> (bak
    -> ([Word8] -> [Word8])
    -> LLVMPtr sym 8
    -> m (ControlFlow ([Word8] -> [Word8]) [Word8]))
-> ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]
forall a b. (a -> b) -> a -> b
$ \bak
bak [Word8] -> [Word8]
acc LLVMPtr sym 8
bytePtr -> do
    SymExpr sym (BaseBVType 8)
byte <- IO (SymExpr sym (BaseBVType 8)) -> m (SymExpr sym (BaseBVType 8))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak -> LLVMPtr sym 8 -> IO (SymExpr sym (BaseBVType 8))
forall sym bak.
IsSymBackend sym bak =>
bak -> LLVMPtr sym 8 -> IO (SymBV sym 8)
ptrToBv8 bak
bak LLVMPtr sym 8
bytePtr)
    case BV 8 -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV 8 -> Integer) -> Maybe (BV 8) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymExpr sym (BaseBVType 8) -> Maybe (BV 8)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
WI.asBV SymExpr sym (BaseBVType 8)
byte of
      Just Integer
0 -> ControlFlow ([Word8] -> [Word8]) [Word8]
-> m (ControlFlow ([Word8] -> [Word8]) [Word8])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Word8] -> ControlFlow ([Word8] -> [Word8]) [Word8]
forall a b. b -> ControlFlow a b
Break ([Word8] -> [Word8]
acc []))
      Just Integer
c -> do
        let c' :: Word8
c' = forall a. Enum a => Int -> a
toEnum @Word8 (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
c)
        ControlFlow ([Word8] -> [Word8]) [Word8]
-> m (ControlFlow ([Word8] -> [Word8]) [Word8])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (([Word8] -> [Word8]) -> ControlFlow ([Word8] -> [Word8]) [Word8]
forall a b. a -> ControlFlow a b
Continue (\[Word8]
l -> [Word8] -> [Word8]
acc (Word8
c' Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: [Word8]
l)))
      Maybe Integer
Nothing -> do
        let msg :: String
msg = String
"Symbolic value encountered when loading a string"
        IO (ControlFlow ([Word8] -> [Word8]) [Word8])
-> m (ControlFlow ([Word8] -> [Word8]) [Word8])
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> SimErrorReason -> IO (ControlFlow ([Word8] -> [Word8]) [Word8])
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
LCB.addFailedAssertion bak
bak (CallStack -> String -> SimErrorReason
LCS.Unsupported CallStack
HasCallStack => CallStack
GHC.callStack String
msg))

-- | 'ByteChecker' for loading symbolic strings with a concrete null terminator.
--
-- Used in 'loadConcretelyNullTerminatedString'.
concretelyNullTerminatedString ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]
concretelyNullTerminatedString :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
concretelyNullTerminatedString =
  (bak
 -> ([SymBV sym 8] -> [SymBV sym 8])
 -> LLVMPtr sym 8
 -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
-> ByteChecker
     m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> ByteChecker m sym bak a b
ByteChecker ((bak
  -> ([SymBV sym 8] -> [SymBV sym 8])
  -> LLVMPtr sym 8
  -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
 -> ByteChecker
      m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
-> (bak
    -> ([SymBV sym 8] -> [SymBV sym 8])
    -> LLVMPtr sym 8
    -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
-> ByteChecker
     m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall a b. (a -> b) -> a -> b
$ \bak
bak [SymBV sym 8] -> [SymBV sym 8]
acc LLVMPtr sym 8
bytePtr -> do
    SymBV sym 8
byte <- IO (SymBV sym 8) -> m (SymBV sym 8)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak -> LLVMPtr sym 8 -> IO (SymBV sym 8)
forall sym bak.
IsSymBackend sym bak =>
bak -> LLVMPtr sym 8 -> IO (SymBV sym 8)
ptrToBv8 bak
bak LLVMPtr sym 8
bytePtr)
    if SymBV sym 8 -> Bool
forall {e :: BaseType -> Type} {w :: Natural}.
IsExpr e =>
e (BaseBVType w) -> Bool
isConcreteNullTerminator SymBV sym 8
byte
    then ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
-> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([SymBV sym 8]
-> ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall a b. b -> ControlFlow a b
Break ([SymBV sym 8] -> [SymBV sym 8]
acc []))
    else  ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
-> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (([SymBV sym 8] -> [SymBV sym 8])
-> ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall a b. a -> ControlFlow a b
Continue (\[SymBV sym 8]
l -> [SymBV sym 8] -> [SymBV sym 8]
acc (SymBV sym 8
byte SymBV sym 8 -> [SymBV sym 8] -> [SymBV sym 8]
forall a. a -> [a] -> [a]
: [SymBV sym 8]
l)))
  where
    isConcreteNullTerminator :: e (BaseBVType w) -> Bool
isConcreteNullTerminator e (BaseBVType w)
symByte =
      case BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e (BaseBVType w) -> Maybe (BV w)
forall (w :: Natural). e (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
WI.asBV e (BaseBVType w)
symByte of
        Just Integer
0 -> Bool
True
        Maybe Integer
_ -> Bool
False

-- | 'ByteChecker' for loading symbolic strings with a null terminator.
--
-- Used in 'loadSymbolicString'.
nullTerminatedString ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  sym ~ WEB.ExprBuilder scope st fs =>
  bak ~ LCBO.OnlineBackend solver scope st fs =>
  WPO.OnlineSolver solver =>
  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]
nullTerminatedString :: forall (m :: Type -> Type) sym bak scope (st :: Type -> Type) fs
       solver.
(MonadIO m, HasCallStack, IsSymBackend sym bak,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker
  m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
nullTerminatedString =
  (bak
 -> ([SymBV sym 8] -> [SymBV sym 8])
 -> LLVMPtr sym 8
 -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
-> ByteChecker
     m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> ByteChecker m sym bak a b
ByteChecker ((bak
  -> ([SymBV sym 8] -> [SymBV sym 8])
  -> LLVMPtr sym 8
  -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
 -> ByteChecker
      m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
-> (bak
    -> ([SymBV sym 8] -> [SymBV sym 8])
    -> LLVMPtr sym 8
    -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
-> ByteChecker
     m sym bak ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]
forall a b. (a -> b) -> a -> b
$ \bak
bak [SymBV sym 8] -> [SymBV sym 8]
acc LLVMPtr sym 8
bytePtr -> do
    Expr scope (BaseBVType 8)
byte <- IO (Expr scope (BaseBVType 8)) -> m (Expr scope (BaseBVType 8))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> LLVMPtr (ExprBuilder scope st fs) 8
-> IO (SymBV (ExprBuilder scope st fs) 8)
forall sym bak.
IsSymBackend sym bak =>
bak -> LLVMPtr sym 8 -> IO (SymBV sym 8)
ptrToBv8 bak
bak LLVMPtr sym 8
LLVMPtr (ExprBuilder scope st fs) 8
bytePtr)
    let sym :: ExprBuilder scope st fs
sym = bak -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
    Bool
isNullTerm <- IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (OnlineBackend solver scope st fs
-> ExprBuilder scope st fs -> Expr scope (BaseBVType 8) -> IO Bool
forall {sym} {scope} {solver} {st :: Type -> Type} {fs}.
(SymExpr sym ~ Expr scope, OnlineSolver solver,
 IsExprBuilder sym) =>
OnlineBackend solver scope st fs
-> sym -> Expr scope (BaseBVType 8) -> IO Bool
isNullTerminator bak
OnlineBackend solver scope st fs
bak ExprBuilder scope st fs
sym Expr scope (BaseBVType 8)
byte)
    if Bool
isNullTerm
    then ControlFlow
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
  [Expr scope (BaseBVType 8)]
-> m (ControlFlow
        ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
        [Expr scope (BaseBVType 8)])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Expr scope (BaseBVType 8)]
-> ControlFlow
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
     [Expr scope (BaseBVType 8)]
forall a b. b -> ControlFlow a b
Break ([SymBV sym 8] -> [SymBV sym 8]
acc []))
    else  ControlFlow
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
  [Expr scope (BaseBVType 8)]
-> m (ControlFlow
        ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
        [Expr scope (BaseBVType 8)])
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
-> ControlFlow
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
     [Expr scope (BaseBVType 8)]
forall a b. a -> ControlFlow a b
Continue (\[Expr scope (BaseBVType 8)]
l -> [SymBV sym 8] -> [SymBV sym 8]
acc (Expr scope (BaseBVType 8)
byte Expr scope (BaseBVType 8)
-> [Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)]
forall a. a -> [a] -> [a]
: [Expr scope (BaseBVType 8)]
l)))
  where
    isNullTerminator :: OnlineBackend solver scope st fs
-> sym -> Expr scope (BaseBVType 8) -> IO Bool
isNullTerminator OnlineBackend solver scope st fs
bak sym
sym Expr scope (BaseBVType 8)
symByte =
      case BV 8 -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV 8 -> Integer) -> Maybe (BV 8) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr scope (BaseBVType 8) -> Maybe (BV 8)
forall (w :: Natural). Expr scope (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
WI.asBV Expr scope (BaseBVType 8)
symByte of
        Just Integer
0 -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
        Just Integer
_ -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False
        Maybe Integer
_ ->
          OnlineBackend solver scope st fs
-> IO Bool -> (SolverProcess scope solver -> IO Bool) -> IO Bool
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
LCBO.withSolverProcess OnlineBackend solver scope st fs
bak (Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False) ((SolverProcess scope solver -> IO Bool) -> IO Bool)
-> (SolverProcess scope solver -> IO Bool) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \SolverProcess scope solver
proc -> do
            SymExpr sym (BaseBVType 8)
z <- sym -> NatRepr 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
WI.knownNat @8)
            BoolExpr scope
p <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym (SymExpr sym BaseBoolType -> IO (BoolExpr scope))
-> IO (SymExpr sym BaseBoolType) -> IO (BoolExpr scope)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym (BaseBVType 8)
-> SymExpr sym (BaseBVType 8)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymExpr sym (BaseBVType 8)
z Expr scope (BaseBVType 8)
SymExpr sym (BaseBVType 8)
symByte
            SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
WPO.checkSatisfiable SolverProcess scope solver
proc String
"nullTerminatedString" BoolExpr scope
p IO (SatResult () ()) -> (SatResult () () -> Bool) -> IO Bool
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&>
              \case
                WS.Unsat () -> Bool
True
                WS.Sat () -> Bool
False
                SatResult () ()
WS.Unknown -> Bool
False

-- | 'ByteChecker' for adding a maximum character length.
withMaxChars ::
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  Functor m =>
  -- | Maximum number of bytes to load
  Int ->
  -- | What to do when the maximum is reached
  (a -> m b) ->
  ByteChecker m sym bak a b ->
  ByteChecker m sym bak (a, Int) b
withMaxChars :: forall sym bak (m :: Type -> Type) a b.
(HasCallStack, IsSymBackend sym bak, Functor m) =>
Int
-> (a -> m b)
-> ByteChecker m sym bak a b
-> ByteChecker m sym bak (a, Int) b
withMaxChars Int
limit a -> m b
done ByteChecker m sym bak a b
checker =
  (bak -> (a, Int) -> LLVMPtr sym 8 -> m (ControlFlow (a, Int) b))
-> ByteChecker m sym bak (a, Int) b
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> ByteChecker m sym bak a b
ByteChecker ((bak -> (a, Int) -> LLVMPtr sym 8 -> m (ControlFlow (a, Int) b))
 -> ByteChecker m sym bak (a, Int) b)
-> (bak -> (a, Int) -> LLVMPtr sym 8 -> m (ControlFlow (a, Int) b))
-> ByteChecker m sym bak (a, Int) b
forall a b. (a -> b) -> a -> b
$ \bak
bak (a
acc, Int
i) LLVMPtr sym 8
bytePtr ->
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
limit
    then b -> ControlFlow (a, Int) b
forall a b. b -> ControlFlow a b
Break (b -> ControlFlow (a, Int) b) -> m b -> m (ControlFlow (a, Int) b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
done a
acc
    else (a -> (a, Int)) -> ControlFlow a b -> ControlFlow (a, Int) b
forall a b c. (a -> b) -> ControlFlow a c -> ControlFlow b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ControlFlow a b -> ControlFlow (a, Int) b)
-> m (ControlFlow a b) -> m (ControlFlow (a, Int) b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteChecker m sym bak a b
-> bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b)
forall (m :: Type -> Type) sym bak a b.
ByteChecker m sym bak a b
-> bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b)
runByteChecker ByteChecker m sym bak a b
checker bak
bak a
acc LLVMPtr sym 8
bytePtr

---------------------------------------------------------------------
-- ** 'ByteLoader'

-- | Load a byte from memory.
--
-- The only 'ByteLoader' defined here is 'llvmByteLoader', but Macaw users will
-- most often want one based on @doReadMemModel@.
newtype ByteLoader m sym bak wptr
  = ByteLoader { forall (m :: Type -> Type) sym bak (wptr :: Natural).
ByteLoader m sym bak wptr
-> bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8)
runByteLoader :: bak -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8) }

-- | A 'ByteLoader' for LLVM memory based on 'Mem.doLoad'.
llvmByteLoader ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , MonadIO m
  ) =>
  Mem.MemImpl sym ->
  ByteLoader m sym bak wptr
llvmByteLoader :: forall sym bak (wptr :: Natural) (m :: Type -> Type).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
MemImpl sym -> ByteLoader m sym bak wptr
llvmByteLoader MemImpl sym
mem =
  (bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8))
-> ByteLoader m sym bak wptr
forall (m :: Type -> Type) sym bak (wptr :: Natural).
(bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8))
-> ByteLoader m sym bak wptr
ByteLoader ((bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8))
 -> ByteLoader m sym bak wptr)
-> (bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8))
-> ByteLoader m sym bak wptr
forall a b. (a -> b) -> a -> b
$ \bak
bak LLVMPtr sym wptr
ptr -> do
    let i1 :: StorageType
i1 = Bytes -> StorageType
Mem.bitvectorType Bytes
1
    let p8 :: TypeRepr (LLVMPointerType 8)
p8 = NatRepr 8 -> TypeRepr (LLVMPointerType 8)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
Mem.LLVMPointerRepr (forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @8)
    IO (LLVMPointer sym 8) -> m (LLVMPointer sym 8)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr (LLVMPointerType 8)
-> Alignment
-> IO (LLVMPtr sym 8)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (RegValue sym tp)
Mem.doLoad bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr StorageType
i1 TypeRepr (LLVMPointerType 8)
p8 Alignment
CLD.noAlignment)

---------------------------------------------------------------------
-- * 'loadBytes'

-- | Load a sequence of bytes, one at a time.
--
-- Used to implement 'loadConcretelyNullTerminatedString' and
-- 'loadSymbolicString'. Highly customizable via 'ByteLoader' and 'ByteChecker'.
loadBytes ::
  forall m a b sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , MonadIO m
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Initial accumulator
  a ->
  -- | Pointer to load from
  Mem.LLVMPtr sym wptr ->
  -- | How to load a byte from memory
  ByteLoader m sym bak wptr ->
  -- | How to check if we should continue loading the next byte
  ByteChecker m sym bak a b ->
  m b
loadBytes :: forall (m :: Type -> Type) a b sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
bak
-> MemImpl sym
-> a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
loadBytes bak
bak MemImpl sym
mem = a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
go
 where
  sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  go ::
    a ->
    Mem.LLVMPtr sym wptr ->
    ByteLoader m sym bak wptr ->
    ByteChecker m sym bak a b ->
    m b
  go :: a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
go a
acc LLVMPtr sym wptr
ptr ByteLoader m sym bak wptr
loader ByteChecker m sym bak a b
checker = do
    LLVMPointer sym 8
byte <- ByteLoader m sym bak wptr
-> bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8)
forall (m :: Type -> Type) sym bak (wptr :: Natural).
ByteLoader m sym bak wptr
-> bak -> LLVMPtr sym wptr -> m (LLVMPtr sym 8)
runByteLoader ByteLoader m sym bak wptr
loader bak
bak LLVMPtr sym wptr
ptr
    ByteChecker m sym bak a b
-> bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b)
forall (m :: Type -> Type) sym bak a b.
ByteChecker m sym bak a b
-> bak -> a -> LLVMPtr sym 8 -> m (ControlFlow a b)
runByteChecker ByteChecker m sym bak a b
checker bak
bak a
acc LLVMPtr sym 8
LLVMPointer sym 8
byte m (ControlFlow a b) -> (ControlFlow a b -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      \case
        Break b
result -> b -> m b
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure b
result
        Continue a
acc' -> do
          -- It is important that safety assertions for later loads can use
          -- the assumption that earlier bytes were nonzero, see #1463 or
          -- `crucible-llvm-cli/test-data/T1463-read-bytes.cbl` for details.
          SymExpr sym BaseBoolType
prevByteWasNonNull <-
            IO (SymExpr sym BaseBoolType) -> m (SymExpr sym BaseBoolType)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 8 -> LLVMPtr sym 8 -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)
Mem.ptrIsNull sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
WI.knownNat @8) LLVMPtr sym 8
LLVMPointer sym 8
byte)
          ProgramLoc
loc <- IO ProgramLoc -> m ProgramLoc
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
WI.getCurrentProgramLoc sym
sym)
          let assump :: CrucibleAssumption (SymExpr sym)
assump = ProgramLoc
-> Maybe ProgramLoc
-> SymExpr sym BaseBoolType
-> CrucibleAssumption (SymExpr sym)
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
LCB.BranchCondition ProgramLoc
loc Maybe ProgramLoc
forall a. Maybe a
Nothing SymExpr sym BaseBoolType
prevByteWasNonNull
          IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak -> CrucibleAssumption (SymExpr sym) -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
LCB.addAssumption bak
bak CrucibleAssumption (SymExpr sym)
assump)

          LLVMPointer sym wptr
ptr' <- IO (LLVMPointer sym wptr) -> m (LLVMPointer sym wptr)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (LLVMPtr sym wptr)
Mem.doPtrAddOffset bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr (SymExpr sym (BaseBVType wptr) -> IO (LLVMPointer sym wptr))
-> IO (SymExpr sym (BaseBVType wptr)) -> IO (LLVMPointer sym wptr)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
Mem.PtrWidth)
          a
-> LLVMPtr sym wptr
-> ByteLoader m sym bak wptr
-> ByteChecker m sym bak a b
-> m b
go a
acc' LLVMPtr sym wptr
LLVMPointer sym wptr
ptr' ByteLoader m sym bak wptr
loader ByteChecker m sym bak a b
checker