-- 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 NegativeLiterals #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Manipulating C-style null-terminated strings
module Lang.Crucible.LLVM.MemModel.Strings
  ( storeString
  -- * Loading strings
  , Mem.loadString
  , Mem.loadMaybeString
  , loadConcretelyNullTerminatedString
  , loadProvablyNullTerminatedString
  -- * String length
  , Mem.strLen
  , strnlen
  , strlenConcreteString
  , strlenConcretelyNullTerminatedString
  , strlenProvablyNullTerminatedString
  -- * String copying
  , copyConcreteString
  , copyConcretelyNullTerminatedString
  , copyProvablyNullTerminatedString
  -- * String duplication
  , dupConcreteString
  , dupConcretelyNullTerminatedString
  , dupProvablyNullTerminatedString
  -- * Memory comparison
  , memcmp
  , memcmpConcreteLen
  -- * String comparison
  , strncmp
  , strncmpConcreteLen
  , cmpConcreteString
  , cmpConcretelyNullTerminatedString
  , cmpProvablyNullTerminatedString
  -- * Low-level string loading primitives
  -- ** 'ByteChecker'
  , ControlFlow(..)
  , ByteChecker(..)
  , withMaxChars
  -- *** For loading strings
  , fullyConcreteNullTerminatedString
  , concretelyNullTerminatedString
  , provablyNullTerminatedString
  -- *** For string length
  , fullyConcreteNullTerminatedStringLength
  , concretelyNullTerminatedStringLength
  , provablyNullTerminatedStringLength
  -- ** 'ByteLoader'
  , ByteLoader(..)
  , llvmByteLoader
  -- * 'loadBytes'
  , loadBytes
  -- * Loading and checking two byte streams
  -- ** 'BytesLoader'
  , BytesLoader(..)
  , llvmBytesLoader
  , llvmStringsLoader
  -- ** 'BytesChecker'
  , BytesChecker(..)
  , withMaxBytes
  -- ** 'loadTwoBytes'
  , loadTwoBytes
  -- ** 'BytesChecker's for string comparison
  , fullyConcreteNullTerminatedStrings
  , concretelyNullTerminatedStrings
  , provablyNullTerminatedStrings
  , lengthBoundedStringComparison
  , lengthBoundedProvablyNullTerminatedStringComparison
  -- ** 'BytesChecker's for length-bounded comparison
  , simpleByteComparison
  , lengthBoundedByteComparison
  ) where

import           Data.Bifunctor (Bifunctor(bimap))

import           Control.Monad.IO.Class (MonadIO, liftIO)
import qualified Control.Monad.State.Strict as State
import qualified Data.BitVector.Sized as BV
import           Data.Functor ((<&>))
import           Lens.Micro ((^.), to)
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.Errors.MemoryError as MemErr
import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.LLVM.MemModel as Mem
import qualified Lang.Crucible.LLVM.MemModel.Generic as Mem.G
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

-- | Store a null-terminated string to memory.
storeNullTerminatedString ::
  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 included)
  Vec.Vector (WI.SymBV sym 8) ->
  IO (LCLM.MemImpl sym)
storeNullTerminatedString :: 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)
storeNullTerminatedString 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
  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)
bytes
  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

-- | 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
  SymBV sym 8
zeroByte <- 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 (SymBV sym 8)
nullTerminatedBytes = Vector (SymBV sym 8) -> SymBV sym 8 -> Vector (SymBV sym 8)
forall a. Vector a -> a -> Vector a
Vec.snoc Vector (SymBV sym 8)
bytesBvs SymBV sym 8
zeroByte
  bak
-> MemImpl sym
-> LLVMPtr sym w
-> Vector (SymBV sym 8)
-> IO (MemImpl sym)
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)
storeNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym w
ptr Vector (SymBV sym 8)
nullTerminatedBytes

---------------------------------------------------------------------
-- * Loading strings

-- | 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 (m :: Type -> Type) sym bak a b.
(MonadIO m, 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,
-- 'loadProvablyNullTerminatedString' 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.
loadProvablyNullTerminatedString ::
  ( 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]
loadProvablyNullTerminatedString :: 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]
loadProvablyNullTerminatedString 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]
provablyNullTerminatedString
    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 (m :: Type -> Type) sym bak a b.
(MonadIO m, 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]
provablyNullTerminatedString 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

---------------------------------------------------------------------
-- * String length

-- | Implementation of libc @strnlen@.
strnlen ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Pointer to null-terminated string
  Mem.LLVMPtr sym wptr ->
  -- | Size
  --
  -- If this is not concrete, this will generate an assertion failure.
  WI.SymBV sym wptr ->
  IO (WI.SymBV sym wptr)
strnlen :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (SymBV sym wptr)
strnlen bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr SymBV sym wptr
bound = do
  case BV wptr -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV wptr -> Integer) -> Maybe (BV wptr) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym wptr -> Maybe (BV wptr)
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 SymBV sym wptr
bound of
    Maybe Integer
Nothing ->
      let err :: SimErrorReason
err = String -> String -> SimErrorReason
LCS.AssertFailureSimError String
"`strnlen` called with symbolic max length" String
"" in
      bak -> SimErrorReason -> IO (SymBV sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
LCB.addFailedAssertion bak
bak SimErrorReason
err
    Just Integer
b ->
      let bound' :: Maybe Int
bound' = Int -> Maybe Int
forall a. a -> Maybe a
Just (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
b) in
      bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym wptr)
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 wptr)
strlenConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
bound'
 
-- | @strlen@ of a concrete string.
--
-- If any symbolic bytes are encountered, an assertion failure will be
-- generated. If a maximum number of characters is provided, no more than that
-- number of characters will be read. In either case, 'strlenConcreteString'
-- will stop reading if it encounters a null terminator.
strlenConcreteString ::
  ( 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 Int
strlenConcreteString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO Int
strlenConcreteString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
limit = do
  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
  case Maybe Int
limit of
    Maybe Int
Nothing -> bak
-> MemImpl sym
-> Int
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker IO sym bak Int Int
-> IO Int
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 Int
0 LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker IO sym bak Int Int
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker m sym bak Int Int
fullyConcreteNullTerminatedStringLength
    Just Int
0 -> Int -> IO Int
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Int
0
    Just Int
l -> do
      let byteChecker :: ByteChecker IO sym bak (Int, Int) Int
byteChecker = Int
-> (Int -> IO Int)
-> ByteChecker IO sym bak Int Int
-> ByteChecker IO sym bak (Int, Int) Int
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, 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 Int -> IO Int
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ByteChecker IO sym bak Int Int
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker m sym bak Int Int
fullyConcreteNullTerminatedStringLength
      bak
-> MemImpl sym
-> (Int, Int)
-> LLVMPtr sym wptr
-> ByteLoader IO sym bak wptr
-> ByteChecker IO sym bak (Int, Int) Int
-> IO Int
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 (Int
0, Int
0) LLVMPtr sym wptr
ptr ByteLoader IO sym bak wptr
loader ByteChecker IO sym bak (Int, Int) Int
byteChecker
 
-- | @strlen@ of a null-terminated string (with a concrete null terminator).
--
-- 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, 'strlenConcretelyNullTerminatedString' will stop reading if
-- it encounters a (concretely) null terminator.
--
-- This has the same behavior as 'Lang.Crucible.LLVM.MemModel.strLen', except
-- that it supports a maximum length.
strlenConcretelyNullTerminatedString ::
  ( 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 wptr)
strlenConcretelyNullTerminatedString :: 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 wptr)
strlenConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
limit = do
  let loader :: ByteLoader (StateT (SymExpr sym BaseBoolType) IO) sym bak wptr
loader = MemImpl sym
-> ByteLoader (StateT (SymExpr sym BaseBoolType) 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
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymBV sym wptr
z <- sym -> NatRepr wptr -> IO (SymBV sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  (StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
 -> SymExpr sym BaseBoolType -> IO (SymBV sym wptr))
-> SymExpr sym BaseBoolType
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
-> IO (SymBV sym wptr)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
-> SymExpr sym BaseBoolType -> IO (SymBV sym wptr)
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m a
State.evalStateT (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred sym
sym) (StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
 -> IO (SymBV sym wptr))
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
-> IO (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$
    case Maybe Int
limit of
      Maybe Int
Nothing -> bak
-> MemImpl sym
-> SymBV sym wptr
-> LLVMPtr sym wptr
-> ByteLoader (StateT (SymExpr sym BaseBoolType) IO) sym bak wptr
-> ByteChecker
     (StateT (SymExpr sym BaseBoolType) IO)
     sym
     bak
     (SymBV sym wptr)
     (SymBV sym wptr)
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
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 wptr
z LLVMPtr sym wptr
ptr ByteLoader (StateT (SymExpr sym BaseBoolType) IO) sym bak wptr
loader ByteChecker
  (StateT (SymExpr sym BaseBoolType) IO)
  sym
  bak
  (SymBV sym wptr)
  (SymBV sym wptr)
forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
concretelyNullTerminatedStringLength
      Just Int
0 -> IO (SymBV sym wptr)
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
forall a. IO a -> StateT (SymExpr sym BaseBoolType) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr wptr -> IO (SymBV sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak) ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
      Just Int
l -> do
        let byteChecker :: ByteChecker
  (StateT (SymExpr sym BaseBoolType) IO)
  sym
  bak
  (SymBV sym wptr, Int)
  (SymBV sym wptr)
byteChecker = Int
-> (SymBV sym wptr
    -> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr))
-> ByteChecker
     (StateT (SymExpr sym BaseBoolType) IO)
     sym
     bak
     (SymBV sym wptr)
     (SymBV sym wptr)
-> ByteChecker
     (StateT (SymExpr sym BaseBoolType) IO)
     sym
     bak
     (SymBV sym wptr, Int)
     (SymBV sym wptr)
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, 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 wptr
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
forall a. a -> StateT (SymExpr sym BaseBoolType) IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ByteChecker
  (StateT (SymExpr sym BaseBoolType) IO)
  sym
  bak
  (SymBV sym wptr)
  (SymBV sym wptr)
forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
concretelyNullTerminatedStringLength
        bak
-> MemImpl sym
-> (SymBV sym wptr, Int)
-> LLVMPtr sym wptr
-> ByteLoader (StateT (SymExpr sym BaseBoolType) IO) sym bak wptr
-> ByteChecker
     (StateT (SymExpr sym BaseBoolType) IO)
     sym
     bak
     (SymBV sym wptr, Int)
     (SymBV sym wptr)
-> StateT (SymExpr sym BaseBoolType) IO (SymBV sym wptr)
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 wptr
z, Int
0) LLVMPtr sym wptr
ptr ByteLoader (StateT (SymExpr sym BaseBoolType) IO) sym bak wptr
loader ByteChecker
  (StateT (SymExpr sym BaseBoolType) IO)
  sym
  bak
  (SymBV sym wptr, Int)
  (SymBV sym wptr)
byteChecker

-- | @strlen@ of a provably null-terminated string.
--
-- 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,
-- 'strlenProvablyNullTerminatedString' will stop reading if it encounters a
-- (provably) null terminator.
strlenProvablyNullTerminatedString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , sym ~ WEB.ExprBuilder scope st fs
  , bak ~ LCBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  IO (WI.SymBV sym wptr)
strlenProvablyNullTerminatedString :: forall sym bak (wptr :: Natural) scope (st :: Type -> Type) fs
       solver.
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym wptr)
strlenProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr Maybe Int
limit = do
  let loader :: ByteLoader (StateT (Expr scope BaseBoolType) IO) sym bak wptr
