package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
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

    *)
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

    *)
}

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

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.

type check = Alarm.check = ..
val pp_check : Stdlib.Format.formatter -> check -> unit

Print a check

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

type alarm_kind = Alarm.alarm_kind = ..
type alarm_kind +=
  1. | A_generic of check
type 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

val check_of_alarm : alarm -> check

Return the check associate to an alarm

val range_of_alarm : alarm -> Mopsa_utils.Location.range

Return the range of an alarm

val callstack_of_alarm : alarm -> Mopsa_utils.Callstack.callstack

Return the callstack of an alarm

val compare_alarm : alarm -> alarm -> int

Compare two alarms

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

Print an alarm

val compare_alarm_kind : alarm_kind -> alarm_kind -> int

Compare two kinds of alarms

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

Print an alarm kind

val join_alarm_kind : alarm_kind -> alarm_kind -> alarm_kind option

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

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

Register a comparison function for alarms

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

Register a print function for alarms

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

Register a function giving the check of an alarm

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

Register a join function for alarms

type 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

val 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

type 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

type '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;
}
type diagnosticWoCs = unit diagnostic_

Create a diagnostic that says that a check is safe

val 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

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

Print a diagnostic kind

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

Print a diagnostic

val subset_diagnostic : diagnostic -> diagnostic -> bool

Check whether a diagnostic is covered by another

val join_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the union of two diagnostics

val meet_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the intersection of two diagnostics

val add_alarm_to_diagnostic : alarm -> diagnostic -> diagnostic

Add an alarm to a diagnostic

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

type 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

type assumption_kind = Alarm.assumption_kind = ..

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

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

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

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

Register a new kind of assumptions

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

Print an assumption kind

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

Print an assumption

val compare_assumption_kind : assumption_kind -> assumption_kind -> int

Compare two assumption kinds

val compare_assumption : assumption -> assumption -> int

Compare two assumptions

val mk_global_assumption : assumption_kind -> assumption

Create a global assumption

val mk_local_assumption : assumption_kind -> Mopsa_utils.Location.range -> 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
type report = Alarm.report = {
  1. report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
  2. report_assumptions : AssumptionSet.t;
}
val empty_report : report

Return an empty report

val is_empty_report : report -> bool

Checks whether a report is empty

val is_safe_report : report -> bool

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

val is_sound_report : report -> bool

Checks whether a report is sound

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

Print a report

val subset_report : report -> report -> bool

subset_report r1 r2 checks whether report r1 is included in r2

val join_report : report -> report -> report

Compute the union of two reports

val meet_report : report -> report -> report

Compute the intersection of two reports

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

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

val singleton_report : alarm -> report

Create a report with a single true alarm

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

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

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

val 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

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

Check whether any diagnostic verifies a predicate

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

Check whether all diagnostics verify a predicate

val 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

val add_assumption : assumption -> report -> report

Add an assumption to a report

val add_global_assumption : assumption_kind -> report -> report

Add a global assumption to a report

val add_local_assumption : assumption_kind -> Mopsa_utils.Location.range -> report -> report

Add a local assumption to a report

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

Key to access an element in the context

type 'a ctx = 'a Context.ctx

The context

val empty_ctx : 'a ctx

Empty context

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

Context with one element

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

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

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

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

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

val most_recent_ctx : 'a ctx -> 'a ctx -> 'a ctx

Get the most recent context between two

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

Print a context

type 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

type 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

val register_ctx : ctx_info -> unit

Register a new key

module GenContextKey = Context.GenContextKey

Generate a new key

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

Key for storing the callstack

module Context = Context
module Cases = Cases
type 'r case = 'r Cases.case
type ('a, 'r) cases = ('a, 'r) Cases.cases
val bind : ('a Cases.case -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases
val (>>=) : ('a, 'b) Cases.cases -> ('b Cases.case -> 'a Flow.flow -> ('a, 'c) Cases.cases) -> ('a, 'c) Cases.cases
val bind_opt : ('a Cases.case -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases option
val (>>=?) : ('a, 'b) Cases.cases -> ('b Cases.case -> 'a Flow.flow -> ('a, 'c) Cases.cases option) -> ('a, 'c) Cases.cases option
val bind_result : ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases
val (>>$) : ('a, 'b) Cases.cases -> ('b -> 'a Flow.flow -> ('a, 'c) Cases.cases) -> ('a, 'c) Cases.cases
val bind_result_opt : ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> ('b, 'a) Cases.cases -> ('b, 'c) Cases.cases option
val (>>$?) : ('a, 'b) Cases.cases -> ('b -> 'a Flow.flow -> ('a, 'c) Cases.cases option) -> ('a, 'c) Cases.cases option
val bind_list : 'a list -> ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases) -> 'b Flow.flow -> ('b, 'c list) Cases.cases
val bind_list_opt : 'a list -> ('a -> 'b Flow.flow -> ('b, 'c) Cases.cases option) -> 'b Flow.flow -> ('b, 'c list) Cases.cases option
module Eval = Eval
type 'a eval = 'a Eval.eval
module Flow = Flow
type 'a flow = 'a Flow.flow
module Post = Post
type 'a post = 'a Post.post
val (>>%) : 'a Post.post -> ('a Flow.flow -> ('a, 'b) Cases.cases) -> ('a, 'b) Cases.cases
val (>>%?) : 'a Post.post -> ('a Flow.flow -> ('a, 'b) Cases.cases option) -> ('a, 'b) Cases.cases option
module Effect = Effect
include module type of struct include Effect end

Effects

type effect = Effect.effect =
  1. | Effect_empty
  2. | Effect_block of Ast.Stmt.stmt list
  3. | Effect_seq of effect list
  4. | Effect_join of effect * effect
  5. | Effect_meet of effect * effect
val pp_effect : Stdlib.Format.formatter -> effect -> unit

Print a effect

val compare_effect : effect -> effect -> int

Compare two effects

val empty_effect : effect

Empty effect

val is_empty_effect : effect -> bool

Check whether a effect is empty

val join_effect : effect -> effect -> effect

Compute the union of two effects

val meet_effect : effect -> effect -> effect

Compute the intersection of two effects

val fold_stmt_effect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> effect -> 'a

Fold over the statements in the effect

Effect trees

type teffect = Effect.teffect =
  1. | Teffect_empty
  2. | Teffect_node of effect * teffect * teffect

Effects are presented as binary trees. Each node of the tree is associated to a domain in the abstraction and stores the statements executed by the domain when computing a post-condition.

Note that this representation is also useful when we have an abstraction DAG (i.e. when there are shared domains) thanks to the compose (stack) operator:

A x B \___/ | C

is represented as:

o / \ x C / \ A B

val empty_teffect : teffect

Create an empty effects tree

val mk_teffect : effect -> teffect -> teffect -> teffect

mk_teffect effect left right creates an effect tree with a root containing effect and having left and right as the two sub-trees

val pp_teffect : Stdlib.Format.formatter -> teffect -> unit

Print an effects tree

val compare_teffect : teffect -> teffect -> int

Compare two effects trees

val is_empty_teffect : teffect -> bool

Check whether an effects tree is empty

val get_left_teffect : teffect -> teffect

get_left_teffect te returns the left sub-tree of te

val get_right_teffect : teffect -> teffect

get_right_teffect te returns the right sub-tree of te

val get_root_effect : teffect -> effect

get_log_stmts te returns the effect at the root node of te

val set_left_teffect : teffect -> teffect -> teffect

get_left_teffect left te sets left as the left sub-tree of te

val set_right_teffect : teffect -> teffect -> teffect

get_right_teffect right te sets right as the right sub-tree of te

val map_left_teffect : (teffect -> teffect) -> teffect -> teffect

map_left_teffect f te is equivalent to set_left_teffect (f (get_left_teffect te)) te

val map_right_teffect : (teffect -> teffect) -> teffect -> teffect

map_right_teffect f te is equivalent to set_right_teffect (f (get_right_teffect te)) te

val add_stmt_to_teffect : Ast.Stmt.stmt -> teffect -> teffect

add_stmt_to_teffect stmt teffect adds stmt to the the effects of the root no of te

val merge_teffect : (effect -> effect) -> (effect -> effect) -> (effect -> effect -> effect) -> teffect -> teffect -> teffect

merge_teffect f1 f2 f te1 te2 combines te1 and te2

val concat_teffect : old:teffect -> recent:teffect -> teffect

concat_teffect old recent puts effects in old before those in recent

val meet_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two intersected post-states

val join_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two joined post-states

val fold_stmt_teffect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> teffect -> 'a

Fold over the statements in the effects tree

Generic merge

type var_effect = Effect.var_effect = {
  1. modified : Ast.Var.VarSet.t;
  2. removed : Ast.Var.VarSet.t;
}

Effect of a statement in terms of modified and removed variables

val generic_merge : add:(Ast.Var.var -> 'b -> 'a -> 'a) -> find:(Ast.Var.var -> 'a -> 'b) -> remove:(Ast.Var.var -> 'a -> 'a) -> ?custom:(Ast.Stmt.stmt -> var_effect option) -> ('a * effect) -> ('a * effect) -> 'a * 'a

Generic merge operator. generic_merge ~add ~find ~remove ~custom (a1,e1) (a2,e2) applies a generic merge of states a1 and a2:

  • It searches for modified variables in one state's effects, gets their value using find and adds them to the other state using add.
  • It searches for removed variables in one state's effects and remove them from the other state using remove. This function handles common statements (assign,assume,add,remove,fold,expand and rename). Other statements can be handled using the custom function that returns the var_effect of a given statement.
val enable_effects : unit -> unit
val disable_effects : unit -> unit
val are_effects_enabled : unit -> bool
val set_effects_state : bool -> unit
val with_effects : (unit -> 'a) -> 'a
include module type of struct include Query end
type ('a, _) query = ('a, _) Query.query = ..

Extensible type of queries

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

Join two queries

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

Meet two queries

Registration

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

type 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

type 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

val register_query : query_info -> unit

Register a new query

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

type 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

val register_lattice_query : lattice_query_info -> unit

Register a new lattice query

Common queries

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

type 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
type token = Token.token = ..

Flow tokens are used to distinguish between different control flows

type token +=
  1. | T_cur
    (*

    Token of current (active) execution flow

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

Register a new token with its compare and print functions

val compare_token : token -> token -> int

Compare two tokens with a total order

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

Pretty printer of tokens

module 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
type domain = string
type 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
val compare_route : route -> route -> int

Set of domains

Compare two routes

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

Print a route

val toplevel : route

Toplevel tree

type routing_table = Route.routing_table

Routing table providing the domains that are part of a route

val empty_routing_table : routing_table

Empty routing table

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

Resolve a route into domains

val add_route : route -> domain -> routing_table -> routing_table

Add a route between a route and a domain

val add_routes : route -> DomainSet.t -> routing_table -> routing_table

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

val get_routes : routing_table -> route list

Get all routing_table in a routing table

val join_routing_table : routing_table -> routing_table -> routing_table

Join two routing_table table

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

Print a routing table

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

Signature of a lattice module.

type '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 * Effect.teffect) -> ('a * Effect.teffect) -> 'a;
  9. print : Print.printer -> 'a -> unit;
}

Lattice operators

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

Identifiers

type witness = Id.witness = {
  1. eq : 'a 'b. 'a id -> 'b id -> ('a, 'b) Mopsa_utils.Eq.eq option;
}
type 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

val register_id : witness_chain -> unit

Register a new descriptor

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

Equality witness of identifiers

module GenDomainId = Id.GenDomainId

Generator of a new domain identifier

module GenStatelessDomainId = Id.GenStatelessDomainId

Generator of a new identifier for stateless domains

module GenValueId = Id.GenValueId

Generator of a new value identifier

include module type of struct include Manager end

Managers

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

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

    *)
  2. get : 'a -> 't;
    (*

    Returns the domain's abstract element 't.

    *)
  3. set : 't -> 'a -> 'a;
    (*

    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. get_effects : Effect.teffect -> Effect.teffect;
    (*

    Gets the effects tree.

    *)
  9. set_effects : Effect.teffect -> Effect.teffect -> Effect.teffect;
    (*

    Sets the effect tree.

    *)
}

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

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

Symbols for printing maps, lists and sets

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

Structured print objects

type 'v set = 'v Mopsa_utils.SetExtPoly.t
type 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

type printer = Print.printer

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

val empty_printer : unit -> printer

Create an empty printer

val get_printed_object : printer -> print_object

Get the structured print object of a printer

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

Get the expressions that were already printed

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

Mark an expression as printed

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

Check whether an expression was already printed

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

Selectors of print objects

type print_path = print_selector list

Path of a print object

val find_print_object : print_path -> print_object -> print_object

find_print_object path obj returns the object placed at path in obj

val 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

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

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

val 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
val fbox : ('a, Stdlib.Format.formatter, unit, print_object) Stdlib.format4 -> 'a

fbox fmt returns a string object of a formatted value

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

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

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

fkey fmt returns a key selector with a formatted string

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

pkey f x returns a key selector with a printed string

Typed print functions

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

Print a string object

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

Print a boolean object

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

Print an integer object

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

Print an integer object

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

Print a float object

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

Print a variable

val 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

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

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

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

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

val 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

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

Pretty-print a printer objct

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

Pretty-print the printer output in a format string

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

Convert a printer function into a format function

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

Convert a format function into a printer

JSON

val print_object_to_json : print_object -> Yojson.Basic.t

Convert a printer object to JSON

val json_to_print_object : Yojson.Basic.t -> print_object

Convert JSON to a printer object

module Print = Print
include module type of struct include Avalue end
type _ avalue_kind = _ Avalue.avalue_kind = ..
type 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;
}
type 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;
}
val register_avalue : avalue_info -> unit
val type_of_avalue : 'v avalue_kind -> Ast.Typ.typ
val bottom_avalue : 'v avalue_kind -> 'v
val top_avalue : 'v avalue_kind -> 'v
val join_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
val meet_avalue : 'v avalue_kind -> 'v -> 'v -> 'v
val compare_avalue : 'v avalue_kind -> 'v -> 'w avalue_kind -> 'w -> int
val pp_avalue : 'v avalue_kind -> Stdlib.Format.formatter -> 'v -> unit
val mk_avalue_expr : 'v avalue_kind -> 'v -> Mopsa_utils.Location.range -> Ast.Expr.expr
val mk_avalue_constant : 'v avalue_kind -> 'v -> Ast.Constant.constant
type Query.query +=
  1. | Q_avalue : Ast.Expr.expr * 'v avalue_kind -> ('a, 'v) Query.query
val mk_avalue_query : Ast.Expr.expr -> 'v avalue_kind -> ('a, 'v) Query.query
include module type of struct include Utils end
val exec_cleaner : Ast.Stmt.stmt -> ('a, 'b) Manager.man -> 'a Flow.flow -> ('a, unit) Cases.cases
val exec_cleaners : ('a, 'b) Manager.man -> ('a, unit) Cases.cases -> ('a, unit) Cases.cases
val post_to_flow : ('a, 'b) Manager.man -> 'a Post.post -> 'a Flow.flow
val 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
val 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
val set_env : Token.token -> 't -> ('a, 't) Manager.man -> 'a Flow.flow -> 'a Flow.flow
val get_env : Token.token -> ('a, 't) Manager.man -> 'a Flow.flow -> 't
val map_env : Token.token -> ('t -> 't) -> ('a, 't) Manager.man -> 'a Flow.flow -> 'a Flow.flow
val get_pair_fst : ('a, 'b * 'c) Manager.man -> 'a -> 'b
val set_pair_fst : ('a, 'b * 'c) Manager.man -> 'b -> 'a -> 'a
val get_pair_snd : ('a, 'b * 'c) Manager.man -> 'a -> 'c
val set_pair_snd : ('a, 'b * 'c) Manager.man -> 'c -> 'a -> 'a
val env_exec : ('a Flow.flow -> 'a Post.post) -> 'a Context.ctx -> ('a, 't) Manager.man -> 'a -> 'a
val ask_and_reduce_cases : (('a, 'b) Query.query -> 'c -> ('d, 'b) Cases.cases) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val ask_and_reduce_list : (('a, 'b) Query.query -> 'c -> ('d * 'b) list) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val ask_and_reduce : (('a, 'b) Query.query -> 'c -> ('d, 'b) Cases.cases) -> ('a, 'b) Query.query -> ?bottom:(unit -> 'b) -> 'c -> 'b
val find_var_by_name : ?function_scope:string option -> string -> ('a, 'b) Manager.man -> 'a Flow.flow -> Ast.Var.var
val dummy_range : Mopsa_utils.Location.range
val pp_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Var.var list -> unit
val pp_vars_info_by_name : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> string list -> unit
val pp_expr_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Expr.expr -> unit
val pp_stmt_vars_info : ('a, 'b) Manager.man -> 'a Flow.flow -> Stdlib.Format.formatter -> Ast.Stmt.stmt -> unit
val breakpoint : string -> ('a, 'b) Manager.man -> 'a Flow.flow -> unit
module 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