-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.String
-- Description      : Override definitions for C @string.h@ functions
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Galois, Inc. <crux@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Libc.String
  ( -- * @string.h@ overrides
    stringOverrides
    -- * Override declarations
  , llvmMemcpyOverride
  , llvmMemcpyChkOverride
  , llvmMemmoveOverride
  , llvmMemsetOverride
  , llvmMemsetChkOverride
  , llvmMemcmpOverride
  , llvmStrlenOverride
  , llvmStrnlenOverride
  , llvmStrcpyOverride
  , llvmStrcmpOverride
  , llvmStrncmpOverride
  , llvmStrdupOverride
  , llvmStrndupOverride
    -- * Implementation functions
  , callMemcpy
  , callMemmove
  , callMemset
  , callMemcmp
  , callStrlen
  , callStrnlen
  , callStrcpy
  , callStrcmp
  , callStrncmp
  , callStrdup
  , callStrndup
  ) where

import           Control.Monad.IO.Class (liftIO)
import qualified Data.BitVector.Sized as BV
import           Lens.Micro ((^.), _1, _2, _3)

import           Data.Parameterized.Context ( pattern (:>), pattern Empty )
import qualified Data.Parameterized.Context as Ctx

import           What4.Interface
import           What4.ProgramLoc (plSourceLoc)

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.MemModel.Strings as CStr
import           Lang.Crucible.LLVM.QQ( llvmOvr )

import           Lang.Crucible.LLVM.Intrinsics.Common

-- | All @string.h@ overrides
stringOverrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
  , ?memOpts :: MemOptions ) =>
  [SomeLLVMOverride p sym ext]
stringOverrides :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stringOverrides =
  [ LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemcpyOverride
  , LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemcpyChkOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemmoveOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
  (LLVMPointerType wptr)
forall p sym ext (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemsetOverride
  , LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemsetChkOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
llvmMemcmpOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
llvmStrlenOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (BVType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (BVType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (BVType wptr)
llvmStrnlenOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmStrcpyOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (BVType 32)
llvmStrcmpOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
llvmStrncmpOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmStrdupOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmStrndupOverride
  ]

------------------------------------------------------------------------
-- ** Declarations

llvmMemcpyOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
           (EmptyCtx ::> LLVMPointerType wptr
                     ::> LLVMPointerType wptr
                     ::> BVType wptr)
           (LLVMPointerType wptr)
llvmMemcpyOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemcpyOverride =
  [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args ->
       do sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
          RegEntry sym (BVType 1)
volatile <- IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegEntry sym (BVType 1))
 -> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1)))
-> IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a b. (a -> b) -> a -> b
$ TypeRepr (BVType 1)
-> RegValue sym (BVType 1) -> RegEntry sym (BVType 1)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 1)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (RegValue sym (BVType 1) -> RegEntry sym (BVType 1))
-> IO (RegValue sym (BVType 1)) -> IO (RegEntry sym (BVType 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 1 -> IO (SymBV sym 1)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat
          CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  f
  x
-> Assignment
     f
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemcpy GlobalVar Mem
memOps)
                                (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> RegEntry sym (BVType 1)
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType 1)
volatile)
          LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym wptr
 -> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym (LLVMPointerType wptr)
 -> RegValue sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall a b. (a -> b) -> a -> b
$ Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1 -- return first argument
    )


llvmMemcpyChkOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr
                   ::> LLVMPointerType wptr
                   ::> BVType wptr
                   ::> BVType wptr)
         (LLVMPointerType wptr)
llvmMemcpyChkOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemcpyChkOverride =
  [llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
args ->
      do let args' :: Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args' = Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym (LLVMPointerType wptr)
-> Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> (Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1) Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> (Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_2) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> (Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (BVType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (BVType wptr))
-> RegEntry sym (BVType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
forall s t a b. Field3 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
  (RegEntry sym (BVType wptr))
_3)
         sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
         RegEntry sym (BVType 1)
volatile <- IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegEntry sym (BVType 1))
 -> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1)))
-> IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a b. (a -> b) -> a -> b
$ TypeRepr (BVType 1)
-> RegValue sym (BVType 1) -> RegEntry sym (BVType 1)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 1)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (RegValue sym (BVType 1) -> RegEntry sym (BVType 1))
-> IO (RegValue sym (BVType 1)) -> IO (RegEntry sym (BVType 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 1 -> IO (SymBV sym 1)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat
         CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  f
  x
-> Assignment
     f
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemcpy GlobalVar Mem
memOps)
                               (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args' Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> RegEntry sym (BVType 1)
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType 1)
volatile)
         LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym wptr
 -> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym (LLVMPointerType wptr)
 -> RegValue sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall a b. (a -> b) -> a -> b
$ Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1 -- return first argument
    )

llvmMemmoveOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> (LLVMPointerType wptr)
                   ::> (LLVMPointerType wptr)
                   ::> BVType wptr)
         (LLVMPointerType wptr)
llvmMemmoveOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemmoveOverride =
  [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args ->
      do sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
         RegEntry sym (BVType 1)
volatile <- IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (TypeRepr (BVType 1)
-> RegValue sym (BVType 1) -> RegEntry sym (BVType 1)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 1)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (RegValue sym (BVType 1) -> RegEntry sym (BVType 1))
-> IO (RegValue sym (BVType 1)) -> IO (RegEntry sym (BVType 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 1 -> IO (SymBV sym 1)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
         CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   ::> BVType 1)
  f
  x
-> Assignment
     f
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemmove GlobalVar Mem
memOps)
                               (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> RegEntry sym (BVType 1)
-> Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
       ::> BVType wptr)
      ::> BVType 1)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType 1)
volatile)
         LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym wptr
 -> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym (LLVMPointerType wptr)
 -> RegValue sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall a b. (a -> b) -> a -> b
$ Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1 -- return first argument
    )

llvmMemsetOverride :: forall p sym ext wptr.
     (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr
                   ::> BVType 32
                   ::> BVType wptr)
         (LLVMPointerType wptr)
llvmMemsetOverride :: forall p sym ext (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemsetOverride =
  [llvmOvr| i8* @memset( i8*, i32, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
args ->
      do sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
         LeqProof 9 wptr
LeqProof <- LeqProof 9 wptr
-> OverrideSim p sym ext rtp args' ret' (LeqProof 9 wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans @9 @16 @wptr LeqProof 9 16
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof LeqProof 16 wptr
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof)
         let dest :: RegEntry sym (LLVMPointerType wptr)
dest = Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1
         RegEntry sym (BVType 8)
val <- IO (RegEntry sym (BVType 8))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 8))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (TypeRepr (BVType 8)
-> RegValue sym (BVType 8) -> RegEntry sym (BVType 8)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 8)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (SymExpr sym ('BaseBVType 8) -> RegEntry sym (BVType 8))
-> IO (SymExpr sym ('BaseBVType 8)) -> IO (RegEntry sym (BVType 8))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr 8 -> SymBV sym 32 -> IO (SymExpr sym ('BaseBVType 8))
forall (r :: Natural) (w :: Natural).
(1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (BVType 32))
     (Assignment
        (RegEntry sym)
        (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
         ::> BVType wptr))
     (RegEntry sym (BVType 32))
-> RegEntry sym (BVType 32)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (BVType 32))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (BVType 32))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (BVType 32))
  (RegEntry sym (BVType 32))
_2)))
         let len :: RegEntry sym (BVType wptr)
len = Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (BVType wptr))
     (Assignment
        (RegEntry sym)
        (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
         ::> BVType wptr))
     (RegEntry sym (BVType wptr))
-> RegEntry sym (BVType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
forall s t a b. Field3 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
  (RegEntry sym (BVType wptr))
_3
         RegEntry sym (BVType 1)
volatile <- IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO
            (TypeRepr (BVType 1)
-> RegValue sym (BVType 1) -> RegEntry sym (BVType 1)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 1)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (SymExpr sym ('BaseBVType 1) -> RegEntry sym (BVType 1))
-> IO (SymExpr sym ('BaseBVType 1)) -> IO (RegEntry sym (BVType 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 1 -> IO (SymExpr sym ('BaseBVType 1))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
         GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemset GlobalVar Mem
memOps RegEntry sym (LLVMPointerType wptr)
dest RegEntry sym (BVType 8)
val RegEntry sym (BVType wptr)
len RegEntry sym (BVType 1)
volatile
         LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (LLVMPointerType wptr)
dest)
    )

llvmMemsetChkOverride
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr
                 ::> BVType 32
                 ::> BVType wptr
                 ::> BVType wptr)
         (LLVMPointerType wptr)
llvmMemsetChkOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
  (LLVMPointerType wptr)
