| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Macaw.AbsDomain.JumpBounds
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 RangePred (u :: Nat) = RangePred {
- rangeWidth :: !(NatRepr u)
- rangeLowerBound :: !Natural
- rangeUpperBound :: !Natural
- rangeNotTotal :: forall (u :: Nat). RangePred u -> Bool
- data SubRange (tp :: Type) where
- type BlockStartRangePred arch = LocMap (ArchReg arch) SubRange
- data InitJumpBounds arch
- initBndsMap :: InitJumpBounds arch -> BlockStartStackConstraints arch
- initRngPredMap :: InitJumpBounds arch -> BlockStartRangePred 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)
Range predicates
data RangePred (u :: Nat) Source #
A lower and or upper bound on a value when the value is interpreted as an unsigned integer.
Constructors
| RangePred |
|
Fields
| |
rangeNotTotal :: forall (u :: Nat). RangePred u -> Bool Source #
Return true if range does not include whole domain.
data SubRange (tp :: Type) where Source #
This indicates a range predicate on a selected number of bits.
Constructors
| SubRange :: forall (u :: Nat) (w :: Nat). u <= w => !(RangePred u) -> SubRange ('BVType w) |
Instances
| Pretty (SubRange tp) Source # | |
Defined in Data.Macaw.AbsDomain.JumpBounds | |
type BlockStartRangePred arch = LocMap (ArchReg arch) SubRange Source #
Constraints on start of block
Initial jump bounds
data InitJumpBounds arch Source #
Bounds for a function as the start of a block.
Instances
| ShowF (ArchReg arch) => Show (InitJumpBounds arch) Source # | |
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 # | |
Defined in Data.Macaw.AbsDomain.JumpBounds | |
initBndsMap :: InitJumpBounds arch -> BlockStartStackConstraints arch Source #
initRngPredMap :: InitJumpBounds arch -> BlockStartRangePred 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
| ShowF (ArchReg arch) => Pretty (IntraJumpBounds arch ids) Source # | |
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.
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) |
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
MemSegmentOffis the address to jump to next (within the function) - The
AbsBlockStateis the abstract state to use at the start of the block returned to (reflecting any changes made by the architecture-specific terminator) - The
InitJumpBoundsis a collection of relations between values in registers and on the stack that should hold (seepostCallBoundsfor to construct this in the common case)
Note: This is defined here (despite not being used here) to avoid import cycles elsewhere