loader = MemImpl sym
-> ByteLoader (StateT (Expr scope BaseBoolType) 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
  let sym :: ExprBuilder scope st fs
sym = bak -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  Expr scope (BaseBVType wptr)
z <- ExprBuilder scope st fs
-> NatRepr wptr -> IO (SymBV (ExprBuilder scope st fs) wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero ExprBuilder scope st fs
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  (StateT (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
 -> Expr scope BaseBoolType -> IO (Expr scope (BaseBVType wptr)))
-> Expr scope BaseBoolType
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
-> IO (Expr scope (BaseBVType wptr))
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
-> Expr scope BaseBoolType -> IO (Expr scope (BaseBVType wptr))
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m a
State.evalStateT (ExprBuilder scope st fs -> Pred (ExprBuilder scope st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred ExprBuilder scope st fs
sym) (StateT (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
 -> IO (Expr scope (BaseBVType wptr)))
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
-> IO (Expr scope (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$
    case Maybe Int
limit of
      Maybe Int
Nothing -> bak
-> MemImpl sym
-> Expr scope (BaseBVType wptr)
-> LLVMPtr sym wptr
-> ByteLoader (StateT (Expr scope BaseBoolType) IO) sym bak wptr
-> ByteChecker
     (StateT (Expr scope BaseBoolType) IO)
     sym
     bak
     (Expr scope (BaseBVType wptr))
     (Expr scope (BaseBVType wptr))
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
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 wptr)
z LLVMPtr sym wptr
ptr ByteLoader (StateT (Expr scope BaseBoolType) IO) sym bak wptr
loader ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  sym
  bak
  (Expr scope (BaseBVType wptr))
  (Expr scope (BaseBVType wptr))
ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  sym
  bak
  (SymBV sym wptr)
  (SymBV sym wptr)
forall (m :: Type -> Type) sym bak (wptr :: Natural) scope
       (st :: Type -> Type) fs solver.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 IsSymBackend sym bak, HasPtrWidth wptr,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
provablyNullTerminatedStringLength
      Just Int
0 -> IO (Expr scope (BaseBVType wptr))
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
forall a. IO a -> StateT (Expr scope BaseBoolType) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ExprBuilder scope st fs
-> NatRepr wptr -> IO (SymBV (ExprBuilder scope st fs) wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero (bak -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak) ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
      Just Int
l -> do
        let byteChecker :: ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  (Expr scope (BaseBVType wptr), Int)
  (Expr scope (BaseBVType wptr))
byteChecker = Int
-> (Expr scope (BaseBVType wptr)
    -> StateT
         (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr)))
-> ByteChecker
     (StateT (Expr scope BaseBoolType) IO)
     (ExprBuilder scope st fs)
     (OnlineBackend solver scope st fs)
     (Expr scope (BaseBVType wptr))
     (Expr scope (BaseBVType wptr))
-> ByteChecker
     (StateT (Expr scope BaseBoolType) IO)
     (ExprBuilder scope st fs)
     (OnlineBackend solver scope st fs)
     (Expr scope (BaseBVType wptr), Int)
     (Expr scope (BaseBVType wptr))
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, 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 wptr)
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
forall a. a -> StateT (Expr scope BaseBoolType) IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  (Expr scope (BaseBVType wptr))
  (Expr scope (BaseBVType wptr))
ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  (SymBV (ExprBuilder scope st fs) wptr)
  (SymBV (ExprBuilder scope st fs) wptr)
forall (m :: Type -> Type) sym bak (wptr :: Natural) scope
       (st :: Type -> Type) fs solver.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 IsSymBackend sym bak, HasPtrWidth wptr,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
provablyNullTerminatedStringLength
        bak
-> MemImpl sym
-> (Expr scope (BaseBVType wptr), Int)
-> LLVMPtr sym wptr
-> ByteLoader (StateT (Expr scope BaseBoolType) IO) sym bak wptr
-> ByteChecker
     (StateT (Expr scope BaseBoolType) IO)
     sym
     bak
     (Expr scope (BaseBVType wptr), Int)
     (Expr scope (BaseBVType wptr))
-> StateT
     (Expr scope BaseBoolType) IO (Expr scope (BaseBVType wptr))
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 wptr)
z, Int
0) LLVMPtr sym wptr
ptr ByteLoader (StateT (Expr scope BaseBoolType) IO) sym bak wptr
loader ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  sym
  bak
  (Expr scope (BaseBVType wptr), Int)
  (Expr scope (BaseBVType wptr))
ByteChecker
  (StateT (Expr scope BaseBoolType) IO)
  (ExprBuilder scope st fs)
  (OnlineBackend solver scope st fs)
  (Expr scope (BaseBVType wptr), Int)
  (Expr scope (BaseBVType wptr))
byteChecker

---------------------------------------------------------------------
-- * String copying

-- | Helper, not exported
strcpyAssertDisjoint ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Loaded bytes
  Vec.Vector (WI.SymBV sym 8) ->
  -- | Destination pointer
  Mem.LLVMPtr sym wptr ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  IO ()
strcpyAssertDisjoint :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
strcpyAssertDisjoint bak
bak MemImpl sym
mem Vector (SymBV sym 8)
bytes LLVMPtr sym wptr
dst LLVMPtr sym wptr
src = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  let len :: Integer
len = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (SymBV sym 8) -> Int
forall a. Vector a -> Int
Vec.length Vector (SymBV sym 8)
bytes)
  SymExpr sym (BaseBVType wptr)
sz <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
len)
  let heap :: Mem sym
heap = MemImpl sym
mem MemImpl sym -> Getting (Mem sym) (MemImpl sym) (Mem sym) -> Mem sym
forall s a. s -> Getting a s a -> a
^. (MemImpl sym -> Mem sym) -> SimpleGetter (MemImpl sym) (Mem sym)
forall s a. (s -> a) -> SimpleGetter s a
to MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
Mem.memImplHeap
  let memOp :: MemoryOp sym wptr
memOp =
        (Maybe String, LLVMPtr sym wptr)
-> (Maybe String, LLVMPtr sym wptr)
-> SymExpr sym (BaseBVType wptr)
-> Mem sym
-> MemoryOp sym wptr
forall sym (w :: Natural) (wlen :: Natural).
(1 <= wlen) =>
(Maybe String, LLVMPtr sym w)
-> (Maybe String, LLVMPtr sym w)
-> SymBV sym wlen
-> Mem sym
-> MemoryOp sym w
MemErr.MemCopyOp (String -> Maybe String
forall a. a -> Maybe a
Just String
"strcpy dst", LLVMPtr sym wptr
dst) (String -> Maybe String
forall a. a -> Maybe a
Just String
"strcpy src", LLVMPtr sym wptr
src) SymExpr sym (BaseBVType wptr)
sz Mem sym
heap
  bak
-> MemoryOp sym wptr
-> NatRepr wptr
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> IO ()
forall (w :: Natural) (wptr :: Natural) sym bak.
(1 <= w, HasPtrWidth wptr, IsSymBackend sym bak, HasLLVMAnn sym) =>
bak
-> MemoryOp sym wptr
-> NatRepr w
-> LLVMPtr sym wptr
-> SymBV sym w
-> LLVMPtr sym wptr
-> SymBV sym w
-> IO ()
Mem.assertDisjointRegions bak
bak MemoryOp sym wptr
memOp ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth LLVMPtr sym wptr
dst SymExpr sym (BaseBVType wptr)
sz LLVMPtr sym wptr
src SymExpr sym (BaseBVType wptr)
sz

-- | @strcpy@ of a concrete string.
--
-- Uses 'Mem.loadString' to load the string, see that function for details.
--
-- Asserts that the regions are disjoint.
copyConcreteString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Destination pointer
  Mem.LLVMPtr sym wptr ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  IO (Mem.MemImpl sym)
copyConcreteString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO (MemImpl sym)
copyConcreteString bak
bak MemImpl sym
mem LLVMPtr sym wptr
dst LLVMPtr sym wptr
src = do
  [Word8]
bytes <- bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
Mem.loadString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
forall a. Maybe a
Nothing
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  [SymExpr sym (BaseBVType 8)]
symBytes <- (Word8 -> IO (SymExpr sym (BaseBVType 8)))
-> [Word8] -> IO [SymExpr sym (BaseBVType 8)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 8
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
WI.knownRepr (BV 8 -> IO (SymExpr sym (BaseBVType 8)))
-> (Word8 -> BV 8) -> Word8 -> IO (SymExpr sym (BaseBVType 8))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> BV 8
BV.word8) [Word8]
bytes
  let bytesVec :: Vector (SymExpr sym (BaseBVType 8))
bytesVec = [SymExpr sym (BaseBVType 8)] -> Vector (SymExpr sym (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [SymExpr sym (BaseBVType 8)]
symBytes
  bak
-> MemImpl sym
-> Vector (SymExpr sym (BaseBVType 8))
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
strcpyAssertDisjoint bak
bak MemImpl sym
mem Vector (SymExpr sym (BaseBVType 8))
bytesVec LLVMPtr sym wptr
dst LLVMPtr sym wptr
src
  bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Vector (SymExpr sym (BaseBVType 8))
-> IO (MemImpl sym)
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 wptr
dst ([SymExpr sym (BaseBVType 8)] -> Vector (SymExpr sym (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [SymExpr sym (BaseBVType 8)]
symBytes)

-- | @strcpy@ of a concretely null-terminated string.
--
-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that
-- function for details.
--
-- Asserts that the regions are disjoint.
copyConcretelyNullTerminatedString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Destination pointer
  Mem.LLVMPtr sym wptr ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  IO (Mem.MemImpl sym)
copyConcretelyNullTerminatedString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (MemImpl sym)
copyConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
dst LLVMPtr sym wptr
src Maybe Int
bounds = do
  [SymExpr sym (BaseBVType 8)]
bytes <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Maybe Int
-> IO [SymExpr sym (BaseBVType 8)]
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
src Maybe Int
bounds
  let bytesVec :: Vector (SymExpr sym (BaseBVType 8))
bytesVec = [SymExpr sym (BaseBVType 8)] -> Vector (SymExpr sym (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [SymExpr sym (BaseBVType 8)]
bytes
  bak
-> MemImpl sym
-> Vector (SymExpr sym (BaseBVType 8))
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
strcpyAssertDisjoint bak
bak MemImpl sym
mem Vector (SymExpr sym (BaseBVType 8))
bytesVec LLVMPtr sym wptr
dst LLVMPtr sym wptr
src
  bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Vector (SymExpr sym (BaseBVType 8))
-> IO (MemImpl sym)
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 wptr
dst Vector (SymExpr sym (BaseBVType 8))
bytesVec

-- | @strcpy@ of a concrete string.
--
-- Uses 'loadProvablyNullTerminatedString' to load the string, see that
-- function for details.
--
-- Asserts that the regions are disjoint.
copyProvablyNullTerminatedString ::
  ( 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 ->
  -- | Destination pointer
  Mem.LLVMPtr sym wptr ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  IO (Mem.MemImpl sym)
copyProvablyNullTerminatedString :: 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
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (MemImpl sym)
copyProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
dst LLVMPtr sym wptr
src Maybe Int
bounds = do
  [Expr scope (BaseBVType 8)]
bytes <- bak
-> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [SymBV sym 8]
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]
loadProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
bounds
  let bytesVec :: Vector (Expr scope (BaseBVType 8))
bytesVec = [Expr scope (BaseBVType 8)] -> Vector (Expr scope (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [Expr scope (BaseBVType 8)]
bytes
  bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO ()
strcpyAssertDisjoint bak
bak MemImpl sym
mem Vector (Expr scope (BaseBVType 8))
Vector (SymBV sym 8)
bytesVec LLVMPtr sym wptr
dst LLVMPtr sym wptr
src
  bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Vector (SymBV sym 8)
-> IO (MemImpl sym)
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 wptr
dst Vector (Expr scope (BaseBVType 8))
Vector (SymBV sym 8)
bytesVec

---------------------------------------------------------------------
-- * String duplication

-- | Helper function: allocate memory and store bytes for string duplication.
--
-- Takes a vector of bytes (NOT including null terminator) and:
-- 1. Allocates memory of the appropriate size (length + 1 for null terminator)
-- 2. Stores the bytes with null terminator to the allocated memory
-- 3. Returns the new pointer and updated memory
dupFromLoadedBytes ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Vec.Vector (WI.SymBV sym 8) ->
  String ->
  CLD.Alignment ->
  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
dupFromLoadedBytes :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupFromLoadedBytes bak
bak MemImpl sym
mem Vector (SymBV sym 8)
bytesVec String
displayString Alignment
alignment = do
  let len :: Integer
len = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (SymBV sym 8) -> Int
forall a. Vector a -> Int
Vec.length Vector (SymBV sym 8)
bytesVec) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1  -- +1 for null terminator
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymExpr sym (BaseBVType wptr)
sz <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
len)
  (LLVMPointer sym wptr
dst, MemImpl sym
mem') <- bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymExpr sym (BaseBVType wptr)
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
Mem.doMalloc bak
bak AllocType
Mem.G.HeapAlloc Mutability
Mem.G.Mutable String
displayString MemImpl sym
mem SymExpr sym (BaseBVType wptr)
sz Alignment
alignment
  MemImpl sym
mem'' <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Vector (SymBV sym 8)
-> IO (MemImpl sym)
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 wptr
LLVMPointer sym wptr
dst Vector (SymBV sym 8)
bytesVec
  (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (LLVMPointer sym wptr
dst, MemImpl sym
mem'')

-- | @strdup@ of a concrete string.
--
-- Uses 'Mem.loadString' to load the string, see that function for details.
--
-- Allocates memory and copies the string to it, returning the new pointer.
dupConcreteString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  -- | Display string for allocation
  String ->
  -- | Alignment
  CLD.Alignment ->
  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
dupConcreteString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupConcreteString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src String
displayString Alignment
alignment = do
  [Word8]
bytes <- bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
Mem.loadString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
forall a. Maybe a
Nothing
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  [SymExpr sym (BaseBVType 8)]
symBytes <- (Word8 -> IO (SymExpr sym (BaseBVType 8)))
-> [Word8] -> IO [SymExpr sym (BaseBVType 8)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 8
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
WI.knownRepr (BV 8 -> IO (SymExpr sym (BaseBVType 8)))
-> (Word8 -> BV 8) -> Word8 -> IO (SymExpr sym (BaseBVType 8))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> BV 8
BV.word8) [Word8]
bytes
  bak
-> MemImpl sym
-> Vector (SymExpr sym (BaseBVType 8))
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupFromLoadedBytes bak
bak MemImpl sym
mem ([SymExpr sym (BaseBVType 8)] -> Vector (SymExpr sym (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [SymExpr sym (BaseBVType 8)]
symBytes) String
displayString Alignment
alignment

-- | @strdup@ of a concretely null-terminated string.
--
-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that
-- function for details.
--
-- Allocates memory and copies the string to it, returning the new pointer.
dupConcretelyNullTerminatedString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  -- | Display string for allocation
  String ->
  CLD.Alignment ->
  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
dupConcretelyNullTerminatedString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Maybe Int
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
bounds String
displayString Alignment
alignment = do
  [SymExpr sym (BaseBVType 8)]
bytes <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Maybe Int
-> IO [SymExpr sym (BaseBVType 8)]
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
src Maybe Int
bounds
  bak
-> MemImpl sym
-> Vector (SymExpr sym (BaseBVType 8))
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupFromLoadedBytes bak
bak MemImpl sym
mem ([SymExpr sym (BaseBVType 8)] -> Vector (SymExpr sym (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [SymExpr sym (BaseBVType 8)]
bytes) String
displayString Alignment
alignment

-- | @strdup@ of a provably null-terminated string.
--
-- Uses 'loadProvablyNullTerminatedString' to load the string, see that
-- function for details.
--
-- Allocates memory and copies the string to it, returning the new pointer.
dupProvablyNullTerminatedString ::
  ( 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 ->
  -- | Source pointer
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to read
  Maybe Int ->
  -- | Display string for allocation
  String ->
  CLD.Alignment ->
  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
dupProvablyNullTerminatedString :: 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
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
bounds String
displayString Alignment
alignment = do
  [Expr scope (BaseBVType 8)]
bytes <- bak
-> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [SymBV sym 8]
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]
loadProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
src Maybe Int
bounds
  bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> Vector (SymBV sym 8)
-> String
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
dupFromLoadedBytes bak
bak MemImpl sym
mem ([Expr scope (BaseBVType 8)] -> Vector (Expr scope (BaseBVType 8))
forall a. [a] -> Vector a
Vec.fromList [Expr scope (BaseBVType 8)]
bytes) String
displayString Alignment
alignment

---------------------------------------------------------------------
-- * String comparison

-- | Compare two concrete strings.
--
-- Uses 'fullyConcreteNullTerminatedStrings' checker. Both strings must be
-- fully concrete (no symbolic bytes).
--
-- Returns:
-- * 0 if the strings are equal
-- * A negative value if the first differing byte in s1 is less than in s2
-- * A positive value if the first differing byte in s1 is greater than in s2
cmpConcreteString ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  IO (WI.SymBV sym 32)
cmpConcreteString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> IO (SymBV sym 32)
cmpConcreteString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymBV sym 32
zero <- sym -> NatRepr 32 -> IO (SymBV sym 32)
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 @32)
  bak
-> MemImpl sym
-> SymBV sym 32
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker IO sym bak (SymBV sym 32) (SymBV sym 32)
-> IO (SymBV sym 32)
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem SymBV sym 32
zero LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem) BytesChecker IO sym bak (SymBV sym 32) (SymBV sym 32)
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
fullyConcreteNullTerminatedStrings

-- | Compare two strings with concrete null terminators.
--
-- Uses 'concretelyNullTerminatedStrings' checker. The strings must have
-- concrete null terminators, but may contain symbolic bytes before the terminator.
--
-- If a maximum length is provided, comparison stops at that length even if
-- no null terminator is encountered.
--
-- Returns:
-- * 0 if the strings are equal
-- * A negative value if the first differing byte in s1 is less than in s2
-- * A positive value if the first differing byte in s1 is greater than in s2
cmpConcretelyNullTerminatedString ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to compare
  Maybe Int ->
  IO (WI.SymBV sym 32)
cmpConcretelyNullTerminatedString :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym 32)
cmpConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 Maybe Int
maxLen = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymBV sym 32
zero <- sym -> NatRepr 32 -> IO (SymBV sym 32)
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 @32)
  case Maybe Int
maxLen of
    Maybe Int
Nothing ->
      bak
-> MemImpl sym
-> SymBV sym 32
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker IO sym bak (SymBV sym 32) (SymBV sym 32)
-> IO (SymBV sym 32)
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem SymBV sym 32
zero LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem) BytesChecker IO sym bak (SymBV sym 32) (SymBV sym 32)
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
concretelyNullTerminatedStrings
    Just Int
0 ->
      sym -> NatRepr 32 -> IO (SymBV sym 32)
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 @32)
    Just Int
n ->
      bak
-> MemImpl sym
-> (SymBV sym 32, Integer)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker IO sym bak (SymBV sym 32, Integer) (SymBV sym 32)
-> IO (SymBV sym 32)
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem (SymBV sym 32
zero, Integer
0) LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem) (Integer
-> BytesChecker IO sym bak (SymBV sym 32, Integer) (SymBV sym 32)
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
Integer
-> BytesChecker m sym bak (SymBV sym 32, Integer) (SymBV sym 32)
lengthBoundedStringComparison (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n))

-- | Compare two strings with provably null terminators.
--
-- Uses 'provablyNullTerminatedStrings' checker. Consults an SMT solver to
-- check if bytes are provably null terminators.
--
-- If a maximum length is provided, comparison stops at that length even if
-- no null terminator is encountered.
--
-- Returns:
-- * 0 if the strings are equal
-- * A negative value if the first differing byte in s1 is less than in s2
-- * A positive value if the first differing byte in s1 is greater than in s2
cmpProvablyNullTerminatedString ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , sym ~ WEB.ExprBuilder scope st fs
  , bak ~ LCBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  -- | Maximum number of characters to compare
  Maybe Int ->
  IO (WI.SymBV sym 32)
cmpProvablyNullTerminatedString :: forall sym bak (wptr :: Natural) scope (st :: Type -> Type) fs
       solver.
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym 32)
cmpProvablyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 Maybe Int
maxLen = do
  let sym :: ExprBuilder scope st fs
sym = bak -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  SymExpr (ExprBuilder scope st fs) (BaseBVType 32)
zero <- ExprBuilder scope st fs
-> NatRepr 32
-> IO (SymExpr (ExprBuilder scope st fs) (BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero ExprBuilder scope st fs
sym (forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32)
  case Maybe Int
maxLen of
    Maybe Int
Nothing ->
      bak
-> MemImpl sym
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 32)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker
     IO
     sym
     bak
     (SymExpr (ExprBuilder scope st fs) (BaseBVType 32))
     (Expr scope (BaseBVType 32))
-> IO (Expr scope (BaseBVType 32))
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem SymExpr (ExprBuilder scope st fs) (BaseBVType 32)
zero LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem) BytesChecker IO sym bak (SymBV sym 32) (SymBV sym 32)
BytesChecker
  IO
  sym
  bak
  (SymExpr (ExprBuilder scope st fs) (BaseBVType 32))
  (Expr scope (BaseBVType 32))
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) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
provablyNullTerminatedStrings
    Just Int
0 ->
      ExprBuilder scope st fs
-> NatRepr 32
-> IO (SymExpr (ExprBuilder scope st fs) (BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero ExprBuilder scope st fs
sym (forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32)
    Just Int
n ->
      bak
-> MemImpl sym
-> (SymExpr (ExprBuilder scope st fs) (BaseBVType 32), Integer)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker
     IO
     sym
     bak
     (SymExpr (ExprBuilder scope st fs) (BaseBVType 32), Integer)
     (Expr scope (BaseBVType 32))
-> IO (Expr scope (BaseBVType 32))
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem (SymExpr (ExprBuilder scope st fs) (BaseBVType 32)
zero, Integer
0) LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem) (Integer
-> BytesChecker IO sym bak (SymBV sym 32, Integer) (SymBV sym 32)
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) =>
Integer
-> BytesChecker m sym bak (SymBV sym 32, Integer) (SymBV sym 32)
lengthBoundedProvablyNullTerminatedStringComparison (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n))

-- | @strncmp@ - compare two null-terminated strings up to n characters.
--
-- See 'strncmpConcreteLen' for the return value.
--
-- Asserts that the length is concrete (non-symbolic).
strncmp ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  WI.SymBV sym wptr ->
  IO (WI.SymBV sym 32)
strncmp :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (SymBV sym 32)
strncmp bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 SymBV sym wptr
len =
  case BV wptr -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV wptr -> Integer) -> Maybe (BV wptr) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym wptr -> Maybe (BV wptr)
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 SymBV sym wptr
len of
    Just Integer
n -> bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
strncmpConcreteLen bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (Integer -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
    Maybe Integer
Nothing -> do
      let err :: SimErrorReason
err = String -> String -> SimErrorReason
LCS.AssertFailureSimError String
"`strncmp` called with symbolic length" String
""
      bak -> SimErrorReason -> IO (SymBV sym 32)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
LCB.addFailedAssertion bak
bak SimErrorReason
err

-- | Compare two null-terminated strings up to n characters with a concrete length.
--
-- Returns:
-- * 0 if the strings are equal (up to n characters or null terminator)
-- * A negative value if the first differing byte in s1 is less than in s2
-- * A positive value if the first differing byte in s1 is greater than in s2
--
-- Requires that both strings have concrete null terminators.
strncmpConcreteLen ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  Integer ->
  IO (WI.SymBV sym 32)
strncmpConcreteLen :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
strncmpConcreteLen bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 Integer
n =
  bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym 32)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Maybe Int
-> IO (SymBV sym 32)
cmpConcretelyNullTerminatedString bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (Int -> Maybe Int
forall a. a -> Maybe a
Just (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n))

---------------------------------------------------------------------
-- * Memory comparison

-- | @memcmp@.
--
-- See 'memcmpConcreteLen' for the return value.
--
-- Asserts that the length is concrete (non-symbolic).
memcmp ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  WI.SymBV sym wptr ->
  IO (WI.SymBV sym 32)
memcmp :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (SymBV sym 32)
memcmp bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 SymBV sym wptr
len =
  case BV wptr -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV wptr -> Integer) -> Maybe (BV wptr) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym wptr -> Maybe (BV wptr)
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 SymBV sym wptr
len of
    Just Integer
n -> bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
memcmpConcreteLen bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (Integer -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
    Maybe Integer
Nothing -> do
      let err :: SimErrorReason
err = String -> String -> SimErrorReason
LCS.AssertFailureSimError String
"`memcmp` called with symbolic length" String
""
      bak -> SimErrorReason -> IO (SymBV sym 32)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
LCB.addFailedAssertion bak
bak SimErrorReason
err

-- | Compare two memory regions byte-by-byte with a concrete length.
--
-- Returns:
-- * 0 if the regions are equal
-- * A negative value if the first differing byte in s1 is less than in s2
-- * A positive value if the first differing byte in s1 is greater than in s2
memcmpConcreteLen ::
  forall sym bak wptr.
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Partial.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  ) =>
  bak ->
  Mem.MemImpl sym ->
  Mem.LLVMPtr sym wptr ->
  Mem.LLVMPtr sym wptr ->
  Integer ->
  IO (WI.SymBV sym 32)
memcmpConcreteLen :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> Integer
-> IO (SymBV sym 32)
memcmpConcreteLen bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = do
      let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
      sym -> NatRepr 32 -> IO (SymBV sym 32)
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 @32)
  | Bool
otherwise =
      bak
-> MemImpl sym
-> ((), Integer)
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader IO sym bak wptr
-> BytesChecker IO sym bak ((), Integer) (SymBV sym 32)
-> IO (SymBV sym 32)
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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem ((), Integer
0) LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 (MemImpl sym -> BytesLoader 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 -> BytesLoader m sym bak wptr
llvmBytesLoader MemImpl sym
mem) (Integer -> BytesChecker IO sym bak ((), Integer) (SymBV sym 32)
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
Integer -> BytesChecker m sym bak ((), Integer) (SymBV sym 32)
lengthBoundedByteComparison Integer
n)

---------------------------------------------------------------------
-- * 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 adding a maximum character length.
withMaxChars ::
  MonadIO m =>
  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 (m :: Type -> Type) sym bak a b.
(MonadIO m, 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 ->
    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 m (ControlFlow a b)
-> (ControlFlow a b -> m (ControlFlow (a, Int) b))
-> m (ControlFlow (a, Int) 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
r -> ControlFlow (a, Int) b -> m (ControlFlow (a, Int) b)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (b -> ControlFlow (a, Int) b
forall a b. b -> ControlFlow a b
Break b
r)
        Continue a
r ->
          if Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 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
r
          else ControlFlow (a, Int) b -> m (ControlFlow (a, Int) b)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((a, Int) -> ControlFlow (a, Int) b
forall a b. a -> ControlFlow a b
Continue (a
r, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

---------------------------------------------------------------------
-- *** For loading strings

-- | '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 provably-null terminator.
--
-- Used in 'loadSymbolicString'.
provablyNullTerminatedString ::
  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]
provablyNullTerminatedString :: 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]
provablyNullTerminatedString =
  (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 -> IO (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
-> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
 -> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8]))
-> IO (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
-> m (ControlFlow ([SymBV sym 8] -> [SymBV sym 8]) [SymBV sym 8])
forall a b. (a -> b) -> a -> b
$ do
    SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte <- bak
-> LLVMPtr (ExprBuilder scope st fs) 8
-> IO (SymExpr (ExprBuilder scope st fs) (BaseBVType 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 <- bak
-> ExprBuilder scope st fs
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> IO Bool
forall sym bak scope (st :: Type -> Type) fs solver.
(HasCallStack, IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak -> sym -> SymBV sym 8 -> IO Bool
isProvablyNullTerminator bak
bak ExprBuilder scope st fs
sym SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte
    if Bool
isNullTerm
    then ControlFlow
  ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
  [Expr scope (BaseBVType 8)]
-> IO
     (ControlFlow
        ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
        [Expr scope (BaseBVType 8)])
forall a. a -> IO 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)]
-> IO
     (ControlFlow
        ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
        [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)])
-> ControlFlow
     ([Expr scope (BaseBVType 8)] -> [Expr scope (BaseBVType 8)])
     [Expr scope (BaseBVType 8)]
forall a b. a -> ControlFlow a b
Continue (\[SymExpr (ExprBuilder scope st fs) (BaseBVType 8)]
l -> [SymBV sym 8] -> [SymBV sym 8]
acc (SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> [SymExpr (ExprBuilder scope st fs) (BaseBVType 8)]
-> [SymExpr (ExprBuilder scope st fs) (BaseBVType 8)]
forall a. a -> [a] -> [a]
: [SymExpr (ExprBuilder scope st fs) (BaseBVType 8)]
l)))

-- Helper, not exported
isProvablyNullTerminator ::
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  sym ~ WEB.ExprBuilder scope st fs =>
  bak ~ LCBO.OnlineBackend solver scope st fs =>
  WPO.OnlineSolver solver =>
  bak ->
  sym ->
  WI.SymBV sym 8 ->
  IO Bool
isProvablyNullTerminator :: forall sym bak scope (st :: Type -> Type) fs solver.
(HasCallStack, IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak -> sym -> SymBV sym 8 -> IO Bool
isProvablyNullTerminator bak
bak sym
sym SymBV sym 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)
SymBV sym 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 bak
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
        Expr scope (BaseBVType 8)
z <- 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
WI.knownNat @8)
        BoolExpr scope
p <- 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 8 -> SymBV sym 8 -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym Expr scope (BaseBVType 8)
SymBV sym 8
z SymBV sym 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
"isProvablyNullTerminator" 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

---------------------------------------------------------------------
-- *** For string length

-- | 'ByteChecker' for @strlen@ of concrete strings.
fullyConcreteNullTerminatedStringLength ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  ByteChecker m sym bak Int Int
fullyConcreteNullTerminatedStringLength :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
ByteChecker m sym bak Int Int
fullyConcreteNullTerminatedStringLength =
  (bak -> Int -> LLVMPtr sym 8 -> m (ControlFlow Int Int))
-> ByteChecker m sym bak Int Int
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 -> Int -> LLVMPtr sym 8 -> m (ControlFlow Int Int))
 -> ByteChecker m sym bak Int Int)
