Copyright | (c) Galois Inc 2015-2016 |
---|---|
License | BSD3 |
Maintainer | Rob Dockins <rdockins@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w)
- pattern PtrWidth :: HasPtrWidth w => w ~ w' => NatRepr w'
- withPtrWidth :: forall w a. 16 <= w => NatRepr w -> (HasPtrWidth w => a) -> a
- type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)
- type LLVMPtr sym w = RegValue sym (LLVMPointerType w)
- data SomePointer sym = forall w.1 <= w => SomePointer !(LLVMPtr sym w)
- pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty
- pattern PtrRepr :: HasPtrWidth wptr => ty ~ LLVMPointerType wptr => TypeRepr ty
- pattern SizeT :: HasPtrWidth wptr => ty ~ BVType wptr => TypeRepr ty
- pattern LLVMPointer :: SymNat sym -> SymBV sym w -> LLVMPointer sym w
- ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w
- llvmPointerView :: LLVMPtr sym w -> (SymNat sym, SymBV sym w)
- 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)
- llvmPointer_bv :: IsSymInterface sym => sym -> SymBV sym w -> IO (LLVMPtr sym w)
- mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w)
- 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))
- constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> Addr -> IO (SymBV sym w)
- ptrEq :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym)
- ptrLe :: (1 <= w, IsSymInterface sym, ?memOpts :: MemOptions) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym, Pred sym)
- ptrAdd :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
- ptrDiff :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (SymBV sym w, Pred sym)
- ptrSub :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
- ptrIsNull :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)
- isGlobalPointer :: forall sym w. IsSymInterface sym => Map Natural Symbol -> LLVMPtr sym w -> Maybe Symbol
- isGlobalPointer' :: forall sym w. IsSymInterface sym => Map Natural Symbol -> LLVMPtr sym w -> Maybe Symbol
- ppPtr :: IsExpr (SymExpr sym) => LLVMPtr sym wptr -> Doc ann
- 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)
Pointer bitwidth
type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w) Source #
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).
withPtrWidth :: forall w a. 16 <= w => NatRepr w -> (HasPtrWidth w => a) -> a Source #
Crucible pointer representation
type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w) Source #
Crucible type of pointers/bitvector values of width w
.
type LLVMPtr sym w = RegValue sym (LLVMPointerType w) Source #
Symbolic LLVM pointer or bitvector values of width w
.
data SomePointer sym Source #
A pointer with an existentially-quantified width
forall w.1 <= w => SomePointer !(LLVMPtr sym w) |
pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty Source #
This pattern synonym makes it easy to build and destruct runtime
representatives of
.LLVMPointerType
w
pattern PtrRepr :: HasPtrWidth wptr => ty ~ LLVMPointerType wptr => TypeRepr ty Source #
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 Source #
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 Source #
A pointer is a base point offset.
ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w Source #
Compute the width of a pointer value.
llvmPointerView :: LLVMPtr sym w -> (SymNat sym, SymBV sym w) Source #
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 Source #
llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w Source #
llvmPointerType :: IsExpr (SymExpr sym) => LLVMPtr sym w -> TypeRepr (LLVMPointerType w) Source #
muxLLVMPtr :: 1 <= w => IsSymInterface sym => sym -> Pred sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (LLVMPtr sym w) Source #
Mux function specialized to LLVM pointer values.
llvmPointer_bv :: IsSymInterface sym => sym -> SymBV sym w -> IO (LLVMPtr sym w) Source #
Convert a raw bitvector value into an LLVM pointer value.
mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w) Source #
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) Source #
concPtr :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue sym (LLVMPointerType w) -> IO (RegValue sym (LLVMPointerType w)) Source #
concPtr' :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue' sym (LLVMPointerType w) -> IO (RegValue' sym (LLVMPointerType w)) Source #
Operations on valid pointers
constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> Addr -> IO (SymBV sym w) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Subtract an offset from a pointer.
ptrIsNull :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym) Source #
Test if a pointer value is the null pointer.
:: forall sym w. IsSymInterface sym | |
=> Map Natural Symbol | c.f. |
-> 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.
:: forall sym w. IsSymInterface sym | |
=> Map Natural Symbol | c.f. |
-> LLVMPtr sym w | |
-> Maybe Symbol |
For when you don't know 1 <= w
Pretty printing
Annotation
annotatePointerBlock :: forall sym w. IsSymInterface sym => sym -> LLVMPtr sym w -> IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w) Source #
annotatePointerOffset :: forall sym w. IsSymInterface sym => sym -> LLVMPtr sym w -> IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w) Source #
Orphan instances
IsSymInterface sym => IntrinsicClass sym "LLVM_pointer" Source # | |
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) # |