package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install

Dune Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (2)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/core/Core/All/index.html

Module Core.AllSource

include module type of struct include Ast.Semantic end
include module type of struct include Ast.Constant end
type constant = Ast.Constant.constant = ..

Extensible constants

val compare_constant : constant -> constant -> int

compare_constant c1 c2 provides a total order between any pair c1 and c2 of registered constants

val pp_constant : Stdlib.Format.formatter -> constant -> unit

pp_constant fmt c pretty-prints a registered constant c with formatter fmt

Registration

val register_constant : constant Mopsa_utils.TypeExt.info -> unit

register_constant info registers a new constant with a comparison function info.compare and a pretty-printer info.print

val register_constant_compare : constant Mopsa_utils.TypeExt.compare -> unit

register_constant_compare compare registers a new comparison function for constants

val register_constant_pp : constant Mopsa_utils.TypeExt.print -> unit

register_constant_compare compare registers a new pretty-printer for constants

Common constants

type constant +=
  1. | C_top of Ast.Typ.typ
  2. | C_bool of bool
include module type of struct include Ast.Expr end
type expr_kind = Ast.Expr.expr_kind = ..

Extensible type of expression kinds

type expr = Ast.Expr.expr = {
  1. ekind : expr_kind;
    (*

    kind of the expression

    *)
  2. etyp : Ast.Typ.typ;
    (*

    type of the expression

    *)
  3. erange : Mopsa_utils.Location.range;
    (*

    location range of the expression

    *)
  4. etrans : expr Ast.Semantic.SemanticMap.t;
    (*

    translations of the expression into other semantics

    *)
  5. ehistory : expr list;
    (*

    History of preceding evaluations of the expression

    *)
}

Expressions

val compare_expr : expr -> expr -> int

compare_expr e1 e2 implements a total order between expressions

val pp_expr : Stdlib.Format.formatter -> expr -> unit

pp_expr fmt e pretty-prints expression e with format fmt

val ekind : expr -> expr_kind

Get the kind of an expression

val etyp : expr -> Ast.Typ.typ

Get the type of an expression

Get the location of an expression

Get the translation map of an expression

val ehistory : expr -> expr list

Get the evaluation history of an expression

val mk_expr : ?etyp:Ast.Typ.typ -> ?etrans:expr Ast.Semantic.SemanticMap.t -> ?ehistory:expr list -> expr_kind -> Mopsa_utils.Location.range -> expr

Construct an expression

val add_expr_translation : Ast.Semantic.semantic -> expr -> expr -> expr

Add a translation of an expression

val get_expr_translations : expr -> expr Ast.Semantic.SemanticMap.t

Get all translations of an expression

val get_expr_translation : Ast.Semantic.semantic -> expr -> expr

Get the translation of an expression into a given semantic

val get_expr_history : expr -> expr list

Get the evaluation history of an expression

val get_orig_expr : expr -> expr

Get the original form of an expression

val find_expr_ancestor : (expr -> bool) -> expr -> expr

Get the ancestor expression verifying a predicate

Registration

val register_expr : expr Mopsa_utils.TypeExt.info -> unit

register_expr info registers new expressions with their comparison function info.compare and pretty-printer info.print

val register_expr_compare : expr Mopsa_utils.TypeExt.compare -> unit

register_expr_compare compare registers a new expression comparison

val register_expr_pp : expr Mopsa_utils.TypeExt.print -> unit

register_expr_compare compare registers a new expression printer

Some common expressions

Variable expressions

type expr_kind +=
  1. | E_var of Ast.Var.var * Ast.Var.mode option
    (*

    optional access mode overloading the variable's access mode

    *)

Variables

val mk_var : Ast.Var.var -> ?mode:Ast.Var.mode option -> Mopsa_utils.Location.range -> expr

Create a variable expression

val weaken_var_expr : expr -> expr

Change the access mode of a variable expression to WEAK

val strongify_var_expr : expr -> expr

Change the access mode of a variable expression to STRONG

val var_mode : Ast.Var.var -> Ast.Var.mode option -> Ast.Var.mode

Get the overloaded access mode of a variable

Heap addresses expressions

type expr_kind +=
  1. | E_addr of Ast.Addr.addr * Ast.Var.mode option
    (*

    optional access mode overloading the address access mode

    *)
  2. | E_alloc_addr of Ast.Addr.addr_kind * Ast.Var.mode

Heap addresses

val mk_addr : Ast.Addr.addr -> ?etyp:Ast.Typ.typ -> ?mode:Ast.Var.mode option -> Mopsa_utils.Location.range -> expr

Create an address expression

Create an allocation expression

val weaken_addr_expr : expr -> expr

Change the access mode of an address expression to WEAK

val strongify_addr_expr : expr -> expr

Change the access mode of an address expression to STRONG

Constant expressions

type expr_kind +=
  1. | E_constant of Ast.Constant.constant

Constants

Create a constant expression

Create ⊤ expression of a given type

Unary expressions

type expr_kind +=
  1. | E_unop of Ast.Operator.operator * expr
    (*

    operand

    *)

Unary operator expressions

Create a unary operator expression

mk_not e range returns the negation of expression e using the operator Operator.O_log_not

Binary expressions

type expr_kind +=
  1. | E_binop of Ast.Operator.operator * expr * expr
    (*

    second operand

    *)

Binary operator expressions

Create a binary operator expression

val negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

module ExprSet = Ast.Expr.ExprSet

Sets of expression

module ExprMap = Ast.Expr.ExprMap

Maps of expressions

include module type of struct include Ast.Stmt end
type stmt_kind = Ast.Stmt.stmt_kind = ..

Extensible kinds of statements

type stmt = Ast.Stmt.stmt = {
  1. skind : stmt_kind;
    (*

    kind of the statement

    *)
  2. srange : Mopsa_utils.Location.range;
    (*

    location range of the statement

    *)
}

Statements

Create a statement

val skind : stmt -> stmt_kind

Get the kind of a statement

Get the location range of a statement

val compare_stmt : stmt -> stmt -> int

Total order between statements

val pp_stmt : Stdlib.Format.formatter -> stmt -> unit

Pretty-printer of statements

Registration

val register_stmt : stmt Mopsa_utils.TypeExt.info -> unit

register_stmt info registers a new statement by registering its compare function info.compare and pretty-printer info.print

val register_stmt_compare : stmt Mopsa_utils.TypeExt.compare -> unit

Register a comparison function for statements

val register_stmt_pp : stmt Mopsa_utils.TypeExt.print -> unit

Register a pretty-printer function for statements

Blocks

type block = stmt list

Blocks are sequences of statements

val pp_block : Stdlib.Format.formatter -> block -> unit

Pretty-printer for blocks

Common statements

type stmt_kind +=
  1. | S_program of Ast.Program.program * string list option
    (*

    Command-line arguments as given to Mopsa after --

    *)

Programs

type stmt_kind +=
  1. | S_assign of Ast.Expr.expr * Ast.Expr.expr
    (*

    rhs

    *)

Assignments

mk_assign lhs rhs range creates the assignment lhs = rhs;

type stmt_kind +=
  1. | S_assume of Ast.Expr.expr
    (*

    condition

    *)

Tests

Create a test statement

