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

Lang.Crucible.LLVM.Intrinsics.Libc

Description

 
Synopsis

Declarations

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

Allocation

Strings and I/O

Implementations

Allocation

callRealloc :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> GlobalVar Mem -> Alignment -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callPosixMemalign :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?lc :: TypeContext, ?memOpts :: MemOptions) => bak -> 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 #

callMalloc :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callCalloc :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) Source #

callFree :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) => bak -> GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret () Source #

Memory manipulation

callMemcpy :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> 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 :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => bak -> 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 :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) => bak -> 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 #

Strings and I/O

callPutChar :: IsSymBackend sym bak => bak -> GlobalVar Mem -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callPuts :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) Source #

callStrlen :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)) Source #

callAssert Source #

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) 
=> Bool

True if this is __assert_fail(), False otherwise.

-> GlobalVar Mem 
-> bak 
-> Assignment (RegEntry sym) ((((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr) ::> BVType 32) ::> LLVMPointerType wptr) 
-> forall r args reg. OverrideSim p sym ext r args reg (RegValue sym UnitType) 

callExit :: (IsSymBackend sym bak, ?intrinsicsOpts :: IntrinsicsOptions) => bak -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym UnitType) Source #

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

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

Math

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

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

callCeil :: forall fi p sym bak ext r args ret. IsSymBackend sym bak => bak -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callFloor :: forall fi p sym bak ext r args ret. IsSymBackend sym bak => bak -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

callFMA :: forall fi p sym bak ext r args ret. IsSymBackend sym bak => bak -> 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 w p sym bak ext r args ret. (IsSymBackend sym bak, 1 <= w) => bak -> 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 w p sym bak ext r args ret. (IsSymBackend sym bak, 1 <= w) => bak -> NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callSqrt :: forall fi p sym bak ext r args ret. IsSymBackend sym bak => bak -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) Source #

Circular trigonometry functions

Hyperbolic trigonometry functions

Rectangular to polar coordinate conversion

Exponential and logarithm functions

Base 2 exponential and logarithm

Base 10 exponential and logarithm

Other

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

callBSwap :: (1 <= width, IsSymBackend sym bak) => bak -> NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) Source #

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.

callAbs :: forall w p sym bak ext r args ret. (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => bak -> 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.

callLibcAbs :: (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => bak -> CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callLLVMAbs :: (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => bak -> CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) Source #

callBSwapIfLittleEndian :: (1 <= width, IsSymBackend sym bak, ?lc :: TypeContext) => bak -> 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.

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.