{-# 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
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))
, 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)
]
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))
, 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))
, 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
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)
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
(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
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)
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