llvmMemsetChkOverride =
  [llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
args ->
      do sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
         let dest :: RegEntry sym (LLVMPointerType wptr)
dest = Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (LLVMPointerType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (LLVMPointerType wptr))
-> RegEntry sym (LLVMPointerType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (LLVMPointerType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (LLVMPointerType wptr))
  (RegEntry sym (LLVMPointerType wptr))
_1
         RegEntry sym (BVType 8)
val <- IO (RegEntry sym (BVType 8))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 8))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO
              (TypeRepr (BVType 8)
-> RegValue sym (BVType 8) -> RegEntry sym (BVType 8)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 8)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (SymExpr sym ('BaseBVType 8) -> RegEntry sym (BVType 8))
-> IO (SymExpr sym ('BaseBVType 8)) -> IO (RegEntry sym (BVType 8))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr 8 -> SymBV sym 32 -> IO (SymExpr sym ('BaseBVType 8))
forall (r :: Natural) (w :: Natural).
(1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (BVType 32))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (BVType 32))
-> RegEntry sym (BVType 32)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (BVType 32))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType 32))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType 32))
  (RegEntry sym (BVType 32))
_2)))
         let len :: RegEntry sym (BVType wptr)
len = Assignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
argsAssignment
  (RegEntry sym)
  ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
    ::> BVType wptr)
   ::> BVType wptr)
-> Getting
     (RegEntry sym (BVType wptr))
     (Assignment
        (RegEntry sym)
        ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
          ::> BVType wptr)
         ::> BVType wptr))
     (RegEntry sym (BVType wptr))
-> RegEntry sym (BVType wptr)
forall s a. s -> Getting a s a -> a
^.Getting
  (RegEntry sym (BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
forall s t a b. Field3 s t a b => Lens s t a b
Lens
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (Assignment
     (RegEntry sym)
     ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
       ::> BVType wptr)
      ::> BVType wptr))
  (RegEntry sym (BVType wptr))
  (RegEntry sym (BVType wptr))
_3
         RegEntry sym (BVType 1)
volatile <- IO (RegEntry sym (BVType 1))
-> OverrideSim p sym ext rtp args' ret' (RegEntry sym (BVType 1))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO
            (TypeRepr (BVType 1)
-> RegValue sym (BVType 1) -> RegEntry sym (BVType 1)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr (BVType 1)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (SymExpr sym ('BaseBVType 1) -> RegEntry sym (BVType 1))
-> IO (SymExpr sym ('BaseBVType 1)) -> IO (RegEntry sym (BVType 1))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 1 -> IO (SymExpr sym ('BaseBVType 1))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
         GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemset GlobalVar Mem
memOps RegEntry sym (LLVMPointerType wptr)
dest RegEntry sym (BVType 8)
val RegEntry sym (BVType wptr)
len RegEntry sym (BVType 1)
volatile
         LLVMPointer sym wptr
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (LLVMPointerType wptr)
dest)
    )

llvmStrlenOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
llvmStrlenOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
llvmStrlenOverride =
  [llvmOvr| size_t @strlen( i8* ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args -> CurryAssignment
  (EmptyCtx ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType wptr)))
-> Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType wptr))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> LLVMPointerType wptr) f x
-> Assignment f (EmptyCtx ::> LLVMPointerType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrlen GlobalVar Mem
memOps) Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args)

llvmStrnlenOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr)
llvmStrnlenOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (BVType wptr)
llvmStrnlenOverride =
  [llvmOvr| size_t @strnlen( i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType wptr)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType wptr))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrnlen GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args)

llvmStrcpyOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr)
llvmStrcpyOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmStrcpyOverride =
  [llvmOvr| i8* @strcpy( i8*, i8* ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrcpy GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
args)

llvmStrdupOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr)
llvmStrdupOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmStrdupOverride =
  [llvmOvr| i8* @strdup( i8* ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args -> CurryAssignment
  (EmptyCtx ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> LLVMPointerType wptr) f x
-> Assignment f (EmptyCtx ::> LLVMPointerType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrdup GlobalVar Mem
memOps) Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args)

llvmStrndupOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr)
llvmStrndupOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmStrndupOverride =
  [llvmOvr| i8* @strndup( i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrndup GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args)

llvmMemcmpOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> BVType wptr) (BVType 32)
llvmMemcmpOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
llvmMemcmpOverride =
  [llvmOvr| i32 @memcmp( i8*, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args -> CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callMemcmp GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args)

llvmStrcmpOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (BVType 32)
llvmStrcmpOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (BVType 32)
llvmStrcmpOverride =
  [llvmOvr| i32 @strcmp( i8*, i8* ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrcmp GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
args)

llvmStrncmpOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> BVType wptr) (BVType 32)
llvmStrncmpOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType 32)
llvmStrncmpOverride =
  [llvmOvr| i32 @strncmp( i8*, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args -> CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrncmp GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args)

------------------------------------------------------------------------
-- ** Implementations

------------------------------------------------------------------------
-- *** Memory manipulation

callMemcpy
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType w)
  -> RegEntry sym (BVType 1)
  -> OverrideSim p sym ext r args ret ()
