Module `Analyze.Create`Source

Parameters

Signature

Sourcemodule Dba2CodexC : sig ... end

Sourceval results_tbl : (string, string) Hashtbl.t

Sourcemodule Arch : sig ... end

Sourcemodule Dba2CState : sig ... end

Sourcemodule Record_cfg : sig ... end

Sourcemodule Settings : sig ... end

Sourcemodule Addr_tbl = Hooks.Addr_tbl

Sourcemodule Cfg = Cfg_analysis.Cfg

Sourcemodule Dhunk_regex = Dhunk_analysis.Dhunk_regex

Sourceval ret_special_address : Z.t

Sourceval ret_addr : Binsec.Virtual_address.t

Sourceval exploration_result : Dba2CState.State.t option ref

Utility functions. *

Sourceval find_opt : (unit -> 'a) -> 'a option

Sourcemodule Dhunk_regex_hash : sig ... end

Sourcemodule Dhunk_regex_tbl : sig ... end

Source

val do_regex : 
  locid:'a Syntax_tree.Location_identifier.t ->
  Binsec.Dhunk.t ->
  Dba2CState.State.t Dhunk_regex_tbl.t ->
  Dhunk_regex_tbl.key ->
  Dba2CState.State.t option

Sourceval filter_map : ('a -> 'b option) -> 'a list -> 'b list

Source

val transfer_dhunk : 
  locid:'a Syntax_tree.Location_identifier.t ->
  Binsec.Dhunk.t ->
  Dba2CState.State.t ->
  (Binsec.Virtual_address.t * Dba2CState.State.t) list

Sourceval instr_cache : Binsec.Instruction.t Addr_tbl.t

Sourceval decode_instr : Addr_tbl.key -> Binsec.Instruction.t

Sourcemodule Addr_map : sig ... end

Sourceval check_return_type : Dba2CState.State.t -> TypedC.typ option -> unit

Source

val transfer_instruction_nostub : 
  Addr_tbl.key ->
  Dba2CState.State.t ->
  Dba2CState.State.t Addr_map.t

Source

val transfer_instruction : 
  Binsec.Virtual_address.t ->
  Record_cfg.t ->
  Dba2CState.State.t ->
  Record_cfg.t * Dba2CState.State.t Addr_map.t

Source

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

Source

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

Source

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.

Source

val analyze_address : 
  Dba2CState.State.t ->
  Record_cfg.t ->
  Binsec.Virtual_address.t ->
  unit

Source

val analyze_address' : 
  Dba2CState.State.t ->
  Record_cfg.t ->
  Binsec.Virtual_address.t ->
  unit

Sourceexception Recursive_call

Sourceval destination : ('a * 'b) Codex.Fixpoint.Regex.tagged_regex -> 'b

Sourcemodule Regex_tbl_0 : sig ... end

Sourcemodule Regex_tbl : sig ... end

Source

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 ->
  Binsec_codex_lib.Cfg_analysis.Cfg.V.t ->
  unit

Source

val analyze_regex : 
  Dba2CState.State.t Regex_tbl.t ->
  Dba2CState.State.Domain.Context.t ->
  Record_cfg.t ->
  Regex_tbl.key ->
  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.

Sourceval find_end_nodes : Cfg.t -> Cfg.vertex -> Cfg.vertex list

Sourceval catch_exc : string -> (unit -> 'a) -> (unit -> 'a) -> 'a

Sourcemodule Wto_cfg = Cfg_analysis.Wto

Sourcemodule Reduce_cfg = Cfg_analysis.Reduce

Sourcemodule G' : sig ... end

Sourcemodule OutputCfg : sig ... end

Source

val setup_entrypoint : 
  Binsec.Loader.Img.t ->
  int ->
  Dba2CState.State.t ->
  Binsec.Virtual_address.t * Record_cfg.t * Dba2CState.State.t Regex_tbl.t

Source

val analyze_path_expression : 
  Dba2CState.State.t Regex_tbl.t ->
  Dba2CState.State.t ->
  Record_cfg.t ->
  Cfg.t ->
  Cfg.vertex ->
  Regex_tbl.key ->
  unit

Source

val compute_fixpoint : 
  string ->
  string option ->
  (string, string) Hashtbl.t ->
  Binsec.Loader.Img.t ->
  Dba2CState.State.t ->
  Binsec.Virtual_address.t ->
  Record_cfg.t ->
  Dba2CState.State.t Regex_tbl.t ->
  bool

Sourceval report_graph_informations : Cfg.t -> unit

Sourceval report_instruction_informations : Cfg.t -> unit

Sourceval report_results : Record_cfg.t -> unit

Source

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

Source

val analyze : 
  Binsec.Loader.Img.t ->
  int ->
  Dba2CState.State.t ->
  string ->
  Addr_tbl.key option ->
  string option ->
  (string, string) Hashtbl.t ->
  (Binsec.Virtual_address.Set.t * Binsec.Virtual_address.Set.t)
  * Dba2CState.State.t option
  * Binsec.Virtual_address.Set.t

Source

val interprete_concrete : 
  Binsec.Loader.Img.t ->
  int ->
  Dba2CState.State.t ->
  string ->
  string option ->
  (string, string) Hashtbl.t ->
  (Binsec.Virtual_address.Set.t * Binsec.Virtual_address.Set.t)
  * Dba2CState.State.t option
  * Binsec.Virtual_address.Set.t

Sourceval list_init : int -> (int -> 'a) -> 'a list

Sourceval cpu_sp : Binsec.Virtual_address.t ref list

Source

module ReadMem : 
  Heap_typing.MEMORY
    with type t = Dba2CodexC.Domain.Context.t * Dba2CState.State.t

Sourcemodule Heap_typechecker : sig ... end

Source

val add_stack_arg : 
  int ->
  Types.TypedC.typ ->
  Dba2CState.State.t ->
  Dba2CState.State.t

Source

val add_stack_arg_value : 
  int ->
  Dba2CodexC.Domain.binary ->
  Dba2CState.State.t ->
  Dba2CState.State.t

Sourceval add_stack_return : Dba2CState.State.t -> Dba2CState.State.t

Source

val populate_stack_with_args : 
  Types.TypedC.typ list ->
  Dba2CState.State.t ->
  Dba2CState.State.t

Source

val populate_globals_with_types : 
  (Z.t * TypedC.typ) list ->
  Dba2CState.State.t ->
  Dba2CState.State.t

Source

val populate_globals_with_symbols : 
  (string * TypedC.typ) list ->
  Dba2CodexC.Domain.Context.t ->
  unit

Source

val populate_hook : 
  (Binsec.Virtual_address.t
   * [> `nop
     | `return_unknown of Types.TypedC.typ
     | `skip_to of Binsec.Virtual_address.t
     | `stop ])
    list ->
  unit

Sourceval set_mmio : (int * int) list -> Dba2CState.State.t -> Dba2CState.State.t

Sourceval fresh_int : unit -> int

Sourceval fresh_symbol : unit -> string

Source

val initial_function_args_ret_types : 
  Codex.Types.TypedC.typ ->
  Dba2CodexC.Domain.Context.t ->
  Codex.Types.TypedC.typ list * Codex.Types.TypedC.typ

package binsec_codex

Module Analyze.CreateSource

Parameters

Signature

Module `Analyze.Create`Source