Copyright	(c) Galois Inc 2015-2019
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.LLVM.Intrinsics.Libc

Description

Synopsis

libc_overrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext]
llvmAssertRtnOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) UnitType
llvmAssertFailOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) UnitType
llvmHtonlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32)
llvmHtonsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 16) (BVType 16)
llvmNtohlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32)
llvmNtohsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 16) (BVType 16)
callAssert :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => GlobalVar Mem -> Assignment (RegEntry sym) (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) -> forall r (args :: Ctx CrucibleType) (reg :: CrucibleType). OverrideSim p sym ext r args reg (RegValue sym UnitType)
callBSwapIfLittleEndian :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= width, IsSymInterface sym, ?lc :: TypeContext) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= width, IsSymInterface sym) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
mathOverrides :: IsSymInterface sym => [SomeLLVMOverride p sym ext]
llvmCeilOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmCeilfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmFloorOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmFloorfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmFmaOverride :: IsSymInterface sym => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmFmafOverride :: IsSymInterface sym => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmIsinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32)
llvm__isinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32)
llvm__isinffOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (BVType 32)
llvmIsnanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32)
llvm__isnanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32)
llvm__isnanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (BVType 32)
llvm__isnandOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32)
llvmSqrtOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmSqrtfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmSinOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmSinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmCosOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmCosfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmTanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmTanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAsinOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAsinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAcosOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAcosfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAtanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAtanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmSinhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmSinhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmCoshOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmCoshfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmTanhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmTanhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAsinhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAsinhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAcoshOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAcoshfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAtanhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAtanhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmHypotOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmHypotfOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmAtan2Override :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmAtan2fOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmPowfOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmPowOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmExpOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmExpfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmLogOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmLogfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmExpm1Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmExpm1fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmLog1pOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmLog1pfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmExp2Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmExp2fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmLog2Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmLog2fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmExp10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmExp10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvm__exp10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvm__exp10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
llvmLog10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat)
llvmLog10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat)
callCeil :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callIsinf :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callSqrt :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => SpecialFunction ((EmptyCtx :: Ctx Type) ::> R) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) ::> R) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
defaultRM :: RoundingMode
stdioOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext]
llvmPrintfOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> VectorType AnyType) (BVType 32)
llvmPrintfChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) ::> LLVMPointerType wptr) ::> VectorType AnyType) (BVType 32)
llvmPutsOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (BVType 32)
llvmPutCharOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32)
callPrintf :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (VectorType AnyType) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar :: forall sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => GlobalVar Mem -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
printfOps :: forall sym bak (wptr :: Natural). (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> Vector (AnyValue sym) -> PrintfOperations (StateT (MemImpl sym) IO)
stdlibOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext]
llvmMallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType wptr) (LLVMPointerType wptr)
llvmCallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr)
llvmFreeOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) UnitType
llvmReallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr)
posixMemalignOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) ::> BVType wptr) (BVType 32)
llvmAbortOverride :: (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => LLVMOverride p sym ext (EmptyCtx :: Ctx CrucibleType) UnitType
llvmExitOverride :: (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) UnitType
llvmGetenvOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (LLVMPointerType wptr)
llvmAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32)
llvmLAbsOverride_32 :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32)
llvmLAbsOverride_64 :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) (BVType 64)
llvmLLAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) (BVType 64)
cxa_atexitOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (BVType 32)
callMalloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callCalloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callFree :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret ()
callRealloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callPosixMemalign :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callExit :: forall sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callLibcAbs :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callLLVMAbs :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callAbs :: forall (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> CheckAbsIntMin -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
data CheckAbsIntMin
- = LibcAbsIntMinUB
- | LLVMAbsIntMinPoison Bool
stringOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext]
llvmMemcpyOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr)
llvmMemcpyChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr)
llvmMemmoveOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr)
llvmMemsetOverride :: forall p sym ext (wptr :: Natural). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType wptr) (LLVMPointerType wptr)
llvmMemsetChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr)
llvmMemcmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType 32)
llvmStrlenOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (BVType wptr)
llvmStrnlenOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType wptr)
llvmStrcpyOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (LLVMPointerType wptr)
llvmStrcmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (BVType 32)
llvmStrncmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType 32)
llvmStrdupOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (LLVMPointerType wptr)
llvmStrndupOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr)
callMemcpy :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret ()
callMemmove :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret ()
callMemset :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 8) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret ()
callMemcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrnlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrcpy :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrncmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callStrdup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callStrndup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))

Documentation

libc_overrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext] Source #

All libc overrides.

This list is useful to other Crucible frontends based on the LLVM memory model (e.g., Macaw).

llvmAssertRtnOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) UnitType Source #

llvmAssertFailOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) UnitType Source #

llvmHtonlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32) Source #

llvmHtonsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 16) (BVType 16) Source #

llvmNtohlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32) Source #

llvmNtohsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 16) (BVType 16) Source #

callAssert :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => GlobalVar Mem -> Assignment (RegEntry sym) (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) -> forall r (args :: Ctx CrucibleType) (reg :: CrucibleType). OverrideSim p sym ext r args reg (RegValue sym UnitType) Source #

callBSwapIfLittleEndian :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= width, IsSymInterface sym, ?lc :: TypeContext) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) Source #

If the data layout is little-endian, run callBSwap on the input. Otherwise, return the input unchanged. This is the workhorse for the hton{s,l} and ntoh{s,l} overrides.

callBSwap :: forall (width :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= width, IsSymInterface sym) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) Source #

mathOverrides :: IsSymInterface sym => [SomeLLVMOverride p sym ext] Source #