callMemcpy :: forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemcpy GlobalVar Mem
mvar
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
dest)
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
src)
           (RegEntry (BVRepr NatRepr n
w) RegValue sym (BVType w)
len)
           RegEntry sym (BVType 1)
_volatile =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret ())
 -> OverrideSim p sym ext r args ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
 -> OverrideSim p sym ext r args ret ())
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ((), RegValue sym Mem)
 -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      do MemImpl sym
mem' <- bak
-> NatRepr n
-> MemImpl sym
-> Bool
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym n
-> IO (MemImpl sym)
forall (w :: Natural) sym bak (wptr :: Natural).
(1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> NatRepr w
-> MemImpl sym
-> Bool
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> SymBV sym w
-> IO (MemImpl sym)
doMemcpy bak
bak NatRepr n
w RegValue sym Mem
MemImpl sym
mem Bool
True RegValue sym (LLVMPointerType wptr)
dest RegValue sym (LLVMPointerType wptr)
src RegValue sym (BVType w)
SymBV sym n
len
         ((), MemImpl sym) -> IO ((), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((), MemImpl sym
mem')

-- NB the only difference between memcpy and memove
-- is that memmove does not assert that the memory
-- ranges are disjoint.  The underlying operation
-- works correctly in both cases.
callMemmove
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType w)
  -> RegEntry sym (BVType 1)
  -> OverrideSim p sym ext r args ret ()
callMemmove :: forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemmove GlobalVar Mem
mvar
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
dest)
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
src)
           (RegEntry (BVRepr NatRepr n
w) RegValue sym (BVType w)
len)
           RegEntry sym (BVType 1)
_volatile =
  -- FIXME? add assertions about alignment
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret ())
 -> OverrideSim p sym ext r args ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
 -> OverrideSim p sym ext r args ret ())
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ((), RegValue sym Mem)
 -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      do MemImpl sym
mem' <- bak
-> NatRepr n
-> MemImpl sym
-> Bool
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym n
-> IO (MemImpl sym)
forall (w :: Natural) sym bak (wptr :: Natural).
(1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> NatRepr w
-> MemImpl sym
-> Bool
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> SymBV sym w
-> IO (MemImpl sym)
doMemcpy bak
bak NatRepr n
w RegValue sym Mem
MemImpl sym
mem Bool
False RegValue sym (LLVMPointerType wptr)
dest RegValue sym (LLVMPointerType wptr)
src RegValue sym (BVType w)
SymBV sym n
len
         ((), MemImpl sym) -> IO ((), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((), MemImpl sym
mem')

callMemset
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType 8)
  -> RegEntry sym (BVType w)
  -> RegEntry sym (BVType 1)
  -> OverrideSim p sym ext r args ret ()
callMemset :: forall sym (wptr :: Natural) (w :: Natural) p ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemset GlobalVar Mem
mvar
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
dest)
           (RegEntry sym (BVType 8) -> RegValue sym (BVType 8)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType 8)
val)
           (RegEntry (BVRepr NatRepr n
w) RegValue sym (BVType w)
len)
           RegEntry sym (BVType 1)
_volatile =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret ())
 -> OverrideSim p sym ext r args ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
 -> OverrideSim p sym ext r args ret ())
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ((), RegValue sym Mem)
 -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      do MemImpl sym
