crucible-llvm-0.8.0.0: Support for translating and executing LLVM code in Crucible
Copyright(c) Galois Inc 2015-2016
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

Lang.Crucible.LLVM.Intrinsics.LLVM

Description

 
Synopsis

Documentation

mkNull :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, HasPtrWidth wptr) => OverrideSim p sym ext rtp args ret (LLVMPtr sym wptr) Source #

Local helper to make a null pointer in OverrideSim

Lists

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

All "basic"/"monomorphic" LLVM overrides.

Can be turned into OverrideTemplates via basic_llvm_override.

newtype Poly1LLVMOverride p sym ext Source #

An LLVM override that is polymorphic in a single argument

Constructors

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

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

newtype Poly1VecLLVMOverride p sym ext Source #

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 :: Nat) (intSz :: Natural). 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext) 

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

Declarations

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

This intrinsic is currently a no-op.

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

LLVM docs

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

See comment on llvmLifetimeStartOverride

LLVM docs

llvmLifetimeOverrideOverload Source #

Arguments

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

"start" or "end"

-> NatRepr width 
-> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) ::> LLVMPointerType wptr) UnitType 

This is a no-op.

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

llvmLifetimeOverrideOverload_opaque Source #

Arguments

:: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) 
=> String

"start" or "end"

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

Like llvmLifetimeOverrideOverload, but with an opaque pointer type.

llvmInvariantStartOverride :: forall sym (wptr :: Natural) (width :: Nat) p ext. (IsSymInterface sym, HasPtrWidth wptr) => NatRepr width -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) ::> LLVMPointerType wptr) (LLVMPointerType wptr) Source #

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 :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType 64) ::> LLVMPointerType wptr) (LLVMPointerType wptr) Source #

Like llvmInvariantStartOverride, but with an opaque pointer type.

llvmInvariantEndOverride :: forall sym (wptr :: Natural) (width :: Nat) p ext. (IsSymInterface sym, HasPtrWidth wptr) => NatRepr width -> LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType 64) ::> LLVMPointerType wptr) UnitType Source #

See comment on llvmInvariantStartOverride.

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

See comment on llvmInvariantStartOverride_opaque.

llvmExpectOverride :: forall sym (width :: Natural) p ext. (IsSymInterface sym, 1 <= width) => NatRepr width -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType width) ::> BVType width) (BVType width) Source #

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 :: Ctx CrucibleType) ::> BVType 1) UnitType Source #

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 :: Ctx CrucibleType) UnitType Source #

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 :: Ctx CrucibleType) ::> BVType 8) UnitType Source #

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 :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx :: Ctx CrucibleType) (LLVMPointerType wptr) Source #

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

llvmMemmoveOverride_8_8_32 :: 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) ::> BVType 32) ::> BVType 1) UnitType Source #

llvmMemmoveOverride_8_8_32_noalign :: 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) ::> BVType 1) UnitType Source #

llvmMemmoveOverride_8_8_32_noalign_opaque :: 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) ::> BVType 1) UnitType Source #

llvmMemmoveOverride_8_8_64 :: 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 64) ::> BVType 32) ::> BVType 1) UnitType Source #

llvmMemmoveOverride_8_8_64_noalign :: 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 64) ::> BVType 1) UnitType Source #

llvmMemmoveOverride_8_8_64_noalign_opaque :: 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 64) ::> BVType 1) UnitType Source #

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

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

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

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

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

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

llvmMemcpyOverride_8_8_32 :: 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) ::> BVType 32) ::> BVType 1) UnitType Source #

llvmMemcpyOverride_8_8_32_noalign :: 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) ::> BVType 1) UnitType Source #

llvmMemcpyOverride_8_8_32_noalign_opaque :: 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) ::> BVType 1) UnitType Source #

llvmMemcpyOverride_8_8_64 :: 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 64) ::> BVType 32) ::> BVType 1) UnitType Source #

llvmMemcpyOverride_8_8_64_noalign :: 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 64) ::> BVType 1) UnitType Source #

llvmMemcpyOverride_8_8_64_noalign_opaque :: 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 64) ::> BVType 1) UnitType Source #

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

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

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

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

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

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

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

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

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

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

LLVM docs

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

Like llvmPrefetchOverride, but with an opaque pointer type.

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

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 :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmFshr :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmSaddWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmUaddWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmSsubWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmUsubWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmSmulWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmUmulWithOverflow :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (StructType (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1)) Source #

llvmUmax :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmUmin :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmSmax :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmSmin :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType w) (BVType w) Source #

llvmCtlz :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1) (BVType w) Source #

llvmCttz :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1) (BVType w) Source #

llvmCtpop :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType w) (BVType w) Source #

llvmBitreverse :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym) => NatRepr w -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> BVType w) (BVType w) Source #

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

LLVM docs

