{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MagicHash #-}
{-# Language ConstraintKinds #-}
{-# Language DataKinds #-}
{-# Language ImplicitParams #-}
{-# Language LambdaCase #-}
{-# Language PatternSynonyms #-}
{-# Language QuasiQuotes #-}
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language ViewPatterns #-}
module Crux.LLVM.Overrides
  ( cruxLLVMOverrides
  , svCompOverrides
  , cbmcOverrides
  , ArchOk
  , TPtr
  ) where

import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BS8
import Control.Monad (when)
import Control.Monad.IO.Class(liftIO)
import GHC.Exts ( Proxy# )
import System.IO (hPutStrLn)
import qualified Data.Text as T

import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Context.Unsafe (Assignment)
import Data.Parameterized.Context(pattern Empty, pattern (:>), singleton)

import What4.ProgramLoc( Position(..), ProgramLoc(..) )
import What4.Symbol(userSymbol, emptySymbol, safeSymbol)
import What4.Interface
          (freshConstant, bvLit, bvAdd, asBV, predToBV,
          getCurrentProgramLoc, printSymExpr, arrayUpdate, bvIsNonzero)

import Lang.Crucible.Types
import Lang.Crucible.CFG.Core(GlobalVar)
import Lang.Crucible.Simulator.RegMap(regValue,RegValue,RegEntry)
import Lang.Crucible.Simulator.ExecutionTree( printHandle )
import Lang.Crucible.Simulator.OverrideSim
        ( getContext
        , readGlobal
        , writeGlobal
        , ovrWithBackend
        )
import Lang.Crucible.Simulator.SimError (SimErrorReason(..),SimError(..))
import Lang.Crucible.Backend
          ( IsSymInterface, IsSymBackend, addDurableAssertion
          , addAssumption, LabeledPred(..), CrucibleAssumption(..)
          , backendGetSym
          )
import Lang.Crucible.LLVM.QQ( llvmOvr )
import Lang.Crucible.LLVM.DataLayout
  (noAlignment)
import Lang.Crucible.LLVM.MemModel
  (Mem, LLVMPointerType, loadString, HasPtrWidth,
   doMalloc, AllocType(HeapAlloc), Mutability(Mutable),
   doArrayStore, doArrayConstStore, HasLLVMAnn,
   isAllocatedAlignedPointer, Mutability(..),
   pattern PtrWidth, doDumpMem, MemOptions
   )

import           Lang.Crucible.LLVM.TypeContext( TypeContext )
import           Lang.Crucible.LLVM.Intrinsics

import Lang.Crucible.LLVM.Extension ( ArchWidth )

import qualified Crux.Overrides as Crux
import Crux.Types

-- | This happens quite a lot, so just a shorter name
type ArchOk arch    = HasPtrWidth (ArchWidth arch)
type TPtr arch      = LLVMPointerType (ArchWidth arch)
type TBits n        = BVType n


cruxLLVMOverrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  [OverrideTemplate (personality sym) sym arch rtp l a]
cruxLLVMOverrides :: forall sym (wptr :: Natural) (arch :: LLVMArch)
       (personality :: * -> *) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> [OverrideTemplate (personality sym) sym arch rtp l a]
cruxLLVMOverrides Proxy# arch
arch =
  [ LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8 @crucible_int8_t( i8* ) |]
        (Proxy# arch
-> NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i16 @crucible_int16_t( i8* ) |]
        (Proxy# arch
-> NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @crucible_int32_t( i8* ) |]
        (Proxy# arch
-> NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @crucible_int64_t( i8* ) |]
        (Proxy# arch
-> NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8 @crucible_uint8_t( i8* ) |]
        (Proxy# arch
-> NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i16 @crucible_uint16_t( i8* ) |]
        (Proxy# arch
-> NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @crucible_uint32_t( i8* ) |]
        (Proxy# arch
-> NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @crucible_uint64_t( i8* ) |]
        (Proxy# arch
-> NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('FloatType 'SingleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| float @crucible_float( i8* ) |]
        (Proxy# arch
-> FloatInfoRepr 'SingleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'SingleFloat))
forall (arch :: LLVMArch) sym bak (fi :: FloatInfo)
       (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (FloatType fi))
fresh_float Proxy# arch
arch FloatInfoRepr 'SingleFloat
SingleFloatRepr)

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> LLVMPointerType wptr)
  ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> LLVMPointerType wptr)
   ('FloatType 'DoubleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> LLVMPointerType wptr)
     ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| double @crucible_double( i8* ) |]
        (Proxy# arch
-> FloatInfoRepr 'DoubleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'DoubleFloat))
forall (arch :: LLVMArch) sym bak (fi :: FloatInfo)
       (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (FloatType fi))
fresh_float Proxy# arch
arch FloatInfoRepr 'DoubleFloat
DoubleFloatRepr)

  , LLVMOverride
  (personality sym)
  sym
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   (LLVMPointerType wptr)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
     (LLVMPointerType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8* @crucible_string( i8*, size_t ) |]
        (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM personality sym LLVM (RegValue sym (TPtr arch))
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM personality sym ext (RegValue sym (TPtr arch))
fresh_str Proxy# arch
arch)

  , LLVMOverride
  (personality sym)
  sym
  (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
    ::> LLVMPointerType wptr)
   ::> 'BaseToType (BaseBVType 32))
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
     ::> LLVMPointerType wptr)
    ::> 'BaseToType (BaseBVType 32))
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
       ::> LLVMPointerType wptr)
      ::> 'BaseToType (BaseBVType 32))
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| void @crucible_assume( i8, i8*, i32 ) |]
        (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_assume Proxy# arch
arch)

  , LLVMOverride
  (personality sym)
  sym
  (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
    ::> LLVMPointerType wptr)
   ::> 'BaseToType (BaseBVType 32))
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
     ::> LLVMPointerType wptr)
    ::> 'BaseToType (BaseBVType 32))
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8))
       ::> LLVMPointerType wptr)
      ::> 'BaseToType (BaseBVType 32))
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| void @crucible_assert( i8, i8*, i32 ) |]
        (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_assert Proxy# arch
arch)

  , LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> 'BaseToType (BaseBVType 32))
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> 'BaseToType (BaseBVType 32))
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> 'BaseToType (BaseBVType 32))
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| void @crucible_print_uint32( i32 ) |]
        GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall bak.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall sym bak (personality :: * -> *) ext.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_print_uint32

  , LLVMOverride
  (personality sym)
  sym
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| void @crucible_havoc_memory( i8*, size_t ) |]
        (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> TBits (ArchWidth arch))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_havoc_memory Proxy# arch