mem' <- bak
-> NatRepr n
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym 8
-> SymBV sym n
-> IO (MemImpl sym)
forall (w :: Natural) sym bak (wptr :: Natural).
(1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) =>
bak
-> NatRepr w
-> MemImpl sym
-> LLVMPtr sym wptr
-> SymBV sym 8
-> SymBV sym w
-> IO (MemImpl sym)
doMemset bak
bak NatRepr n
w RegValue sym Mem
MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
dest RegValue sym (BVType 8)
SymBV sym 8
val RegValue sym (BVType w)
SymBV sym n
len
         ((), MemImpl sym) -> IO ((), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((), MemImpl sym
mem')

------------------------------------------------------------------------
-- *** Strings

callStrlen
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrlen GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
strPtr) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
    IO (SymExpr sym ('BaseBVType wptr))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType wptr))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType wptr))
 -> OverrideSim
      p sym ext r args ret (SymExpr sym ('BaseBVType wptr)))
-> IO (SymExpr sym ('BaseBVType wptr))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> IO (SymExpr sym ('BaseBVType wptr))
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (SymBV sym wptr)
strLen bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
strPtr

callStrnlen
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrnlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrnlen GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
strPtr) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
bound) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
    IO (SymExpr sym ('BaseBVType wptr))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType wptr))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType wptr))
 -> OverrideSim
      p sym ext r args ret (SymExpr sym ('BaseBVType wptr)))
-> IO (SymExpr sym ('BaseBVType wptr))
-> OverrideSim
     p sym ext r args ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> SymExpr sym ('BaseBVType wptr)
-> IO (SymExpr sym ('BaseBVType wptr))
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)
CStr.strnlen bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
strPtr RegValue sym (BVType wptr)
SymExpr sym ('BaseBVType wptr)
bound

callStrcpy
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrcpy :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrcpy GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
dst) (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
src) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> do
      MemImpl sym
mem' <- IO (MemImpl sym) -> OverrideSim p sym ext r args ret (MemImpl sym)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym)
 -> OverrideSim p sym ext r args ret (MemImpl sym))
-> IO (MemImpl sym)
-> OverrideSim p sym ext r args ret (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> Maybe Int
-> IO (MemImpl sym)
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)
CStr.copyConcretelyNullTerminatedString bak
bak RegValue sym Mem
MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
dst RegValue sym (LLVMPointerType wptr)
src Maybe Int
forall a. Maybe a
Nothing
      (LLVMPointer sym wptr, MemImpl sym)
-> OverrideSim
     p sym ext r args ret (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> OverrideSim p sym ext r args ret a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (RegValue sym (LLVMPointerType wptr)
LLVMPointer sym wptr
dst, MemImpl sym
mem')

callStrdup
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrdup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrdup GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
src) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$ do
      let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
      Position
loc <- ProgramLoc -> Position
plSourceLoc (ProgramLoc -> Position) -> IO ProgramLoc -> IO Position
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
      let loc' :: String
loc' = String
"<strdup> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
loc
      bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> Maybe Int
-> String
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
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)
CStr.dupConcretelyNullTerminatedString bak
bak RegValue sym Mem
MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
src Maybe Int
forall a. Maybe a
Nothing String
loc' Alignment
noAlignment

callStrndup
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrndup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrndup GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
src) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
bound) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$ do
      let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
      Position
loc <- ProgramLoc -> Position
plSourceLoc (ProgramLoc -> Position) -> IO ProgramLoc -> IO Position
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
      let loc' :: String
loc' = String
"<strndup> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
loc
      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
<$> SymExpr sym (BaseBVType 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)
asBV RegValue sym (BVType wptr)
SymExpr sym (BaseBVType wptr)
bound of
        Maybe Integer
Nothing -> do
          let err :: SimErrorReason
err = String -> String -> SimErrorReason
AssertFailureSimError String
"`strndup` called with symbolic max length" String
""
          bak -> SimErrorReason -> IO (LLVMPointer sym wptr, MemImpl sym)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
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
-> RegValue sym (LLVMPointerType wptr)
-> Maybe Int
-> String
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
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)
CStr.dupConcretelyNullTerminatedString bak
bak RegValue sym Mem
MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
src Maybe Int
bound' String
loc' Alignment
noAlignment

callMemcmp
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callMemcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callMemcmp GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr1) (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr2) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
len) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
    IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType 32))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym wptr
-> IO (SymExpr sym ('BaseBVType 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
-> SymBV sym wptr
-> IO (SymBV sym 32)
CStr.memcmp bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
ptr1 RegValue sym (LLVMPointerType wptr)
ptr2 RegValue sym (BVType wptr)
SymBV sym wptr
len

callStrcmp
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrcmp GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr1) (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr2) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
    IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType 32))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> Maybe Int
-> IO (SymExpr sym ('BaseBVType 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)
CStr.cmpConcretelyNullTerminatedString bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
ptr1 RegValue sym (LLVMPointerType wptr)
ptr2 Maybe Int
forall a. Maybe a
Nothing

callStrncmp
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (BVType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrncmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrncmp GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr1) (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr2) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
len) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
    IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType 32))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym wptr
-> IO (SymExpr sym ('BaseBVType 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
-> SymBV sym wptr
-> IO (SymBV sym 32)
CStr.strncmp bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
ptr1 RegValue sym (LLVMPointerType wptr)
ptr2 RegValue sym (BVType wptr)
SymBV sym wptr
len