Safe Haskell	None
Language	Haskell2010

Data.Pointers

Description

Synopsis

data FContext = FContext {
- f_ctxt :: Context
- f_entry :: Int
- f_name :: String
- f_init :: FInit
}
mk_fcontext :: Context -> Int -> FContext
get_pointer_domain :: FContext -> SimpleExpr -> PointerDomain
expr_highly_likely_pointer :: FContext -> SimpleExpr -> Bool
expr_is_global_pointer :: FContext -> SimpleExpr -> Bool
expr_is_highly_likely_local_pointer :: FContext -> SimpleExpr -> Bool
expr_is_global_immediate :: Context -> SimpleExpr -> Bool
srcs_of_expr :: FContext -> SimpleExpr -> Set BotSrc
srcs_of_exprs :: FContext -> [SimpleExpr] -> Set BotSrc
is_known_source :: BotSrc -> Bool
join_exprs :: [Char] -> FContext -> [SimpleExpr] -> SimpleExpr
join_single :: FContext -> SimpleExpr -> SimpleExpr
separate_pointer_domains :: (Integral a1, Integral a2) => FContext -> Bool -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool
pointer_bases_separate_necessarily :: FContext -> PointerBase -> PointerBase -> Bool
pointer_bases_separate_possibly :: FContext -> PointerBase -> PointerBase -> Bool
sources_separate_necessarily :: FContext -> BotSrc -> BotSrc -> Bool
sources_separate_possibly :: FContext -> BotSrc -> BotSrc -> Bool
necessarily_equal :: SimpleExpr -> SimpleExpr -> Bool
necessarily_equal_stateparts :: StatePart -> StatePart -> Bool
necessarily_separate :: Integral a => FContext -> SimpleExpr -> a -> SimpleExpr -> a -> Bool
necessarily_separate_stateparts :: FContext -> StatePart -> StatePart -> Bool
necessarily_enclosed :: Integral a => SimpleExpr -> a -> SimpleExpr -> a -> Bool
unfold_non_determinism :: FContext -> SimpleExpr -> [SimpleExpr]
trim_expr :: FContext -> SimpleExpr -> SimpleExpr

Documentation

data FContext Source #

The context augmented with information on the current function

Constructors

FContext
Fields f_ctxt :: Context The context f_entry :: Int The entry address of the current function f_name :: String The name of the current function f_init :: FInit The initialization of the current function

Instances

Instances details

Propagator FContext Pred Source #
Instance details Defined in Analysis.SymbolicExecution Methods tau :: FContext -> [Instruction] -> Maybe [Instruction] -> Pred -> (Pred, Set VerificationCondition) Source # join :: FContext -> Pred -> Pred -> Pred Source # implies :: FContext -> Pred -> Pred -> Bool Source #

mk_fcontext :: Context -> Int -> FContext Source #

get_pointer_domain Source #

Arguments

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

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

Returns true if the expression has known pointerbases.

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

Returns true if the expression has a global pointerbase.

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

Returns true if the expression has a local pointerbase, and no others.

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

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

Returns the set of sources (inputs used to compute the expression) of an expression.

srcs_of_exprs :: FContext -> [SimpleExpr] -> Set BotSrc Source #

Returns the set of sources (state parts used to compute the expression) of two expressions.

is_known_source :: BotSrc -> Bool Source #

join_exprs :: [Char] -> FContext -> [SimpleExpr] -> SimpleExpr Source #

join_single :: FContext -> SimpleExpr -> SimpleExpr Source #

Abstraction for a single expression, even if the expression is concrete.

separate_pointer_domains :: (Integral a1, Integral a2) => FContext -> Bool -> SimpleExpr -> a1 -> SimpleExpr -> a2 -> Bool Source #

Returns true iff the two given expressions can be shown to be separate.

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

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

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

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

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

Returns true iff the given symbolic regions are necessarily equal. For example: [RSP-16,4] is enclosed in [RSP-16,4]

Will return False if the expressions contain bottom.

necessarily_equal_stateparts :: StatePart -> StatePart -> Bool Source #

Returns true iff the given symbolic stateparts are necessarily equal.

necessarily_separate :: Integral a => FContext -> 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_separate_stateparts :: FContext -> StatePart -> StatePart -> Bool Source #

Returns true iff the given symbolic stateparts are necessarily separate.

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.

unfold_non_determinism :: FContext -> SimpleExpr -> [SimpleExpr] Source #

Unfold an expression with non-determinisism to a list of expressions. Keep an eye on the produced size, as this may cause blow-up.

trim_expr :: FContext -> SimpleExpr -> SimpleExpr Source #

If the size of an expression becomes too large, we simply turn it into Bottom.