arch)

  , LLVMOverride (personality sym) sym EmptyCtx 'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride (personality sym) sym EmptyCtx 'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride (personality sym) sym EmptyCtx 'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| void @crucible_dump_memory( ) |]
        (\GlobalVar Mem
mvar bak
_sym Assignment (RegEntry sym) EmptyCtx
_args ->
          do MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (personality sym) sym LLVM rtp 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
             Handle
h <- SimContext (personality sym) sym LLVM -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle (SimContext (personality sym) sym LLVM -> Handle)
-> OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (SimContext (personality sym) sym LLVM)
-> OverrideSim (personality sym) sym LLVM rtp args' ret' Handle
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim
  (personality sym)
  sym
  LLVM
  rtp
  args'
  ret'
  (SimContext (personality sym) sym LLVM)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
             IO () -> OverrideSim (personality sym) sym LLVM rtp args' ret' ()
forall a.
IO a -> OverrideSim (personality sym) sym LLVM rtp args' ret' a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Handle -> MemImpl sym -> IO ()
forall sym. IsExprBuilder sym => Handle -> MemImpl sym -> IO ()
doDumpMem Handle
h MemImpl sym
mem))
  ]


cbmcOverrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  [OverrideTemplate (personality sym) sym arch rtp l a]
cbmcOverrides :: forall sym (wptr :: Natural) (arch :: LLVMArch)
       (personality :: * -> *) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> [OverrideTemplate (personality sym) sym arch rtp l a]
cbmcOverrides Proxy# arch
arch =
  [ LLVMOverride
  (personality sym)
  sym
  (EmptyCtx ::> 'BaseToType (BaseBVType 32))
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   (EmptyCtx ::> 'BaseToType (BaseBVType 32))
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     (EmptyCtx ::> 'BaseToType (BaseBVType 32))
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| void @__CPROVER_assume( i32 ) |]
      GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall bak.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall sym bak (personality :: * -> *) ext.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
cprover_assume
  , LLVMOverride
  (personality sym)
  sym
  ((EmptyCtx ::> 'BaseToType (BaseBVType 32))
   ::> LLVMPointerType wptr)
  'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   ((EmptyCtx ::> 'BaseToType (BaseBVType 32))
    ::> LLVMPointerType wptr)
   'UnitType
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     ((EmptyCtx ::> 'BaseToType (BaseBVType 32))
      ::> LLVMPointerType wptr)
     'UnitType
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| void @__CPROVER_assert( i32, i8* ) |]
      (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> 'BaseToType (BaseBVType 32)) ::> TPtr arch)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> 'BaseToType (BaseBVType 32)) ::> TPtr arch)
-> OverM personality sym ext (RegValue sym 'UnitType)
cprover_assert Proxy# arch
arch)
  , LLVMOverride
  (personality sym)
  sym
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ('BaseToType (BaseBVType 1))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
     ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i1 @__CPROVER_r_ok( i8*, size_t ) |]
      (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 1)))
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM
     personality sym ext (RegValue sym ('BaseToType (BaseBVType 1)))
cprover_r_ok Proxy# arch
arch)
  , LLVMOverride
  (personality sym)
  sym
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym)
   sym
   ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ('BaseToType (BaseBVType 1))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym)
     sym
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
     ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i1 @__CPROVER_w_ok( i8*, size_t ) |]
      (Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 1)))
forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM
     personality sym ext (RegValue sym ('BaseToType (BaseBVType 1)))
cprover_w_ok Proxy# arch
arch)

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i1 @nondet_bool() |]
      (NatRepr 1
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 1)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i8 @nondet_char() |]
      (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i8 @nondet_uchar() |]
      (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i8 @nondet_uint8_t() |]
      (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i8 @nondet_int8_t() |]
      (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i16 @nondet_short() |]
      (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i16 @nondet_ushort() |]
      (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i16 @nondet_int16_t() |]
      (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i16 @nondet_uint16_t() |]
      (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_int() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_uint() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_int32_t() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_uint32_t() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i64 @nondet_int64_t() |]
      (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i64 @nondet_uint64_t() |]
      (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

    -- @nondet_long@ returns a `long`, so we need two overrides for
    -- @nondet_long@. Similarly for @nondet_ulong@.
    -- See Note [Overrides involving (unsigned) long] in
    -- crucible-llvm:Lang.Crucible.LLVM.Intrinsics.
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_long() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i64 @nondet_long() |]
      (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i32 @nondet_ulong() |]
      (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| i64 @nondet_ulong() |]
      (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))
  , LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
      [llvmOvr| size_t @nondet_size_t() |]
      (NatRepr wptr
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym (BVType wptr))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)

  , LLVMOverride
  (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| float @nondet_float() |]
        (FloatInfoRepr 'SingleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'SingleFloat))
forall sym bak (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymBackend sym bak =>
FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float FloatInfoRepr 'SingleFloat
SingleFloatRepr)

  , LLVMOverride
  (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| double @nondet_double() |]
        (FloatInfoRepr 'DoubleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'DoubleFloat))
forall sym bak (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymBackend sym bak =>
FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float FloatInfoRepr 'DoubleFloat
DoubleFloatRepr)

{-
  , basic_llvm_override $
      [llvmOvr| i8* @nondet_voidp() |]
      (sv_comp_fresh_bits ?ptrWidth)
-}
  ]


svCompOverrides ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  [OverrideTemplate (personality sym) sym arch rtp l a]
svCompOverrides :: forall sym (wptr :: Natural) (personality :: * -> *)
       (arch :: LLVMArch) rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
[OverrideTemplate (personality sym) sym arch rtp l a]
svCompOverrides =
  [ LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @__VERIFIER_nondet_longlong() |]
        (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

    -- loff_t is pretty Linux-specific, so we can't point to the C or POSIX
    -- standards for justification about what size it should be. The man page
    -- for lseek64 (https://linux.die.net/man/3/lseek64) is as close to a
    -- definitive reference for this as I can find, which says
    -- "The type loff_t is a 64-bit signed type".
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @__VERIFIER_nondet_loff_t() |]
        (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

    -- @__VERIFIER_nondet_ulong@ returns an `unsigned long`, so we need two
    -- overrides for @__VERIFIER_nondet_ulong@. Similarly for
    -- @__VERIFIER_nondet_long@. See Note [Overrides involving (unsigned) long]
    -- in crucible-llvm:Lang.Crucible.LLVM.Intrinsics.
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_ulong() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @__VERIFIER_nondet_ulong() |]
        (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_long() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 64))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i64 @__VERIFIER_nondet_long() |]
        (NatRepr 64
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 64)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_unsigned() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_u32() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_uint() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 32))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i32 @__VERIFIER_nondet_int() |]
        (NatRepr 32
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 32)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i16 @__VERIFIER_nondet_u16() |]
        (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i16 @__VERIFIER_nondet_ushort() |]
        (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 16))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i16 @__VERIFIER_nondet_short() |]
        (NatRepr 16
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 16)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8 @__VERIFIER_nondet_u8() |]
        (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8 @__VERIFIER_nondet_uchar() |]
        (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 8))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i8 @__VERIFIER_nondet_char() |]
        (NatRepr 8
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 8)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))

  , LLVMOverride
  (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('BaseToType (BaseBVType 1))
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| i1 @__VERIFIER_nondet_bool() |]
        (NatRepr 1
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('BaseToType (BaseBVType 1)))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1))

  , LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride (personality sym) sym EmptyCtx (BVType wptr)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| size_t @__VERIFIER_nondet_size_t() |]
        (NatRepr wptr
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym (BVType wptr))
forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)

  , LLVMOverride
  (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('FloatType 'SingleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| float @__VERIFIER_nondet_float() |]
        (FloatInfoRepr 'SingleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'SingleFloat))
forall sym bak (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymBackend sym bak =>
FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float FloatInfoRepr 'SingleFloat
SingleFloatRepr)

  , LLVMOverride
  (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override (LLVMOverride
   (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
 -> OverrideTemplate (personality sym) sym arch rtp l a)
-> LLVMOverride
     (personality sym) sym EmptyCtx ('FloatType 'DoubleFloat)
-> OverrideTemplate (personality sym) sym arch rtp l a
forall a b. (a -> b) -> a -> b
$
        [llvmOvr| double @__VERIFIER_nondet_double() |]
        (FloatInfoRepr 'DoubleFloat
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     (personality sym)
     sym
     LLVM
     rtp
     args'
     ret'
     (RegValue sym ('FloatType 'DoubleFloat))
forall sym bak (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymBackend sym bak =>
FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float FloatInfoRepr 'DoubleFloat
DoubleFloatRepr)
  ]

--------------------------------------------------------------------------------

lookupString ::
  ( IsSymInterface sym, HasLLVMAnn sym, ArchOk arch
  , ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  GlobalVar Mem -> RegEntry sym (TPtr arch) -> OverM personality sym ext String
lookupString :: forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
_ GlobalVar Mem
mvar RegEntry sym (TPtr arch)
ptr =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim (personality sym) sym ext r args ret String)
-> OverrideSim (personality sym) sym ext r args ret String
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 (personality sym) sym ext r args ret String)
 -> OverrideSim (personality sym) sym ext r args ret String)
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim (personality sym) sym ext r args ret String)
-> OverrideSim (personality sym) sym ext r args ret String
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    do MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (personality sym) 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
       [Word8]
