Module Cfg.Ast

Extends the simple Universal language with Control Flow Graphs.

Graph types

module Loc : sig ... end
module TagLoc : sig ... end
module Range : sig ... end
module 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
module CFG_Param : sig ... end

Build CFG module.

module CFG : sig ... end
type graph = (unit, MopsaLib.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.

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

Graph utilities

val mk_node_id : ?id:int -> ?tag:string -> Loc.t -> node_id
val fresh_node_id : int LocHash.t
val 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.

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

Fresh node without any source location information.

val copy_node_id : node_id -> node_id
val node_loc : node_id -> Loc.t
val pp_node_id : Format.formatter -> TagLoc.t -> unit
val pp_node_as_id : Format.formatter -> ('a, 'b) CFG.node -> unit
val compare_node_id : TagLoc.t -> TagLoc.t -> int
val mk_edge_id : ?tag:string -> MopsaLib.range -> edge_id
val fresh_edge_id : int RangeHash.t
val mk_fresh_edge_id : ?tag:string -> MopsaLib.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.

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

Fresh range without any source range information.

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

Flows

type MopsaLib.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.

type MopsaLib.token +=
  1. | T_true
  2. | T_false

Flow for true and false branch of tests.

Statements

type MopsaLib.stmt_kind +=
  1. | S_cfg of cfg
  2. | S_test of MopsaLib.expr
    (*

    test nodes, with a true and a false branch

    *)
  3. | S_skip
    (*

    empty node

    *)