Copyright	(c) Galois Inc 2015-2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.LLVM.MemModel.Partial

Description

Synopsis

data PartLLVMVal sym where
- Err :: forall sym. Pred sym -> PartLLVMVal sym
- NoErr :: forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym
partErr :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
attachSideCondition :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> CallStack -> Pred sym -> UndefinedBehavior (RegValue' sym) -> PartLLVMVal sym -> IO (PartLLVMVal sym)
attachMemoryError :: forall (w :: Natural) sym. (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => sym -> Pred sym -> MemoryOp sym w -> MemoryErrorReason -> PartLLVMVal sym -> IO (PartLLVMVal sym)
assertSafe :: IsSymBackend sym bak => bak -> PartLLVMVal sym -> IO (LLVMVal sym)
data MemoryError sym where
- MemoryError :: forall (w :: Natural) sym. 1 <= w => MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
totalLLVMVal :: IsExprBuilder sym => sym -> LLVMVal sym -> PartLLVMVal sym
bvConcat :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
consArray :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
appendArray :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
mkArray :: (IsExprBuilder sym, IsSymInterface sym) => sym -> StorageType -> Vector (PartLLVMVal sym) -> IO (PartLLVMVal sym)
mkStruct :: IsExprBuilder sym => sym -> Vector (Field StorageType, PartLLVMVal sym) -> IO (PartLLVMVal sym)
type HasLLVMAnn sym = ?recordLLVMAnnotation :: CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()
type LLVMAnnMap sym = Map (BoolAnn sym) (CallStack, BadBehavior sym)
newtype BoolAnn sym = BoolAnn (SymAnnotation sym BaseBoolType)
annotateME :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym)
annotateUB :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> CallStack -> UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym)
ptrToBv :: forall sym bak (w :: Nat). IsSymBackend sym bak => bak -> SimErrorReason -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv :: forall sym bak (w :: Nat). IsSymBackend sym bak => bak -> LLVMPtr sym w -> IO (SymBV sym w)
floatToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
doubleToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
fp80ToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToDouble :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToFloat :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToX86_FP80 :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
selectHighBv :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym)
selectLowBv :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym)
arrayElt :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Natural -> StorageType -> Natural -> PartLLVMVal sym -> IO (PartLLVMVal sym)
fieldVal :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Vector (Field StorageType) -> Int -> PartLLVMVal sym -> IO (PartLLVMVal sym)
muxLLVMVal :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> Pred sym -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
data CexExplanation sym (tp :: BaseType) where
- NoExplanation :: forall sym (tp :: BaseType). CexExplanation sym tp
- DisjOfFailures :: forall sym. [(CallStack, BadBehavior sym)] -> CexExplanation sym 'BaseBoolType
explainCex :: forall t (st :: Type -> Type) fs sym. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => sym -> LLVMAnnMap sym -> Maybe (GroundEvalFn t) -> IO (Pred sym -> IO (CexExplanation sym BaseBoolType))

Documentation

data PartLLVMVal sym where Source #

Either an LLVMValue paired with a tree of predicates explaining just when it is actually valid, or a type mismatch.

Constructors

Err :: forall sym. Pred sym -> PartLLVMVal sym
NoErr :: forall sym. Pred sym -> LLVMVal sym -> PartLLVMVal sym

partErr :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym) Source #