bytes <- IO [Word8]
-> OverrideSim (personality sym) sym ext r args ret [Word8]
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (bak
-> MemImpl sym
-> LLVMPtr sym (ArchWidth arch)
-> Maybe Int
-> IO [Word8]
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
loadString bak
bak MemImpl sym
mem (RegEntry sym (TPtr arch) -> LLVMPtr sym (ArchWidth arch)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (TPtr arch)
ptr) Maybe Int
forall a. Maybe a
Nothing)
       String -> OverrideSim (personality sym) sym ext r args ret String
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> String
BS8.unpack ([Word8] -> ByteString
BS.pack [Word8]
bytes))

sv_comp_fresh_bits ::
  (IsSymBackend sym bak, 1 <= w) =>
  NatRepr w ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) EmptyCtx ->
  OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits :: forall sym bak (w :: Natural) (personality :: * -> *) ext.
(IsSymBackend sym bak, 1 <= w) =>
NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (BVType w))
sv_comp_fresh_bits NatRepr w
w GlobalVar Mem
_mvar bak
_bak Assignment (RegEntry sym) EmptyCtx
Empty = SolverSymbol
-> BaseTypeRepr ('BaseBVType w)
-> OverM
     personality sym ext (RegValue sym (BaseToType ('BaseBVType w)))
forall sym (ty :: BaseType) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr ty
-> OverM personality sym ext (RegValue sym (BaseToType ty))
Crux.mkFresh (String -> SolverSymbol
safeSymbol String
"X") (NatRepr w -> BaseTypeRepr ('BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)

sv_comp_fresh_float ::
  (IsSymBackend sym bak) =>
  FloatInfoRepr fi ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) EmptyCtx ->
  OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float :: forall sym bak (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymBackend sym bak =>
FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) EmptyCtx
-> OverM personality sym ext (RegValue sym (FloatType fi))
sv_comp_fresh_float FloatInfoRepr fi
fi GlobalVar Mem
_mvar bak
_bak Assignment (RegEntry sym) EmptyCtx
Empty = SolverSymbol
-> FloatInfoRepr fi
-> OverM personality sym ext (RegValue sym (FloatType fi))
forall sym (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> FloatInfoRepr fi
-> OverM personality sym ext (RegValue sym (FloatType fi))
Crux.mkFreshFloat (String -> SolverSymbol
safeSymbol String
"X") FloatInfoRepr fi
fi

fresh_bits ::
  ( ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w
  , ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  NatRepr w ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) ->
  OverM personality sym ext (RegValue sym (BVType w))
fresh_bits :: forall (arch :: LLVMArch) sym bak (w :: Natural)
       (personality :: * -> *) ext.
(ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w,
 ?memOpts::MemOptions) =>
Proxy# arch
-> NatRepr w
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (BVType w))
fresh_bits Proxy# arch
arch NatRepr w
w GlobalVar Mem
mvar bak
_ (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
pName) =
  do String
name <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pName
     SolverSymbol
-> BaseTypeRepr ('BaseBVType w)
-> OverM personality sym ext (RegValue sym (BVType w))
forall sym (ty :: BaseType) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> BaseTypeRepr ty
-> OverM personality sym ext (RegValue sym (BaseToType ty))
Crux.mkFresh (String -> SolverSymbol
safeSymbol String
name) (NatRepr w -> BaseTypeRepr ('BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)

fresh_float ::
  ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  FloatInfoRepr fi ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) ->
  OverM personality sym ext (RegValue sym (FloatType fi))
fresh_float :: forall (arch :: LLVMArch) sym bak (fi :: FloatInfo)
       (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> FloatInfoRepr fi
-> GlobalVar Mem
-> bak
-> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch)
-> OverM personality sym ext (RegValue sym (FloatType fi))
fresh_float Proxy# arch
arch FloatInfoRepr fi
fi GlobalVar Mem
mvar bak
_ (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
pName) =
  do String
name <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pName
     SolverSymbol
-> FloatInfoRepr fi
-> OverM personality sym ext (RegValue sym (FloatType fi))
forall sym (fi :: FloatInfo) (personality :: * -> *) ext.
IsSymInterface sym =>
SolverSymbol
-> FloatInfoRepr fi
-> OverM personality sym ext (RegValue sym (FloatType fi))
Crux.mkFreshFloat (String -> SolverSymbol
safeSymbol String
name) FloatInfoRepr fi
fi

fresh_str ::
  ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) ->
  OverM personality sym ext (RegValue sym (TPtr arch))
fresh_str :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM personality sym ext (RegValue sym (TPtr arch))
fresh_str Proxy# arch
arch GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
pName :> RegEntry sym tp
maxLen) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     String
name <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pName

     -- Compute the allocation length, which is the requested length plus one
     -- to hold the NUL terminator
     SymExpr sym (BaseBVType (ArchWidth arch))
one <- IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (BaseBVType (ArchWidth arch)))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType (ArchWidth arch)))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (SymExpr sym (BaseBVType (ArchWidth arch))))
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (BaseBVType (ArchWidth arch)))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr (ArchWidth arch)
-> BV (ArchWidth arch)
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth (NatRepr (ArchWidth arch) -> BV (ArchWidth arch)
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth)
     -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen)
     SymExpr sym (BaseBVType (ArchWidth arch))
