Safe Haskell	None
Language	Haskell2010

Analysis.Pointers

Contents

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.
Pointer bases
Pointer sources

Description

Synopsis

expr_is_global_immediate :: Context -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer :: FContext -> SimpleExpr -> Bool
expr_is_maybe_local_pointer :: FContext -> SimpleExpr -> Bool
is_local_pointer_domain :: FContext -> Bool -> PointerDomain -> Bool
expr_highly_likely_pointer :: FContext -> SimpleExpr -> Bool
expr_is_highly_likely_heap_pointer :: FContext -> SimpleExpr -> Bool
is_heap_pointer_domain :: p -> PointerDomain -> Bool
necessarily_separate :: FContext -> [Char] -> SimpleExpr -> Maybe SimpleExpr -> SimpleExpr -> Maybe SimpleExpr -> Bool
necessarily_separate_no_size :: FContext -> [Char] -> SimpleExpr -> SimpleExpr -> Bool
necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool
necessarily_separate_expressions :: (Ord a, Num a) => SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_enclosed :: Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
get_pointer_domain :: FContext -> SimpleExpr -> Maybe PointerDomain
separate_pointer_domains :: FContext -> SimpleExpr -> SimpleExpr -> (Bool, Bool)
pointer_bases_separate :: FContext -> Bool -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_necessarily :: FContext -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_possibly :: FContext -> PointerBase -> PointerBase -> Bool
pointers_from_different_global_section :: (Integral a1, Integral a2) => Context -> a1 -> a2 -> Bool
bases_of_domain :: PointerDomain -> Maybe (NESet PointerBase)
get_pointer_bases :: FContext -> SimpleExpr -> Maybe (NESet PointerBase)
srcs_of_expr :: FContext -> SimpleExpr -> NESet BotSrc
srcs_of_bottyp :: FContext -> BotTyp -> NESet BotSrc
srcs_of_base :: FContext -> PointerBase -> NESet BotSrc
is_src_mem :: BotSrc -> Bool
source_sets_separate :: FContext -> Bool -> NESet BotSrc -> NESet BotSrc -> Bool
sources_separate :: FContext -> Bool -> BotSrc -> BotSrc -> Bool
sources_separate_necessarily :: FContext -> BotSrc -> BotSrc -> Bool
sources_separate_possibly :: FContext -> BotSrc -> BotSrc -> Bool

Documentation

expr_is_global_immediate :: Context -> 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 :: FContext -> SimpleExpr -> Bool Source #

Returns true if the expression has a local pointerbase

expr_is_maybe_local_pointer :: FContext -> SimpleExpr -> Bool Source #

is_local_pointer_domain :: FContext -> Bool -> PointerDomain -> Bool Source #

Returns true iff the give domain is highly likelty local to the current function

expr_highly_likely_pointer :: FContext -> SimpleExpr -> Bool Source #

Returns true if the expression has known pointerbases.

expr_is_highly_likely_heap_pointer :: FContext -> SimpleExpr -> Bool Source #

Returns true if the expression has a heap pointerbase

is_heap_pointer_domain :: p -> PointerDomain -> Bool Source #

necessarily_separate :: FContext -> [Char] -> 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 :: FContext -> [Char] -> SimpleExpr -> SimpleExpr -> Bool Source #

necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool Source #

Returns true iff the given symbolic regions are necessarily equal.

necessarily_separate_expressions :: (Ord a, Num a) => SimpleExpr -> a -> SimpleExpr -> a -> 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 a => SimpleExpr -> a -> SimpleExpr -> a -> 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.

get_pointer_domain Source #

Arguments

:: FContext	The current context
-> SimpleExpr	A symbolic expression
-> Maybe PointerDomain	A pointer domain

separate_pointer_domains :: FContext -> 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 :: FContext -> Bool -> 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 :: FContext -> PointerBase -> PointerBase -> Bool Source #

pointer_bases_separate_possibly :: FContext -> PointerBase -> PointerBase -> Bool Source #

pointers_from_different_global_section :: (Integral a1, Integral a2) => Context -> a1 -> a2 -> 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.

bases_of_domain :: PointerDomain -> Maybe (NESet PointerBase) Source #

returns the set of bases of a domain, if any

get_pointer_bases :: FContext -> SimpleExpr -> Maybe (NESet PointerBase) Source #

Returns the set of pointer bases, if any

Pointer sources

srcs_of_expr :: FContext -> SimpleExpr -> NESet BotSrc Source #

srcs_of_bottyp :: FContext -> BotTyp -> NESet BotSrc Source #

Returns the set of sources of the bottom type

srcs_of_base :: FContext -> PointerBase -> NESet BotSrc Source #

Returns the set of sources of the pointerbase

is_src_mem :: BotSrc -> Bool Source #

source_sets_separate :: FContext -> Bool -> NESet BotSrc -> NESet BotSrc -> Bool Source #

sources_separate :: FContext -> Bool -> BotSrc -> BotSrc -> Bool Source #

Two sources are inputs for separate pointers if, e.g., one of them is the stackpointer and the other a malloc-return-value.

sources_separate_necessarily :: FContext -> BotSrc -> BotSrc -> Bool Source #

sources_separate_possibly :: FContext -> BotSrc -> BotSrc -> Bool Source #