attachSideCondition :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> CallStack -> Pred sym -> UndefinedBehavior (RegValue' sym) -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

attachMemoryError :: forall (w :: Natural) sym. (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => sym -> Pred sym -> MemoryOp sym w -> MemoryErrorReason -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

assertSafe :: IsSymBackend sym bak => bak -> PartLLVMVal sym -> IO (LLVMVal sym) Source #

Take a partial value and assert its safety

data MemoryError sym where Source #

Constructors

MemoryError :: forall (w :: Natural) sym. 1 <= w => MemoryOp sym w -> MemoryErrorReason -> MemoryError sym

totalLLVMVal :: IsExprBuilder sym => sym -> LLVMVal sym -> PartLLVMVal sym Source #

An LLVMVal which is always valid.

bvConcat :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Concatenate partial LLVM bitvector values. The least-significant (low) bytes are given first. The allocation block number of each argument is asserted to equal 0, indicating non-pointers.

consArray :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Cons an element onto a partial LLVM array value.

appendArray :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Append two partial LLVM array values.

mkArray :: (IsExprBuilder sym, IsSymInterface sym) => sym -> StorageType -> Vector (PartLLVMVal sym) -> IO (PartLLVMVal sym) Source #

Make a partial LLVM array value.

It returns Err if any of the elements of the vector are Err. Otherwise, the Pred on the returned NoErr value is the And of all the assertions on the values.

mkStruct :: IsExprBuilder sym => sym -> Vector (Field StorageType, PartLLVMVal sym) -> IO (PartLLVMVal sym) Source #

Make a partial LLVM struct value.

It returns Err if any of the struct fields are Err. Otherwise, the Pred on the returned NoErr value is the And of all the assertions on the values.

type HasLLVMAnn sym = ?recordLLVMAnnotation :: CallStack -> BoolAnn sym -> BadBehavior sym -> IO () Source #

type LLVMAnnMap sym = Map (BoolAnn sym) (CallStack, BadBehavior sym) Source #

newtype BoolAnn sym Source #

Constructors

BoolAnn (SymAnnotation sym BaseBoolType)

Instances

Instances details

IsSymInterface sym => Eq (BoolAnn sym) Source #
Instance details Defined in Lang.Crucible.LLVM.MemModel.Partial Methods (==) :: BoolAnn sym -> BoolAnn sym -> Bool # (/=) :: BoolAnn sym -> BoolAnn sym -> Bool #
IsSymInterface sym => Ord (BoolAnn sym) Source #
Instance details Defined in Lang.Crucible.LLVM.MemModel.Partial Methods compare :: BoolAnn sym -> BoolAnn sym -> Ordering # (<) :: BoolAnn sym -> BoolAnn sym -> Bool # (<=) :: BoolAnn sym -> BoolAnn sym -> Bool # (>) :: BoolAnn sym -> BoolAnn sym -> Bool # (>=) :: BoolAnn sym -> BoolAnn sym -> Bool # max :: BoolAnn sym -> BoolAnn sym -> BoolAnn sym # min :: BoolAnn sym -> BoolAnn sym -> BoolAnn sym #

annotateME :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> MemoryErrorReason -> Pred sym -> IO (Pred sym) Source #

annotateUB :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> CallStack -> UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym) Source #

ptrToBv Source #

Arguments

:: forall sym bak (w :: Nat). IsSymBackend sym bak
=> bak
-> SimErrorReason	Error to report if casting the pointer to a bitvector fails
-> LLVMPtr sym w
-> IO (SymBV sym w)

Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

projectLLVM_bv :: forall sym bak (w :: Nat). IsSymBackend sym bak => bak -> LLVMPtr sym w -> IO (SymBV sym w) Source #

Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

Note that this assertion has a very generic message, which can be unhelpful to users when it fails. Consider using ptrToBv instead.

floatToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

doubleToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

fp80ToBV :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

bvToDouble :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Convert a bitvector to a double, asserting that it is not a pointer

bvToFloat :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Convert a bitvector to a float, asserting that it is not a pointer

bvToX86_FP80 :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Convert a bitvector to an FP80 float, asserting that it is not a pointer

selectHighBv :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Select some of the most significant bytes of a partial LLVM bitvector value. The allocation block number of the argument is asserted to equal 0, indicating a non-pointer.

selectLowBv :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Select some of the least significant bytes of a partial LLVM bitvector value. The allocation block number of the argument is asserted to equal 0, indicating a non-pointer.

arrayElt :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Natural -> StorageType -> Natural -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Look up an element in a partial LLVM array value.

fieldVal :: forall sym (w :: Natural). (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Vector (Field StorageType) -> Int -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Look up a field in a partial LLVM struct value.

muxLLVMVal :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> Pred sym -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym) Source #

Mux partial LLVM values.

Will panic if the values are not structurally related. This should never happen, as we only call muxLLVMVal from inside the memory model as we read values, and the shape of values is determined by the memory type at which we read values.

data CexExplanation sym (tp :: BaseType) where Source #

Constructors

NoExplanation :: forall sym (tp :: BaseType). CexExplanation sym tp
DisjOfFailures :: forall sym. [(CallStack, BadBehavior sym)] -> CexExplanation sym 'BaseBoolType

Instances

Instances details

Semigroup (CexExplanation sym BaseBoolType) Source #
Instance details Defined in Lang.Crucible.LLVM.MemModel.Partial Methods (<>) :: CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType # sconcat :: NonEmpty (CexExplanation sym BaseBoolType) -> CexExplanation sym BaseBoolType # stimes :: Integral b => b -> CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType #

explainCex :: forall t (st :: Type -> Type) fs sym. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => sym -> LLVMAnnMap sym -> Maybe (GroundEvalFn t) -> IO (Pred sym -> IO (CexExplanation sym BaseBoolType)) Source #