All math.h overrides

llvmCeilOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmCeilfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmFloorOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmFloorfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmFmaOverride :: IsSymInterface sym => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmFmafOverride :: IsSymInterface sym => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmIsinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32) Source #

llvm__isinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32) Source #

llvm__isinffOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (BVType 32) Source #

llvmIsnanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32) Source #

llvm__isnanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32) Source #

llvm__isnanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (BVType 32) Source #

llvm__isnandOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (BVType 32) Source #

llvmSqrtOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmSqrtfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmSinOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmSinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmCosOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmCosfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmTanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmTanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAsinOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAsinfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAcosOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAcosfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAtanOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAtanfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmSinhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmSinhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmCoshOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmCoshfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmTanhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmTanhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAsinhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAsinhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAcoshOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAcoshfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAtanhOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAtanhfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmHypotOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmHypotfOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmAtan2Override :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmAtan2fOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmPowfOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmPowOverride :: IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmExpOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmExpfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmLogOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmLogfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmExpm1Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmExpm1fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmLog1pOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmLog1pfOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmExp2Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmExp2fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmLog2Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmLog2fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmExp10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmExp10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvm__exp10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvm__exp10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

llvmLog10Override :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType DoubleFloat) (FloatType DoubleFloat) Source #

llvmLog10fOverride :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> FloatType SingleFloat) (FloatType SingleFloat) Source #

callCeil :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callFloor :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callFMA :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

An implementation of libc's fma function.

callIsinf :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

An implementation of libc's isinf macro. This returns 1 when the argument is positive infinity, -1 when the argument is negative infinity, and zero otherwise.

callIsnan :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callSqrt :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callSpecialFunction1 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => SpecialFunction ((EmptyCtx :: Ctx Type) ::> R) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callSpecialFunction2 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) ::> R) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

defaultRM :: RoundingMode Source #

IEEE 754 declares RNE to be the default rounding mode, and most libc implementations agree with this in practice. The only places where we do not use this as the default are operations that specifically require the behavior of a particular rounding mode, such as ceil or floor.

stdioOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext] Source #

All stdio.h overrides

llvmPrintfOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> VectorType AnyType) (BVType 32) Source #

llvmPrintfChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) ::> LLVMPointerType wptr) ::> VectorType AnyType) (BVType 32) Source #

llvmPutsOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (BVType 32) Source #

llvmPutCharOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32) Source #

callPrintf :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (VectorType AnyType) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callPutChar :: forall sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => GlobalVar Mem -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callPuts :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

printfOps :: forall sym bak (wptr :: Natural). (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> Vector (AnyValue sym) -> PrintfOperations (StateT (MemImpl sym) IO) Source #

stdlibOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext] Source #

All stdlib.h overrides

llvmMallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmCallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmFreeOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) UnitType Source #

llvmReallocOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

posixMemalignOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) ::> BVType wptr) (BVType 32) Source #

llvmAbortOverride :: (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => LLVMOverride p sym ext (EmptyCtx :: Ctx CrucibleType) UnitType Source #

llvmExitOverride :: (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) UnitType Source #

llvmGetenvOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (LLVMPointerType wptr) Source #

llvmAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32) Source #

llvmLAbsOverride_32 :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 32) (BVType 32) Source #

llvmLAbsOverride_64 :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) (BVType 64) Source #

llvmLLAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) (BVType 64) Source #

cxa_atexitOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (BVType 32) Source #

callMalloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callCalloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callFree :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret () Source #

callRealloc :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> Alignment -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callPosixMemalign :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callExit :: forall sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, ?intrinsicsOpts :: IntrinsicsOptions) => RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym UnitType) Source #

callLibcAbs :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callLLVMAbs :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callAbs :: forall (w :: Natural) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> CheckAbsIntMin -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

The workhorse for the abs, labs, and llabs functions, as well as the llvm.abs.* family of overloaded intrinsics.

data CheckAbsIntMin Source #

This determines under what circumstances callAbs should check if its argument is equal to the smallest signed integer of a particular size (e.g., INT_MIN), and if it is equal to that value, what kind of error should be reported.

Constructors

LibcAbsIntMinUB	For the `abs`, `labs`, and `llabs` functions, always check if the argument is equal to `INT_MIN`. If so, report it as undefined behavior per the C standard.
LLVMAbsIntMinPoison Bool	For the `llvm.abs.*` family of LLVM intrinsics, check if the argument is equal to `INT_MIN` only when the `Bool` argument is `True`. If it is `True` and the argument is equal to `INT_MIN`, return poison.

stringOverrides :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext] Source #

All string.h overrides

llvmMemcpyOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmMemcpyChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmMemmoveOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmMemsetOverride :: forall p sym ext (wptr :: Natural). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmMemsetChkOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

llvmMemcmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType 32) Source #

llvmStrlenOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (BVType wptr) Source #

llvmStrnlenOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType wptr) Source #

llvmStrcpyOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (LLVMPointerType wptr) Source #

llvmStrcmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) (BVType 32) Source #

llvmStrncmpOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType 32) Source #

llvmStrdupOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) (LLVMPointerType wptr) Source #

llvmStrndupOverride :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType wptr) (LLVMPointerType wptr) Source #

callMemcpy :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () Source #

callMemmove :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () Source #

callMemset :: forall sym (wptr :: Natural) (w :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 8) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () Source #

callMemcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callStrlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)) Source #

callStrnlen :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)) Source #

callStrcpy :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callStrcmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callStrncmp :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callStrdup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callStrndup :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #