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

Lang.Crucible.LLVM.MemModel.Partial

Description

Synopsis

data PartLLVMVal sym where
- Err :: Pred sym -> PartLLVMVal sym
- NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym
partErr :: (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 :: (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 :: 1 <= w => MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
totalLLVMVal :: IsExprBuilder sym => sym -> LLVMVal sym -> PartLLVMVal sym
bvConcat :: forall sym w. (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
consArray :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
appendArray :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
mkArray :: forall sym. (IsExprBuilder sym, IsSymInterface sym) => sym -> StorageType -> Vector (PartLLVMVal sym) -> IO (PartLLVMVal sym)
mkStruct :: forall sym. 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 :: (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)
projectLLVM_bv :: IsSymBackend sym bak => bak -> LLVMPtr sym w -> IO (SymBV sym w)
floatToBV :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
doubleToBV :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
fp80ToBV :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToDouble :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToFloat :: forall sym w. (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
bvToX86_FP80 :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> PartLLVMVal sym -> IO (PartLLVMVal sym)
selectHighBv :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym)
selectLowBv :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Bytes -> Bytes -> PartLLVMVal sym -> IO (PartLLVMVal sym)
arrayElt :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Natural -> StorageType -> Natural -> PartLLVMVal sym -> IO (PartLLVMVal sym)
fieldVal :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> Vector (Field StorageType) -> Int -> PartLLVMVal sym -> IO (PartLLVMVal sym)
muxLLVMVal :: forall sym. (IsSymInterface sym, HasLLVMAnn sym) => sym -> Pred sym -> PartLLVMVal sym -> PartLLVMVal sym -> IO (PartLLVMVal sym)
data CexExplanation sym (tp :: BaseType) where
- NoExplanation :: CexExplanation sym tp
- DisjOfFailures :: [(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType
explainCex :: forall t st 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 :: Pred sym -> PartLLVMVal sym
NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym

partErr :: (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 :: (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 :: 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. (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 :: (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 :: (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 :: forall sym. (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 :: forall sym. 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 :: (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 #

projectLLVM_bv :: 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.

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

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

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

bvToDouble :: (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. (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 :: (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 :: (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 :: (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 :: (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 :: (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 :: forall sym. (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 :: CexExplanation sym tp
DisjOfFailures :: [(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 fs sym. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => sym -> LLVMAnnMap sym -> Maybe (GroundEvalFn t) -> IO (Pred sym -> IO (CexExplanation sym BaseBoolType)) Source #