llvmLoadRelative :: forall (w :: Natural) (wptr :: Natural) sym p ext. (1 <= w, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> LLVMPointerType wptr) ::> BVType w) (LLVMPointerType wptr) Source #

LLVM docs

llvmAbsOverride :: forall (w :: Natural) sym p ext. (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => NatRepr w -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> BVType w) ::> BVType 1) (BVType w) Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

llvmX86_pclmulqdq :: forall sym (wptr :: Natural) p ext. (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext ((((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType 64)) ::> VectorType (BVType 64)) ::> BVType 8) (VectorType (BVType 64)) Source #

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

llvmVectorReduce Source #

Arguments

:: forall (intSz :: Natural) sym p ext (vecSz :: Nat). 1 <= intSz 
=> String

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

-> (forall r (args :: Ctx CrucibleType) (ret :: CrucibleType). 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 :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) 

Build an LLVMOverride for a vector reduce intrinsic.

llvmVectorReduceAdd :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceMul :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceAnd :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceOr :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceXor :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceSmax :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceSmin :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceUmax :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorReduceUmin :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext ((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) (BVType intSz) Source #

llvmVectorMap Source #

Arguments

:: forall (intSz :: Natural) sym p ext (vecSz :: Nat). 1 <= intSz 
=> String

The name of the operation to map (umin, smin, etc.).

-> (forall r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (VectorType (BVType intSz)) -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (Vector (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 :: Ctx CrucibleType) ::> VectorType (BVType intSz)) ::> VectorType (BVType intSz)) (VectorType (BVType intSz)) 

Build an LLVMOverride for a vector map intrinsic.

llvmSmaxVector :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) ::> VectorType (BVType intSz)) (VectorType (BVType intSz)) Source #

llvmSminVector :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) ::> VectorType (BVType intSz)) (VectorType (BVType intSz)) Source #

llvmUmaxVector :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) ::> VectorType (BVType intSz)) (VectorType (BVType intSz)) Source #

llvmUminVector :: forall (intSz :: Natural) (vecSz :: Nat) p sym ext. 1 <= intSz => NatRepr vecSz -> NatRepr intSz -> LLVMOverride p sym ext (((EmptyCtx :: Ctx CrucibleType) ::> VectorType (BVType intSz)) ::> VectorType (BVType intSz)) (VectorType (BVType intSz)) Source #

Implementations

callX86_pclmulqdq :: forall p sym ext (wptr :: Natural) r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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))) Source #

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

callObjectsize :: forall (w :: Natural) sym (wptr :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callObjectsize_null :: forall (w :: Natural) sym (wptr :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callObjectsize_null_dynamic :: forall (w :: Natural) sym (wptr :: Nat) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callCtlz :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callFshl :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callFshr :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

callSaddWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callUaddWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callUsubWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callSsubWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callSmulWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callUmulWithOverflow :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: Ctx CrucibleType) ::> BVType w) ::> BVType 1))) Source #

callUmax :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

bvUmax :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the unsigned maximum of two bitvectors.

callUmin :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

bvUmin :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the unsigned minimum of two bitvectors.

callSmax :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

bvSmax :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the signed maximum of two bitvectors.

callSmin :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

bvSmin :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #

Compute the signed minimum of two bitvectors.

callCttz :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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)) Source #

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

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

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

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 :: FloatInfo) p sym ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 1)) Source #

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 :: forall (w :: Natural) sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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) Source #

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 Source #

Arguments

:: forall sym (tp :: CrucibleType) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (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 :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceMul :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceAnd :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceOr :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceXor :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceSmax :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceSmin :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceUmax :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorReduceUmin :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => NatRepr intSz -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (SymBV sym intSz) Source #

callVectorMap Source #

Arguments

:: forall sym (tp :: CrucibleType) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp))

The operation to apply when mapping (e.g., umin, smin, etc.)

-> RegEntry sym (VectorType tp)

The first vector to map over.

-> RegEntry sym (VectorType tp)

The second vector to map over.

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

The result of mapping over the vectors.

The semantics of an LLVM vector map intrinsic.

callVectorMapSmax :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => RegEntry sym (VectorType (BVType intSz)) -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (Vector (SymBV sym intSz)) Source #

callVectorMapSmin :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => RegEntry sym (VectorType (BVType intSz)) -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (Vector (SymBV sym intSz)) Source #

callVectorMapUmax :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => RegEntry sym (VectorType (BVType intSz)) -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (Vector (SymBV sym intSz)) Source #

callVectorMapUmin :: forall sym (intSz :: Natural) p ext r (args :: Ctx CrucibleType) (ret :: CrucibleType). (IsSymInterface sym, 1 <= intSz) => RegEntry sym (VectorType (BVType intSz)) -> RegEntry sym (VectorType (BVType intSz)) -> OverrideSim p sym ext r args ret (Vector (SymBV sym intSz)) Source #