len <- IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (BaseBVType (ArchWidth arch)))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType (ArchWidth arch)))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (SymExpr sym (BaseBVType (ArchWidth arch))))
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr sym (BaseBVType (ArchWidth arch)))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType (ArchWidth arch))
-> SymExpr sym (BaseBVType (ArchWidth arch))
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
maxLen) SymExpr sym (BaseBVType (ArchWidth arch))
one
     MemImpl sym
mem0 <- GlobalVar Mem
-> OverrideSim
     (personality sym) 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

     -- Allocate memory to hold the string
     (LLVMPointer sym (ArchWidth arch)
ptr, MemImpl sym
mem1) <- IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (LLVMPointer sym (ArchWidth arch), MemImpl sym)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (LLVMPointer sym (ArchWidth arch), MemImpl sym))
-> IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (LLVMPointer sym (ArchWidth arch), MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymExpr sym (BaseBVType (ArchWidth arch))
-> Alignment
-> IO (RegValue sym (TPtr arch), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
HeapAlloc Mutability
Mutable String
name MemImpl sym
mem0 SymExpr sym (BaseBVType (ArchWidth arch))
len Alignment
noAlignment

     -- Allocate contents for the string - we want to make each byte symbolic,
     -- so we allocate a fresh array (which has unbounded length) with symbolic
     -- contents and write it into our allocation.  This write does not cover
     -- the NUL terminator.
     SolverSymbol
contentsName <- case String -> Either SolverSymbolError SolverSymbol
userSymbol (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_contents") of
       Left SolverSymbolError
err -> String
-> OverrideSim (personality sym) sym ext r args ret SolverSymbol
forall a.
String -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (SolverSymbolError -> String
forall a. Show a => a -> String
show SolverSymbolError
err)
       Right SolverSymbol
nm -> SolverSymbol
-> OverrideSim (personality sym) sym ext r args ret SolverSymbol
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return SolverSymbol
nm
     let arrayRep :: BaseTypeRepr
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
arrayRep = Assignment BaseTypeRepr (EmptyCtx ::> BaseBVType (ArchWidth arch))
-> BaseTypeRepr (BaseBVType 8)
-> BaseTypeRepr
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr (Assignment BaseTypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment BaseTypeRepr EmptyCtx
-> BaseTypeRepr (BaseBVType (ArchWidth arch))
-> Assignment
     BaseTypeRepr (EmptyCtx ::> BaseBVType (ArchWidth arch))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr (ArchWidth arch)
-> BaseTypeRepr (BaseBVType (ArchWidth arch))
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth) (NatRepr 8 -> BaseTypeRepr (BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
     SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
initContents <- IO
  (SymExpr
     sym
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (SymExpr
      sym
      ('BaseArrayType
         (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (SymExpr
         sym
         ('BaseArrayType
            (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))))
-> IO
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall a b. (a -> b) -> a -> b
$ sym
-> SolverSymbol
-> BaseTypeRepr
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
-> IO
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
contentsName BaseTypeRepr
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
arrayRep
     SymExpr sym (BaseBVType 8)
zeroByte <- IO (SymExpr sym (BaseBVType 8))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 8))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType 8))
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 8)))
-> IO (SymExpr sym (BaseBVType 8))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 8))
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) (NatRepr 8 -> BV 8
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
     -- Put the NUL terminator in place
     SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
initContentsZ <- IO
  (SymExpr
     sym
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (SymExpr
      sym
      ('BaseArrayType
         (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
 -> OverrideSim
      (personality sym)
      sym
      ext
      r
      args
      ret
      (SymExpr
         sym
         ('BaseArrayType
            (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))))
-> IO
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr
     sym
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
-> Assignment
     (SymExpr sym) (EmptyCtx ::> BaseBVType (ArchWidth arch))
-> SymExpr sym (BaseBVType 8)
-> IO
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
initContents (SymExpr sym (BaseBVType (ArchWidth arch))
-> Assignment
     (SymExpr sym) (EmptyCtx ::> BaseBVType (ArchWidth arch))
forall {k} (f :: k -> *) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
singleton (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
maxLen)) SymExpr sym (BaseBVType 8)
zeroByte
     MemImpl sym
mem2 <- IO (MemImpl sym)
-> OverrideSim (personality sym) sym ext r args ret (MemImpl sym)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym)
 -> OverrideSim (personality sym) sym ext r args ret (MemImpl sym))
-> IO (MemImpl sym)
-> OverrideSim (personality sym) sym ext r args ret (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> RegValue sym (TPtr arch)
-> Alignment
-> SymExpr
     sym
     ('BaseArrayType
        (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
-> SymExpr sym (BaseBVType (ArchWidth arch))
-> IO (MemImpl sym)
forall sym bak (w :: Natural).
(IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Alignment
-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> SymBV sym w
-> IO (MemImpl sym)
doArrayConstStore bak
bak MemImpl sym
mem1 RegValue sym (TPtr arch)
LLVMPointer sym (ArchWidth arch)
ptr Alignment
noAlignment SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> BaseBVType (ArchWidth arch)) (BaseBVType 8))
initContentsZ SymExpr sym (BaseBVType (ArchWidth arch))
len

     GlobalVar Mem
-> RegValue sym Mem
-> OverrideSim (personality sym) sym ext r args ret ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem2
     LLVMPointer sym (ArchWidth arch)
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (LLVMPointer sym (ArchWidth arch))
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return LLVMPointer sym (ArchWidth arch)
ptr

do_assume ::
  ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) ->
  OverM personality sym ext (RegValue sym UnitType)
do_assume :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_assume Proxy# arch
arch GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
p :> RegEntry sym tp
pFile :> RegEntry sym tp
line) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     SymExpr sym BaseBoolType
cond <- IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym 8 -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
p)
     String
file <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pFile
     Int
l <- case SymExpr sym (BaseBVType 32) -> Maybe (BV 32)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
line) of
            Just (BV.BV Integer
l)  -> Int -> OverrideSim (personality sym) sym ext r args ret Int
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
l)
            Maybe (BV 32)
