| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Analysis.Context
Contents
Description
The context stores, among others, information obtained during verification, such as CFGs, invariants, etc. (see ContextContext.
Synopsis
- data FContext = FContext {}
- mk_fcontext :: Context -> Int -> FContext
- read_binary :: String -> String -> IO (Maybe Binary)
- data CFG = CFG {
- cfg_blocks :: IntMap [Int]
- cfg_edges :: IntMap IntSet
- cfg_addr_to_blockID :: IntMap Int
- cfg_fresh :: Int
- cfg_instrs :: IntMap [Instruction]
- data JumpTable = JumpTable {}
- data Indirection
- type Indirections = IntMap Indirection
- data VerificationResult
- type Predicate = Sstate SValue SPointer
- type Invariants = IntMap Predicate
- data NodeInfo
- type Postconditions = Set (NodeInfo, Predicate)
- data PointerDomain
- data MemRelation
- data FInit = FInit (Set (StatePart, Maybe SValue)) (Map (SStatePart, SStatePart) MemRelation)
- data FReturnBehavior
- data SStatePart
- data Context_ = Context_ {
- ctxt__config :: !Config
- ctxt__verbose :: !Bool
- ctxt__syms :: !SymbolTable
- ctxt__sections :: !SectionsInfo
- ctxt__relocs :: !(Set Relocation)
- ctxt__dirname :: !String
- ctxt__name :: !String
- ctxt__start :: !Int
- ctxt__entries :: !Graph
- ctxt__cfgs :: !(IntMap CFG)
- ctxt__calls :: !(IntMap FReturnBehavior)
- ctxt__invs :: !(IntMap Invariants)
- ctxt__posts :: !(IntMap Postconditions)
- ctxt__stateparts :: !(IntMap (Set SStatePart))
- ctxt__inds :: !Indirections
- ctxt__finits :: !(IntMap FInit)
- ctxt__vcs :: !(IntMap VCS)
- ctxt__results :: !(IntMap VerificationResult)
- ctxt__recursions :: !(IntMap IntSet)
- ctxt__runningtime :: !Int64
- data Context = Context {
- ctxt_binary :: !Binary
- ctxt_ioref :: IORef (IntMap Instruction)
- ctxt_ctxt_ :: !Context_
- ctxt_config :: Context -> Config
- ctxt_verbose :: Context -> Bool
- ctxt_syms :: Context -> SymbolTable
- ctxt_sections :: Context -> SectionsInfo
- ctxt_relocs :: Context -> Set Relocation
- ctxt_dirname :: Context -> String
- ctxt_name :: Context -> String
- ctxt_start :: Context -> Int
- ctxt_entries :: Context -> Graph
- ctxt_cfgs :: Context -> IntMap CFG
- ctxt_calls :: Context -> IntMap FReturnBehavior
- ctxt_invs :: Context -> IntMap Invariants
- ctxt_posts :: Context -> IntMap Postconditions
- ctxt_stateparts :: Context -> IntMap (Set SStatePart)
- ctxt_inds :: Context -> Indirections
- ctxt_finits :: Context -> IntMap FInit
- ctxt_vcs :: Context -> IntMap VCS
- ctxt_results :: Context -> IntMap VerificationResult
- ctxt_recursions :: Context -> IntMap IntSet
- ctxt_runningtime :: Context -> Int64
- set_ctxt_syms :: SymbolTable -> Context -> Context
- set_ctxt_sections :: SectionsInfo -> Context -> Context
- set_ctxt_relocs :: Set Relocation -> Context -> Context
- set_ctxt_start :: Int -> Context -> Context
- set_ctxt_entries :: Graph -> Context -> Context
- set_ctxt_calls :: IntMap FReturnBehavior -> Context -> Context
- set_ctxt_inds :: Indirections -> Context -> Context
- set_ctxt_posts :: IntMap Postconditions -> Context -> Context
- set_ctxt_stateparts :: IntMap (Set SStatePart) -> Context -> Context
- set_ctxt_vcs :: IntMap VCS -> Context -> Context
- set_ctxt_finits :: IntMap FInit -> Context -> Context
- set_ctxt_invs :: IntMap Invariants -> Context -> Context
- set_ctxt_cfgs :: IntMap CFG -> Context -> Context
- set_ctxt_results :: IntMap VerificationResult -> Context -> Context
- set_ctxt_recursions :: IntMap IntSet -> Context -> Context
- set_ctxt_runningtime :: Int64 -> Context -> Context
- init_finit :: FInit
- init_context :: Binary -> IORef (IntMap Instruction) -> Config -> Bool -> String -> String -> Context
- purge_context :: Context -> Context_
- ctxt_symbol_table :: Context -> IntMap Symbol
- read_from_ro_datasection :: Context -> Word64 -> Int -> Maybe Word64
- read_from_datasection :: Context -> Word64 -> Int -> Maybe Word64
- is_roughly_an_address :: Context -> Word64 -> Bool
- find_section_for_address :: Context -> Word64 -> Maybe (String, String, Word64, Word64)
- find_section_ending_at :: Context -> Word64 -> Maybe (String, String, Word64, Word64)
- fetch_instruction :: Context -> Word64 -> IO (Maybe Instruction)
- pp_instruction :: Context -> Instruction -> String
- is_assertion :: VerificationCondition -> Bool
- is_precondition :: VerificationCondition -> Bool
- is_func_constraint :: VerificationCondition -> Bool
- is_functionpointers :: VerificationCondition -> Bool
- count_instructions_with_assertions :: Set VerificationCondition -> Int
- ctxt_continue_on_unknown_instruction :: Context -> Bool
- ctxt_generate_pdfs :: Context -> Bool
- ctxt_verbose_logs :: Context -> Bool
- ctxt_store_preconditions_in_L0 :: Context -> Bool
- ctxt_store_assertions_in_L0 :: Context -> Bool
- ctxt_max_time :: Context -> Int
- ctxt_max_num_of_cases :: Context -> Int
- ctxt_max_num_of_bases :: Context -> Int
- ctxt_max_num_of_sources :: Context -> Int
- ctxt_max_jump_table_size :: Context -> Int
- ctxt_max_expr_size :: Context -> Int
- ctxt_read_L0 :: String -> String -> IO Context
- address_has_instruction :: Integral a => Context -> a -> Bool
Documentation
The context augmented with information on the current function
Constructors
| FContext | |
Instances
read_binary :: String -> String -> IO (Maybe Binary) Source #
Reading a binary given a filename (ELF or MachO)
A control flow graph with blocks and edges.
A blockID (represented as an Int) is a unique identifier of a basic block.
We store basic blocks twice: once as addresses, and once as instructions.
Constructors
| CFG | |
Fields
| |
Instances
| Eq CFG Source # | |
| Show CFG Source # | |
| Generic CFG Source # | |
| Serialize CFG Source # | |
| NFData CFG Source # | |
Defined in Analysis.Context | |
| type Rep CFG Source # | |
Defined in Analysis.Context type Rep CFG = D1 ('MetaData "CFG" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "CFG" 'PrefixI 'True) ((S1 ('MetaSel ('Just "cfg_blocks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap [Int])) :*: S1 ('MetaSel ('Just "cfg_edges") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap IntSet))) :*: (S1 ('MetaSel ('Just "cfg_addr_to_blockID") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap Int)) :*: (S1 ('MetaSel ('Just "cfg_fresh") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "cfg_instrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap [Instruction])))))) | |
A jump table with : index: an operand containing a bounded index at the beginning of execution of the block bound: the bound on idx trgt: the operand containg the jump target at the end of execution of the block tbl: a table from values of idx to resulting jump targets
Constructors
| JumpTable | |
Fields
| |
Instances
| Eq JumpTable Source # | |
| Show JumpTable Source # | |
| Generic JumpTable Source # | |
| Serialize JumpTable Source # | |
| NFData JumpTable Source # | |
Defined in Analysis.Context | |
| type Rep JumpTable Source # | |
Defined in Analysis.Context type Rep JumpTable = D1 ('MetaData "JumpTable" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "JumpTable" 'PrefixI 'True) ((S1 ('MetaSel ('Just "jtbl_index") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Operand) :*: S1 ('MetaSel ('Just "jtbl_bound") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "jtbl_target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Operand) :*: S1 ('MetaSel ('Just "jtbl_table") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap Word64))))) | |
data Indirection Source #
An indirection is either a jump table or a set of resolved jump targets
Constructors
| Indirection_JumpTable JumpTable | |
| Indirection_Resolved (Set ResolvedJumpTarget) | |
| Indirection_Unresolved |
Instances
type Indirections = IntMap Indirection Source #
Per instruction address, a set of possibly resolved jump targets
data VerificationResult Source #
An enumeration indicating the result of verification over a function
Constructors
| VerificationSuccess | Function was succesfully verified |
| VerificationSuccesWithAssumptions | Function was succesfully verified, but required assertions |
| VerificationUnresolvedIndirection | Function contains an unresolved indirection |
| VerificationError String | There was some verification error, e.g., return adresss overwrite |
| Unverified | The function has not been verified. |
Instances
type Invariants = IntMap Predicate Source #
Invariants: a mapping of blockIDs to predicates
For each leaf-node in a CFG we store the following info. (TODO MOVE?)
Constructors
| Normal | The basic block behaves normally, e.g., a ret |
| UnresolvedIndirection | The basic block ends in an unresolved indirection |
| Terminal | The basic blocks ends with, e.g., a call to exit() |
Instances
| Eq NodeInfo Source # | |
| Ord NodeInfo Source # | |
Defined in Analysis.Context | |
| Show NodeInfo Source # | |
| Generic NodeInfo Source # | |
| Serialize NodeInfo Source # | |
| NFData NodeInfo Source # | |
Defined in Analysis.Context | |
| type Rep NodeInfo Source # | |
Defined in Analysis.Context type Rep NodeInfo = D1 ('MetaData "NodeInfo" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Normal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnresolvedIndirection" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Terminal" 'PrefixI 'False) (U1 :: Type -> Type))) | |
type Postconditions = Set (NodeInfo, Predicate) Source #
Postconditions: for each final block the NodeInfo and the final predicate after execution of the block
data PointerDomain Source #
An abstract domain for pointers
Constructors
| Domain_Bases (NESet PointerBase) | |
| Domain_Sources (NESet BotSrc) |
Instances
data MemRelation Source #
A function initialisation consists of a mapping of registers to symbolic pointers TODO
Instances
Constructors
| FInit (Set (StatePart, Maybe SValue)) (Map (SStatePart, SStatePart) MemRelation) |
Instances
| Eq FInit Source # | |
| Ord FInit Source # | |
| Show FInit Source # | Show function initialisation |
| Generic FInit Source # | |
| Serialize FInit Source # | |
| NFData FInit Source # | |
Defined in Analysis.Context | |
| type Rep FInit Source # | |
Defined in Analysis.Context type Rep FInit = D1 ('MetaData "FInit" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "FInit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Set (StatePart, Maybe SValue))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Map (SStatePart, SStatePart) MemRelation)))) | |
data FReturnBehavior Source #
A function call
Constructors
| Terminating | The function does never return |
| ReturningWith Predicate | The function returns withg the symbolic changes stored in the predicate |
| UnknownRetBehavior | It is unknown whether the function returns or not |
Instances
data SStatePart Source #
A symbolic state part
Instances
The context datastructure.
S: Information Statically obtained by reading from the binary
D: Information Dynamically updated during verification
Constructors
| Context_ | |
Fields
| |
Instances
Constructors
| Context | |
Fields
| |
ctxt_config :: Context -> Config Source #
ctxt_verbose :: Context -> Bool Source #
ctxt_syms :: Context -> SymbolTable Source #
ctxt_sections :: Context -> SectionsInfo Source #
ctxt_relocs :: Context -> Set Relocation Source #
ctxt_dirname :: Context -> String Source #
ctxt_start :: Context -> Int Source #
ctxt_entries :: Context -> Graph Source #
ctxt_posts :: Context -> IntMap Postconditions Source #
ctxt_stateparts :: Context -> IntMap (Set SStatePart) Source #
ctxt_inds :: Context -> Indirections Source #
ctxt_runningtime :: Context -> Int64 Source #
set_ctxt_syms :: SymbolTable -> Context -> Context Source #
set_ctxt_sections :: SectionsInfo -> Context -> Context Source #
set_ctxt_relocs :: Set Relocation -> Context -> Context Source #
set_ctxt_calls :: IntMap FReturnBehavior -> Context -> Context Source #
set_ctxt_inds :: Indirections -> Context -> Context Source #
set_ctxt_posts :: IntMap Postconditions -> Context -> Context Source #
set_ctxt_stateparts :: IntMap (Set SStatePart) -> Context -> Context Source #
set_ctxt_invs :: IntMap Invariants -> Context -> Context Source #
init_finit :: FInit Source #
intialize an empty context based on the command-line parameters
init_context :: Binary -> IORef (IntMap Instruction) -> Config -> Bool -> String -> String -> Context Source #
purge_context :: Context -> Context_ Source #
purge the context before exporting it (may save a lot of disk space)
read_from_ro_datasection Source #
Arguments
| :: Context | The context |
| -> Word64 | An address |
| -> Int | Size, i.e., the number of bytes to read |
| -> Maybe Word64 |
Reading from a read-only data section.
Reads maximally up to 8 bytes. Returns Nothing if the given address is out-of-range.
read_from_datasection Source #
Arguments
| :: Context | The context |
| -> Word64 | An address |
| -> Int | Size, i.e., the number of bytes to read |
| -> Maybe Word64 |
Reading from a writable data section.
Reads maximally up to 8 bytes. Returns Nothing if the given address is out-of-range.
is_roughly_an_address Source #
Is the immediate roughly in range to be an address?
find_section_for_address Source #
Find a section for an address (see SectionsInfo
find_section_ending_at Source #
Find a section ending at address (see SectionsInfo
Arguments
| :: Context | The context |
| -> Word64 | An address |
| -> IO (Maybe Instruction) |
Fetching an instruction
Returns Nothing if the given address is out-of-range.
Arguments
| :: Context | The context |
| -> Instruction | An instruction |
| -> String |
Pretty printing an instruction
is_assertion :: VerificationCondition -> Bool Source #
Is the given verification condition an assertion?
is_precondition :: VerificationCondition -> Bool Source #
Is the given verification condition a precondition?
is_func_constraint :: VerificationCondition -> Bool Source #
Is the given verification condition a function constraint?
is_functionpointers :: VerificationCondition -> Bool Source #
Is the given verification condition a function pointer introduction?
count_instructions_with_assertions :: Set VerificationCondition -> Int Source #
Count the number of assertions in the set of verification conditions.
ctxt_generate_pdfs :: Context -> Bool Source #
ctxt_verbose_logs :: Context -> Bool Source #
ctxt_max_time :: Context -> Int Source #
ctxt_max_num_of_cases :: Context -> Int Source #
ctxt_max_num_of_bases :: Context -> Int Source #
ctxt_max_num_of_sources :: Context -> Int Source #
ctxt_max_expr_size :: Context -> Int Source #
Read in the .L0 file from a file with the given file name. May produce an error if no L0 can be read from the file. Returns the L0 stored in the .L0 file.
address_has_instruction :: Integral a => Context -> a -> Bool Source #
Returns true iff an instruction can be fetched from the address.
Orphan instances
| Show VerificationCondition Source # | |
Methods showsPrec :: Int -> VerificationCondition -> ShowS # show :: VerificationCondition -> String # showList :: [VerificationCondition] -> ShowS # | |
| Serialize ResolvedJumpTarget Source # | |
| Serialize Relocation Source # | |
| Serialize SymbolTable Source # | |
| Serialize Symbol Source # | |
| Serialize SectionsInfo Source # | |
| Serialize VerificationCondition Source # | |
| NFData ResolvedJumpTarget Source # | |
Methods rnf :: ResolvedJumpTarget -> () # | |
| NFData Relocation Source # | |
Methods rnf :: Relocation -> () # | |
| NFData SymbolTable Source # | |
Methods rnf :: SymbolTable -> () # | |
| NFData Symbol Source # | |
| NFData SectionsInfo Source # | |
Methods rnf :: SectionsInfo -> () # | |
| NFData VerificationCondition Source # | |
Methods rnf :: VerificationCondition -> () # | |