-> (bak -> Int -> LLVMPtr sym 8 -> m (ControlFlow Int Int))
-> ByteChecker m sym bak Int Int
forall a b. (a -> b) -> a -> b
$ \bak
bak Int
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 Int Int -> m (ControlFlow Int Int)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Int -> ControlFlow Int Int
forall a b. b -> ControlFlow a b
Break Int
acc)
      Just Integer
_ -> ControlFlow Int Int -> m (ControlFlow Int Int)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Int -> ControlFlow Int Int
forall a b. a -> ControlFlow a b
Continue (Int -> ControlFlow Int Int) -> Int -> ControlFlow Int Int
forall a b. (a -> b) -> a -> b
$! Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      Maybe Integer
Nothing -> do
        let msg :: String
msg = String
"Symbolic value encountered when loading a string"
        IO (ControlFlow Int Int) -> m (ControlFlow Int Int)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak -> SimErrorReason -> IO (ControlFlow Int Int)
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))

-- Helper, not exported
symStringLength ::
  MonadIO m =>
  State.MonadState (WI.Pred sym) m =>
  GHC.HasCallStack =>
  Mem.HasPtrWidth wptr =>
  LCB.IsSymBackend sym bak =>
  -- | How to check if a predicate is false
  (bak -> WI.Pred sym -> m Bool) ->
  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
