| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
WithNoAbstraction.Pointers
Contents
- Pointer Domains
- A
PointerBaseis a positive addend of a symbolic expression that likely represents a pointer. It can be a stack pointer, an immediate pointer into a section, or a pointer to a known symbol. - A source is some statepart whose initial value affects the value of the pointer.
- Pointer bases
- Pointer sources
Description
Synopsis
- data PointerDomain
- address_has_external_symbol :: (BinaryClass a, Integral a) => a -> a -> Bool
- expr_is_global_immediate :: BinaryClass bin => bin -> SimpleExpr -> Bool
- expr_is_highly_likely_local_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool
- expr_is_maybe_local_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool
- expr_is_highly_likely_global_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool
- expr_is_maybe_global_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool
- no_finit :: FInit v p
- is_local_pointer_domain :: Bool -> PointerDomain -> Bool
- is_global_pointer_domain :: Bool -> PointerDomain -> Bool
- expr_highly_likely_pointer :: BinaryClass bin => bin -> FInit SValue SPointer -> SimpleExpr -> Bool
- necessarily_separate :: BinaryClass p => p -> FInit SValue SPointer -> String -> SimpleExpr -> Maybe SimpleExpr -> SimpleExpr -> Maybe SimpleExpr -> Bool
- necessarily_separate_no_size :: BinaryClass p => p -> FInit SValue SPointer -> String -> SimpleExpr -> SimpleExpr -> Bool
- necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool
- necessarily_separate_expressions :: (Ord b, Num b) => SimpleExpr -> b -> SimpleExpr -> b -> Bool
- necessarily_enclosed :: Integral p => SimpleExpr -> p -> SimpleExpr -> p -> Bool
- get_pointer_domain :: BinaryClass bin => bin -> FInit SValue SPointer -> SimpleExpr -> Maybe PointerDomain
- get_pointer_base_set :: BinaryClass bin => bin -> FInit SValue SPointer -> SimpleExpr -> Set PointerBase
- separate_pointer_domains :: BinaryClass p => p -> FInit SValue SPointer -> SimpleExpr -> SimpleExpr -> (Bool, Bool)
- pointer_bases_separate :: p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool
- pointer_bases_separate_necessarily :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool
- pointer_bases_separate_possibly :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool
- pointers_from_different_global_section :: (BinaryClass bin, Integral a, Integral a) => bin -> a -> a -> Bool
- srcs_of_expr :: BinaryClass t => t -> SimpleExpr -> Set BotSrc
- srcs_of_bottyp :: BinaryClass t => t -> BotTyp -> Set BotSrc
- srcs_of_base :: BinaryClass t => t -> PointerBase -> Set BotSrc
- source_sets_separate :: p -> FInit v SPointer -> Bool -> Set BotSrc -> Set BotSrc -> Bool
- sources_separate :: p -> FInit v SPointer -> Bool -> BotSrc -> BotSrc -> Bool
- sources_separate_necessarily :: p -> FInit v SPointer -> BotSrc -> BotSrc -> Bool
- sources_separate_possibly :: p -> FInit v SPointer -> BotSrc -> BotSrc -> Bool
Documentation
data PointerDomain Source #
An abstract domain for pointers
Constructors
| Domain_Bases (NESet PointerBase) | |
| Domain_Sources (NESet BotSrc) |
Instances
address_has_external_symbol :: (BinaryClass a, Integral a) => a -> a -> Bool Source #
Returns true iff a symbol is associated with the address.
expr_is_global_immediate :: BinaryClass bin => bin -> SimpleExpr -> Bool Source #
Returns true iff the expression is an immediate address falling into the range of sections of the binary
expr_is_highly_likely_local_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool Source #
Returns true if the expression has a local pointerbase
expr_is_maybe_local_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool Source #
expr_is_highly_likely_global_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool Source #
expr_is_maybe_global_pointer :: BinaryClass bin => bin -> SimpleExpr -> Bool Source #
is_local_pointer_domain :: Bool -> PointerDomain -> Bool Source #
Returns true iff the give domain is highly likely local to the current function
is_global_pointer_domain :: Bool -> PointerDomain -> Bool Source #
Returns true iff the give domain is highly likely global
expr_highly_likely_pointer :: BinaryClass bin => bin -> FInit SValue SPointer -> SimpleExpr -> Bool Source #
Returns true if the expression has known pointerbases.
necessarily_separate :: BinaryClass p => p -> FInit SValue SPointer -> String -> SimpleExpr -> Maybe SimpleExpr -> SimpleExpr -> Maybe SimpleExpr -> Bool Source #
Returns true iff the given symbolic regions are necessarily separate. TODO: add VCS, not necc
necessarily_separate_no_size :: BinaryClass p => p -> FInit SValue SPointer -> String -> SimpleExpr -> SimpleExpr -> Bool Source #
necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool Source #
Returns true iff the given symbolic regions are necessarily equal.
necessarily_separate_expressions :: (Ord b, Num b) => SimpleExpr -> b -> SimpleExpr -> b -> Bool Source #
Returns true iff the given symbolic regions are ncessarily separate.
For example:
[RSP-16,4] is separate from [RSP-12,8]
[RSP+8,4] is separate from [RSP,8]
If none of the cases apply where it can be shjown arithmetically that the expressions are separate,
we check whether the expressions can be proven separate based on their domains (see separate_pointer_domains).
necessarily_enclosed :: Integral p => SimpleExpr -> p -> SimpleExpr -> p -> Bool Source #
Returns true iff the given symbolic region is necessarily enclosed in the other.
For example:
[RSP-16,4] is enclosed in [RSP-18,8]
[RSP+4,4] is enclosed in [RSP,8]
Will return False if the expressions contain bottom.
Pointer Domains
A PointerBase is a positive addend of a symbolic expression that likely represents a pointer. It can be a stack pointer, an immediate pointer into a section, or a pointer to a known symbol.
A source is some statepart whose initial value affects the value of the pointer.
Arguments
| :: BinaryClass bin | |
| => bin | The binary |
| -> FInit SValue SPointer | The current context |
| -> SimpleExpr | A symbolic expression |
| -> Maybe PointerDomain | A pointer domain |
Arguments
| :: BinaryClass bin | |
| => bin | The binary |
| -> FInit SValue SPointer | The current context |
| -> SimpleExpr | |
| -> Set PointerBase |
separate_pointer_domains :: BinaryClass p => p -> FInit SValue SPointer -> SimpleExpr -> SimpleExpr -> (Bool, Bool) Source #
Returns true iff the two given expressions can be shown to be separate based on their domains.
Pointer bases
pointer_bases_separate :: p -> FInit v SPointer -> p -> PointerBase -> PointerBase -> Bool Source #
Two pointerbases are separate if they refer to completely different parts of the memory.
We assume Stackframe, Global address space, and Heap are separate.
Two different malloc's point to different regions.
pointer_bases_separate_necessarily :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool Source #
pointer_bases_separate_possibly :: p -> FInit v SPointer -> PointerBase -> PointerBase -> Bool Source #
pointers_from_different_global_section :: (BinaryClass bin, Integral a, Integral a) => bin -> a -> a -> Bool Source #
Returns true iff the two given expressions have global pointerbases in different segments/sections of the binary. We do not assume that such pointers are separate, but do assert it.
Pointer sources
srcs_of_expr :: BinaryClass t => t -> SimpleExpr -> Set BotSrc Source #
srcs_of_bottyp :: BinaryClass t => t -> BotTyp -> Set BotSrc Source #
Returns the set of sources of the bottom type
srcs_of_base :: BinaryClass t => t -> PointerBase -> Set BotSrc Source #
Returns the set of sources of the pointerbase