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:??? ->
  (quant * MopsaLib.var * set) list ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_stub_otherwise : 
  MopsaLib.expr ->
  MopsaLib.expr option ->
  ?etyp:??? ->
  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:??? ->
  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

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

Module Stubs.Ast

Stub sections

Leaf sections

Formulas

Expressions

Statements

Heap addresses for resources

Utility functions

Pretty printers

Registration of expressions

Registration of statements

Module `Stubs.Ast`