Nothing -> Int -> OverrideSim (personality sym) sym ext r args ret Int
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
     let pos :: Position
pos = Text -> Int -> Int -> Position
SourcePos (String -> Text
T.pack String
file) Int
l Int
0
     ProgramLoc
loc <- IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> OverrideSim (personality sym) sym ext r args ret ProgramLoc)
-> IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     let loc' :: ProgramLoc
loc' = ProgramLoc
loc{ plSourceLoc = pos }
     IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> String -> SymExpr sym BaseBoolType -> Assumption sym
forall (e :: BaseType -> *).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
loc' String
"crucible_assume" SymExpr sym BaseBoolType
cond)

do_assert ::
  ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) ->
  OverM personality sym ext (RegValue sym UnitType)
do_assert :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> 'BaseToType (BaseBVType 8)) ::> TPtr arch)
      ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_assert Proxy# arch
arch GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
p :> RegEntry sym tp
pFile :> RegEntry sym tp
line) =
  Bool
-> OverrideSim (personality sym) sym ext r args ret ()
-> OverrideSim (personality sym) sym ext r args ret ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior ?intrinsicsOpts::IntrinsicsOptions
IntrinsicsOptions
?intrinsicsOpts AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== AbnormalExitBehavior
AlwaysFail) (OverrideSim (personality sym) sym ext r args ret ()
 -> OverrideSim (personality sym) sym ext r args ret ())
-> OverrideSim (personality sym) sym ext r args ret ()
-> OverrideSim (personality sym) sym ext r args ret ()
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
     SymExpr sym BaseBoolType
cond <- IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym 8 -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
p)
     String
file <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pFile
     Int
l <- case SymExpr sym (BaseBVType 32) -> Maybe (BV 32)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
line) of
            Just (BV.BV Integer
l)  -> Int -> OverrideSim (personality sym) sym ext r args ret Int
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
l)
            Maybe (BV 32)
Nothing -> Int -> OverrideSim (personality sym) sym ext r args ret Int
forall a. a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
     let pos :: Position
pos = Text -> Int -> Int -> Position
SourcePos (String -> Text
T.pack String
file) Int
l Int
0
     ProgramLoc
loc <- IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> OverrideSim (personality sym) sym ext r args ret ProgramLoc)
-> IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     let loc' :: ProgramLoc
loc' = ProgramLoc
loc{ plSourceLoc = pos }
     let msg :: SimErrorReason
msg = String -> SimErrorReason
GenericSimError String
"crucible_assert"
     IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableAssertion bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred SymExpr sym BaseBoolType
cond (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc' SimErrorReason
msg))

do_print_uint32 ::
  (IsSymBackend sym bak) =>
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) ->
  OverM personality sym ext (RegValue sym UnitType)
