package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (21)

Authors

  1. A
    Adel Djoudi
  2. B
    Benoit Boero
  3. B
    Benjamin Farinier
  4. C
    Chakib Foulani
  5. D
    Dorian Lesbre
  6. F
    Frédéric Recoules
  7. G
    Guillaume Girol
  8. J
    Josselin Feist
  9. L
    Lesly-Ann Daniel
  10. M
    Mahmudul Faisal Al Ameen
  11. M
    Manh-Dung Nguyen
  12. M
    Mathéo Vergnolle
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.11.2.tbz
sha256=b758f3428b62a03103403196af99a5bb7df77a35afbcc5ce2d2b1fbe6d2ab36b
sha512=afa4fdf09ae0c2ab02530d674f9f2c1473d156e0438b4cb9c262ffea2d98c448251de55cd6fb176562edaae3897aeabe873ffa1ad47f861c75e1943792d90261

doc/binsec.sse/Binsec_sse/Revision/index.html

Module Binsec_sse.RevisionSource

include module type of struct include Binsec_sse_loader.Disassembly.Revision end
include Binsec_sse_loader.Ir.GRAPH
include Graph.Sig.G with type V.t = int and type E.t = int * bool * int

Graph structure

Abstract type of graphs

Vertices have type V.t and are labeled with type V.label (note that an implementation may identify the vertex with its label)

type vertex = V.t

Edges have type E.t and are labeled with type E.label. src (resp. dst) returns the origin (resp. the destination) of a given edge.

type edge = E.t
val is_directed : bool

Is this an implementation of directed graphs?

Size functions

val is_empty : t -> bool
val nb_vertex : t -> int
val nb_edges : t -> int

Degree of a vertex

val out_degree : t -> vertex -> int

out_degree g v returns the out-degree of v in g.

val in_degree : t -> vertex -> int

in_degree g v returns the in-degree of v in g.

Membership functions

val mem_vertex : t -> vertex -> bool
val mem_edge : t -> vertex -> vertex -> bool
val mem_edge_e : t -> edge -> bool
val find_edge : t -> vertex -> vertex -> edge

find_edge g v1 v2 returns the edge from v1 to v2 if it exists. Unspecified behaviour if g has several edges from v1 to v2.

val find_all_edges : t -> vertex -> vertex -> edge list

find_all_edges g v1 v2 returns all the edges from v1 to v2.

  • since ocamlgraph 1.8

Successors and predecessors

You should better use iterators on successors/predecessors (see Section "Vertex iterators").

val succ : t -> vertex -> vertex list

succ g v returns the successors of v in g.

val pred : t -> vertex -> vertex list

pred g v returns the predecessors of v in g.

Labeled edges going from/to a vertex

val succ_e : t -> vertex -> edge list

succ_e g v returns the edges going from v in g.

val pred_e : t -> vertex -> edge list

pred_e g v returns the edges going to v in g.

Graph iterators

val iter_vertex : (vertex -> unit) -> t -> unit

Iter on all vertices of a graph.

val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all vertices of a graph.

val iter_edges : (vertex -> vertex -> unit) -> t -> unit

Iter on all edges of a graph. Edge label is ignored.

val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph. Edge label is ignored.

val iter_edges_e : (edge -> unit) -> t -> unit

Iter on all edges of a graph.

val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph.

val map_vertex : (vertex -> vertex) -> t -> t

Map on all vertices of a graph.

The current implementation requires the supplied function to be injective. Said otherwise, map_vertex cannot be used to contract a graph by mapping several vertices to the same vertex. To contract a graph, use instead create, add_vertex, and add_edge.

Vertex iterators

Each iterator iterator f v g iters f to the successors/predecessors of v in the graph g and raises Invalid_argument if v is not in g. It is the same for functions fold_* which use an additional accumulator.

<b>Time complexity for ocamlgraph implementations:</b> operations on successors are in O(1) amortized for imperative graphs and in O(ln(|V|)) for persistent graphs while operations on predecessors are in O(max(|V|,|E|)) for imperative graphs and in O(max(|V|,|E|)*ln|V|) for persistent graphs.

iter/fold on all successors/predecessors of a vertex.

val iter_succ : (vertex -> unit) -> t -> vertex -> unit
val iter_pred : (vertex -> unit) -> t -> vertex -> unit
val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

iter/fold on all edges going from/to a vertex.

val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val fold_entries : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
val fold_exits : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
val iter_entries : (vertex -> unit) -> t -> unit
val iter_exits : (vertex -> unit) -> t -> unit
include Binsec_sse_loader.Ir.INSTRUMENT with type t := t and type vertex := vertex
val insert_before : t -> vertex -> ?label:Binsec_sse_loader.Ir.label -> Binsec_sse_loader.Ir.fallthrough -> unit
val insert_list_before : t -> vertex -> ?label:Binsec_sse_loader.Ir.label -> Binsec_sse_loader.Ir.fallthrough list -> unit
val insert_list_before_v : t -> vertex -> ?label:Binsec_sse_loader.Ir.label -> Binsec_sse_loader.Ir.fallthrough list -> vertex
val is_new_vertex : t -> vertex -> bool
val iter_new_vertex : (vertex -> unit) -> t -> unit