| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Macaw.AbsDomain.JumpBounds.Internal
Description
NOT A PUBLIC API. This module contains the full implementation of Data.Macaw.AbsDomain.JumpBounds. It is exposed only so that the test suite can access symbols that are intentionally omitted from the public interface. Do not import this module in production code; use Data.Macaw.AbsDomain.JumpBounds instead.
Synopsis
- data RangePred (u :: Nat) = RangePred {
- rangeWidth :: !(NatRepr u)
- rangeLowerBound :: !Natural
- rangeUpperBound :: !Natural
- mkLowerBound :: forall (u :: Nat). NatRepr u -> Natural -> RangePred u
- mkUpperBound :: forall (u :: Nat). NatRepr u -> Natural -> RangePred u
- mkRangeBound :: forall (u :: Nat). NatRepr u -> Natural -> Natural -> RangePred u
- rangeNotTotal :: forall (u :: Nat). RangePred u -> Bool
- disjoinRangePred :: forall (u :: Nat). RangePred u -> RangePred u -> Maybe (RangePred u)
- data SubRange (tp :: Type) where
- disjoinSubRange :: forall (tp :: Type). SubRange tp -> SubRange tp -> Maybe (SubRange tp)
- type BlockStartRangePred arch = LocMap (ArchReg arch) SubRange
- data InitJumpBounds arch = InitJumpBounds {
- initBndsMap :: !(BlockStartStackConstraints arch)
- initRngPredMap :: !(BlockStartRangePred arch)
- initAddrPredMap :: !(Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange))
- 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)
- joinRangePredMap :: forall (r :: Type -> Type). (OrdF r, MemWidth (RegAddrWidth r)) => LocMap r SubRange -> LocMap r SubRange -> (LocMap r SubRange, Bool)
- joinAddrPredMap :: Ord k => Map k (MemVal SubRange) -> Map k (MemVal SubRange) -> (Map k (MemVal SubRange), Bool)
- 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.
disjoinRangePred :: forall (u :: Nat). RangePred u -> RangePred u -> Maybe (RangePred u) Source #
Take the union of two subranges, and return Nothing if this is
a maximum range bound.
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.Internal | |
disjoinSubRange :: forall (tp :: Type). SubRange tp -> SubRange tp -> Maybe (SubRange tp) Source #
Take the union of two subranges.
Return Nothing if range is not value.
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.
Constructors
| InitJumpBounds | |
Fields
| |
Instances
| ShowF (ArchReg arch) => Show (InitJumpBounds arch) Source # | |
Defined in Data.Macaw.AbsDomain.JumpBounds.Internal 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.Internal | |
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.
Arguments
| :: forall (r :: Type -> Type). (OrdF r, MemWidth (RegAddrWidth r)) | |
| => LocMap r SubRange | old |
| -> LocMap r SubRange | new |
| -> (LocMap r SubRange, Bool) |
Pointwise union of two range-predicate maps, returning the joined map
alongside a flag indicating whether old lost any precision in the join.
A location is present in the result iff it is present in BOTH inputs and
the union of the two ranges is not saturated. This is the lattice-theoretic
join: a fact survives iff it holds on every incoming edge. The flag is
True when some location in old is either absent from the result or
present with bounds that are strictly looser than old's.
Arguments
| :: Ord k | |
| => Map k (MemVal SubRange) | old |
| -> Map k (MemVal SubRange) | new |
| -> (Map k (MemVal SubRange), Bool) |
Pointwise union of two address-predicate maps, mirroring
joinRangePredMap: returns the joined map along with a flag indicating
whether old lost any precision.
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.Internal 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