symStringLength :: forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
(bak -> Pred sym -> m Bool)
-> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
symStringLength bak -> Pred sym -> m Bool
predIsFalse =
  (bak
 -> SymBV sym wptr
 -> LLVMPtr sym 8
 -> m (ControlFlow (SymBV sym wptr) (SymBV sym wptr)))
-> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
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 wptr
  -> LLVMPtr sym 8
  -> m (ControlFlow (SymBV sym wptr) (SymBV sym wptr)))
 -> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr))
-> (bak
    -> SymBV sym wptr
    -> LLVMPtr sym 8
    -> m (ControlFlow (SymBV sym wptr) (SymBV sym wptr)))
-> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak SymBV sym wptr
len 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)
    Pred sym
keepGoing <- m (Pred sym)
forall s (m :: Type -> Type). MonadState s m => m s
State.get
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
    Pred sym
byteWasNonNull <- IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym (BaseBVType 8) -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
WI.bvIsNonzero sym
sym SymExpr sym (BaseBVType 8)
byte)
    Pred sym
keepGoing' <- IO (Pred sym) -> m (Pred sym)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred sym
sym Pred sym
keepGoing Pred sym
byteWasNonNull)
    Bool
stopHere <- bak -> Pred sym -> m Bool
predIsFalse bak
bak Pred sym
keepGoing'
    if Bool
stopHere
    then ControlFlow (SymBV sym wptr) (SymBV sym wptr)
-> m (ControlFlow (SymBV sym wptr) (SymBV sym wptr))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym wptr -> ControlFlow (SymBV sym wptr) (SymBV sym wptr)
forall a b. b -> ControlFlow a b
Break SymBV sym wptr
len)
    else do
      Pred sym -> m ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
State.put Pred sym
keepGoing'
      SymBV sym wptr
lenPlusOne <- IO (SymBV sym wptr) -> m (SymBV sym wptr)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAdd sym
sym SymBV sym wptr
len (SymBV sym wptr -> IO (SymBV sym wptr))
-> IO (SymBV sym wptr) -> IO (SymBV sym wptr)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr wptr -> IO (SymBV sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
      SymBV sym wptr -> ControlFlow (SymBV sym wptr) (SymBV sym wptr)
forall a b. a -> ControlFlow a b
Continue (SymBV sym wptr -> ControlFlow (SymBV sym wptr) (SymBV sym wptr))
-> m (SymBV sym wptr)
-> m (ControlFlow (SymBV sym wptr) (SymBV sym wptr))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (SymBV sym wptr) -> m (SymBV sym wptr)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym
-> Pred sym
-> SymBV sym wptr
-> SymBV sym wptr
-> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
keepGoing' SymBV sym wptr
lenPlusOne SymBV sym wptr
len)

-- | 'ByteChecker' for @strlen@ of strings with a concrete null terminator.
concretelyNullTerminatedStringLength ::
  MonadIO m =>
  State.MonadState (WI.Pred sym) m =>
  GHC.HasCallStack =>
  Mem.HasPtrWidth wptr =>
  LCB.IsSymBackend sym bak =>
  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
concretelyNullTerminatedStringLength :: forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
concretelyNullTerminatedStringLength =
  (bak -> Pred sym -> m Bool)
-> ByteChecker
     m
     sym
     bak
     (SymExpr sym ('BaseBVType wptr))
     (SymExpr sym ('BaseBVType wptr))
forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
(bak -> Pred sym -> m Bool)
-> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
symStringLength (\bak
_bak Pred sym
p -> Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
WI.asConstantPred Pred sym
p Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False))

-- | 'ByteChecker' for @strlen@ for strings with a provably-null terminator.
provablyNullTerminatedStringLength ::
  MonadIO m =>
  State.MonadState (WI.Pred sym) m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  Mem.HasPtrWidth wptr =>
  sym ~ WEB.ExprBuilder scope st fs =>
  bak ~ LCBO.OnlineBackend solver scope st fs =>
  WPO.OnlineSolver solver =>
  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
provablyNullTerminatedStringLength :: forall (m :: Type -> Type) sym bak (wptr :: Natural) scope
       (st :: Type -> Type) fs solver.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 IsSymBackend sym bak, HasPtrWidth wptr,
 sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
provablyNullTerminatedStringLength =
  (bak -> Pred sym -> m Bool)
-> ByteChecker
     m
     sym
     bak
     (SymExpr sym ('BaseBVType wptr))
     (SymExpr sym ('BaseBVType wptr))
forall (m :: Type -> Type) sym (wptr :: Natural) bak.
(MonadIO m, MonadState (Pred sym) m, HasCallStack,
 HasPtrWidth wptr, IsSymBackend sym bak) =>
(bak -> Pred sym -> m Bool)
-> ByteChecker m sym bak (SymBV sym wptr) (SymBV sym wptr)
symStringLength ((bak -> Pred sym -> m Bool)
 -> ByteChecker
      m
      sym
      bak
      (SymExpr sym ('BaseBVType wptr))
      (SymExpr sym ('BaseBVType wptr)))
-> (bak -> Pred sym -> m Bool)
-> ByteChecker
     m
     sym
     bak
     (SymExpr sym ('BaseBVType wptr))
     (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak Pred sym
p ->
    case Expr scope BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
WI.asConstantPred Expr scope BaseBoolType
Pred sym
p of
      Just Bool
b -> Bool -> m Bool
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
b
      Maybe Bool
_ ->
        IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ 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 bak
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
          SolverProcess scope solver
-> String -> Expr scope BaseBoolType -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
WPO.checkSatisfiable SolverProcess scope solver
proc String
"provablyNullTerminatedStringLength" Expr scope BaseBoolType
Pred sym
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

---------------------------------------------------------------------
-- ** '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

---------------------------------------------------------------------
-- * Loading and checking two byte streams

-- ** 'BytesLoader'

-- | Load a byte from each of two memory locations.
--
-- The loader can optionally add assumptions after loading bytes when iteration
-- continues. This is used for null-terminated string operations where we need
-- to assume loaded bytes are non-null.
--
-- Like 'ByteLoader', but for two bytes (usually from different strings) at
-- once.
data BytesLoader m sym bak wptr
  = BytesLoader
      { forall (m :: Type -> Type) sym bak (wptr :: Natural).
BytesLoader m sym bak wptr
-> bak
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> m (LLVMPtr sym 8, LLVMPtr sym 8)
runBytesLoader :: bak -> Mem.LLVMPtr sym wptr -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8, Mem.LLVMPtr sym 8)
      -- | Called when the 'BytesChecker' returns 'Continue', allowing the
      -- loader to add assumptions about the loaded bytes (e.g., that they are
      -- non-null).
      , forall (m :: Type -> Type) sym bak (wptr :: Natural).
BytesLoader m sym bak wptr
-> bak -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m ()
onContinue :: bak -> Mem.LLVMPtr sym 8 -> Mem.LLVMPtr sym 8 -> m ()
      }

-- | A 'BytesLoader' for LLVM memory based on 'Mem.doLoad'.
--
-- This version does not add any assumptions about loaded bytes.
-- Use this for length-bounded operations like @memcmp@ that need to handle
-- null bytes in the middle of the data.
llvmBytesLoader ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , MonadIO m
  ) =>
  Mem.MemImpl sym ->
  BytesLoader m sym bak wptr
llvmBytesLoader :: forall sym bak (wptr :: Natural) (m :: Type -> Type).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
MemImpl sym -> BytesLoader m sym bak wptr
llvmBytesLoader MemImpl sym
mem =
  BytesLoader
    { runBytesLoader :: bak
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> m (LLVMPtr sym 8, LLVMPtr sym 8)
runBytesLoader = \bak
bak LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 -> 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)
        LLVMPointer sym 8
byte1 <- 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
ptr1 StorageType
i1 TypeRepr (LLVMPointerType 8)
p8 Alignment
CLD.noAlignment)
        LLVMPointer sym 8
byte2 <- 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
ptr2 StorageType
i1 TypeRepr (LLVMPointerType 8)
p8 Alignment
CLD.noAlignment)
        (LLVMPointer sym 8, LLVMPointer sym 8)
-> m (LLVMPointer sym 8, LLVMPointer sym 8)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (LLVMPointer sym 8
byte1, LLVMPointer sym 8
byte2)
    , onContinue :: bak -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m ()
onContinue = \bak
_ LLVMPtr sym 8
_ LLVMPtr sym 8
_ -> () -> m ()
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    }

-- | A 'BytesLoader' for LLVM memory that adds non-null assumptions.
--
-- This version adds assumptions that loaded bytes are non-null when iteration
-- continues. Use this for null-terminated string operations like @strcmp@.
llvmStringsLoader ::
  ( LCB.IsSymBackend sym bak
  , Mem.HasPtrWidth wptr
  , Mem.HasLLVMAnn sym
  , ?memOpts :: Mem.MemOptions
  , GHC.HasCallStack
  , MonadIO m
  ) =>
  Mem.MemImpl sym ->
  BytesLoader m sym bak wptr
llvmStringsLoader :: forall sym bak (wptr :: Natural) (m :: Type -> Type).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack, MonadIO m) =>
MemImpl sym -> BytesLoader m sym bak wptr
llvmStringsLoader MemImpl sym
mem =
  BytesLoader
    { runBytesLoader :: bak
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> m (LLVMPtr sym 8, LLVMPtr sym 8)
runBytesLoader = \bak
bak LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 -> 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)
        LLVMPointer sym 8
byte1 <- 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
ptr1 StorageType
i1 TypeRepr (LLVMPointerType 8)
p8 Alignment
CLD.noAlignment)
        LLVMPointer sym 8
byte2 <- 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
ptr2 StorageType
i1 TypeRepr (LLVMPointerType 8)
p8 Alignment
CLD.noAlignment)
        (LLVMPointer sym 8, LLVMPointer sym 8)
-> m (LLVMPointer sym 8, LLVMPointer sym 8)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (LLVMPointer sym 8
byte1, LLVMPointer sym 8
byte2)
    , onContinue :: bak -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m ()
onContinue = \bak
bak LLVMPtr sym 8
byte1 LLVMPtr sym 8
byte2 -> IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
        -- Add assumptions that both bytes were nonzero
        SymExpr sym BaseBoolType
prevByte1WasNonNull <- 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
byte1
        SymExpr sym BaseBoolType
prevByte2WasNonNull <- 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
byte2
        ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
WI.getCurrentProgramLoc sym
sym
        let assump1 :: CrucibleAssumption (SymExpr sym)
assump1 = 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
prevByte1WasNonNull
        let assump2 :: CrucibleAssumption (SymExpr sym)
assump2 = 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
prevByte2WasNonNull
        bak -> CrucibleAssumption (SymExpr sym) -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
LCB.addAssumption bak
bak CrucibleAssumption (SymExpr sym)
assump1
        bak -> CrucibleAssumption (SymExpr sym) -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
LCB.addAssumption bak
bak CrucibleAssumption (SymExpr sym)
assump2
    }

---------------------------------------------------------------------
-- ** 'BytesChecker'

-- | Compute a result from two symbolic bytes, and check if loading should
-- continue to the next pair of bytes.
--
-- Used to compare two byte streams simultaneously, e.g., for 'strcmp'.
--
-- Like 'ByteChecker', but for two bytes (usually from different strings) at
-- once.
newtype BytesChecker m sym bak a b
  = BytesChecker
      { forall (m :: Type -> Type) sym bak a b.
BytesChecker m sym bak a b
-> bak
-> a
-> LLVMPtr sym 8
-> LLVMPtr sym 8
-> m (ControlFlow a b)
runBytesChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }

-- | 'BytesChecker' for adding a maximum byte length.
withMaxBytes ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  Functor m =>
  -- | Maximum number of bytes to compare
  Integer ->
  -- | What to do when the maximum is reached
  (bak -> a -> m b) ->
  BytesChecker m sym bak a b ->
  BytesChecker m sym bak (a, Integer) b
withMaxBytes :: forall (m :: Type -> Type) sym bak a b.
(MonadIO m, HasCallStack, IsSymBackend sym bak, Functor m) =>
Integer
-> (bak -> a -> m b)
-> BytesChecker m sym bak a b
-> BytesChecker m sym bak (a, Integer) b
withMaxBytes Integer
limit bak -> a -> m b
done BytesChecker m sym bak a b
checker =
  (bak
 -> (a, Integer)
 -> LLVMPtr sym 8
 -> LLVMPtr sym 8
 -> m (ControlFlow (a, Integer) b))
-> BytesChecker m sym bak (a, Integer) b
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> BytesChecker m sym bak a b
BytesChecker ((bak
  -> (a, Integer)
  -> LLVMPtr sym 8
  -> LLVMPtr sym 8
  -> m (ControlFlow (a, Integer) b))
 -> BytesChecker m sym bak (a, Integer) b)
-> (bak
    -> (a, Integer)
    -> LLVMPtr sym 8
    -> LLVMPtr sym 8
    -> m (ControlFlow (a, Integer) b))
-> BytesChecker m sym bak (a, Integer) b
forall a b. (a -> b) -> a -> b
$ \bak
bak (a
acc, Integer
i) LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr ->
    BytesChecker m sym bak a b
-> bak
-> a
-> LLVMPtr sym 8
-> LLVMPtr sym 8
-> m (ControlFlow a b)
forall (m :: Type -> Type) sym bak a b.
BytesChecker m sym bak a b
-> bak
-> a
-> LLVMPtr sym 8
-> LLVMPtr sym 8
-> m (ControlFlow a b)
runBytesChecker BytesChecker m sym bak a b
checker bak
bak a
acc LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr m (ControlFlow a b)
-> (ControlFlow a b -> m (ControlFlow (a, Integer) b))
-> m (ControlFlow (a, Integer) 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
r -> ControlFlow (a, Integer) b -> m (ControlFlow (a, Integer) b)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (b -> ControlFlow (a, Integer) b
forall a b. b -> ControlFlow a b
Break b
r)
        Continue a
r ->
          if Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
limit
          then b -> ControlFlow (a, Integer) b
forall a b. b -> ControlFlow a b
Break (b -> ControlFlow (a, Integer) b)
-> m b -> m (ControlFlow (a, Integer) b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> bak -> a -> m b
done bak
bak a
r
          else ControlFlow (a, Integer) b -> m (ControlFlow (a, Integer) b)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((a, Integer) -> ControlFlow (a, Integer) b
forall a b. a -> ControlFlow a b
Continue (a
r, Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))

-- ** 'loadTwoBytes'

-- | Load sequences of bytes from two pointers simultaneously.
--
-- Used to implement 'strcmp'. Similar to 'loadBytes' but operates on two byte streams.
loadTwoBytes ::
  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 ->
  -- | First pointer to load from
  Mem.LLVMPtr sym wptr ->
  -- | Second pointer to load from
  Mem.LLVMPtr sym wptr ->
  -- | How to load a byte from each memory location
  BytesLoader m sym bak wptr ->
  -- | How to check if we should continue loading the next bytes
  BytesChecker m sym bak a b ->
  m b
loadTwoBytes :: 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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
loadTwoBytes bak
bak MemImpl sym
mem = a
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker 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 ->
    Mem.LLVMPtr sym wptr ->
    BytesLoader m sym bak wptr ->
    BytesChecker m sym bak a b ->
    m b
  go :: a
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
go a
acc LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2 BytesLoader m sym bak wptr
loader BytesChecker m sym bak a b
checker = do
    (LLVMPointer sym 8
byte1, LLVMPointer sym 8
byte2) <- BytesLoader m sym bak wptr
-> bak
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> m (LLVMPtr sym 8, LLVMPtr sym 8)
forall (m :: Type -> Type) sym bak (wptr :: Natural).
BytesLoader m sym bak wptr
-> bak
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> m (LLVMPtr sym 8, LLVMPtr sym 8)
runBytesLoader BytesLoader m sym bak wptr
loader bak
bak LLVMPtr sym wptr
ptr1 LLVMPtr sym wptr
ptr2
    BytesChecker m sym bak a b
-> bak
-> a
-> LLVMPtr sym 8
-> LLVMPtr sym 8
-> m (ControlFlow a b)
forall (m :: Type -> Type) sym bak a b.
BytesChecker m sym bak a b
-> bak
-> a
-> LLVMPtr sym 8
-> LLVMPtr sym 8
-> m (ControlFlow a b)
runBytesChecker BytesChecker m sym bak a b
checker bak
bak a
acc LLVMPtr sym 8
LLVMPointer sym 8
byte1 LLVMPtr sym 8
LLVMPointer sym 8
byte2 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
          -- Let the loader add any assumptions it needs (e.g., non-null for strcmp)
          BytesLoader m sym bak wptr
-> bak -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m ()
forall (m :: Type -> Type) sym bak (wptr :: Natural).
BytesLoader m sym bak wptr
-> bak -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m ()
onContinue BytesLoader m sym bak wptr
loader bak
bak LLVMPtr sym 8
LLVMPointer sym 8
byte1 LLVMPtr sym 8
LLVMPointer sym 8
byte2

          LLVMPointer sym wptr
ptr1' <- 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
ptr1 (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)
          LLVMPointer sym wptr
ptr2' <- 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
ptr2 (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
-> LLVMPtr sym wptr
-> BytesLoader m sym bak wptr
-> BytesChecker m sym bak a b
-> m b
go a
acc' LLVMPtr sym wptr
LLVMPointer sym wptr
ptr1' LLVMPtr sym wptr
LLVMPointer sym wptr
ptr2' BytesLoader m sym bak wptr
loader BytesChecker m sym bak a b
checker

---------------------------------------------------------------------
-- ** BytesCheckers for string comparison

-- Helper, not exported
-- Common logic for comparing two bytes after null-terminator checking.
-- Returns Nothing if bytes are equal (should continue), or Just result if different.
compareBytesForStrings ::
  MonadIO m =>
  LCB.IsSymBackend sym bak =>
  bak ->
  WI.SymBV sym 8 ->
  WI.SymBV sym 8 ->
  m (Maybe (WI.SymBV sym 32))
compareBytesForStrings :: forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak -> SymBV sym 8 -> SymBV sym 8 -> m (Maybe (SymBV sym 32))
compareBytesForStrings bak
bak SymBV sym 8
byte1 SymBV sym 8
byte2 = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  let i32 :: NatRepr 32
i32 = forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32
  SymExpr sym BaseBoolType
eq <- 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 -> SymBV sym 8 -> SymBV sym 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 SymBV sym 8
byte1 SymBV sym 8
byte2)
  case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
WI.asConstantPred SymExpr sym BaseBoolType
eq of
    Just Bool
False -> do
      SymExpr sym BaseBoolType
lt <- 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 -> SymBV sym 8 -> SymBV sym 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.bvUlt sym
sym SymBV sym 8
byte1 SymBV sym 8
byte2)
      SymBV sym 32
negOne <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 32
i32 (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
i32 Integer
-1))
      SymBV sym 32
one <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> IO (SymBV sym 32)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym NatRepr 32
i32)
      SymBV sym 32
result <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymBV sym 32
-> SymBV sym 32
-> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym SymExpr sym BaseBoolType
lt SymBV sym 32
negOne SymBV sym 32
one)
      Maybe (SymBV sym 32) -> m (Maybe (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> Maybe (SymBV sym 32)
forall a. a -> Maybe a
Just SymBV sym 32
result)
    Maybe Bool
_ -> Maybe (SymBV sym 32) -> m (Maybe (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (SymBV sym 32)
forall a. Maybe a
Nothing

-- Helper, not exported
-- Common logic for handling null terminator cases in string comparison.
-- Returns Nothing if bytes are equal (should continue), or Just result if different or at null terminator.
handleNullTerminators ::
  MonadIO m =>
  LCB.IsSymBackend sym bak =>
  bak ->
  WI.SymBV sym 32 ->
  Bool ->
  Bool ->
  WI.SymBV sym 8 ->
  WI.SymBV sym 8 ->
  m (Maybe (WI.SymBV sym 32))
handleNullTerminators :: forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak
-> SymBV sym 32
-> Bool
-> Bool
-> SymBV sym 8
-> SymBV sym 8
-> m (Maybe (SymBV sym 32))
handleNullTerminators bak
bak SymBV sym 32
bothNullResult Bool
isNull1 Bool
isNull2 SymBV sym 8
byte1 SymBV sym 8
byte2 = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
  let i32 :: NatRepr 32
i32 = forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32
  case (Bool
isNull1, Bool
isNull2) of
    (Bool
True, Bool
True) -> Maybe (SymBV sym 32) -> m (Maybe (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> Maybe (SymBV sym 32)
forall a. a -> Maybe a
Just SymBV sym 32
bothNullResult)
    (Bool
True, Bool
False) -> do
      SymBV sym 32
negOne <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 32
i32 (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
i32 Integer
-1))
      Maybe (SymBV sym 32) -> m (Maybe (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> Maybe (SymBV sym 32)
forall a. a -> Maybe a
Just SymBV sym 32
negOne)
    (Bool
False, Bool
True) -> do
      SymBV sym 32
one <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> IO (SymBV sym 32)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym NatRepr 32
i32)
      Maybe (SymBV sym 32) -> m (Maybe (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> Maybe (SymBV sym 32)
forall a. a -> Maybe a
Just SymBV sym 32
one)
    (Bool
False, Bool
False) -> bak -> SymBV sym 8 -> SymBV sym 8 -> m (Maybe (SymBV sym 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak -> SymBV sym 8 -> SymBV sym 8 -> m (Maybe (SymBV sym 32))
compareBytesForStrings bak
bak SymBV sym 8
byte1 SymBV sym 8
byte2

-- | 'BytesChecker' for comparing concrete strings.
--
-- Stops when either string has a concrete null terminator.
fullyConcreteNullTerminatedStrings ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)
fullyConcreteNullTerminatedStrings :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
fullyConcreteNullTerminatedStrings =
  (bak
 -> SymBV sym 32
 -> LLVMPtr sym 8
 -> LLVMPtr sym 8
 -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> BytesChecker m sym bak a b
BytesChecker ((bak
  -> SymBV sym 32
  -> LLVMPtr sym 8
  -> LLVMPtr sym 8
  -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
 -> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32))
-> (bak
    -> SymBV sym 32
    -> LLVMPtr sym 8
    -> LLVMPtr sym 8
    -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ \bak
bak SymBV sym 32
acc LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr -> do
    SymExpr sym (BaseBVType 8)
byte1 <- 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
byte1Ptr)
    SymExpr sym (BaseBVType 8)
byte2 <- 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
byte2Ptr)
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak
    let i32 :: NatRepr 32
i32 = forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32

    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)
byte1, 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)
byte2) of
      (Just Integer
0, Just Integer
0) -> ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
acc)
      (Just Integer
0, Just Integer
_) -> do
        SymBV sym 32
negOne <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 32
i32 (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
i32 Integer
-1))
        ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
negOne)
      (Just Integer
_, Just Integer
0) -> do
        SymBV sym 32
one <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> IO (SymBV sym 32)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym NatRepr 32
i32)
        ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
one)
      (Just Integer
c1, Just Integer
c2) | Integer
c1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
c2 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. a -> ControlFlow a b
Continue SymBV sym 32
acc)
      (Just Integer
c1, Just Integer
c2) -> do
        if Integer