do_print_uint32 :: forall sym bak (personality :: * -> *) ext.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_print_uint32 GlobalVar Mem
_mvar bak
_bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
x) =
  do Handle
h <- SimContext (personality sym) sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle (SimContext (personality sym) sym ext -> Handle)
-> OverrideSim
     (personality sym)
     sym
     ext
     r
     args
     ret
     (SimContext (personality sym) sym ext)
-> OverrideSim (personality sym) sym ext r args ret Handle
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim
  (personality sym)
  sym
  ext
  r
  args
  ret
  (SimContext (personality sym) sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
     IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h (Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType 32) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
x)))

do_havoc_memory ::
  (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> TBits (ArchWidth arch)) ->
  OverM personality sym ext (RegValue sym UnitType)
do_havoc_memory :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> TBits (ArchWidth arch))
-> OverM personality sym ext (RegValue sym 'UnitType)
do_havoc_memory Proxy# arch
_ GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
ptr :> RegEntry sym tp
len) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     let tp :: BaseTypeRepr
  ('BaseArrayType
     (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
tp = Assignment BaseTypeRepr (EmptyCtx ::> 'BaseBVType (ArchWidth arch))
-> BaseTypeRepr (BaseBVType 8)
-> BaseTypeRepr
     ('BaseArrayType
        (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr (Assignment BaseTypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment BaseTypeRepr EmptyCtx
-> BaseTypeRepr ('BaseBVType (ArchWidth arch))
-> Assignment
     BaseTypeRepr (EmptyCtx ::> 'BaseBVType (ArchWidth arch))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr (ArchWidth arch)
-> BaseTypeRepr ('BaseBVType (ArchWidth arch))
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth) (NatRepr 8 -> BaseTypeRepr (BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
     MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (personality sym) 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
     MemImpl sym
mem' <- IO (MemImpl sym)
-> OverrideSim (personality sym) sym ext r args ret (MemImpl sym)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym)
 -> OverrideSim (personality sym) sym ext r args ret (MemImpl sym))
-> IO (MemImpl sym)
-> OverrideSim (personality sym) sym ext r args ret (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ do
               SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
arr <- sym
-> SolverSymbol
-> BaseTypeRepr
     ('BaseArrayType
        (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
-> IO
     (SymExpr
        sym
        ('BaseArrayType
           (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8)))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol BaseTypeRepr
  ('BaseArrayType
     (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
tp
               bak
-> MemImpl sym
-> LLVMPtr sym (ArchWidth arch)
-> Alignment
-> SymExpr
     sym
     ('BaseArrayType
        (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
-> SymBV sym (ArchWidth arch)
-> IO (MemImpl sym)
forall sym bak (w :: Natural).
(IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Alignment
-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> SymBV sym w
-> IO (MemImpl sym)
doArrayStore bak
bak MemImpl sym
mem (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
ptr) Alignment
noAlignment SymExpr
  sym
  ('BaseArrayType
     (EmptyCtx ::> 'BaseBVType (ArchWidth arch)) (BaseBVType 8))
arr (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
len)
     GlobalVar Mem
-> RegValue sym Mem
-> OverrideSim (personality sym) sym ext r args ret ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'

cprover_assume ::
  (IsSymBackend sym bak) =>
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) ->
  OverM personality sym ext (RegValue sym UnitType)
cprover_assume :: forall sym bak (personality :: * -> *) ext.
IsSymBackend sym bak =>
GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 32))
-> OverM personality sym ext (RegValue sym 'UnitType)
cprover_assume GlobalVar Mem
_mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
p) = IO (RegValue sym 'UnitType)
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym 'UnitType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym 'UnitType)
 -> OverrideSim
      (personality sym) sym ext r args ret (RegValue sym 'UnitType))
-> IO (RegValue sym 'UnitType)
-> OverrideSim
     (personality sym) sym ext r args ret (RegValue sym 'UnitType)
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
     SymExpr sym BaseBoolType
cond <- sym -> SymBV sym 32 -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
p)
     ProgramLoc
loc  <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> String -> SymExpr sym BaseBoolType -> Assumption sym
forall (e :: BaseType -> *).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
loc String
"__CPROVER_assume" SymExpr sym BaseBoolType
cond)


cprover_assert ::
  ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TBits 32 ::> TPtr arch) ->
  OverM personality sym ext (RegValue sym UnitType)
cprover_assert :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> 'BaseToType (BaseBVType 32)) ::> TPtr arch)
-> OverM personality sym ext (RegValue sym 'UnitType)
cprover_assert Proxy# arch
arch GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
p :> RegEntry sym tp
pMsg) =
  Bool
-> OverrideSim (personality sym) sym ext r args ret ()
-> OverrideSim (personality sym) sym ext r args ret ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior ?intrinsicsOpts::IntrinsicsOptions
IntrinsicsOptions
?intrinsicsOpts AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== AbnormalExitBehavior
AlwaysFail) (OverrideSim (personality sym) sym ext r args ret ()
 -> OverrideSim (personality sym) sym ext r args ret ())
-> OverrideSim (personality sym) sym ext r args ret ()
-> OverrideSim (personality sym) sym ext r args ret ()
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
     SymExpr sym BaseBoolType
cond <- IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym 32 -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
p)
     String
str <- Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
forall sym (arch :: LLVMArch) (personality :: * -> *) ext.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch,
 ?memOpts::MemOptions) =>
Proxy# arch
-> GlobalVar Mem
-> RegEntry sym (TPtr arch)
-> OverM personality sym ext String
lookupString Proxy# arch
arch GlobalVar Mem
mvar RegEntry sym tp
RegEntry sym (TPtr arch)
pMsg
     ProgramLoc
loc <- IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> OverrideSim (personality sym) sym ext r args ret ProgramLoc)
-> IO ProgramLoc
-> OverrideSim (personality sym) sym ext r args ret ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     let msg :: SimErrorReason
msg = String -> String -> SimErrorReason
AssertFailureSimError String
"__CPROVER_assert" String
str
     IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym ext r args ret ())
-> IO () -> OverrideSim (personality sym) sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableAssertion bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred SymExpr sym BaseBoolType
cond (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg))

cprover_r_ok ::
  (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::>  BVType (ArchWidth arch)) ->
  OverM personality sym ext (RegValue sym (BVType 1))
cprover_r_ok :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM
     personality sym ext (RegValue sym ('BaseToType (BaseBVType 1)))
cprover_r_ok Proxy# arch
_ GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym tp
p) :> (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym tp
sz)) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (personality sym) 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
     SymExpr sym BaseBoolType
x <- IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr (ArchWidth arch)
-> Alignment
-> Mutability
-> LLVMPtr sym (ArchWidth arch)
-> Maybe (SymBV sym (ArchWidth arch))
-> MemImpl sym
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> NatRepr w
-> Alignment
-> Mutability
-> LLVMPtr sym w
-> Maybe (SymBV sym w)
-> MemImpl sym
-> IO (Pred sym)
isAllocatedAlignedPointer sym
sym NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth Alignment
noAlignment Mutability
Immutable RegValue sym tp
LLVMPtr sym (ArchWidth arch)
p (SymBV sym (ArchWidth arch) -> Maybe (SymBV sym (ArchWidth arch))
forall a. a -> Maybe a
Just RegValue sym tp
SymBV sym (ArchWidth arch)
sz) MemImpl sym
mem
     IO (SymExpr sym (BaseBVType 1))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType 1))
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1)))
-> IO (SymExpr sym (BaseBVType 1))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> NatRepr 1
-> IO (SymExpr sym (BaseBVType 1))
forall (w :: Natural).
(1 <= w) =>
sym -> SymExpr sym BaseBoolType -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
predToBV sym
sym SymExpr sym BaseBoolType
x NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

cprover_w_ok ::
  (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
  Proxy# arch ->
  GlobalVar Mem ->
  bak ->
  Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::>  BVType (ArchWidth arch)) ->
  OverM personality sym ext (RegValue sym (BVType 1))
cprover_w_ok :: forall (arch :: LLVMArch) sym bak (personality :: * -> *) ext.
(ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
Proxy# arch
-> GlobalVar Mem
-> bak
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> TPtr arch) ::> BVType (ArchWidth arch))
-> OverM
     personality sym ext (RegValue sym ('BaseToType (BaseBVType 1)))
cprover_w_ok Proxy# arch
_ GlobalVar Mem
mvar bak
bak (Assignment (RegEntry sym) ctx
Empty :> (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym tp
p) :> (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym tp
sz)) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (personality sym) 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
     SymExpr sym BaseBoolType
x <- IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr (ArchWidth arch)
-> Alignment
-> Mutability
-> LLVMPtr sym (ArchWidth arch)
-> Maybe (SymBV sym (ArchWidth arch))
-> MemImpl sym
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> NatRepr w
-> Alignment
-> Mutability
-> LLVMPtr sym w
-> Maybe (SymBV sym w)
-> MemImpl sym
-> IO (Pred sym)
isAllocatedAlignedPointer sym
sym NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth Alignment
noAlignment Mutability
Mutable RegValue sym tp
LLVMPtr sym (ArchWidth arch)
p (SymBV sym (ArchWidth arch) -> Maybe (SymBV sym (ArchWidth arch))
forall a. a -> Maybe a
Just RegValue sym tp
SymBV sym (ArchWidth arch)
sz) MemImpl sym
mem
     IO (SymExpr sym (BaseBVType 1))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1))
forall a.
IO a -> OverrideSim (personality sym) sym ext r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType 1))
 -> OverrideSim
      (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1)))
-> IO (SymExpr sym (BaseBVType 1))
-> OverrideSim
     (personality sym) sym ext r args ret (SymExpr sym (BaseBVType 1))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> NatRepr 1
-> IO (SymExpr sym (BaseBVType 1))
forall (w :: Natural).
(1 <= w) =>
sym -> SymExpr sym BaseBoolType -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
predToBV sym
sym SymExpr sym BaseBoolType
x NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat