Module `Cfg.Ast`Source

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 = {

cfg_graph : graph;
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 +=

| T_cfg_node of node_id
| T_cfg_edge_post of edge_id * port
| 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 +=

| T_true
| T_false

Flow for true and false branch of tests.

Statements

Sourcetype Mopsa.stmt_kind +=

| S_cfg of cfg
| S_test of Mopsa.expr
(*
test nodes, with a true and a false branch
*)
| S_skip
(*
empty node
*)

Sourceval mk_skip : Mopsa_utils.Location.range -> Mopsa.stmt

Sourceval mk_test : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Sourceval mk_cfg : cfg -> Mopsa_utils.Location.range -> Mopsa.stmt

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cfg/Cfg/Ast/index.html

Module `Cfg.Ast`Source

Graph types

Graph utilities

Flows

Statements

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cfg/Cfg/Ast/index.html

Module Cfg.AstSource

Graph types

Graph utilities

Flows

Statements

Module `Cfg.Ast`Source