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

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

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

type MopsaLib.token +=

| T_true
| T_false

Flow for true and false branch of tests.

Statements

type MopsaLib.stmt_kind +=

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

val mk_skip : Mopsa_utils.Core.Location.range -> MopsaLib.stmt

val mk_test : MopsaLib.expr -> Mopsa_utils.Core.Location.range -> MopsaLib.stmt

val mk_cfg : cfg -> Mopsa_utils.Core.Location.range -> MopsaLib.stmt

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Cfg/Ast/index.html

Module `Cfg.Ast`

Graph types

Graph utilities

Flows

Statements

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Cfg/Ast/index.html

Module Cfg.Ast

Graph types

Graph utilities

Flows

Statements

dune-project
Dependency

Module `Cfg.Ast`