crucible-llvm-0.6: Support for translating and executing LLVM code in Crucible
Copyright(c) Galois Inc 2018
LicenseBSD3
MaintainerLangston Barrett <lbarrett@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

Lang.Crucible.LLVM.Errors.UndefinedBehavior

Description

This module is intended to be imported qualified.

This module serves as an ad-hoc reference for the sort of undefined behaviors that the Crucible LLVM memory model is aware of. The information contained here is used in * providing helpful error messages * configuring which safety checks to perform

Disabling checks for undefined behavior does not change the behavior of any memory operations. If it is used to enable the simulation of undefined behavior, the result is that any guarantees that Crucible provides about the code essentially have an additional hypothesis: that the LLVM compiler/hardware platform behave identically to Crucible's simulator when encountering such behavior.

Synopsis

Undefined Behavior

data PtrComparisonOperator Source #

The various comparison operators you can use on pointers

Constructors

Eq 
Leq 

Instances

Instances details
Data PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PtrComparisonOperator -> c PtrComparisonOperator #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PtrComparisonOperator #

toConstr :: PtrComparisonOperator -> Constr #

dataTypeOf :: PtrComparisonOperator -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PtrComparisonOperator) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PtrComparisonOperator) #

gmapT :: (forall b. Data b => b -> b) -> PtrComparisonOperator -> PtrComparisonOperator #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r #

gmapQ :: (forall d. Data d => d -> u) -> PtrComparisonOperator -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PtrComparisonOperator -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PtrComparisonOperator -> m PtrComparisonOperator #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PtrComparisonOperator -> m PtrComparisonOperator #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PtrComparisonOperator -> m PtrComparisonOperator #

Enum PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

succ :: PtrComparisonOperator -> PtrComparisonOperator #

pred :: PtrComparisonOperator -> PtrComparisonOperator #

toEnum :: Int -> PtrComparisonOperator #

fromEnum :: PtrComparisonOperator -> Int #

enumFrom :: PtrComparisonOperator -> [PtrComparisonOperator] #

enumFromThen :: PtrComparisonOperator -> PtrComparisonOperator -> [PtrComparisonOperator] #

enumFromTo :: PtrComparisonOperator -> PtrComparisonOperator -> [PtrComparisonOperator] #

enumFromThenTo :: PtrComparisonOperator -> PtrComparisonOperator -> PtrComparisonOperator -> [PtrComparisonOperator] #

Generic PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Associated Types

type Rep PtrComparisonOperator :: Type -> Type #

Methods

from :: PtrComparisonOperator -> Rep PtrComparisonOperator x #

to :: Rep PtrComparisonOperator x -> PtrComparisonOperator #

Read PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

readsPrec :: Int -> ReadS PtrComparisonOperator #

readList :: ReadS [PtrComparisonOperator] #

readPrec :: ReadPrec PtrComparisonOperator #

readListPrec :: ReadPrec [PtrComparisonOperator] #

Show PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

showsPrec :: Int -> PtrComparisonOperator -> ShowS #

show :: PtrComparisonOperator -> String #

showList :: [PtrComparisonOperator] -> ShowS #

Eq PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

(==) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

(/=) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

Ord PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

compare :: PtrComparisonOperator -> PtrComparisonOperator -> Ordering #

(<) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

(<=) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

(>) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

(>=) :: PtrComparisonOperator -> PtrComparisonOperator -> Bool #

max :: PtrComparisonOperator -> PtrComparisonOperator -> PtrComparisonOperator #

min :: PtrComparisonOperator -> PtrComparisonOperator -> PtrComparisonOperator #

type Rep PtrComparisonOperator Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

