Lang.Crucible.LLVM.Intrinsics.LLVM

Documentation

mkNull :: (IsSymInterface sym, HasPtrWidth wptr) => OverrideSim p sym ext rtp args ret (LLVMPtr sym wptr)

Local helper to make a null pointer in OverrideSim

Lists

basic_llvm_overrides :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => [SomeLLVMOverride p sym ext]

All "basic"/"monomorphic" LLVM overrides.

Can be turned into OverrideTemplates via basic_llvm_override.

newtype Poly1LLVMOverride p sym ext

An LLVM override that is polymorphic in a single argument

Constructors

Poly1LLVMOverride (forall w. 1 <= w => NatRepr w -> SomeLLVMOverride p sym ext)

poly1_llvm_overrides :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => [(String, Poly1LLVMOverride p sym ext)]

newtype Poly1VecLLVMOverride p sym ext

An LLVM override that is polymorphic in a single integer argument (intSz) that is used in combination with a vector type, which can be of varying sizes (vecSz).

Constructors

Poly1VecLLVMOverride (forall vecSz intSz. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext)

poly1_vec_llvm_overrides :: IsSymInterface sym => [(String, Poly1VecLLVMOverride p sym ext)]

Declarations

llvmLifetimeStartOverride :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) UnitType

This intrinsic is currently a no-op.

We might want to support this in the future to catch undefined memory accesses.

LLVM docs

llvmLifetimeEndOverride :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) UnitType

See comment on llvmLifetimeStartOverride

LLVM docs

llvmLifetimeOverrideOverload

Arguments

:: forall width sym wptr p ext. (1 <= width, KnownNat width, IsSymInterface sym, HasPtrWidth wptr)

=> String

"start" or "end"

-> NatRepr width

-> LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) UnitType

This is a no-op.

The language reference doesn't mention the use of this intrinsic.

llvmLifetimeOverrideOverload_opaque

Arguments

:: forall sym wptr p ext. (IsSymInterface sym, HasPtrWidth wptr)

=> String

"start" or "end"

-> LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) UnitType

Like llvmLifetimeOverrideOverload, but with an opaque pointer type.

llvmInvariantStartOverride :: (IsSymInterface sym, HasPtrWidth wptr) => NatRepr width -> LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) (LLVMPointerType wptr)

This intrinsic is currently a no-op.

We might want to support this in the future to catch undefined memory writes.

LLVM docs

llvmInvariantStartOverride_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx ::> BVType 64) ::> LLVMPointerType wptr) (LLVMPointerType wptr)

Like llvmInvariantStartOverride, but with an opaque pointer type.

llvmInvariantEndOverride :: (IsSymInterface sym, HasPtrWidth wptr) => NatRepr width -> LLVMOverride p sym ext (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 64) ::> LLVMPointerType wptr) UnitType

See comment on llvmInvariantStartOverride.

llvmInvariantEndOverride_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 64) ::> LLVMPointerType wptr) UnitType

See comment on llvmInvariantStartOverride_opaque.

llvmExpectOverride :: (IsSymInterface sym, 1 <= width) => NatRepr width -> LLVMOverride p sym ext ((EmptyCtx ::> BVType width) ::> BVType width) (BVType width)

This instruction is a hint to optimizers, it isn't really useful for us.

Its runtime behavior of that of Haskell's const: just ignore the second argument.

llvmAssumeOverride :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> BVType 1) UnitType

This intrinsic asserts that its argument is equal to 1.

We could have this generate a verification condition, but that would catch clang compiler bugs (or Crucible bugs) more than user code bugs.

llvmTrapOverride :: IsSymInterface sym => LLVMOverride p sym ext EmptyCtx UnitType

This intrinsic is sometimes inserted by clang, and we interpret it as an assertion failure, similar to calling abort().

llvmUBSanTrapOverride :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> BVType 8) UnitType

This is like llvm.trap(), but with an argument indicating which sort of undefined behavior was trapped. The argument acts as an index into this list. Ideally, we would do something intelligent with this argument—see #368.

llvmStacksave :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr)

llvmStackrestore :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType

llvmMemmoveOverride_8_8_32 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 32) ::> BVType 1) UnitType

llvmMemmoveOverride_8_8_32_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 1) UnitType

llvmMemmoveOverride_8_8_32_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 1) UnitType

llvmMemmoveOverride_8_8_64 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 32) ::> BVType 1) UnitType

