Lang.Crucible.LLVM.MemModel.Pointer

Pointer bitwidth

type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w)

This constraint captures the idea that there is a distinguished pointer width in scope which is appropriate according to the C notion of pointer, and object size. In particular, it must be at least 16-bits wide (as required for the size_t type).

pattern PtrWidth :: HasPtrWidth w => w ~ w' => NatRepr w'

withPtrWidth :: forall w a. 16 <= w => NatRepr w -> (HasPtrWidth w => a) -> a

Crucible pointer representation

type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)

Crucible type of pointers/bitvector values of width w.

type LLVMPtr sym w = RegValue sym (LLVMPointerType w)

Symbolic LLVM pointer or bitvector values of width w.

data SomePointer sym

A pointer with an existentially-quantified width

Constructors

forall w.1 <= w => SomePointer !(LLVMPtr sym w)

pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty

This pattern synonym makes it easy to build and destruct runtime representatives of LLVMPointerType w.

pattern PtrRepr :: HasPtrWidth wptr => ty ~ LLVMPointerType wptr => TypeRepr ty

This pattern creates/matches against the TypeRepr for LLVM pointer values that are of the distinguished pointer width.

pattern SizeT :: HasPtrWidth wptr => ty ~ BVType wptr => TypeRepr ty

This pattern creates/matches against the TypeRepr for raw bitvector values that are of the distinguished pointer width.

pattern LLVMPointer :: SymNat sym -> SymBV sym w -> LLVMPointer sym w

A pointer is a base point offset.

ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w

Compute the width of a pointer value.

llvmPointerView :: LLVMPtr sym w -> (SymNat sym, SymBV sym w)

Alternative to the LLVMPointer pattern synonym, this function can be used as a view constructor instead to silence incomplete pattern warnings.

llvmPointerBlock :: LLVMPtr sym w -> SymNat sym

llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w

llvmPointerType :: IsExpr (SymExpr sym) => LLVMPtr sym w -> TypeRepr (LLVMPointerType w)

muxLLVMPtr :: 1 <= w => IsSymInterface sym => sym -> Pred sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (LLVMPtr sym w)

Mux function specialized to LLVM pointer values.

llvmPointer_bv :: IsSymInterface sym => sym -> SymBV sym w -> IO (LLVMPtr sym w)

Convert a raw bitvector value into an LLVM pointer value.

mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w)

Produce the distinguished null pointer value.

Concretization

concBV :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> SymBV sym w -> IO (SymBV sym w)

concPtr :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue sym (LLVMPointerType w) -> IO (RegValue sym (LLVMPointerType w))

concPtr' :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue' sym (LLVMPointerType w) -> IO (RegValue' sym (LLVMPointerType w))

Operations on valid pointers

constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> Addr -> IO (SymBV sym w)

Generate a concrete offset value from an Addr value.

ptrEq :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym)

Test whether two pointers are equal.

ptrLe :: (1 <= w, IsSymInterface sym, ?memOpts :: MemOptions) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym, Pred sym)

Test whether one pointer is less than or equal to the other.

The returned predicates assert (in this order): * the first pointer is less than or equal to the second * the comparison is valid: the pointers are to the same allocation

ptrAdd :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)

Add an offset to a pointer.

ptrDiff :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (SymBV sym w, Pred sym)

Compute the difference between two pointers. The returned predicate asserts that the pointers point into the same allocation block.

ptrSub :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)

Subtract an offset from a pointer.

ptrIsNull :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)

Test if a pointer value is the null pointer.

isGlobalPointer

Arguments

:: forall sym w. IsSymInterface sym

=> Map Natural Symbol

c.f. memImplSymbolMap

-> LLVMPtr sym w

-> Maybe Symbol

Look up a pointer in the memImplGlobalMap to see if it's a global.

This is best-effort and will only work if the pointer is fully concrete and matches the address of the global on the nose. It is used in SAWscript for friendly error messages.

isGlobalPointer'

Arguments

:: forall sym w. IsSymInterface sym

=> Map Natural Symbol

c.f. memImplSymbolMap

-> LLVMPtr sym w

-> Maybe Symbol

For when you don't know 1 <= w

Pretty printing

ppPtr :: IsExpr (SymExpr sym) => LLVMPtr sym wptr -> Doc ann

Annotation

annotatePointerBlock :: forall sym w. IsSymInterface sym => sym -> LLVMPtr sym w -> IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)

annotatePointerOffset :: forall sym w. IsSymInterface sym => sym -> LLVMPtr sym w -> IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)

Orphan instances

IsSymInterface sym => IntrinsicClass sym "LLVM_pointer"

Associated Types

type Intrinsic sym "LLVM_pointer" ctx

Methods

pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_pointer" -> CtxRepr ctx -> Intrinsic sym "LLVM_pointer" ctx -> IO (Intrinsic sym "LLVM_pointer" ctx)

abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_pointer" -> CtxRepr ctx -> Intrinsic sym "LLVM_pointer" ctx -> IO (Intrinsic sym "LLVM_pointer" ctx)

muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_pointer" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "LLVM_pointer" ctx -> Intrinsic sym "LLVM_pointer" ctx -> IO (Intrinsic sym "LLVM_pointer" ctx)