c1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
c2
          then do
            SymBV sym 32
negOne <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr 32
i32 (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
i32 Integer
-1))
            ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
negOne)
          else do
            SymBV sym 32
one <- IO (SymBV sym 32) -> m (SymBV sym 32)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> IO (SymBV sym 32)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvOne sym
sym NatRepr 32
i32)
            ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
one)
      (Maybe Integer, Maybe Integer)
_ -> do
        let msg :: String
msg = String
"Symbolic value encountered when comparing strings"
        IO (ControlFlow (SymBV sym 32) (SymBV sym 32))
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> SimErrorReason -> IO (ControlFlow (SymBV sym 32) (SymBV sym 32))
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))

-- | 'BytesChecker' for comparing strings with concrete null terminators.
--
-- Stops when either string has a concrete null terminator.
concretelyNullTerminatedStrings ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)
concretelyNullTerminatedStrings :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
concretelyNullTerminatedStrings =
  (bak
 -> SymBV sym 32
 -> LLVMPtr sym 8
 -> LLVMPtr sym 8
 -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> BytesChecker m sym bak a b
BytesChecker ((bak
  -> SymBV sym 32
  -> LLVMPtr sym 8
  -> LLVMPtr sym 8
  -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
 -> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32))
-> (bak
    -> SymBV sym 32
    -> LLVMPtr sym 8
    -> LLVMPtr sym 8
    -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ \bak
bak SymBV sym 32
acc LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr -> do
    SymExpr sym (BaseBVType 8)
byte1 <- 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
byte1Ptr)
    SymExpr sym (BaseBVType 8)
byte2 <- 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
byte2Ptr)

    let isNull1 :: Bool
isNull1 = (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)
byte1) Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
    let isNull2 :: Bool
isNull2 = (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)
byte2) Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0

    bak
-> SymBV sym 32
-> Bool
-> Bool
-> SymExpr sym (BaseBVType 8)
-> SymExpr sym (BaseBVType 8)
-> m (Maybe (SymBV sym 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak
-> SymBV sym 32
-> Bool
-> Bool
-> SymBV sym 8
-> SymBV sym 8
-> m (Maybe (SymBV sym 32))
handleNullTerminators bak
bak SymBV sym 32
acc Bool
isNull1 Bool
isNull2 SymExpr sym (BaseBVType 8)
byte1 SymExpr sym (BaseBVType 8)
byte2 m (Maybe (SymBV sym 32))
-> (Maybe (SymBV sym 32)
    -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
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
      Just SymBV sym 32
result -> ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
result)
      Maybe (SymBV sym 32)
Nothing -> ControlFlow (SymBV sym 32) (SymBV sym 32)
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow (SymBV sym 32) (SymBV sym 32)
forall a b. a -> ControlFlow a b
Continue SymBV sym 32
acc)

-- | 'BytesChecker' for comparing strings with provably null terminators.
--
-- Stops when either string is provably null-terminated.
provablyNullTerminatedStrings ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  sym ~ WEB.ExprBuilder scope st fs =>
  bak ~ LCBO.OnlineBackend solver scope st fs =>
  WPO.OnlineSolver solver =>
  BytesChecker m sym bak (WI.SymBV sym 32) (WI.SymBV sym 32)
provablyNullTerminatedStrings :: 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) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
provablyNullTerminatedStrings =
  (bak
 -> SymBV sym 32
 -> LLVMPtr sym 8
 -> LLVMPtr sym 8
 -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> BytesChecker m sym bak a b
BytesChecker ((bak
  -> SymBV sym 32
  -> LLVMPtr sym 8
  -> LLVMPtr sym 8
  -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
 -> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32))
-> (bak
    -> SymBV sym 32
    -> LLVMPtr sym 8
    -> LLVMPtr sym 8
    -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ \bak
bak SymBV sym 32
acc LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr -> IO (ControlFlow (SymBV sym 32) (SymBV sym 32))
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ControlFlow (SymBV sym 32) (SymBV sym 32))
 -> m (ControlFlow (SymBV sym 32) (SymBV sym 32)))
-> IO (ControlFlow (SymBV sym 32) (SymBV sym 32))
-> m (ControlFlow (SymBV sym 32) (SymBV sym 32))
forall a b. (a -> b) -> a -> b
$ do
    SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte1 <- bak
-> LLVMPtr (ExprBuilder scope st fs) 8
-> IO (SymExpr (ExprBuilder scope st fs) (BaseBVType 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
byte1Ptr
    SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte2 <- bak
-> LLVMPtr (ExprBuilder scope st fs) 8
-> IO (SymExpr (ExprBuilder scope st fs) (BaseBVType 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
byte2Ptr
    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
isNull1 <- bak
-> ExprBuilder scope st fs
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> IO Bool
forall sym bak scope (st :: Type -> Type) fs solver.
(HasCallStack, IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak -> sym -> SymBV sym 8 -> IO Bool
isProvablyNullTerminator bak
bak ExprBuilder scope st fs
sym SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte1
    Bool
isNull2 <- bak
-> ExprBuilder scope st fs
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> IO Bool
forall sym bak scope (st :: Type -> Type) fs solver.
(HasCallStack, IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 bak ~ OnlineBackend solver scope st fs, OnlineSolver solver) =>
bak -> sym -> SymBV sym 8 -> IO Bool
isProvablyNullTerminator bak
bak ExprBuilder scope st fs
sym SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte2

    bak
-> SymBV (ExprBuilder scope st fs) 32
-> Bool
-> Bool
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
-> IO (Maybe (SymBV (ExprBuilder scope st fs) 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak
-> SymBV sym 32
-> Bool
-> Bool
-> SymBV sym 8
-> SymBV sym 8
-> m (Maybe (SymBV sym 32))
handleNullTerminators bak
bak SymBV sym 32
SymBV (ExprBuilder scope st fs) 32
acc Bool
isNull1 Bool
isNull2 SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte1 SymExpr (ExprBuilder scope st fs) (BaseBVType 8)
byte2 IO (Maybe (Expr scope (BaseBVType 32)))
-> (Maybe (Expr scope (BaseBVType 32))
    -> IO
         (ControlFlow
            (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))))
-> IO
     (ControlFlow
        (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32)))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Expr scope (BaseBVType 32)
result -> ControlFlow
  (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
-> IO
     (ControlFlow
        (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Expr scope (BaseBVType 32)
-> ControlFlow
     (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
forall a b. b -> ControlFlow a b
Break Expr scope (BaseBVType 32)
result)
      Maybe (Expr scope (BaseBVType 32))
Nothing -> ControlFlow
  (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
-> IO
     (ControlFlow
        (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Expr scope (BaseBVType 32)
-> ControlFlow
     (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
forall a b. a -> ControlFlow a b
Continue Expr scope (BaseBVType 32)
SymBV sym 32
acc)

-- | 'BytesChecker' for comparing strings with concrete null terminators
-- up to a maximum length.
--
-- Combines null-terminator checking (like strcmp) with length bounding
-- (like memcmp). Used for strncmp.
--
-- The accumulator is a pair of the comparison result so far and the current index.
lengthBoundedStringComparison ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  Integer ->
  BytesChecker m sym bak (WI.SymBV sym 32, Integer) (WI.SymBV sym 32)
lengthBoundedStringComparison :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
Integer
-> BytesChecker m sym bak (SymBV sym 32, Integer) (SymBV sym 32)
lengthBoundedStringComparison Integer
maxLen =
  let onMaxBytes :: p -> a -> f a
onMaxBytes p
_bak a
zero = a -> f a
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
zero
  in Integer
-> (bak
    -> SymExpr sym (BaseBVType 32) -> m (SymExpr sym (BaseBVType 32)))
-> BytesChecker
     m
     sym
     bak
     (SymExpr sym (BaseBVType 32))
     (SymExpr sym (BaseBVType 32))
-> BytesChecker
     m
     sym
     bak
     (SymExpr sym (BaseBVType 32), Integer)
     (SymExpr sym (BaseBVType 32))
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, HasCallStack, IsSymBackend sym bak, Functor m) =>
Integer
-> (bak -> a -> m b)
-> BytesChecker m sym bak a b
-> BytesChecker m sym bak (a, Integer) b
withMaxBytes Integer
maxLen bak
-> SymExpr sym (BaseBVType 32) -> m (SymExpr sym (BaseBVType 32))
forall {f :: Type -> Type} {p} {a}. Applicative f => p -> a -> f a
onMaxBytes BytesChecker
  m
  sym
  bak
  (SymExpr sym (BaseBVType 32))
  (SymExpr sym (BaseBVType 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
concretelyNullTerminatedStrings

-- | 'BytesChecker' for comparing strings with provably null terminators
-- up to a maximum length.
--
-- Combines provably null-terminator checking with length bounding.
--
-- The accumulator is a pair of the comparison result so far and the current index.
lengthBoundedProvablyNullTerminatedStringComparison ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  sym ~ WEB.ExprBuilder scope st fs =>
  bak ~ LCBO.OnlineBackend solver scope st fs =>
  WPO.OnlineSolver solver =>
  Integer ->
  BytesChecker m sym bak (WI.SymBV sym 32, Integer) (WI.SymBV sym 32)
lengthBoundedProvablyNullTerminatedStringComparison :: 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) =>
Integer
-> BytesChecker m sym bak (SymBV sym 32, Integer) (SymBV sym 32)
lengthBoundedProvablyNullTerminatedStringComparison Integer
maxLen =
  let onMaxBytes :: p -> a -> f a
onMaxBytes p
_bak a
zero = a -> f a
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
zero
  in Integer
-> (bak
    -> Expr scope (BaseBVType 32) -> m (Expr scope (BaseBVType 32)))
-> BytesChecker
     m sym bak (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
-> BytesChecker
     m
     sym
     bak
     (Expr scope (BaseBVType 32), Integer)
     (Expr scope (BaseBVType 32))
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, HasCallStack, IsSymBackend sym bak, Functor m) =>
Integer
-> (bak -> a -> m b)
-> BytesChecker m sym bak a b
-> BytesChecker m sym bak (a, Integer) b
withMaxBytes Integer
maxLen bak -> Expr scope (BaseBVType 32) -> m (Expr scope (BaseBVType 32))
forall {f :: Type -> Type} {p} {a}. Applicative f => p -> a -> f a
onMaxBytes BytesChecker
  m sym bak (Expr scope (BaseBVType 32)) (Expr scope (BaseBVType 32))
BytesChecker
  m
  sym
  bak
  (SymExpr sym (BaseBVType 32))
  (SymExpr sym (BaseBVType 32))
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) =>
BytesChecker m sym bak (SymBV sym 32) (SymBV sym 32)
provablyNullTerminatedStrings

---------------------------------------------------------------------
-- ** BytesCheckers for length-bounded comparison

-- | 'BytesChecker' for comparing two bytes without length bounds.
--
-- Stops when bytes differ, otherwise continues indefinitely.
simpleByteComparison ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  BytesChecker m sym bak () (WI.SymBV sym 32)
simpleByteComparison :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak () (SymBV sym 32)
simpleByteComparison =
  (bak
 -> ()
 -> LLVMPtr sym 8
 -> LLVMPtr sym 8
 -> m (ControlFlow () (SymBV sym 32)))
-> BytesChecker m sym bak () (SymBV sym 32)
forall (m :: Type -> Type) sym bak a b.
(bak -> a -> LLVMPtr sym 8 -> LLVMPtr sym 8 -> m (ControlFlow a b))
-> BytesChecker m sym bak a b
BytesChecker ((bak
  -> ()
  -> LLVMPtr sym 8
  -> LLVMPtr sym 8
  -> m (ControlFlow () (SymBV sym 32)))
 -> BytesChecker m sym bak () (SymBV sym 32))
-> (bak
    -> ()
    -> LLVMPtr sym 8
    -> LLVMPtr sym 8
    -> m (ControlFlow () (SymBV sym 32)))
-> BytesChecker m sym bak () (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ \bak
bak () LLVMPtr sym 8
byte1Ptr LLVMPtr sym 8
byte2Ptr -> do
    SymExpr sym (BaseBVType 8)
byte1 <- 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
byte1Ptr)
    SymExpr sym (BaseBVType 8)
byte2 <- 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
byte2Ptr)
    bak
-> SymExpr sym (BaseBVType 8)
-> SymExpr sym (BaseBVType 8)
-> m (Maybe (SymBV sym 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, IsSymBackend sym bak) =>
bak -> SymBV sym 8 -> SymBV sym 8 -> m (Maybe (SymBV sym 32))
compareBytesForStrings bak
bak SymExpr sym (BaseBVType 8)
byte1 SymExpr sym (BaseBVType 8)
byte2 m (Maybe (SymBV sym 32))
-> (Maybe (SymBV sym 32) -> m (ControlFlow () (SymBV sym 32)))
-> m (ControlFlow () (SymBV sym 32))
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
      Just SymBV sym 32
result -> ControlFlow () (SymBV sym 32) -> m (ControlFlow () (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymBV sym 32 -> ControlFlow () (SymBV sym 32)
forall a b. b -> ControlFlow a b
Break SymBV sym 32
result)
      Maybe (SymBV sym 32)
Nothing -> ControlFlow () (SymBV sym 32) -> m (ControlFlow () (SymBV sym 32))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (() -> ControlFlow () (SymBV sym 32)
forall a b. a -> ControlFlow a b
Continue ())

-- | 'BytesChecker' for comparing memory regions with a concrete length bound.
--
-- The accumulator is a pair of unit and the current index. Stops when the index reaches the
-- maximum length, or when bytes differ.
--
-- Returns:
-- * 0 if all bytes up to the length are equal
-- * A negative value if the first differing byte in the first region is less
-- * A positive value if the first differing byte in the first region is greater
lengthBoundedByteComparison ::
  MonadIO m =>
  GHC.HasCallStack =>
  LCB.IsSymBackend sym bak =>
  -- | Maximum length
  Integer ->
  BytesChecker m sym bak ((), Integer) (WI.SymBV sym 32)
lengthBoundedByteComparison :: forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
Integer -> BytesChecker m sym bak ((), Integer) (SymBV sym 32)
lengthBoundedByteComparison Integer
maxLen =
  let onMaxBytes :: bak -> () -> m (SymExpr sym (BaseBVType 32))
onMaxBytes bak
bak () = IO (SymExpr sym (BaseBVType 32)) -> m (SymExpr sym (BaseBVType 32))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr 32 -> IO (SymExpr sym (BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
WI.bvZero (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
LCB.backendGetSym bak
bak) (forall (n :: Natural). KnownNat n => NatRepr n
DPN.knownNat @32))
  in Integer
-> (bak -> () -> m (SymExpr sym (BaseBVType 32)))
-> BytesChecker m sym bak () (SymExpr sym (BaseBVType 32))
-> BytesChecker
     m sym bak ((), Integer) (SymExpr sym (BaseBVType 32))
forall (m :: Type -> Type) sym bak a b.
(MonadIO m, HasCallStack, IsSymBackend sym bak, Functor m) =>
Integer
-> (bak -> a -> m b)
-> BytesChecker m sym bak a b
-> BytesChecker m sym bak (a, Integer) b
withMaxBytes Integer
maxLen bak -> () -> m (SymExpr sym (BaseBVType 32))
forall {m :: Type -> Type} {sym} {bak}.
(MonadIO m, IsExprBuilder sym, HasSymInterface sym bak) =>
bak -> () -> m (SymExpr sym (BaseBVType 32))
onMaxBytes BytesChecker m sym bak () (SymExpr sym (BaseBVType 32))
forall (m :: Type -> Type) sym bak.
(MonadIO m, HasCallStack, IsSymBackend sym bak) =>
BytesChecker m sym bak () (SymBV sym 32)
simpleByteComparison