llvmMemmoveOverride_8_8_64_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 1) UnitType

llvmMemmoveOverride_8_8_64_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 1) UnitType

llvmMemsetOverride_8_64 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 64) ::> BVType 32) ::> BVType 1) UnitType

llvmMemsetOverride_8_64_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 64) ::> BVType 1) UnitType

llvmMemsetOverride_8_64_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 64) ::> BVType 1) UnitType

llvmMemsetOverride_8_32 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 32) ::> BVType 32) ::> BVType 1) UnitType

llvmMemsetOverride_8_32_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 32) ::> BVType 1) UnitType

llvmMemsetOverride_8_32_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 8) ::> BVType 32) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_32 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 32) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_32_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_32_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_64 :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext (((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 32) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_64_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 1) UnitType

llvmMemcpyOverride_8_8_64_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 64) ::> BVType 1) UnitType

llvmObjectsizeOverride_32 :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) (BVType 32)

llvmObjectsizeOverride_32_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) (BVType 32)

llvmObjectsizeOverride_32_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) ::> BVType 1) (BVType 32)

llvmObjectsizeOverride_32_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) ::> BVType 1) (BVType 32)

llvmObjectsizeOverride_64 :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) (BVType 64)

llvmObjectsizeOverride_64_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) (BVType 64)

llvmObjectsizeOverride_64_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) ::> BVType 1) (BVType 64)

llvmObjectsizeOverride_64_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 1) ::> BVType 1) ::> BVType 1) (BVType 64)

llvmPrefetchOverride :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 32) ::> BVType 32) UnitType

This instruction is a hint to code generators, which means that it is a no-op for us.

LLVM docs

llvmPrefetchOverride_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 32) ::> BVType 32) UnitType

Like llvmPrefetchOverride, but with an opaque pointer type.

llvmPrefetchOverride_preLLVM10 :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32) ::> BVType 32) ::> BVType 32) UnitType

This instruction is a hint to code generators, which means that it is a no-op for us.

See also llvmPrefetchOverride. This version exists for compatibility with pre-10 versions of LLVM, where llvm.prefetch always assumed that the first argument resides in address space 0.

LLVM docs

llvmFshl :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx ::> BVType w) ::> BVType w) ::> BVType w) (BVType w)

llvmFshr :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx ::> BVType w) ::> BVType w) ::> BVType w) (BVType w)

llvmSaddWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmUaddWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmSsubWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmUsubWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmSmulWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmUmulWithOverflow :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (StructType ((EmptyCtx ::> BVType w) ::> BVType 1))

llvmUmax :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (BVType w)

llvmUmin :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (BVType w)

llvmSmax :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (BVType w)

llvmSmin :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType w) (BVType w)

llvmCtlz :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType 1) (BVType w)

llvmCttz :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType 1) (BVType w)

llvmCtpop :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (EmptyCtx ::> BVType w) (BVType w)

llvmBitreverse :: (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (EmptyCtx ::> BVType w) (BVType w)

llvmBSwapOverride :: forall width sym p ext. (1 <= width, IsSymInterface sym) => NatRepr width -> LLVMOverride p sym ext (EmptyCtx ::> BVType (width * 8)) (BVType (width * 8))

LLVM docs

llvmLoadRelative :: (1 <= w, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType w) (LLVMPointerType wptr)

LLVM docs

llvmAbsOverride :: (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx ::> BVType w) ::> BVType 1) (BVType w)

llvmCopysignOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmCopysignOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmFabsF32 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmFabsF64 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmCeilOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmCeilOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmFloorOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmFloorOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmSqrtOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmSqrtOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmSinOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmSinOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmCosOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmCosOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmPowOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmPowOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmExpOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmExpOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmLogOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmLogOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmExp2Override_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmExp2Override_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmLog2Override_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmLog2Override_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmLog10Override_F32 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmLog10Override_F64 :: IsSymInterface sym => LLVMOverride p sym ext (EmptyCtx ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmIsFpclassOverride_F32 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType SingleFloat) ::> BVType 32) (BVType 1)

llvmIsFpclassOverride_F64 :: IsSymInterface sym => LLVMOverride p sym ext ((EmptyCtx ::> FloatType DoubleFloat) ::> BVType 32) (BVType 1)

llvmFmaOverride_F32 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmFmaOverride_F64 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmFmuladdOverride_F32 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat) ::> FloatType SingleFloat) (FloatType SingleFloat)

