Module Analyze.Create

Parameters

Signature

module Dba2CodexC : sig ... end
val results_tbl : (string, string) Stdlib.Hashtbl.t
module Arch : sig ... end
module Dba2CState : sig ... end
module Record_cfg : sig ... end
module Settings : sig ... end
module Addr_tbl = Hooks.Addr_tbl
module Cfg = Cfg_analysis.Cfg
module Dhunk_regex = Dhunk_analysis.Dhunk_regex
val ret_special_address : Z.t
val ret_addr : Binsec.Virtual_address.t
val exploration_result : Dba2CState.State.t option Stdlib.ref

Utility functions. *

val find_opt : (unit -> 'a) -> 'a option
module Dhunk_regex_hash : sig ... end
module Dhunk_regex_tbl : sig ... end
val filter_map : ('a -> 'b option) -> 'a list -> 'b list
val transfer_dhunk : locid:'a Syntax_tree.Location_identifier.t -> Binsec.Dhunk.t -> Dba2CState.State.t -> (Binsec.Virtual_address.t * Dba2CState.State.t) list
val instr_cache : Binsec.Instruction.t Addr_tbl.t
val decode_instr : Addr_tbl.key -> Binsec.Instruction.t
module Addr_map : sig ... end
val check_return_type : Dba2CState.State.t -> TypedC.typ option -> unit
val transfer_instruction_nostub : Addr_tbl.key -> Dba2CState.State.t -> Dba2CState.State.t Addr_map.t
val transfer_instruction : Binsec.Virtual_address.t -> Record_cfg.t -> Dba2CState.State.t -> Record_cfg.t * Dba2CState.State.t Addr_map.t
val transfer_from_to_generic : transfer_instruction:('a -> 'b -> 'c -> Record_cfg.t * 'd Addr_map.t) -> self: (stop_pred:'e -> Addr_map.key -> Record_cfg.t -> 'd -> Record_cfg.t * Dba2CState.State.t Addr_map.t) -> stop_pred:'e -> 'a -> 'b -> 'c -> Record_cfg.t * Dba2CState.State.t Addr_map.t
val transfer_from_to : Addr_tbl.key -> stop_pred:(Binsec.Virtual_address.t -> Record_cfg.context_change -> bool) -> Record_cfg.t -> Dba2CState.State.t -> Record_cfg.t * Dba2CState.State.t Addr_map.t
val analyze_address_nocheck : Dba2CState.State.t -> Record_cfg.t -> Binsec.Virtual_address.t -> unit

Like analyze_address but does not call next on the first, and thus will not stop if address was already visited.

val analyze_address : Dba2CState.State.t -> Record_cfg.t -> Binsec.Virtual_address.t -> unit
val analyze_address' : Dba2CState.State.t -> Record_cfg.t -> Binsec.Virtual_address.t -> unit
exception Recursive_call
val destination : ('a * 'b) Codex.Fixpoint.Regex.tagged_regex -> 'b
module Regex_tbl_0 : sig ... end
module Regex_tbl : sig ... end
val handle_successors : (Binsec.Virtual_address.t * Dba2CState.State.t) list -> Dba2CState.State.t Regex_tbl.t -> Dba2CState.State.t -> Record_cfg.t -> Cfg_analysis.CfgRegex.t -> Cfg_analysis.Cfg.V.t -> unit

Analyze a set of paths in the CFG (described by a regex) to possibly discover new edges. When that happens, the new path set is explored immediately, enriching the instruction graph by a depth-first search without merge (analyze_address). If that happens, it means that the fixpoint was not reached, and analyze_regex returns false. Otherwise, if no new instruction is discovered, a fixpoint was reached and analyze_regex returns true. Please note: The instruction at the end of the path is not analyzed by this function.

  • parameter state_table

    A table associating a path expression of an instruction to the entry state of that expression. When analyzing a regex, all intermediary regexes (i.e. expressions of subpaths) are updated in this table.

val find_end_nodes : Cfg.t -> Cfg.vertex -> Cfg.vertex list
val catch_exc : string -> (unit -> 'a) -> (unit -> 'a) -> 'a
module Wto_cfg = Cfg_analysis.Wto
module Reduce_cfg = Cfg_analysis.Reduce
module G' : sig ... end
module OutputCfg : sig ... end
val setup_entrypoint : Binsec.Loader.Img.t -> int -> Dba2CState.State.t -> Binsec.Virtual_address.t * Record_cfg.t * Dba2CState.State.t Regex_tbl.t
val analyze_path_expression : Dba2CState.State.t Regex_tbl.t -> Dba2CState.State.t -> Record_cfg.t -> Cfg.t -> Cfg.vertex -> Regex_tbl.key -> unit
val compute_fixpoint : string -> string option -> (string, string) Stdlib.Hashtbl.t -> Binsec.Loader.Img.t -> Dba2CState.State.t -> Binsec.Virtual_address.t -> Record_cfg.t -> Dba2CState.State.t Regex_tbl.t -> bool
val report_graph_informations : Cfg.t -> unit
val report_instruction_informations : Cfg.t -> unit
val report_results : Record_cfg.t -> unit
val return_final_state : Record_cfg.t -> Addr_tbl.key option -> (Binsec.Virtual_address.Set.t * Binsec.Virtual_address.Set.t) * Dba2CState.State.t option * Binsec.Virtual_address.Set.t
val analyze : Binsec.Loader.Img.t -> int -> Dba2CState.State.t -> string -> Addr_tbl.key option -> string option -> (string, string) Stdlib.Hashtbl.t -> (Binsec.Virtual_address.Set.t * Binsec.Virtual_address.Set.t) * Dba2CState.State.t option * Binsec.Virtual_address.Set.t
val interprete_concrete : Binsec.Loader.Img.t -> int -> Dba2CState.State.t -> string -> string option -> (string, string) Stdlib.Hashtbl.t -> (Binsec.Virtual_address.Set.t * Binsec.Virtual_address.Set.t) * Dba2CState.State.t option * Binsec.Virtual_address.Set.t
val list_init : int -> (int -> 'a) -> 'a list
val cpu_sp : Binsec.Virtual_address.t Stdlib.ref list
module Heap_typechecker : sig ... end
val add_stack_arg : int -> Types.TypedC.typ -> Dba2CState.State.t -> Dba2CState.State.t
val add_stack_arg_value : int -> Dba2CodexC.Domain.binary -> Dba2CState.State.t -> Dba2CState.State.t
val add_stack_return : Dba2CState.State.t -> Dba2CState.State.t
val populate_stack_with_args : Types.TypedC.typ list -> Dba2CState.State.t -> Dba2CState.State.t
val populate_globals_with_types : (Z.t * TypedC.typ) list -> Dba2CState.State.t -> Dba2CState.State.t
val populate_globals_with_symbols : (string * TypedC.typ) list -> Dba2CodexC.Domain.Context.t -> unit
val populate_hook : (Binsec.Virtual_address.t * [> `nop | `return_unknown of Types.TypedC.typ | `skip_to of Binsec.Virtual_address.t | `stop ]) list -> unit
val set_mmio : (int * int) list -> Dba2CState.State.t -> Dba2CState.State.t
val fresh_int : unit -> int
val fresh_symbol : unit -> string