type Rep PtrComparisonOperator = D1 ('MetaData "PtrComparisonOperator" "Lang.Crucible.LLVM.Errors.UndefinedBehavior" "crucible-llvm-0.6-JJ7tfvbGrbFFTkl5eJBN3H" 'False) (C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Leq" 'PrefixI 'False) (U1 :: Type -> Type))

data UndefinedBehavior (e :: CrucibleType -> Type) where Source #

This type is parameterized on a higher-kinded term constructor so that it can be instantiated for expressions at translation time (i.e. the Expr in LLVMGenerator), or for expressions at runtime (SymExpr).

See cite and explain for what each constructor means at the C/LLVM level.

The commented-out constructors correspond to behaviors that don't have explicit checks yet (but probably should!).

Constructors

FreeBadOffset :: 1 <= w => e (LLVMPointerType w) -> UndefinedBehavior e 
FreeUnallocated :: 1 <= w => e (LLVMPointerType w) -> UndefinedBehavior e 
DoubleFree :: 1 <= w => e (LLVMPointerType w) -> UndefinedBehavior e 
MemsetInvalidRegion :: (1 <= w, 1 <= v) => e (LLVMPointerType w) -> e (BVType 8) -> e (BVType v) -> UndefinedBehavior e

Arguments: Destination pointer, fill byte, length

ReadBadAlignment :: 1 <= w => e (LLVMPointerType w) -> Alignment -> UndefinedBehavior e

Arguments: Read destination, alignment

WriteBadAlignment :: 1 <= w => e (LLVMPointerType w) -> Alignment -> UndefinedBehavior e

Arguments: Write destination, alignment

PtrAddOffsetOutOfBounds :: 1 <= w => e (LLVMPointerType w) -> e (BVType w) -> UndefinedBehavior e 
CompareInvalidPointer :: 1 <= w => PtrComparisonOperator -> e (LLVMPointerType w) -> e (LLVMPointerType w) -> UndefinedBehavior e

Arguments: kind of comparison, the invalid pointer, the other pointer

CompareDifferentAllocs :: 1 <= w => e (LLVMPointerType w) -> e (LLVMPointerType w) -> UndefinedBehavior e

"In all other cases, the behavior is undefined" TODO: PtrComparisonOperator argument?

PtrSubDifferentAllocs :: 1 <= w => e (LLVMPointerType w) -> e (LLVMPointerType w) -> UndefinedBehavior e

"When two pointers are subtracted, both shall point to elements of the same array object"

PointerIntCast :: 1 <= w => e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e

Pointer cast to an integer type other than pointer width integers

PointerUnsupportedOp :: 1 <= w => e (LLVMPointerType w) -> String -> UndefinedBehavior e

Pointer used in an unsupported arithmetic or bitvector operation

PointerFloatCast :: 1 <= w => e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e

Pointer cast to a floating-point type

ComparePointerToBV :: 1 <= w => e (LLVMPointerType w) -> e (BVType w) -> UndefinedBehavior e

"One of the following shall hold: [...] one operand is a pointer and the other is a null pointer constant."

UDivByZero :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e

SymBV or Expr _ _ (BVType w)

SDivByZero :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e 
URemByZero :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e 
SRemByZero :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e 
SDivOverflow :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e 
SRemOverflow :: 1 <= w => e (BVType w) -> e (BVType w) -> UndefinedBehavior e 
AbsIntMin :: 1 <= w => e (BVType w) -> UndefinedBehavior e 
PoisonValueCreated :: Poison e -> UndefinedBehavior e 

Instances

Instances details
OrdC UndefinedBehavior Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

compareC :: (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y) -> UndefinedBehavior f -> UndefinedBehavior g -> Ordering #

TestEqualityC UndefinedBehavior Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

testEqualityC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> UndefinedBehavior f -> UndefinedBehavior f -> Bool #

FoldableF UndefinedBehavior Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> UndefinedBehavior e -> m #

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> UndefinedBehavior e -> b #

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> UndefinedBehavior e -> b #

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> UndefinedBehavior e -> b #

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> UndefinedBehavior e -> b #

toListF :: (forall (tp :: k). f tp -> a) -> UndefinedBehavior f -> [a] #

FunctorF UndefinedBehavior Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

fmapF :: (forall (x :: k). f x -> g x) -> UndefinedBehavior f -> UndefinedBehavior g #

TraversableF UndefinedBehavior Source # 
Instance details

Defined in Lang.Crucible.LLVM.Errors.UndefinedBehavior

Methods

traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> UndefinedBehavior e -> m (UndefinedBehavior f) #

cite :: UndefinedBehavior e -> Doc ann Source #

Which section(s) of the document prohibit this behavior?

details :: IsExpr (SymExpr sym) => UndefinedBehavior (RegValue' sym) -> [Doc ann] Source #

Pretty-print the additional information held by the constructors (for symbolic expressions)

explain :: UndefinedBehavior e -> Doc ann Source #

What happened, and why is it a problem?

This is a generic explanation that doesn't use the included data.

ppDetails :: IsExpr (SymExpr sym) => UndefinedBehavior (RegValue' sym) -> Doc ann Source #

Pretty-printer for symbolic backends

ppCitation :: UndefinedBehavior e -> [Doc ann] Source #

pp Source #

Arguments

:: (UndefinedBehavior e -> [Doc ann])

Printer for constructor data

-> UndefinedBehavior e 
-> Doc ann 

concUB :: forall sym. IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> UndefinedBehavior (RegValue' sym) -> IO (UndefinedBehavior (RegValue' sym)) Source #