package bap-std

  1. Overview
  2. Docs
package bap-std
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

empty is an empty graph

val nodes : t -> node Regular.Std.seq

nodes g returns all nodes of graph g in an unspecified order

val edges : t -> edge Regular.Std.seq

edges g returns all edges of graph g in an unspecified order

val is_directed : bool

is_directed is true if graph is a directed graph.

val number_of_edges : t -> int

number_of_edges g returns the size of a graph g.

val number_of_nodes : t -> int

number_of_nodes g returns the order of a graph g

All graphs provides a common interface for any opaque data structure

include Regular.Std.Opaque.S with type t := t
include Core_kernel.Comparable.S with type t := t
include Base.Comparable.S with type t := t
include Base.Comparisons.S with type t := t
include Base.Comparisons.Infix with type t := t
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

ascending is identical to compare. descending x y = ascending y x. These are intended to be mnemonic when used like List.sort ~compare:ascending and List.sort ~cmp:descending, since they cause the list to be sorted in ascending or descending order, respectively.

val descending : t -> t -> int
val between : t -> low:t -> high:t -> bool

between t ~low ~high means low <= t <= high

val clamp_exn : t -> min:t -> max:t -> t

clamp_exn t ~min ~max returns t', the closest value to t such that between t' ~low:min ~high:max is true.

Raises if not (min <= max).

val clamp : t -> min:t -> max:t -> t Base.Or_error.t
include Base.Comparator.S with type t := t
type comparator_witness
val validate_lbound : min:t Core.Maybe_bound.t -> t Validate.check
val validate_ubound : max:t Core.Maybe_bound.t -> t Validate.check
val validate_bound : min:t Core.Maybe_bound.t -> max:t Core.Maybe_bound.t -> t Validate.check
include Core_kernel.Hashable.S with type t := t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t -> t -> int
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : Base.Hash.state -> t -> Base.Hash.state
val hash : t -> Base.Hash.hash_value
val hashable : t Base.Hashable.t
module Table : Core.Hashtbl.S with type key = t
module Hash_set : Core.Hash_set.S with type elt = t
module Hash_queue : Core.Hash_queue.S with type key = t

All graphs are printable.

include Regular.Std.Printable.S with type t := t
val to_string : t -> string

to_string x returns a human-readable representation of x

val str : unit -> t -> string

str () t is formatted output function that matches "%a" conversion format specifier in functions, that prints to string, e.g., sprintf, failwithf, errorf and, surprisingly all Lwt printing function, including Lwt_io.printf and logging (or any other function with type ('a,unit,string,...) formatN`. Example:

Or_error.errorf "type %a is not valid for %a"
  Type.str ty Exp.str exp
val pps : unit -> t -> string

synonym for str

val ppo : Core_kernel.Out_channel.t -> t -> unit

will print to a standard output_channel, useful for using in printf, fprintf, etc.

val pp_seq : Format.formatter -> t Core_kernel.Sequence.t -> unit

prints a sequence of values of type t

this will include pp function from Core that has type t printer, and can be used in Format.printf family of functions

include Core_kernel.Pretty_printer.S with type t := t
val pp : Base.Formatter.t -> t -> unit