package bap-std

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Graph view over IR.

This module implements a graph view on an intermediate representation of a subroutine. To create an instance of a graph, using existing subroutine use Sub.to_cfg. At any moment current sub term can be obtained using Sub.of_cfg function. This is a just a projection operation, so it doesn't take any computing time.

All Graph modification operations, like insert, remove and update in Node and Edge modules are mapped to corresponding Term operations. Also, for performance reasons, graph is augmented with auxiliary data structures, that performs most of the operations in O(log(N)) time.

Although this implements all operations of Graph interface it is recommended to use Term or Builder interfaces to build and modify underlying terms. The next few sections will clarify the behavior of a graph when it is modified using Graph interface. If you do not want to read the following sections, then better do not use this module to build your terms.

Inserting nodes

When node is inserted into a graph g all jumps of a node, that lead to blocks that are already in a graph will be represented as edges. Also, all jumps from other nodes to the inserted node, will be added as edges (assuming that this other nodes are also in the graph g). Thus inserting node can create an arbitrary number of edges, from zero to N. If jump target is not yet in the graph, then jump is not removed from a sequence of jumps of the inserted node, but just ignored.

Updating nodes

When node is updated with the same node (but possibly with different set of terms, see description of sameness) then all changes that affects control flow will be applied. For example, if jump is absent in a new version of a block, and this jump corresponds to an edge in the graph, then this edge will be removed.

Removing nodes

The node will be removed from the underlying sub term, and all edges incident to the removed node will be also removed. This will not affect jmp terms of blk terms.

Inserting edges

Edges in IR graph represents a transfer of a control flow between basic blocks. The basic block in IR is more reach, rather then a node in a graph. For example, in blk term the order of jumps matters. Jump n is taken, only if guard conditions of jumps 0 to n-1 evaluated to false (like switch statement in C language). The order of edges in a graph is unspecified. So, some precaution should be taken, to handle edge removing and inserting correctly. Each edge is labeled with abstract label, that represents the jump position in a graph.

When an edge is created it will look for corresponding jumps in source node. If there exists such jump, and it points to the destination, then it will be left untouched. If it points to a different node, then it will be fixed to point at the a given destination. If there is no position in a slot, represented by the a given label, then it will be inserted. Dummy jumps will be prepended before the inserted jump, if needed.

When an edge is inserted into the graph, then source and destination nodes are inserted or updated (depending on whether they were already present in the graph). As a result, the graph must contain at least nodes, incident to the edge, and the edge itself.

Updating edge

Updating an edge is basically the same, as updating incident nodes, a given that the edge exists in the graph.

Removing edge

Removing an edge is not symmetric with edge insertion. It doesn't remove the incident nodes, but instead removes jumps from the source node to destination. The jumps are removed accurately, so that the order (and semantics) is preserved. If the removed jump was in the middle of the sequence then it is substituted by a dummy jump with false guard.

type t
type edge
type node
module Edge : sig ... end

since in IR the order of edges defines semantics, we provide extra functions

module Node : sig ... end

IR Graph node.

include Graphlib.Std.Graph with type t := t and type node := node and type edge := edge and type Node.label = blk term and module Node := Node and module Edge := Edge
val empty : t
val nodes : t -> node Regular.Std.seq
val edges : t -> edge Regular.Std.seq
val is_directed : bool
val number_of_edges : t -> int
val number_of_nodes : t -> int
val (>=) : t -> t -> bool
val (<=) : t -> t -> bool
val (=) : t -> t -> bool
val (>) : t -> t -> bool
val (<) : t -> t -> bool
val (<>) : t -> t -> bool
val equal : t -> t -> bool
val min : t -> t -> t
val max : t -> t -> t
val ascending : t -> t -> int
val descending : t -> t -> int
val between : t -> low:t -> high:t -> bool
val clamp_exn : t -> min:t -> max:t -> t
val clamp : t -> min:t -> max:t -> t Base__.Or_error.t
type comparator_witness
val comparator : (t, comparator_witness) Base__Comparator.comparator
val validate_lbound : min:t Base__.Maybe_bound.t -> t Base__.Validate.check
val validate_ubound : max:t Base__.Maybe_bound.t -> t Base__.Validate.check
val validate_bound : min:t Base__.Maybe_bound.t -> max:t Base__.Maybe_bound.t -> t Base__.Validate.check
module Replace_polymorphic_compare : sig ... end
module Map : sig ... end
module Set : sig ... end
val compare : t -> t -> Core_kernel__.Import.int
val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
val hash : t -> Ppx_hash_lib.Std.Hash.hash_value
val hashable : t Core_kernel__.Hashtbl.Hashable.t
module Table : sig ... end
module Hash_set : sig ... end
module Hash_queue : sig ... end
val to_string : t -> string
val str : unit -> t -> string
val pps : unit -> t -> string
val ppo : Core_kernel.Out_channel.t -> t -> unit
val pp_seq : Stdlib.Format.formatter -> t Core_kernel.Sequence.t -> unit
val pp : Base__.Formatter.t -> t -> unit
OCaml

Innovation. Community. Security.