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 = {

stub_func_name : string;
stub_func_body : section list;
stub_func_params : MopsaLib.var list;
stub_func_locals : local MopsaLib.with_range list;
stub_func_assigns : assigns MopsaLib.with_range list;
stub_func_return_type : MopsaLib.typ option;
stub_func_range : MopsaLib.range;

}

Stub for a function

and stub_directive = {

stub_directive_body : section list;
stub_directive_locals : local MopsaLib.with_range list;
stub_directive_assigns : assigns MopsaLib.with_range list;
stub_directive_range : MopsaLib.range;

}

Stub for a global directive

Stub sections

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

and section =

| S_case of case
| S_leaf of leaf

and leaf =

| S_local of local MopsaLib.with_range
| S_assumes of assumes MopsaLib.with_range
| S_requires of requires MopsaLib.with_range
| S_assigns of assigns MopsaLib.with_range
| S_ensures of ensures MopsaLib.with_range
| S_free of free MopsaLib.with_range
| S_message of message MopsaLib.with_range

and case = {

case_label : string;
case_body : leaf list;
case_locals : local MopsaLib.with_range list;
case_assigns : assigns MopsaLib.with_range list;
case_range : MopsaLib.range;

}

Leaf sections

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

and requires = formula MopsaLib.with_range

and ensures = formula MopsaLib.with_range

and assumes = formula MopsaLib.with_range

and local = {

lvar : MopsaLib.var;
lval : local_value;

}

and local_value =

| L_new of resource
| L_call of MopsaLib.expr * MopsaLib.expr list

and assigns = {

assign_target : MopsaLib.expr;
assign_offset : interval list;

}

and free = MopsaLib.expr

and message = {

message_kind : message_kind;
message_body : string;

}

and message_kind =

| WARN
| UNSOUND

and log_binop = Mopsa_c_stubs_parser.Cst.log_binop =

| AND
| OR
| IMPLIES

and set =

| S_interval of interval
| S_resource of resource

and interval = MopsaLib.expr * MopsaLib.expr

and resource = Mopsa_c_stubs_parser.Ast.resource

and builtin = Mopsa_c_stubs_parser.Ast.builtin

Formulas

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

and formula =

| F_expr of MopsaLib.expr
| F_binop of log_binop * formula MopsaLib.with_range * formula MopsaLib.with_range
| F_not of formula MopsaLib.with_range
| F_forall of MopsaLib.var * set * formula MopsaLib.with_range
| F_exists of MopsaLib.var * set * formula MopsaLib.with_range
| F_in of MopsaLib.expr * set
| F_otherwise of formula MopsaLib.with_range * MopsaLib.expr
| F_if of formula MopsaLib.with_range * formula MopsaLib.with_range * formula MopsaLib.with_range

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 =

| FORALL
| EXISTS

Quantifiers

type MopsaLib.expr_kind +=

| E_stub_call of stub_func * MopsaLib.expr list
(*
arguments
*)
| E_stub_return
(*
Returned value of a stub
*)
| E_stub_builtin_call of builtin * MopsaLib.expr list
(*
Call to a built-in function
*)
| E_stub_attribute of MopsaLib.expr * string
(*
Access to an attribute of a resource
*)
| E_stub_alloc of string * MopsaLib.mode
(*
strong or weak
*)
| E_stub_resource_mem of MopsaLib.expr * resource
(*
Filter environments in which an instance is in a resource pool
*)
| E_stub_primed of MopsaLib.expr
(*
Primed expressions denoting values in the post-state
*)
| E_stub_quantified_formula of (quant * MopsaLib.var * set) list * MopsaLib.expr
(*
Quantifier-free formula
*)
| E_stub_otherwise of MopsaLib.expr * MopsaLib.expr option
(*
alarm
*)
| E_stub_raise of string
(*
message
*)
| E_stub_if of MopsaLib.expr * MopsaLib.expr * MopsaLib.expr
(*
else
*)

Conditional stub expression

Statements

type MopsaLib.stmt_kind +=

| 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.
*)
| S_stub_free of MopsaLib.expr
(*
Release a resource
*)
| S_stub_requires of MopsaLib.expr
(*
Filter the current environments that verify a condition, and raise an alarm if the condition may be violated.
*)
| S_stub_prepare_all_assigns of assigns list
(*
Prepare primed copies of assigned objects
*)
| S_stub_assigns of assigns
(*
Declare an assigned object
*)
| S_stub_clean_all_assigns of assigns list
(*
Clean the post-state of primed copies
*)

Heap addresses for resources

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

type MopsaLib.addr_kind +=

| A_stub_resource of string
(*
resource address
*)

val opt_stub_resource_allocation_policy : string ref

Utility functions

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

val mk_stub_call : 
  stub_func ->
  MopsaLib.expr list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_builtin_call : 
  builtin ->
  MopsaLib.expr list ->
  etyp:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_resource_mem : 
  MopsaLib.expr ->
  resource ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_primed : 
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_directive : 
  stub_directive ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_stub_free : 
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_stub_prepare_all_assigns : 
  assigns MopsaLib.with_range list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_stub_assigns : 
  MopsaLib.expr ->
  interval list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_stub_clean_all_assigns : 
  assigns MopsaLib.with_range list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_stub_requires : 
  MopsaLib.expr ->
  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 mk_stub_otherwise : 
  MopsaLib.expr ->
  MopsaLib.expr option ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_if : 
  MopsaLib.expr ->
  MopsaLib.expr ->
  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

val visit_expr_in_formula : 
  (Framework.Core.Ast.Expr.expr ->
    Framework.Core.Ast.Expr.expr Mopsa_analyzer.MopsaLib.Visitor.visit_action) ->
  formula MopsaLib.with_range ->
  formula MopsaLib.with_range

Visit expressions present in a formula

val visit_set : 
  (Framework.Core.Ast.Expr.expr ->
    Framework.Core.Ast.Expr.expr Mopsa_analyzer.MopsaLib.Visitor.visit_action) ->
  set ->
  set

val visit_expr : 
  (Framework.Core.Ast.Expr.expr ->
    Framework.Core.Ast.Expr.expr Mopsa_analyzer.MopsaLib.Visitor.visit_action) ->
  MopsaLib.expr ->
  MopsaLib.expr

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_log_binop : 
  Format.formatter ->
  Mopsa_c_stubs_parser.Ast.log_binop ->
  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_requires : 
  Format.formatter ->
  formula MopsaLib.with_range MopsaLib.with_range ->
  unit

val pp_assigns : Format.formatter -> assigns MopsaLib.with_range -> unit

val pp_assumes : Format.formatter -> assumes MopsaLib.with_range -> unit

val pp_ensures : 
  Format.formatter ->
  formula MopsaLib.with_range MopsaLib.with_range ->
  unit

val pp_free : Format.formatter -> MopsaLib.expr 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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Stubs/Ast/index.html

Module `Stubs.Ast`

Stub sections

Leaf sections

Formulas

Expressions

Statements

Heap addresses for resources

Utility functions

Pretty printers

Registration of expressions

Registration of statements

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Stubs/Ast/index.html

Module Stubs.Ast

Stub sections

Leaf sections

Formulas

Expressions

Statements

Heap addresses for resources

Utility functions

Pretty printers

Registration of expressions

Registration of statements

dune-project
Dependency

Module `Stubs.Ast`