llvmFmuladdOverride_F64 :: forall sym p ext. IsSymInterface sym => LLVMOverride p sym ext (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) ::> FloatType DoubleFloat) (FloatType DoubleFloat)

llvmX86_pclmulqdq :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((EmptyCtx ::> VectorType (BVType 64)) ::> VectorType (BVType 64)) ::> BVType 8) (VectorType (BVType 64))

llvmX86_SSE2_storeu_dq :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMOverride p sym ext ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType (BVType 8)) UnitType

llvmVectorReduce

Arguments

:: 1 <= intSz

=> String

The name of the operation to reduce (add, mul, etc.).

-> (forall r args ret. IsSymInterface sym => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz))

The semantics of the override.

-> NatRepr vecSz

The size of the vector type.

-> NatRepr intSz

The size of the integer type.

-> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

Build an LLVMOverride for a vector reduce intrinsic.

llvmVectorReduceAdd :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceMul :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceAnd :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceOr :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceXor :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceSmax :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceSmin :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceUmax :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

llvmVectorReduceUmin :: 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (EmptyCtx ::> VectorType (BVType intSz)) (BVType intSz)

Implementations

callX86_pclmulqdq :: forall p sym ext wptr r args ret. (IsSymInterface sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (VectorType (BVType 64)) -> RegEntry sym (VectorType (BVType 64)) -> RegEntry sym (BVType 8) -> OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType 64)))

callStoreudq :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (VectorType (BVType 8)) -> OverrideSim p sym ext r args ret ()

callObjectsize :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callObjectsize_null :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callObjectsize_null_dynamic :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callCtlz :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callFshl :: (1 <= w, IsSymInterface sym) => NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callFshr :: (1 <= w, IsSymInterface sym) => NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callSaddWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callUaddWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callUsubWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callSsubWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callSmulWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callUmulWithOverflow :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType ((EmptyCtx ::> BVType w) ::> BVType 1)))

callUmax :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

bvUmax :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Compute the unsigned maximum of two bitvectors.

callUmin :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

bvUmin :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Compute the unsigned minimum of two bitvectors.

callSmax :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

bvSmax :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Compute the signed maximum of two bitvectors.

callSmin :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

bvSmin :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Compute the signed minimum of two bitvectors.

callCttz :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callCtpop :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callBitreverse :: (1 <= w, IsSymInterface sym) => GlobalVar Mem -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w))

callCopysign :: forall fi p sym ext r args ret. IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))

Strictly speaking, this doesn't quite conform to the C99 description of copysign, since copysign(NaN, -1.0) should return NaN with a negative sign bit. libBF does not provide a way to distinguish between NaN values with different sign bits, however, so copysign will always turn a NaN argument into a positive, "quiet" NaN.

callIsFpclass :: forall fi p sym ext r args ret. IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 1))

An implementation of the llvm.is.fpclass intrinsic. This essentially combines several different floating-point checks (checking for NaN, infinity, zero, etc.) into a single function. The second argument is a bitmask that controls which properties to check of the first argument. The different checks in the bitmask are described by the table here: https://llvm.org/docs/LangRef.html#id1566

The specification requires being able to distinguish between signaling NaNs (bit 0 of the bitmask) and quit NaNs (bit 1 of the bitmask), but crucible-llvm does not have the ability to do this. As a result, both NaN checks will always return true in this implementation, regardless of whether they are signaling or quiet NaNs.

callLoadRelative :: (1 <= w, IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (LLVMPtr sym wptr)

An override for the llvm.load.relative.i* family of intrinsics. Broadly speaking, this loads a pointer at from the first argument (a pointer to an array) at the value of the second argument (the offset). However, due to the reasons described in Note [Undoing LLVM's relative table lookup conversion pass] in Lang.Crucible.LLVM.Globals, this override adjusts the offset before performing the load.

callVectorReduce

Arguments

:: (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp))

The operation which performs the reduction (e.g., addition, multiplication, etc.)

-> RegValue sym tp

The identity element for the reduction operation. (For addition, this is 0; for multiplication, this is 1, and so on.)

-> RegEntry sym (VectorType tp)

The vector to reduce.

-> OverrideSim p sym ext r args ret (RegValue sym tp)

The semantics of an LLVM vector reduce intrinsic.

callVectorReduceAdd :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceMul :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceAnd :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceOr :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceXor :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceSmax :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceSmin :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceUmax :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)

callVectorReduceUmin :: (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz)