package mopsa

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

Abstract Syntax Tree for stub specification. Similar to the AST of the parser, except for expressions, types and variables for which MOPSA counterparts are used.

type stub_func = {
  1. stub_func_name : string;
  2. stub_func_body : section list;
  3. stub_func_params : Mopsa.var list;
  4. stub_func_locals : local Mopsa.with_range list;
  5. stub_func_assigns : assigns Mopsa.with_range list;
  6. stub_func_return_type : Mopsa.typ option;
  7. stub_func_range : Mopsa.range;
}

Stub for a function

and stub_directive = {
  1. stub_directive_body : section list;
  2. stub_directive_locals : local Mopsa.with_range list;
  3. stub_directive_assigns : assigns Mopsa.with_range list;
  4. stub_directive_range : Mopsa.range;
}

Stub for a global directive

Stub sections

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

and section =
  1. | S_case of case
  2. | S_leaf of leaf
and leaf =
  1. | S_local of local Mopsa.with_range
  2. | S_assumes of assumes Mopsa.with_range
  3. | S_requires of requires Mopsa.with_range
  4. | S_assigns of assigns Mopsa.with_range
  5. | S_ensures of ensures Mopsa.with_range
  6. | S_free of free Mopsa.with_range
  7. | S_message of message Mopsa.with_range
and case = {
  1. case_label : string;
  2. case_body : leaf list;
  3. case_locals : local Mopsa.with_range list;
  4. case_assigns : assigns Mopsa.with_range list;
  5. case_range : Mopsa.range;
}

Leaf sections

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

and requires = formula Mopsa.with_range
and local = {
  1. lvar : Mopsa.var;
  2. lval : local_value;
}
and local_value =
  1. | L_new of resource
  2. | L_call of Mopsa.expr * Mopsa.expr list
and assigns = {
  1. assign_target : Mopsa.expr;
  2. assign_offset : interval list;
}
and free = Mopsa.expr
and message = {
  1. message_kind : message_kind;
  2. message_body : string;
}
and message_kind =
  1. | WARN
  2. | UNSOUND
and log_binop = Mopsa_c_stubs_parser.Cst.log_binop =
  1. | AND
  2. | OR
  3. | IMPLIES
and set =
  1. | S_interval of interval
  2. | S_resource of resource
and interval = Mopsa.expr * Mopsa.expr

Formulas

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

val compare_assigns : assigns -> assigns -> int
val compare_resource : 'a -> 'a -> int
val compare_set : set -> set -> int
val compare_formula : formula Mopsa.with_range -> formula Mopsa.with_range -> int

Expressions

type quant =
  1. | FORALL
  2. | EXISTS

Quantifiers

type Mopsa.expr_kind +=
  1. | E_stub_call of stub_func * Mopsa.expr list
    (*

    arguments

    *)
  2. | E_stub_return
    (*

    Returned value of a stub

    *)
  3. | E_stub_builtin_call of builtin * Mopsa.expr list
    (*

    Call to a built-in function

    *)
  4. | E_stub_attribute of Mopsa.expr * string
    (*

    Access to an attribute of a resource

    *)
  5. | E_stub_alloc of string * Mopsa.mode
    (*

    strong or weak

    *)
  6. | E_stub_resource_mem of Mopsa.expr * resource
    (*

    Filter environments in which an instance is in a resource pool

    *)
  7. | E_stub_primed of Mopsa.expr
    (*

    Primed expressions denoting values in the post-state

    *)
  8. | E_stub_quantified_formula of (quant * Mopsa.var * set) list * Mopsa.expr
    (*

    Quantifier-free formula

    *)
  9. | E_stub_otherwise of Mopsa.expr * Mopsa.expr option
    (*

    alarm

    *)
  10. | E_stub_raise of string
    (*

    message

    *)
  11. | E_stub_if of Mopsa.expr * Mopsa.expr * Mopsa.expr
    (*

    else

    *)

Conditional stub expression

Statements

type Mopsa.stmt_kind +=
  1. | S_stub_directive of stub_directive
    (*

    A call to a stub directive, which are stub functions called at the initialization of the analysis. Useful to initialize variables with stub formulas.

    *)
  2. | S_stub_free of Mopsa.expr
    (*

    Release a resource

    *)
  3. | S_stub_requires of Mopsa.expr
    (*

    Filter the current environments that verify a condition, and raise an alarm if the condition may be violated.

    *)
  4. | S_stub_prepare_all_assigns of assigns list
    (*

    Prepare primed copies of assigned objects

    *)
  5. | S_stub_assigns of assigns
    (*

    Declare an assigned object

    *)
  6. | S_stub_clean_all_assigns of assigns list
    (*

    Clean the post-state of primed copies

    *)

Heap addresses for resources

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

type Mopsa.addr_kind +=
  1. | A_stub_resource of string
    (*

    resource address

    *)

Utility functions

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

val mk_stub_builtin_call : builtin -> Mopsa.expr list -> etyp:Ast.Typ.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_stub_resource_mem : Mopsa.expr -> resource -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_stub_prepare_all_assigns : assigns Mopsa.with_range list -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_stub_assigns : Mopsa.expr -> interval list -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_stub_clean_all_assigns : assigns Mopsa.with_range list -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_stub_requires : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_stub_quantified_formula : ?etyp:Mopsa.typ -> (quant * Mopsa.var * set) list -> Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_stub_otherwise : Mopsa.expr -> Mopsa.expr option -> ?etyp:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val is_stub_primed : Ast.Expr.expr -> bool
val find_var_quantifier : Mopsa.var -> ('a * Mopsa.var * 'b) list -> 'a * 'b
val find_var_quantifier_opt : Mopsa.var -> ('a * Mopsa.var * 'b) list -> ('a * 'b) option
val is_quantified_var : Mopsa.var -> ('a * Mopsa.var * 'b) list -> bool
val is_forall_quantified_var : Mopsa.var -> (quant * Mopsa.var * 'a) list -> bool
val is_exists_quantified_var : Mopsa.var -> (quant * Mopsa.var * 'a) list -> bool
val find_quantified_var_interval : Mopsa.var -> ('a * Mopsa.var * set) list -> Mopsa.expr * Mopsa.expr
val find_quantified_var_interval_opt : Mopsa.var -> ('a * Mopsa.var * set) list -> (Mopsa.expr * Mopsa.expr) option
val negate_stub_quantified_formula : (quant * 'a * 'b) list -> Mopsa.expr -> (quant * 'c * 'd) list * Mopsa.expr

Visit expressions present in a formula

val mk_stub_alloc_resource : ?mode:Mopsa.mode -> string -> Mopsa_utils.Location.range -> Mopsa.expr
val negate_log_binop : log_binop -> log_binop

Pretty printers

=-=-=-=-=-=-=-=-=-=

val pp_builtin : Format.formatter -> Parsing.Cst.builtin -> unit
val pp_quantifier : Format.formatter -> quant -> unit
val pp_formula : Format.formatter -> formula Mopsa.with_range -> unit
val pp_set : Format.formatter -> set -> unit
val pp_interval : Format.formatter -> interval -> unit
val pp_resource : Format.formatter -> resource -> unit
val pp_list : (Format.formatter -> 'a -> unit) -> (unit, Format.formatter, unit) format -> Format.formatter -> 'a list -> unit
val pp_opt : ('a -> 'b -> unit) -> 'c -> 'd option -> unit
val pp_local : Format.formatter -> local Mopsa.with_range -> unit
val pp_local_value : Format.formatter -> local_value -> unit
val pp_assigns : Format.formatter -> assigns Mopsa.with_range -> unit
val pp_assumes : Format.formatter -> assumes Mopsa.with_range -> unit
val pp_message : Format.formatter -> message Mopsa.with_range -> unit
val pp_leaf_section : Format.formatter -> leaf -> unit
val pp_leaf_sections : Format.formatter -> leaf list -> unit
val pp_case : Format.formatter -> case -> unit
val pp_section : Format.formatter -> section -> unit
val pp_sections : Format.formatter -> section list -> unit
val pp_stub_func : Format.formatter -> stub_func -> unit
val pp_stub_directive : Format.formatter -> stub_directive -> unit

Registration of expressions

Registration of statements

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