type stmt_kind +=
  1. | S_add of Ast.Expr.expr
    (*

    Add a dimension to the environment

    *)
  2. | S_remove of Ast.Expr.expr
    (*

    Remove a dimension from the environment and invalidate all references to it

    *)
  3. | S_invalidate of Ast.Expr.expr
    (*

    Invalidate all references to a dimension without removing it

    *)
  4. | S_rename of Ast.Expr.expr * Ast.Expr.expr
    (*

    new

    *)
  5. | S_forget of Ast.Expr.expr
    (*

    Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed

    *)
  6. | S_project of Ast.Expr.expr list
    (*

    Project the environment on the given list of dimensions. All other dimensions are removed

    *)
  7. | S_expand of Ast.Expr.expr * Ast.Expr.expr list
    (*

    Expand a dimension into a list of other dimensions. The expanded dimension is untouched

    *)
  8. | S_fold of Ast.Expr.expr * Ast.Expr.expr list
    (*

    Fold a list of dimensions into a single one. The folded dimensions are removed

    *)
  9. | S_block of stmt list * Ast.Var.var list
    (*

    local variables declared within the block

    *)
  10. | S_breakpoint of string
    (*

    Trigger a breakpoint

    *)

Dimensions

Utility functions to create various statements for dimension management

val mk_remove_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_invalidate_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_project : Ast.Expr.expr list -> Mopsa_utils.Location.range -> stmt
val mk_project_vars : Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_forget_var : Ast.Var.var -> Mopsa_utils.Location.range -> stmt
val mk_expand_var : Ast.Var.var -> Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_fold_var : Ast.Var.var -> Ast.Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_breakpoint : string -> Mopsa_utils.Location.range -> stmt

Containers of statements

module StmtSet = Ast.Stmt.StmtSet

Sets of statements

module StmtMap = Ast.Stmt.StmtMap

Maps of statements

include module type of struct include Ast.Typ end
type typ = Ast.Typ.typ = ..

Extensible types

val compare_typ : typ -> typ -> int

Compare two types

val pp_typ : Stdlib.Format.formatter -> typ -> unit

Pretty-print a type

Registration

val register_typ : typ Mopsa_utils.TypeExt.info -> unit

Register a new type

val register_typ_compare : typ Mopsa_utils.TypeExt.compare -> unit

Register a new type comparison

val register_typ_pp : typ Mopsa_utils.TypeExt.print -> unit

Register a new type pretty-printer

Common types

type typ +=
  1. | T_any
    (*

    Generic unknown type

    *)
  2. | T_addr
    (*

    Heap addresses type

    *)
  3. | T_bool
    (*

    Boolean type

    *)
include module type of struct include Ast.Program end
type prog_kind = Ast.Program.prog_kind = ..

Extensible type of program kinds

type program = Ast.Program.program = {
  1. prog_kind : prog_kind;
    (*

    kind of the program

    *)
  2. prog_range : Mopsa_utils.Location.range;
    (*

    program location

    *)
}

Programs

val compare_program : program -> program -> int

Total order between programs

val pp_program : Stdlib.Format.formatter -> program -> unit

Pretty-printer for programs

Registration

val register_program : program Mopsa_utils.TypeExt.info -> unit

register_program info registers a new program kind by registering its comparison function info.compare and pretty-printer info.print

val register_program_compare : program Mopsa_utils.TypeExt.compare -> unit

Register a comparison function between programs

val register_program_pp : program Mopsa_utils.TypeExt.print -> unit

Register a pretty-printer for programs

include module type of struct include Ast.Frontend end
type frontend = Ast.Frontend.frontend = {
  1. lang : string;
    (*

    Language of the frontend

    *)
  2. parse : string list -> Ast.Program.program;
    (*

    Parser function that translates a list of input source files into a Mopsa Program.program

    *)
  3. on_panic : exn -> string list -> float -> unit;
    (*

    Function called when the analysis of a program terminates with an exception, and *when the output is in text mode*. Provided with the exception, list of files and analysis time. Current usecase: provide automated testcase reduction capabilities in the C analysis.

    *)
}

Frontends

val register_frontend : frontend -> unit

Register a new frontend

val find_language_frontend : string -> frontend

Find the frontend of a given language

include module type of struct include Ast.Operator end
type operator = Ast.Operator.operator = ..

Extensible type of operators

val compare_operator : operator -> operator -> int

Total order between operators

val pp_operator : Stdlib.Format.formatter -> operator -> unit

Pretty-printer of operators

Registration

val register_operator : operator Mopsa_utils.TypeExt.info -> unit

register_operator info registers a new operator by registering its compare function info.compare and pretty-printer info.print

val register_operator_compare : operator Mopsa_utils.TypeExt.compare -> unit

Register a comparison function for operators

val register_operator_pp : operator Mopsa_utils.TypeExt.print -> unit

Register a pretty-printer for operators

Some common operators

type operator +=
  1. | O_eq
    (*

    equality ==

    *)
  2. | O_ne
    (*

    inequality !=

    *)
  3. | O_lt
    (*

    less than <

    *)
  4. | O_le
    (*

    less or equal <=

    *)
  5. | O_gt
    (*

    greater than >

    *)
  6. | O_ge
    (*

    greater or equal >=

    *)
  7. | O_log_not
    (*

    logical negation

    *)
  8. | O_log_or
    (*

    logical disjunction ||

    *)
  9. | O_log_and
    (*

    logical conjunction &&

    *)
  10. | O_log_xor
    (*

    logical strict disjonction xor

    *)
  11. | O_cast
    (*

    type cast

    *)

Common operators

val is_comparison_op : operator -> bool

Test whether an operator is a comparison operator

val is_logic_op : operator -> bool

Test whether an is a logical operator

val negate_comparison_op : operator -> operator

Return the negation of a comparison operator

val negate_logic_op : operator -> operator

Return the negation of a logical operator

include module type of struct include Ast.Var end
val print_uniq_with_uid : bool Stdlib.ref
val force_print_uniq_with_uid : bool -> (unit -> 'a) -> 'a

Access modes

type var_kind = Ast.Var.var_kind = ..

Extensible kind of variables

type mode = Ast.Var.mode =
  1. | WEAK
    (*

    Weak updates are used when the variable summarizes several concrete dimensions

    *)
  2. | STRONG
    (*

    Strong updates are used when the variable represents a single concrete dimension

    *)

Access mode of a variable

val pp_mode : Stdlib.Format.formatter -> mode -> unit

Pretty-print an access mode

val compare_mode : mode -> mode -> int

Compare two access modes

Variables

type var = Ast.Var.var = {
  1. vname : string;
    (*

    unique name of the variable

    *)
  2. vkind : var_kind;
    (*

    kind the variable

    *)
  3. vtyp : Ast.Typ.typ;
    (*

    type of the variable

    *)
  4. vmode : mode;
    (*

    access mode of the variable

    *)
  5. vsemantic : Ast.Semantic.semantic;
    (*

    semantic of the variable

    *)
}

Variables

val vname : var -> string

Accessor function to the fields of a variable

val vkind : var -> var_kind
val vtyp : var -> Ast.Typ.typ
val vmode : var -> mode
val vsemantic : var -> Ast.Semantic.semantic
val mkv : string -> var_kind -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> Ast.Typ.typ -> var

Create a variable with a unique name, a kind, a type and an access mode (STRONG if not given)

val pp_var : Stdlib.Format.formatter -> var -> unit

Pretty-print a variable

val compare_var : var -> var -> int

Total order between variables

Registration

val register_var : var Mopsa_utils.TypeExt.info -> unit

Register a new kind of variables

val register_var_compare : var Mopsa_utils.TypeExt.compare -> unit

Register a new variable comparison

val register_var_pp : var Mopsa_utils.TypeExt.print -> unit

Register a new variable pretty-printer

Common variables

type var_kind +=
  1. | V_uniq of string * int
    (*

    Unique ID

    *)
  2. | V_tmp of int
    (*

    Unique ID

    *)
  3. | V_var_attr of var * string
    (*

    Attribute

    *)
  4. | V_range_attr of Mopsa_utils.Location.range * string
    (*

    Attribute

    *)
val mk_uniq_var : string -> int -> ?mode:mode -> Ast.Typ.typ -> var

Create a unique variable

val mk_fresh_uniq_var : string -> ?mode:mode -> Ast.Typ.typ -> unit -> var

Create a fresh variable with a fresh ID

val mktmp : ?typ:Ast.Typ.typ -> ?mode:mode -> unit -> var

Create a fresh temporary variable

val mk_attr_var : var -> string -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> Ast.Typ.typ -> var

mk_attr_var v a t creates a variable representing an attribute a of another variable v

val mk_range_attr_var : Mopsa_utils.Location.range -> string -> ?mode:mode -> ?semantic:Ast.Semantic.semantic -> Ast.Typ.typ -> var

mk_range_attr_var r a t creates a variable representing an attribute a of a program location r

Containers for variables

module VarSet = Ast.Var.VarSet

Sets of variables

module VarMap = Ast.Var.VarMap

Maps of variables

Deprecated

val start_vcounter_at : int -> unit
val get_vcounter_val : unit -> int
val get_orig_vname : var -> string
val set_orig_vname : string -> var -> var
include module type of struct include Ast.Addr end
type addr_kind = Ast.Addr.addr_kind = ..

Kind of heap addresses, used to store extra information.

val addr_kind_compare_chain : (addr_kind -> addr_kind -> int) Stdlib.ref
val addr_kind_pp_chain : (Stdlib.Format.formatter -> addr_kind -> unit) Stdlib.ref
val pp_addr_kind : Stdlib.Format.formatter -> addr_kind -> unit
val compare_addr_kind : addr_kind -> addr_kind -> int
val register_addr_kind : addr_kind Mopsa_utils.TypeExt.info -> unit
type addr_partitioning = Ast.Addr.addr_partitioning = ..

Addresses are grouped by static criteria to make them finite

type addr_partitioning +=
  1. | G_all
    (*

    Group all addresses into one

    *)
val addr_partitioning_compare_chain : (addr_partitioning -> addr_partitioning -> int) Stdlib.ref
val addr_partitioning_pp_chain : (Stdlib.Format.formatter -> addr_partitioning -> unit) Stdlib.ref
val opt_hash_addr : bool Stdlib.ref

Command line option to use hashes as address format

val pp_addr_partitioning_hash : Stdlib.Format.formatter -> addr_partitioning -> unit
val pp_addr_partitioning : ?full:bool -> Stdlib.Format.formatter -> addr_partitioning -> unit

Print a partitioning policy. Flag full overloads the option opt_hash_addr and displays the full partitioning string (not its hash, which is useful for creating unique names of addresses)

val pp_addr_partitioning_full : Stdlib.Format.formatter -> addr_partitioning -> unit
val compare_addr_partitioning : addr_partitioning -> addr_partitioning -> int
val register_addr_partitioning : addr_partitioning Mopsa_utils.TypeExt.info -> unit
type addr = Ast.Addr.addr = {
  1. addr_kind : addr_kind;
    (*

    Kind of the address.

    *)
  2. addr_partitioning : addr_partitioning;
    (*

    Partitioning policy of the address

    *)
  3. addr_mode : Ast.Var.mode;
    (*

    Assignment mode of address (string or weak)

    *)
}

Heap addresses.

val akind : addr -> addr_kind
val pp_addr : Stdlib.Format.formatter -> addr -> unit
val addr_uniq_name : addr -> string

Get the unique name of an address. This is safer and faster than calling Format.asprintf "%s" pp_addr a when opt_hash_addr is set.

val compare_addr : addr -> addr -> int
val addr_mode : addr -> Ast.Var.mode option -> Ast.Var.mode
type Ast.Var.var_kind +=
  1. | V_addr_attr of addr * string

Address variables

val mk_addr_attr : addr -> string -> Ast.Typ.typ -> Ast.Var.var
include module type of struct include Ast.Visitor end
type parts = Ast.Visitor.parts = {
  1. exprs : Ast.Expr.expr list;
    (*

    sub-expressions

    *)
  2. stmts : Ast.Stmt.stmt list;
    (*

    sub-statements

    *)
}

Parts of a statement/expression

type 'a structure = parts * (parts -> 'a)

builder function

val structure_of_expr : Ast.Expr.expr -> Ast.Expr.expr structure

Get the structure of an expression

val structure_of_stmt : Ast.Stmt.stmt -> Ast.Stmt.stmt structure

Get the structure of a statement

val leaf : 'a -> 'a structure

Visitor for leaf statements/expressions that have no sub-elements

Registration

type 'a visit_info = 'a Ast.Visitor.visit_info = {
  1. compare : 'a Mopsa_utils.TypeExt.compare;
    (*

    Comparison function for 'a

    *)
  2. print : 'a Mopsa_utils.TypeExt.print;
    (*

    Pretty-printer for 'a'

    *)
  3. visit : ('a -> 'a structure) -> 'a -> 'a structure;
    (*

    Visitor for 'a

    *)
}

Registration descriptor for visitors

val register_expr_with_visitor : Ast.Expr.expr visit_info -> unit

Register an expression with its visitor

val register_expr_visitor : ((Ast.Expr.expr -> Ast.Expr.expr structure) -> Ast.Expr.expr -> Ast.Expr.expr structure) -> unit

Register a visitor of an expression

val register_stmt_with_visitor : Ast.Stmt.stmt visit_info -> unit

Register a statement with its visitor

val register_stmt_visitor : ((Ast.Stmt.stmt -> Ast.Stmt.stmt structure) -> Ast.Stmt.stmt -> Ast.Stmt.stmt structure) -> unit

Register a visitor of a statement

Visiting iterators

type 'a visit_action = 'a Ast.Visitor.visit_action =
  1. | Keep of 'a
    (*

    Keep the given result

    *)
  2. | VisitParts of 'a
    (*

    Continue visiting the parts of the given result

    *)
  3. | Visit of 'a
    (*

    Iterate the visitor on the given result

    *)

Actions of a visiting iterator

map_expr fe fs e transforms the expression e into a new one by applying visitor action fe and fs on its sub-expression and sub-statements respectively

Similar to map_expr but on statements

val fold_expr : ('a -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> Ast.Expr.expr -> 'a

fold_expr fe fs e folds the accumulated result of visitors fe and fs on the structure of expression e

val fold_stmt : ('a -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> Ast.Stmt.stmt -> 'a

Similar to fold_expr but on statements

val fold_map_expr : ('a -> Ast.Expr.expr -> ('a * Ast.Expr.expr) visit_action) -> ('a -> Ast.Stmt.stmt -> ('a * Ast.Stmt.stmt) visit_action) -> 'a -> Ast.Expr.expr -> 'a * Ast.Expr.expr

Combination of map and fold for expressions

val fold_map_stmt : ('a -> Ast.Expr.expr -> ('a * Ast.Expr.expr) visit_action) -> ('a -> Ast.Stmt.stmt -> ('a * Ast.Stmt.stmt) visit_action) -> 'a -> Ast.Stmt.stmt -> 'a * Ast.Stmt.stmt

Combination of map and fold for statements

val exists_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val for_all_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val exists_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val for_all_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val exists_child_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val for_all_child_expr : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Expr.expr -> bool
val exists_child_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool
val for_all_child_stmt : (Ast.Expr.expr -> bool) -> (Ast.Stmt.stmt -> bool) -> Ast.Stmt.stmt -> bool

Utility functions

val is_leaf_expr : Ast.Expr.expr -> bool

Test whether an expression is a leaf expression

val is_atomic_expr : Ast.Expr.expr -> bool

Test whether an expression has no sub-statement

val is_atomic_stmt : Ast.Stmt.stmt -> bool

Test whether a statement has no sub-statement

val expr_vars : Ast.Expr.expr -> Ast.Var.var list

Get all variables present in an expression

val stmt_vars : Ast.Stmt.stmt -> Ast.Var.var list

Get all variables present in a statement

val is_var_in_expr : Ast.Var.var -> Ast.Expr.expr -> bool

Check whether a variable appears in an expression

val is_var_in_stmt : Ast.Var.var -> Ast.Stmt.stmt -> bool

Check whether a variable appears in a statement

Deprecated

val fold_sub_expr : ('a -> Ast.Expr.expr -> 'a visit_action) -> ('a -> Ast.Stmt.stmt -> 'a visit_action) -> 'a -> Ast.Expr.expr -> 'a
include module type of struct include Alarm end

Checks

**********

Domains can add new checks by extending the type check and registering them using register_check. Note that checks should be simple variant constructs without any argument.

Sourcetype check = Alarm.check = ..
Sourceval pp_check : Stdlib.Format.formatter -> check -> unit

Print a check

Sourceval register_check : ((Stdlib.Format.formatter -> check -> unit) -> Stdlib.Format.formatter -> check -> unit) -> unit

Register a check with its printer

Alarms

**********

Alarms are issues related to a check in a given range and a given callstack. Domains can add new kinds of alarms to store information related to the issue, such suspect values that raised the alarm. Nevertheless, domains can use the generic alarm A_generic of check if they don't have addition static information to attach to the alarm.

Sourcetype alarm_kind = Alarm.alarm_kind = ..
Sourcetype alarm_kind +=
  1. | A_generic of check
Sourcetype alarm = Alarm.alarm = {
  1. alarm_kind : alarm_kind;
  2. alarm_check : check;
  3. alarm_range : Mopsa_utils.Location.range;
  4. alarm_callstack : Mopsa_utils.Callstack.callstack;
}

Create an alarm

Sourceval check_of_alarm : alarm -> check

Return the check associate to an alarm

Sourceval range_of_alarm : alarm -> Mopsa_utils.Location.range

Return the range of an alarm

Sourceval callstack_of_alarm : alarm -> Mopsa_utils.Callstack.callstack

Return the callstack of an alarm

Sourceval compare_alarm : alarm -> alarm -> int

Compare two alarms

Sourceval pp_alarm : Stdlib.Format.formatter -> alarm -> unit

Print an alarm

Sourceval compare_alarm_kind : alarm_kind -> alarm_kind -> int

Compare two kinds of alarms

Sourceval pp_alarm_kind : Stdlib.Format.formatter -> alarm_kind -> unit

Print an alarm kind

Sourceval join_alarm_kind : alarm_kind -> alarm_kind -> alarm_kind option

Join two alarm kinds by merging the static information attached to them

