package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type node = (unit, Mopsa.stmt) CFG.node
type edge = (unit, Mopsa.stmt) CFG.edge
type node_id = TagLoc.t
type edge_id = Range.t
type port = Mopsa.token
type cfg = {
  1. cfg_graph : graph;
  2. mutable cfg_order : node Mopsa.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 -> Mopsa.range -> edge_id
val fresh_edge_id : int RangeHash.t
val 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.

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

Fresh range without any source range information.

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

Flows

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

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

Flow for true and false branch of tests.

Statements

type 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

    *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct