Module Cfg.AstSource

Extends the simple Universal language with Control Flow Graphs.

Graph types

Sourcemodule Loc : sig ... end
Sourcemodule TagLoc : sig ... end
Sourcemodule Range : sig ... end
Sourcemodule Port : sig ... end
module LocSet : sig ... end
module LocMap : sig ... end
module LocHash : sig ... end
module TagLocSet : sig ... end
module TagLocMap : sig ... end
module TagLocHash : sig ... end
module RangeSet : sig ... end
module RangeMap : sig ... end
module RangeHash : sig ... end
Sourcemodule CFG_Param : sig ... end

Build CFG module.

module CFG : sig ... end
Sourcetype graph = (unit, Mopsa.stmt) CFG.graph

Edges are labelled with a statement. Nodes have no information in the graph structure. Abstract invariant information will be kept in maps separately from the CFG. This way, CFG can be kept immutable.

Sourcetype node = (unit, Mopsa.stmt) CFG.node
Sourcetype edge = (unit, Mopsa.stmt) CFG.edge
Sourcetype node_id = TagLoc.t
Sourcetype edge_id = Range.t
Sourcetype port = Mopsa.token
Sourcetype cfg = {
  1. cfg_graph : graph;
  2. mutable cfg_order : node Mopsa.GraphSig.nested_list list;
}

Graph utilities

Sourceval mk_node_id : ?id:int -> ?tag:string -> Loc.t -> node_id
Sourceval fresh_node_id : int LocHash.t
Sourceval mk_fresh_node_id : ?tag:string -> Loc.t -> node_id

Fresh node with some source location information. NOTE: Do not mix mk_fresh_node_id and mk_node_id as it can break uniqueness.

Sourceval loc_anonymous : Loc.t
Sourceval mk_anonymous_node_id : ?tag:string -> unit -> node_id

Fresh node without any source location information.

Sourceval copy_node_id : node_id -> node_id
Sourceval node_loc : node_id -> Loc.t
Sourceval pp_node_id : Stdlib.Format.formatter -> TagLoc.t -> unit
Sourceval pp_node_as_id : Stdlib.Format.formatter -> ('a, 'b) CFG.node -> unit
Sourceval compare_node_id : TagLoc.t -> TagLoc.t -> int
Sourceval mk_edge_id : ?tag:string -> Mopsa.range -> edge_id
Sourceval fresh_edge_id : int RangeHash.t
Sourceval mk_fresh_edge_id : ?tag:string -> Mopsa.range -> edge_id

Fresh range with possible some source range information. NOTE: Do not mix mk_fresh_edge_id and mk_edge_id as it can break uniqueness.

Sourceval mk_anonymous_edge_id : ?tag:string -> unit -> edge_id

Fresh range without any source range information.

Sourceval edge_range : edge_id -> Mopsa.range
Sourceval pp_edge_id : Stdlib.Format.formatter -> Mopsa.range -> unit
Sourceval pp_edge_as_id : Stdlib.Format.formatter -> ('a, 'b) CFG.edge -> unit
Sourceval compare_edge_id : Mopsa.range -> Mopsa.range -> int

Flows

Sourcetype Mopsa.token +=
  1. | T_cfg_node of node_id
  2. | T_cfg_edge_post of edge_id * port
  3. | T_cfg_entry of port

Associate a flow to each CFG node. We can store abstract information for the whole graph in a single abstract state, using node flows. We also associate a flow to cache the post-image of each CFG edge.

Sourcetype Mopsa.token +=
  1. | T_true
  2. | T_false

Flow for true and false branch of tests.

Statements

Sourcetype Mopsa.stmt_kind +=
  1. | S_cfg of cfg
  2. | S_test of Mopsa.expr
    (*

    test nodes, with a true and a false branch

    *)
  3. | S_skip
    (*

    empty node

    *)