Sourceval register_alarm_compare : ((alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int) -> unit

Register a comparison function for alarms

Sourceval register_alarm_pp : ((Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.Format.formatter -> alarm_kind -> unit) -> unit

Register a print function for alarms

Sourceval register_alarm_check : ((alarm_kind -> check) -> alarm_kind -> check) -> unit

Register a function giving the check of an alarm

Sourceval register_alarm_join : ((alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option) -> unit

Register a join function for alarms

Sourcetype alarm_info = Alarm.alarm_info = {
  1. check : (alarm_kind -> check) -> alarm_kind -> check;
  2. compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
  3. print : (Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.Format.formatter -> alarm_kind -> unit;
  4. join : (alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option;
}

Registration record for a new kind of alarms

Sourceval register_alarm : alarm_info -> unit

Register a new kind of alarms

Diagnostic

**************

A diagnostic gives the status of all alarms raised at the program location for the same check

module AlarmSet = Alarm.AlarmSet

Set of alarms

Sourcetype diagnostic_kind = Alarm.diagnostic_kind =
  1. | Warning
    (*

    Some executions may have issues

    *)
  2. | Safe
    (*

    All executions are safe

    *)
  3. | Error
    (*

    All executions do have issues

    *)
  4. | Unreachable
    (*

    No execution reaches the check point

    *)

Kind of a diagnostic

Sourcetype 'a diagnostic_ = 'a Alarm.diagnostic_ = {
  1. diag_range : Mopsa_utils.Location.range;
  2. diag_check : check;
  3. diag_kind : diagnostic_kind;
  4. diag_alarms : AlarmSet.t;
  5. diag_callstack : 'a;
}
Sourcetype diagnosticWoCs = unit diagnostic_

Create a diagnostic that says that a check is safe

Sourceval mk_error_diagnostic : alarm -> diagnostic

Create a diagnostic that says that a check is unsafe

Create a diagnostic that says that a check maybe unsafe

Create a diagnostic that says that a check is unreachable

Sourceval pp_diagnostic_kind : Stdlib.Format.formatter -> diagnostic_kind -> unit

Print a diagnostic kind

Sourceval pp_diagnostic : Stdlib.Format.formatter -> diagnostic -> unit

Print a diagnostic

Sourceval subset_diagnostic : diagnostic -> diagnostic -> bool

Check whether a diagnostic is covered by another

Sourceval join_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the union of two diagnostics

Sourceval meet_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the intersection of two diagnostics

Sourceval add_alarm_to_diagnostic : alarm -> diagnostic -> diagnostic

Add an alarm to a diagnostic

Sourceval compare_diagnostic : diagnostic -> diagnostic -> int

Compare two diagnostics

Soundness assumption

************************

When a domain can't ensure total soundness when analyzing a piece of code, it can emit assumptions under which the result is still sound.

Sourcetype assumption_scope = Alarm.assumption_scope =
  1. | A_local of Mopsa_utils.Location.range
    (*

    Local assumptions concern a specific location range in the program

    *)
  2. | A_global
    (*

    Global assumptions can concern the entire program

    *)

Scope of an assumption

Sourcetype assumption_kind = Alarm.assumption_kind = ..

Domains can add new kinds of assumptions by extending the type assumption_kind

Sourcetype assumption_kind +=
  1. | A_ignore_unsupported_stmt of Ast.Stmt.stmt

Generic assumptions for specifying potential unsoundness due to unsupported statements/expressions

Sourcetype assumption_kind +=
  1. | A_ignore_unsupported_expr of Ast.Expr.expr
Sourcetype assumption = Alarm.assumption = {
  1. assumption_scope : assumption_scope;
  2. assumption_kind : assumption_kind;
}
Sourceval register_assumption : assumption_kind Mopsa_utils.TypeExt.info -> unit

Register a new kind of assumptions

Sourceval pp_assumption_kind : Stdlib.Format.formatter -> assumption_kind -> unit

Print an assumption kind

Sourceval pp_assumption : Stdlib.Format.formatter -> assumption -> unit

Print an assumption

Sourceval compare_assumption_kind : assumption_kind -> assumption_kind -> int

Compare two assumption kinds

Sourceval compare_assumption : assumption -> assumption -> int

Compare two assumptions

Sourceval mk_global_assumption : assumption_kind -> assumption

Create a global assumption

Create a local assumption

Analysis report

*******************

Alarms are organized in a report that maps each range and each check to a diagnostic. A report also contains the set of soundness assumptions made by the domains.

module RangeMap = Alarm.RangeMap
module RangeCallStackMap = Alarm.RangeCallStackMap
module CheckMap = Alarm.CheckMap
module AssumptionSet = Alarm.AssumptionSet
Sourcetype report = Alarm.report = {
  1. report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
  2. report_assumptions : AssumptionSet.t;
}
Sourceval empty_report : report

Return an empty report

Sourceval is_empty_report : report -> bool

Checks whether a report is empty

Sourceval is_safe_report : report -> bool

Checks whether a report is safe, i.e. it doesn't contain an error or a warning

Sourceval is_sound_report : report -> bool

Checks whether a report is sound

Sourceval pp_report : Stdlib.Format.formatter -> report -> unit

Print a report

Sourceval subset_report : report -> report -> bool

subset_report r1 r2 checks whether report r1 is included in r2

Sourceval join_report : report -> report -> report

Compute the union of two reports

Sourceval meet_report : report -> report -> report

Compute the intersection of two reports

Sourceval filter_report : (diagnostic -> bool) -> report -> report

filter_report p r keeps only diagnostics in report r that verify predicate p

Sourceval singleton_report : alarm -> report

Create a report with a single true alarm

Sourceval add_alarm : ?warning:bool -> alarm -> report -> report

add_alarm a r adds alarm a to a report r. If a diagnostic exists for the same range and the same check as a, join_diagnostic is used to join it with an error diagnostic containing a.

Sourceval set_diagnostic : diagnostic -> report -> report

set_diagnostic d r adds diagnostic d to r. Any existing diagnostic for the same range and the same check as d is removed.

Sourceval add_diagnostic : diagnostic -> report -> report

add_diagnostic d r adds diagnostic d to r. If a diagnostic exists for the same range and the same check as d, join_diagnostic is used to join it with d.

Sourceval remove_diagnostic : diagnostic -> report -> report

Remove a diagnostic from a report

find_diagnostic range chk r finds the diagnostic of check chk at location range in report r

Sourceval exists_report : (diagnostic -> bool) -> report -> bool

Check whether any diagnostic verifies a predicate

Sourceval forall_report : (diagnostic -> bool) -> report -> bool

Check whether all diagnostics verify a predicate

Sourceval count_alarms : report -> int * int

Count the number of alarms and warnings in a report

module RangeDiagnosticWoCsMap = Alarm.RangeDiagnosticWoCsMap
module CallstackSet = Alarm.CallstackSet

Set of callstacks

Group diagnostics by their range and diagnostic kind

Sourceval add_assumption : assumption -> report -> report

Add an assumption to a report

Sourceval add_global_assumption : assumption_kind -> report -> report

Add a global assumption to a report

Add a local assumption to a report

Sourceval fold2zo_report : (diagnostic -> 'b -> 'b) -> (diagnostic -> 'b -> 'b) -> (diagnostic -> diagnostic -> 'b -> 'b) -> report -> report -> 'b -> 'b
Sourceval exists2zo_report : (diagnostic -> bool) -> (diagnostic -> bool) -> (diagnostic -> diagnostic -> bool) -> report -> report -> bool
Sourceval fold_report : (diagnostic -> 'b -> 'b) -> report -> 'b -> 'b
Sourceval alarms_to_report : alarm list -> report
Sourceval report_to_alarms : report -> alarm list
Sourcemodule Alarm = Alarm
include module type of struct include Context end
Sourcetype ('a, _) ctx_key = ('a, _) Context.ctx_key = ..

Key to access an element in the context

Sourcetype 'a ctx = 'a Context.ctx

The context

Sourceval empty_ctx : 'a ctx

Empty context

Sourceval singleton_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx

Context with one element

Sourceval mem_ctx : ('a, 'v) ctx_key -> 'a ctx -> bool

mem_ctx k ctx returns true when an element at key k is in the context ctx.

Sourceval find_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'v

find_ctx k ctx returns the element at key k in the context ctx. Raises Not_found if no element is found.

Sourceval find_ctx_opt : ('a, 'v) ctx_key -> 'a ctx -> 'v option

find_ctx k ctx returns the element of the key k in the context ctx. Returns None if no element is found.

Sourceval add_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx -> 'a ctx

add_ctx k v ctx add element v at key k in the context ctx. The previous element is overwritten if present.

Sourceval remove_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'a ctx

add_ctx k v ctx removes the element at key k in the context ctx. If key k was not in ctx, ctx is returned unchanged.

Sourceval most_recent_ctx : 'a ctx -> 'a ctx -> 'a ctx

Get the most recent context between two

Sourceval pp_ctx : (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> 'a ctx -> unit

Print a context

Sourcetype ctx_pool = Context.ctx_pool = {
  1. ctx_pool_equal : 'a 'v 'w. ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_pool_print : 'a 'v. (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}

Pool registered keys

Sourcetype ctx_info = Context.ctx_info = {
  1. ctx_equal : 'a 'v 'w. ctx_pool -> ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_print : 'a 'v. ctx_pool -> (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}

Registration information for a new key

Sourceval register_ctx : ctx_info -> unit

Register a new key

Sourcemodule GenContextKey = Context.GenContextKey

Generate a new key

Sourceval callstack_ctx_key : ('a, Mopsa_utils.Callstack.callstack) ctx_key

Key for storing the callstack

Sourcemodule Context = Context
Sourcemodule Cases = Cases
Sourcetype 'r case = 'r Cases.case
Sourcetype ('a, 'r) cases = ('a, 'r) Cases.cases
Sourceval bind : ('a Cases.case -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases
Sourceval (>>=) : ('a, 'b) Cases.cases -> ('b Cases.case -> 'a Flow.flow -> ('a, 'c) Cases.cases) -> ('a, 'c) Cases.cases
Sourceval bind_opt : ('a Cases.case -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases option
Sourceval (>>=?) : ('a, 'b) Cases.cases -> ('b Cases.case -> 'a Flow.flow -> ('a, 'c) Cases.cases option) -> ('a, 'c) Cases.cases option
Sourceval bind_result : ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases
Sourceval (>>$) : ('a, 'b) Cases.cases -> ('b -> 'a Flow.flow -> ('a, 'c) Cases.cases) -> ('a, 'c) Cases.cases
Sourceval bind_result_opt : ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases option
Sourceval (>>$?) : ('a, 'b) Cases.cases -> ('b -> 'a Flow.flow -> ('a, 'c) Cases.cases option) -> ('a, 'c) Cases.cases option
Sourceval bind_list : 'a list -> ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> 'b Flow.flow -> ('b, 'c list) Cases.cases
Sourceval bind_list_opt : 'a list -> ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> 'b Flow.flow -> ('b, 'c list) Cases.cases option
Sourcemodule Eval = Eval
Sourcetype 'a eval = 'a Eval.eval
Sourcemodule Flow = Flow
Sourcetype 'a flow = 'a Flow.flow
Sourcemodule Post = Post
Sourcetype 'a post = 'a Post.post
Sourceval (>>%) : 'a Post.post -> ('a Flow.flow -> ('a, 'b) Cases.cases) -> ('a, 'b) Cases.cases
Sourceval (>>%?) : 'a Post.post -> ('a Flow.flow -> ('a, 'b) Cases.cases option) -> ('a, 'b) Cases.cases option
Sourcemodule Path = Path
include module type of struct include Path end
Sourcetype accessor = Path.accessor = ..
Sourcetype path = accessor list
Sourceval compare_accessor : accessor -> accessor -> int
Sourceval pp_accessor : Stdlib.Format.formatter -> accessor -> unit
Sourceval register_accessor : accessor Mopsa_utils.TypeExt.info -> unit
Sourceval compare_path : accessor list -> accessor list -> int
Sourceval pp_path : Stdlib.Format.formatter -> accessor list -> unit
Sourceval empty_path : path
module PathMap = Path.PathMap
module PathSet = Path.PathSet
Sourcemodule Change = Change
include module type of struct include Change end
Sourcetype change = Change.change =
  1. | Change_empty
  2. | Change_block of Ast.Stmt.stmt list
  3. | Change_seq of change list
  4. | Change_join of change * change
  5. | Change_meet of change * change
Sourceval pp_change : Stdlib.Format.formatter -> change -> unit
Sourceval compare_change : change -> change -> int
Sourceval empty_change : change
Sourceval is_empty_change : change -> bool
Sourceval join_change : change -> change -> change
Sourceval meet_change : change -> change -> change
Sourceval add_stmt_to_change : Ast.Stmt.stmt -> change -> change

Join two changes

Sourceval concat_change : change -> change -> change

Meet two changes

Sourcetype change_map = change Path.PathMap.t
Sourceval pp_change_map : Stdlib.Format.formatter -> change Path.PathMap.t -> unit
Sourceval compare_change_map : change Path.PathMap.t -> change Path.PathMap.t -> int
Sourceval empty_change_map : 'a Path.PathMap.t
Sourceval singleton_change_map : Path.PathMap.key -> 'a -> 'a Path.PathMap.t
Sourceval is_empty_change_map : change Path.PathMap.t -> bool

Generic merge

*****************

Sourcetype change_vars = Change.change_vars = {
  1. modified : Ast.Var.VarSet.t;
  2. removed : Ast.Var.VarSet.t;
}

Change of a statement in terms of modified and removed variables

Sourceval compare_change_vars : change_vars -> change_vars -> int
Sourceval is_empty_change_vars : change_vars -> bool
Sourceval get_stmt_change_vars : custom:(Ast.Stmt.stmt -> change_vars option) -> Ast.Stmt.stmt -> change_vars

Get the changes of a statement

Sourceval get_change_vars : custom:(Ast.Stmt.stmt -> change_vars option) -> change -> change_vars
Sourceval apply_change_vars : change_vars -> add:(Ast.Var.VarSet.elt -> 'b -> 'a -> 'a) -> remove:(Ast.Var.VarSet.elt -> 'a -> 'a) -> find:(Ast.Var.VarSet.elt -> 'a -> 'b) -> 'a -> 'a -> 'a

Apply changes on an abstract element

Sourceval generic_merge : add:(Ast.Var.VarSet.elt -> 'a -> 'b -> 'b) -> find:(Ast.Var.VarSet.elt -> 'b -> 'a) -> remove:(Ast.Var.VarSet.elt -> 'b -> 'b) -> ?custom:(Ast.Stmt.stmt -> change_vars option) -> ('b * change) -> ('b * change) -> 'b * 'b

Generic merge operator for non-relational domains

Sourceval opt_change_tracker_enabled : bool Stdlib.ref
Sourceval enable_change_tracker : unit -> unit
Sourceval disable_change_tracker : unit -> unit
Sourceval is_change_tracker_enabled : unit -> bool
Sourceval set_change_tracker_state : bool -> unit
Sourceval with_change_tracker : (unit -> 'a) -> 'a
include module type of struct include Query end
Sourcetype ('a, _) query = ('a, _) Query.query = ..

Extensible type of queries

Sourceval join_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Join two queries

Sourceval meet_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Meet two queries

Registration

****************

Sourcetype query_pool = Query.query_pool = {
  1. pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered queries

Sourcetype query_info = Query.query_info = {
  1. join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registraction info for new queries

Sourceval register_query : query_info -> unit

Register a new query

Sourcetype lattice_query_pool = Query.lattice_query_pool = {
  1. pool_join : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered lattice queries. Lattice queries are queries that return elements of the global abstract state lattice. Join/meet operators are enriched with the lattice and the context so that we can compute join/meet over the abstract elements.

Sourcetype lattice_query_info = Query.lattice_query_info = {
  1. join : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registration info for new lattice queries

Sourceval register_lattice_query : lattice_query_info -> unit

Register a new lattice query

Common queries

******************

Sourcetype query +=
  1. | Q_defined_variables : string option -> ('a, Ast.Var.var list) query
    (*

    Extract the list of defined variables, in a given function call site, or in all scopes

    *)
  2. | Q_allocated_addresses : ('a, Ast.Addr.addr list) query
    (*

    Query to extract the list of addresses allocated in the heap

    *)
  3. | Q_variables_linked_to : Ast.Expr.expr -> ('a, Ast.Var.VarSet.t) query
    (*

    Query to extract the auxiliary variables related to an expression

    *)
include module type of struct include Token end
Sourcetype token = Token.token = ..

Flow tokens are used to distinguish between different control flows

Sourcetype token +=
  1. | T_cur
    (*

    Token of current (active) execution flow

    *)
Sourceval register_token : token Mopsa_utils.TypeExt.info -> unit

Register a new token with its compare and print functions

Sourceval compare_token : token -> token -> int

Compare two tokens with a total order

Sourceval pp_token : Stdlib.Format.formatter -> token -> unit

Pretty printer of tokens

Sourcemodule TokenMap = Token.TokenMap
include module type of struct include Ast.Semantic end
type semantic = string
val compare_semantic : semantic -> semantic -> int
val pp_semantic : Stdlib.Format.formatter -> semantic -> unit
val any_semantic : semantic
val is_any_semantic : semantic -> bool
module SemanticSet = Ast.Semantic.SemanticSet
module SemanticMap = Ast.Semantic.SemanticMap
include module type of struct include Route end
Sourcetype domain = string
Sourcetype route = Route.route =
  1. | Below of domain
    (*

    Sub-tree below a domain

    *)
  2. | Semantic of Ast.Semantic.semantic
    (*

    Sub-tree identified by a semantic

    *)

Routes

module DomainSet = Route.DomainSet
Sourceval compare_route : route -> route -> int

Set of domains

Compare two routes

Sourceval pp_route : Stdlib.Format.formatter -> route -> unit

Print a route

Sourceval toplevel : route

Toplevel tree

Sourcetype routing_table = Route.routing_table

Routing table providing the domains that are part of a route

Sourceval empty_routing_table : routing_table

Empty routing table

Sourceval resolve_route : route -> routing_table -> DomainSet.t

Resolve a route into domains

Add a route between a route and a domain

Add a set of routing_table linking a route and a set of domains

Sourceval get_routes : routing_table -> route list

Get all routing_table in a routing table

Sourceval join_routing_table : routing_table -> routing_table -> routing_table

Join two routing_table table

Sourceval pp_routing_table : Stdlib.Format.formatter -> routing_table -> unit

Print a routing table

include module type of struct include Lattice end
Sourcemodule type LATTICE = Lattice.LATTICE

Signature of a lattice module.

Sourcetype 'a lattice = 'a Lattice.lattice = {
  1. bottom : 'a;
  2. top : 'a;
  3. is_bottom : 'a -> bool;
  4. subset : 'a Context.ctx -> 'a -> 'a -> bool;
  5. join : 'a Context.ctx -> 'a -> 'a -> 'a;
  6. meet : 'a Context.ctx -> 'a -> 'a -> 'a;
  7. widen : 'a Context.ctx -> 'a -> 'a -> 'a;
  8. merge : 'a -> ('a * Change.change_map) -> ('a * Change.change_map) -> 'a;
  9. print : Print.printer -> 'a -> unit;
}

Lattice operators

include module type of struct include Id end
Sourcetype _ id = _ Id.id = ..

Identifiers

Sourcetype witness = Id.witness = {
  1. eq : 'a 'b. 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Eq.eq option;
}
Sourcetype witness_chain = Id.witness_chain = {
  1. eq : 'a 'b. witness -> 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Eq.eq option;
}

Equality witness of an identifier

Sourceval register_id : witness_chain -> unit

Register a new descriptor

Sourceval equal_id : 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Eq.eq option

Equality witness of identifiers

Sourcemodule GenDomainId = Id.GenDomainId

Generator of a new domain identifier

Sourcemodule GenStatelessDomainId = Id.GenStatelessDomainId

Generator of a new identifier for stateless domains

Sourcemodule GenValueId = Id.GenValueId

Generator of a new value identifier

include module type of struct include Manager end

Managers

Sourcetype ('a, 't) man = ('a, 't) Manager.man = {
  1. lattice : 'a Lattice.lattice;
    (*

    Access to lattice operators on the toplevel abstract element 'a.

    *)
  2. get : Token.token -> 'a Flow.flow -> ('a, 't) Cases.cases;
    (*

    Returns the domain's abstract element 't. A disjunction of cases is returned when partitioning is used.

    *)
  3. set : Token.token -> 't -> 'a Flow.flow -> 'a Post.post;
    (*

    Sets the domain's abstract element 't.

    *)
  4. exec : ?route:Route.route -> Ast.Stmt.stmt -> 'a Flow.flow -> 'a Post.post;
    (*

    man.exec stmt flow executes stmt in flow and returns the post state.

    *)
  5. eval : ?route:Route.route -> ?translate:Ast.Semantic.semantic -> ?translate_when:(Ast.Semantic.semantic * (Ast.Expr.expr -> bool)) list -> Ast.Expr.expr -> 'a Flow.flow -> 'a Eval.eval;
    (*

    man.eval expr flow evaluates expr in flow and returns the result expression.

    There are two kinds of evaluations: within the same semantic (simplifications), or to another semantic (translations). Calling man.eval expr flow performs both kinds of evaluations. The result e' of man.eval expr flow is a simplification of e within the same semantic. To retrieve a translation to another semantic, one can use the ?translate parameter: man.eval expr flow ~translate:semantic is a translation of the simplification of e in semantic. A common use case is to translate expressions to Universal with man.eval expr flow ~translate:"Universal". It is possible to control when the translation is applied with ?translate_when.

    *)
  6. ask : 'r. ?route:Route.route -> ('a, 'r) Query.query -> 'a Flow.flow -> ('a, 'r) Cases.cases;
    (*

    man.ask query flow performs a query to other domains. If no domain can answer the query, man.ask query flow results in a runtime error.

    *)
  7. print_expr : ?route:Route.route -> 'a Flow.flow -> Print.printer -> Ast.Expr.expr -> unit;
    (*

    man.print_expr flow is the expression printer for the type 'a.

    *)
  8. add_change : Ast.Stmt.stmt -> Path.path -> 'a Flow.flow -> Change.change_map -> Change.change_map;
    (*

    Add a statement to the changes map.

    *)
}

Managers provide access to full analyzer.

'a is the type of the toplevel abstract element, and 't is the type of local abstract element (that is, the type of the domain that calls the manager).

Sourcemodule Hook = Hook
include module type of struct include Print end
Sourcetype symbols = Print.symbols = {
  1. sopen : string;
  2. ssep : string;
  3. sbind : string;
  4. sclose : string;
}

Symbols for printing maps, lists and sets

Sourcetype ('k, 'v) map = ('k, 'v) Mopsa_utils.MapExtPoly.t

Structured print objects

Sourcetype print_object = Print.print_object =
  1. | Empty
  2. | Bool of bool
  3. | Int of Z.t
  4. | Float of float
  5. | String of string
  6. | Var of Ast.Var.var
  7. | Map of (print_object, print_object) map * symbols
  8. | List of print_object list * symbols
  9. | Set of print_object set * symbols

Printers

Sourcetype printer = Print.printer

Printers encapsulate the structured objects to print along the history of printed expression

Sourceval empty_printer : unit -> printer

Create an empty printer

Sourceval get_printed_object : printer -> print_object

Get the structured print object of a printer

Sourceval get_printed_exprs : printer -> Ast.Expr.expr list

Get the expressions that were already printed

Sourceval add_printed_expr : printer -> Ast.Expr.expr -> unit

Mark an expression as printed

Sourceval mem_printed_expr : printer -> Ast.Expr.expr -> bool

Check whether an expression was already printed

Sourcetype print_selector = Print.print_selector =
  1. | Key of string
  2. | Index of int
  3. | Obj of print_object

Selectors of print objects

Sourcetype print_path = print_selector list

Path of a print object

Sourceval find_print_object : print_path -> print_object -> print_object

find_print_object path obj returns the object placed at path in obj

Sourceval match_print_object_keys : Str.regexp -> print_object -> print_object

match_print_object_keys re obj slices obj to paths containing keys that match re

Generic print functions

Sourceval pprint : ?path:print_path -> printer -> print_object -> unit

pprint ~path:p printer o prints object o at path p in printer.

Sourceval pbox : (printer -> 'a -> unit) -> 'a -> print_object

pbox f x returns a boxed object created by f when applied to x. It is equivalent to

  let printer = empty_printer () in
  f printer x;
  get_printed_object printer
Sourceval fbox : ('a, Stdlib.Format.formatter, unit, print_object) Stdlib.format4 -> 'a

fbox fmt returns a string object of a formatted value

Sourceval sprint : (printer -> 'a -> unit) -> 'a -> string

sprint f x returns the string representing the boxed object pbox f x

Sourceval fkey : ('a, Stdlib.Format.formatter, unit, print_selector) Stdlib.format4 -> 'a

fkey fmt returns a key selector with a formatted string

Sourceval pkey : (printer -> 'a -> unit) -> 'a -> print_selector

pkey f x returns a key selector with a printed string

Typed print functions

Sourceval pp_string : ?path:print_path -> printer -> string -> unit

Print a string object

Sourceval pp_bool : ?path:print_path -> printer -> bool -> unit

Print a boolean object

Sourceval pp_int : ?path:print_path -> printer -> int -> unit

Print an integer object

Sourceval pp_z : ?path:print_path -> printer -> Z.t -> unit

Print an integer object

Sourceval pp_float : ?path:print_path -> printer -> float -> unit

Print a float object

Sourceval pp_variable : ?path:print_path -> printer -> Ast.Var.var -> unit

Print a variable

Sourceval pp_list : ?path:print_path -> ?lopen:string -> ?lsep:string -> ?lclose:string -> (printer -> 'a -> unit) -> printer -> 'a list -> unit

pp_list ~path:p f printer l prints a list l at path p by boxing f on every element of l

Sourceval pp_obj_list : ?path:print_path -> ?lopen:string -> ?lsep:string -> ?lclose:string -> printer -> print_object list -> unit

pp_obj_list ~path:p printer l prints a list of objects at path p. Useful for printing heterogenous lists.

Sourceval pp_map : ?path:print_path -> ?mopen:string -> ?msep:string -> ?mclose:string -> ?mbind:string -> (printer -> 'k -> unit) -> (printer -> 'v -> unit) -> printer -> ('k * 'v) list -> unit

pp_smap ~path:p fk fv printer l prints a map from a list l of pairs of keys and values. Keys are boxed with function fk and values with function fv.

Sourceval pp_mapi : ?path:print_path -> ?mopen:string -> ?msep:string -> ?mclose:string -> ?mbind:string -> (printer -> 'k -> unit) -> (printer -> ('k * 'v) -> unit) -> printer -> ('k * 'v) list -> unit
Sourceval pp_obj_map : ?path:print_path -> ?mopen:string -> ?msep:string -> ?mclose:string -> ?mbind:string -> printer -> (print_object * print_object) list -> unit

pp_obj_smap ~path:p printer l prints a map from a list of pairs of print objects

Sourceval pp_obj_set : ?path:print_path -> ?sopen:string -> ?ssep:string -> ?sclose:string -> printer -> print_object set -> unit

pp_obj_set ~path:p printer l prints a set of objects at path p. Useful for printing heterogenous sets.

Sourceval pp_set : ?path:print_path -> ?sopen:string -> ?ssep:string -> ?sclose:string -> (printer -> 'a -> unit) -> printer -> 'a set -> unit

pp_set ~path:p f printer l prints a set from a list l at path p by boxing f on every element of l

Format

Sourceval pp_print_object : Stdlib.Format.formatter -> print_object -> unit

Pretty-print a printer objct

Sourceval pflush : Stdlib.Format.formatter -> printer -> unit

Pretty-print the printer output in a format string

Sourceval format : (printer -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit

Convert a printer function into a format function

Sourceval unformat : ?path:print_path -> (Stdlib.Format.formatter -> 'a -> unit) -> printer -> 'a -> unit

Convert a format function into a printer

JSON

Sourceval print_object_to_json : print_object -> Yojson.Basic.t

Convert a printer object to JSON

Sourceval json_to_print_object : Yojson.Basic.t -> print_object

Convert JSON to a printer object

Sourcemodule Print = Print
include module type of struct include Avalue end
Sourcetype _ avalue_kind = _ Avalue.avalue_kind = ..
Sourcetype avalue_pool = Avalue.avalue_pool = {
  1. pool_typ : 'v. 'v avalue_kind -> Ast.Typ.typ;
  2. pool_bottom : 'v. 'v avalue_kind -> 'v;
  3. pool_top : 'v. 'v avalue_kind -> 'v;
  4. pool_join : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
  5. pool_meet : 'v. 'v avalue_kind -> 'v -> 'v -> 'v;
  6. pool_compare : 'v 'w. 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
  7. pool_print : 'v. 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit;
}
Sourcetype avalue_info = Avalue.avalue_info = {
  1. typ : 'v. avalue_pool -> 'v avalue_kind -> Ast.Typ.typ;
  2. bottom : 'v. avalue_pool -> 'v avalue_kind -> 'v;
  3. top : 'v. avalue_pool -> 'v avalue_kind -> 'v;
  4. join : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
  5. meet : 'v. avalue_pool -> 'v avalue_kind -> 'v -> 'v -> 'v;
  6. compare : 'v 'w. avalue_pool -> 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int;
  7. print : 'v. avalue_pool -> 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit;
}
Sourceval register_avalue : avalue_info -> unit
Sourceval type_of_avalue : 'v avalue_kind -> Ast.Typ.typ
Sourceval bottom_avalue : 'v avalue_kind -> 'v
Sourceval top_avalue : 'v avalue_kind -> 'v
Sourceval join_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
Sourceval meet_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
Sourceval compare_avalue : 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int
Sourceval pp_avalue : 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit
Sourceval mk_avalue_expr : 'v avalue_kind -> 'v -> Mopsa_utils.Location.range -> Ast.Expr.expr
Sourceval mk_avalue_constant : 'v avalue_kind -> 'v -> Ast.Constant.constant
Sourcetype Query.query +=
  1. | Q_avalue : Ast.Expr.expr * 'v avalue_kind -> ('a, 'v) Query.query
Sourceval mk_avalue_query : Ast.Expr.expr -> 'v avalue_kind -> ('a, 'v) Query.query
include module type of struct include Utils end
Sourceval exec_cleaner : Ast.Stmt.stmt -> ('a, 'b) Manager.man -> 'a Flow.flow -> ('a, unit) Cases.cases
Sourceval exec_cleaners : ('a, 'b) Manager.man -> ('a, unit) Cases.cases -> ('a, unit) Cases.cases
Sourceval post_to_flow : ('a, 'b) Manager.man -> 'a Post.post -> 'a Flow.flow
Sourceval assume : Ast.Expr.expr -> ?route:Route.route -> ?translate:Ast.Semantic.semantic -> fthen:('a Flow.flow -> ('a, 'b) Cases.cases) -> felse:('a Flow.flow -> ('a, 'b) Cases.cases) -> ?fboth:('a Flow.flow -> 'a Flow.flow -> ('a, 'b) Cases.cases) -> ?fnone:('a Flow.flow -> 'a Flow.flow -> ('a, 'b) Cases.cases) -> ?eval:bool -> ('a, 'c) Manager.man -> 'a Flow.flow -> ('a, 'b) Cases.cases
Sourceval switch : (Ast.Expr.expr list * ('a Flow.flow -> ('a, 'r) Cases.cases)) list -> ?route:Route.route -> ('a, 'b) Manager.man -> 'a Flow.flow -> ('a, 'r) Cases.cases
Sourceval set_env : Token.token -> 't -> ('a, 't) Manager.man -> 'a Flow.flow -> 'a Post.post
Sourceval set_singleton_env : 'a -> 'b Context.ctx -> ('b, 'a) Manager.man -> 'b -> 'b
Sourceval set_env_flow : Token.token -> 'b -> ('a, 'b) Manager.man -> 'a Flow.flow -> 'a Flow.flow
Sourceval get_env : Token.token -> ('a, 't) Manager.man -> 'a Flow.flow -> ('a, 't) Cases.cases
Sourceval get_singleton_env : 'a Context.ctx -> ('a, 'b) Manager.man -> 'a -> 'b
Sourceval get_singleton_env_from_flow : Token.token -> ('a, 't) Manager.man -> 'a Flow.flow -> 't
Sourceval map_env : Token.token -> ('t -> 't) -> ('a, 't) Manager.man -> 'a Flow.flow -> 'a Post.post
Sourceval get_pair_fst : ('a, 'b * 'c) Manager.man -> Token.token -> 'a Flow.flow -> ('a, 'b) Cases.cases
Sourceval set_pair_fst : ('a, 'b * 'c) Manager.man -> Token.token -> 'b -> 'a Flow.flow -> ('a, unit) Cases.cases
Sourceval get_pair_snd : ('a, 'b * 'c) Manager.man -> Token.token -> 'a Flow.flow -> ('a, 'c) Cases.cases
Sourceval set_pair_snd : ('a, 'b * 'c) Manager.man -> Token.token -> 'c -> 'a Flow.flow -> ('a, unit) Cases.cases
Sourceval env_exec : ('a Flow.flow -> 'a Post.post) -> 'a Context.ctx -> ('a, 't) Manager.man -> 'a -> 'a
Sourceval ask_and_reduce_cases : (('a, 'b) Query.query -> 'c -> ('d, 'b) Cases.cases) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
Sourceval ask_and_reduce_list : (('a, 'b) Query.query -> 'c -> ('d * 'b) list) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
Sourceval ask_and_reduce : (('a, 'b) Query.query -> 'c -> ('d, 'b) Cases.cases) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
Sourceval find_var_by_name : ?function_scope:string option -> string -> ('a, 'b) Manager.man -> 'a Flow.flow -> Ast.Var.var
Sourceval pp_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Var.var list -> unit
Sourceval pp_vars_info_by_name : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> string list -> unit
Sourceval pp_expr_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Expr.expr -> unit
Sourceval pp_stmt_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Stmt.stmt -> unit
Sourceval breakpoint : string -> ('a, 'b) Manager.man -> 'a Flow.flow -> unit
include module type of struct include Marker end
Sourcetype marker = Marker.marker = ..
Sourcetype marker_info = Marker.marker_info = {
  1. marker_name : string;
  2. marker_print_name : (marker -> string) -> marker -> string;
  3. marker_print : (Stdlib.Format.formatter -> marker -> unit) -> Stdlib.Format.formatter -> marker -> unit;
  4. marker_compare : (marker -> marker -> int) -> marker -> marker -> int;
}
Sourceval compare_marker : marker -> marker -> int
Sourceval pp_marker : Stdlib.Format.formatter -> marker -> unit
Sourceval get_marker_name : marker -> string
Sourceval register_marker : marker_info -> unit
Sourcetype Ast.Stmt.stmt_kind +=
  1. | S_add_marker of marker
Sourceval enable_marker : string -> unit
Sourceval disable_marker : string -> unit
Sourceval is_marker_enabled : marker -> bool
Sourceval available_markers : unit -> string list
Sourcemodule Var : sig ... end
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