Module Record_cfg.Make

Parameters

Signature

val dump_html_fun : (unit -> unit) option Stdlib.ref
type t
val nb_forks : t -> int
val init : Binsec.Loader.Img.t -> Binsec.Virtual_address.t -> t
val reuse : t -> t

Reopens the file handles and empty the work list that keeps track of forks. The trace recorded is unchanged.

type context_change =
  1. | NoChange
    (*

    We remained in the same function.

    *)
  2. | EnteredFunction of string
    (*

    We entered a new function.

    *)
  3. | LeftFunction of string
    (*

    We left the current function, possibly more.

    *)
exception Visited_vertex
val next : t -> exploration_only:bool -> record_cfg:bool -> Binsec.Virtual_address.t -> unit

next trace addr adds the code address addr to the current trace trace. It returns a value of type context_change to express how the call stack is affected (according to our heuristic). If addr has been visited before, next trace addr raises the exception Visited_vertex, unless exploration_only is set.

val set_position : t -> keep_forks:bool -> Cfg_analysis.Cfg.V.t -> unit

Set the current position. Overwrites the work list that keeps track of forks. This should only be used before starting a depth-first analysis at a given address, never during analysis.

val current_position : t -> Cfg_analysis.V.t

May raise Not_found is next was never called.

val instruction_graph : t -> Cfg_analysis.Cfg.t
val call_stack_after_jump : t -> Cfg_analysis.Cfg.V.t -> Binsec.Virtual_address.t -> Cfg_analysis.V.call_stack * context_change

Given the current state and a destination address, return the call stack after a jump to that destination. The call stack reconstruction assumes that the symbols in the code represent the actual functions of every instruction.

val start_fork : t -> unit
val next_fork : t -> unit
val end_fork : t -> unit
val close : t -> ret_addr:Binsec.Virtual_address.t -> Binsec.Virtual_address.t -> graph_filename:string -> html_filename:string option -> (string, string) Stdlib.Hashtbl.t -> Binsec.Loader.Img.t -> Cfg_analysis.Cfg.t

close tr start computes the CFG (i.e. the graph of basic blocks) from the instruction graph, starting at address start using the record trace tr. The CFG is written to a Graphviz file, as well as an UML sequence diagram.

val graph_changed : t -> bool
val set_graph_changed : t -> bool -> unit
val back_edge : trace:t -> Cfg_analysis.Cfg.V.t -> Cfg_analysis.Cfg.V.t -> bool

Back edges are a relative notion. This tells whether the edge is a back edge relatively to the depth-first search memorized by trace.

val visited_instructions : t -> Binsec.Virtual_address.Set.t