Safe Haskell	None
Language	Haskell2010

Data.Macaw.AbsDomain.JumpBounds

Contents

Initial jump bounds
IntraJumpbounds
Jump Targets

Description

This module defines a relational abstract domain for tracking bounds checks emitted by the compiler on registers and stack location. This is built on top of an underlying stack pointer tracking domain so that we can include checks on stack locations and maintain constraints between known equivalent values.

Synopsis

data InitJumpBounds arch
initBndsMap :: InitJumpBounds arch -> BlockStartStackConstraints arch
functionStartBounds :: RegisterInfo (ArchReg arch) => InitJumpBounds arch
ppInitJumpBounds :: ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc ann]
joinInitialBounds :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr) => InitJumpBounds arch -> InitJumpBounds arch -> Maybe (InitJumpBounds arch)
data IntraJumpBounds arch ids
blockEndBounds :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch), ShowF (ArchReg arch), FoldableFC (ArchFn arch)) => InitJumpBounds arch -> [Stmt arch ids] -> IntraJumpBounds arch ids
postCallBounds :: RegisterInfo (ArchReg arch) => CallParams (ArchReg arch) -> IntraJumpBounds arch ids -> RegState (ArchReg arch) (Value arch ids) -> InitJumpBounds arch
postJumpBounds :: RegisterInfo (ArchReg arch) => IntraJumpBounds arch ids -> RegState (ArchReg arch) (Value arch ids) -> InitJumpBounds arch
data BranchBounds arch
- = InfeasibleBranch
- | TrueFeasibleBranch !(InitJumpBounds arch)
- | FalseFeasibleBranch !(InitJumpBounds arch)
- | BothFeasibleBranch !(InitJumpBounds arch) !(InitJumpBounds arch)
postBranchBounds :: RegisterInfo (ArchReg arch) => IntraJumpBounds arch ids -> RegState (ArchReg arch) (Value arch ids) -> Value arch ids BoolType -> BranchBounds arch
unsignedUpperBound :: forall arch ids (tp :: Type). (OrdF (ArchReg arch), ShowF (ArchReg arch), RegisterInfo (ArchReg arch)) => IntraJumpBounds arch ids -> Value arch ids tp -> Maybe Natural
type IntraJumpTarget arch = (ArchSegmentOff arch, AbsBlockState (ArchReg arch), InitJumpBounds arch)

Initial jump bounds

data InitJumpBounds arch Source #

Bounds for a function as the start of a block.

Instances

Instances details

ShowF (ArchReg arch) => Show (InitJumpBounds arch) Source #
Instance details Defined in Data.Macaw.AbsDomain.JumpBounds Methods showsPrec :: Int -> InitJumpBounds arch -> ShowS # show :: InitJumpBounds arch -> String # showList :: [InitJumpBounds arch] -> ShowS #
ShowF (ArchReg arch) => Pretty (InitJumpBounds arch) Source #
Instance details Defined in Data.Macaw.AbsDomain.JumpBounds Methods pretty :: InitJumpBounds arch -> Doc ann prettyList :: [InitJumpBounds arch] -> Doc ann

initBndsMap :: InitJumpBounds arch -> BlockStartStackConstraints arch Source #

functionStartBounds :: RegisterInfo (ArchReg arch) => InitJumpBounds arch Source #

Bounds at start of function.

ppInitJumpBounds :: ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc ann] Source #

Pretty print jump bounds.

joinInitialBounds :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr) => InitJumpBounds arch -> InitJumpBounds arch -> Maybe (InitJumpBounds arch) Source #

Return a jump bounds that implies both input bounds, or Nothing if every fact in the old bounds is implied by the new bounds.

IntraJumpbounds

data IntraJumpBounds arch ids Source #

This tracks bounds on a block during execution.

Instances

Instances details

ShowF (ArchReg arch) => Pretty (IntraJumpBounds arch ids) Source #
Instance details Defined in Data.Macaw.AbsDomain.JumpBounds Methods pretty :: IntraJumpBounds arch ids -> Doc ann prettyList :: [IntraJumpBounds arch ids] -> Doc ann

blockEndBounds :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch), ShowF (ArchReg arch), FoldableFC (ArchFn arch)) => InitJumpBounds arch -> [Stmt arch ids] -> IntraJumpBounds arch ids Source #

Create bounds for end of block.

postCallBounds :: RegisterInfo (ArchReg arch) => CallParams (ArchReg arch) -> IntraJumpBounds arch ids -> RegState (ArchReg arch) (Value arch ids) -> InitJumpBounds arch Source #

Return the index bounds after a function call.

postJumpBounds Source #

Arguments

:: RegisterInfo (ArchReg arch)
=> IntraJumpBounds arch ids	Bounds at end of this state.
-> RegState (ArchReg arch) (Value arch ids)	Register values at start of next state.
-> InitJumpBounds arch

Bounds for block after jump

data BranchBounds arch Source #

Constructors

InfeasibleBranch
TrueFeasibleBranch !(InitJumpBounds arch)
FalseFeasibleBranch !(InitJumpBounds arch)
BothFeasibleBranch !(InitJumpBounds arch) !(InitJumpBounds arch)

postBranchBounds Source #

Arguments

:: RegisterInfo (ArchReg arch)
=> IntraJumpBounds arch ids	Bounds just before jump
-> RegState (ArchReg arch) (Value arch ids)	Register values at start of next state.
-> Value arch ids BoolType	Branch condition
-> BranchBounds arch

unsignedUpperBound :: forall arch ids (tp :: Type). (OrdF (ArchReg arch), ShowF (ArchReg arch), RegisterInfo (ArchReg arch)) => IntraJumpBounds arch ids -> Value arch ids tp -> Maybe Natural Source #

This returns a natural number with a computed upper bound for the value or Nothing if no explicit bound was inferred.

Jump Targets

type IntraJumpTarget arch = (ArchSegmentOff arch, AbsBlockState (ArchReg arch), InitJumpBounds arch) Source #

This type is used to represent the location to return to *within a function* after executing an architecture-specific terminator instruction.

The MemSegmentOff is the address to jump to next (within the function)
The AbsBlockState is the abstract state to use at the start of the block returned to (reflecting any changes made by the architecture-specific terminator)
The InitJumpBounds is a collection of relations between values in registers and on the stack that should hold (see postCallBounds for to construct this in the common case)

Note: This is defined here (despite not being used here) to avoid import cycles elsewhere