package mopsa

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

Module Stubs.Ast

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 : MopsaLib.var list;
  4. stub_func_locals : local MopsaLib.with_range list;
  5. stub_func_assigns : assigns MopsaLib.with_range list;
  6. stub_func_return_type : MopsaLib.typ option;
  7. stub_func_range : MopsaLib.range;
}

Stub for a function

and stub_directive = {
  1. stub_directive_body : section list;
  2. stub_directive_locals : local MopsaLib.with_range list;
  3. stub_directive_assigns : assigns MopsaLib.with_range list;
  4. stub_directive_range : MopsaLib.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 MopsaLib.with_range
  2. | S_assumes of assumes MopsaLib.with_range
  3. | S_requires of requires MopsaLib.with_range
  4. | S_assigns of assigns MopsaLib.with_range
  5. | S_ensures of ensures MopsaLib.with_range
  6. | S_free of free MopsaLib.with_range
  7. | S_message of message MopsaLib.with_range
and case = {
  1. case_label : string;
  2. case_body : leaf list;
  3. case_locals : local MopsaLib.with_range list;
  4. case_assigns : assigns MopsaLib.with_range list;
  5. case_range : MopsaLib.range;
}

Leaf sections

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

and local = {
  1. lvar : MopsaLib.var;
  2. lval : local_value;
}
and local_value =
  1. | L_new of resource
  2. | L_call of MopsaLib.expr * MopsaLib.expr list
and assigns = {
  1. assign_target : MopsaLib.expr;
  2. assign_offset : interval list;
}
and free = MopsaLib.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 = MopsaLib.expr * MopsaLib.expr

Formulas

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

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

Expressions

type quant =
  1. | FORALL
  2. | EXISTS

Quantifiers

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

    arguments

    *)
  2. | E_stub_return
    (*

    Returned value of a stub

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

    Call to a built-in function

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

    Access to an attribute of a resource

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

    strong or weak

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

    Filter environments in which an instance is in a resource pool

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

    Primed expressions denoting values in the post-state

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

    Quantifier-free formula

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

    alarm

    *)
  10. | E_stub_raise of string
    (*

    message

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

    else

    *)

Conditional stub expression

Statements

type MopsaLib.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 MopsaLib.expr
    (*

    Release a resource

    *)
  3. | S_stub_requires of MopsaLib.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 MopsaLib.addr_kind +=
  1. | A_stub_resource of string
    (*

    resource address

    *)
val opt_stub_resource_allocation_policy : string ref

Utility functions

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

val mk_stub_prepare_all_assigns : assigns MopsaLib.with_range list -> Mopsa_utils.Core.Location.range -> MopsaLib.stmt
val mk_stub_quantified_formula : ?etyp:MopsaLib.typ -> (quant * MopsaLib.var * set) list -> MopsaLib.expr -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val is_stub_primed : Framework.Core.Ast.Expr.expr -> bool
val find_var_quantifier : MopsaLib.var -> ('a * MopsaLib.var * 'b) list -> 'a * 'b
val find_var_quantifier_opt : MopsaLib.var -> ('a * MopsaLib.var * 'b) list -> ('a * 'b) option
val is_quantified_var : MopsaLib.var -> ('a * MopsaLib.var * 'b) list -> bool
val is_forall_quantified_var : MopsaLib.var -> (quant * MopsaLib.var * 'a) list -> bool
val is_exists_quantified_var : MopsaLib.var -> (quant * MopsaLib.var * 'a) list -> bool
val find_quantified_var_interval : MopsaLib.var -> ('a * MopsaLib.var * set) list -> MopsaLib.expr * MopsaLib.expr
val find_quantified_var_interval_opt : MopsaLib.var -> ('a * MopsaLib.var * set) list -> (MopsaLib.expr * MopsaLib.expr) option
val negate_stub_quantified_formula : (quant * 'a * 'b) list -> MopsaLib.expr -> (quant * 'a * 'b) list * MopsaLib.expr

Visit expressions present in a formula

val exprs_in_formula : formula MopsaLib.with_range -> MopsaLib.expr list
val exprs_in_set : set -> MopsaLib.expr list
val exprs_in_local : local -> MopsaLib.expr list
val exprs_in_assigns : assigns -> MopsaLib.expr list
val exprs_in_leaf : leaf -> MopsaLib.expr list
val exprs_in_case : case -> MopsaLib.expr list
val exprs_in_section : section -> MopsaLib.expr list
val exprs_in_stub_func : stub_func -> MopsaLib.expr list
val exprs_in_stub_directive : stub_directive -> MopsaLib.expr list
val mk_stub_alloc_resource : ?mode:MopsaLib.mode -> string -> Mopsa_utils.Core.Location.range -> MopsaLib.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 MopsaLib.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) -> 'a -> 'b option -> unit
val pp_local : Format.formatter -> local MopsaLib.with_range -> unit
val pp_local_value : Format.formatter -> local_value -> unit
val pp_assigns : Format.formatter -> assigns MopsaLib.with_range -> unit
val pp_assumes : Format.formatter -> assumes MopsaLib.with_range -> unit
val pp_message : Format.formatter -> message MopsaLib.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