Ast (p.mopsa.1.2.doc.mopsa.mopsa_analyzer.Mopsa_analyzer.Languages.Universal.Lang.Ast)

Universal types

type float_prec =

| F_SINGLE
(*
IEEE single-precision 32-bit
*)
| F_DOUBLE
(*
IEEE double-precision 64-bit
*)
| F_LONG_DOUBLE
(*
extended precision, abstracted as double
*)
| F_FLOAT128
(*
quadruple precision, abstracted as double
*)
| F_FLOAT16
(*
half precision
*)
| F_REAL
(*
no rounding, abstracted as double
*)

type MopsaLib.typ +=

| T_int
(*
Mathematical integers with arbitrary precision.
*)
| T_float of float_prec
(*
Floating-point real numbers.
*)
| T_string
(*
Strings.
*)
| T_array of MopsaLib.typ
(*
Array of typ
*)
| T_unit
(*
Unit type
*)
| T_char

val pp_float_prec : Format.formatter -> float_prec -> unit

val pp_float_op : string -> string -> Format.formatter -> float_prec -> unit

Universal constants

type MopsaLib.constant +=

| C_unit
| C_int of Z.t
(*
Integer numbers, with arbitrary precision.
*)
| C_float of float
(*
Floating-point numbers.
*)
| C_string of string
(*
String constants.
*)
| C_int_interval of Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t * Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t
(*
Integer ranges.
*)
| C_float_interval of float * float
(*
Float ranges.
*)

Constants.

Universal operators

type float_class = {

float_valid : bool;
float_inf : bool;
float_nan : bool;

}

val pp_float_class : Format.formatter -> float_class -> unit

type MopsaLib.operator +=

| O_sqrt
(*
square root
*)
| O_abs
(*
absolute value
*)
| O_bit_invert
(*
bitwise ~
*)
| O_wrap of Z.t * Z.t
(*
wrap
*)
| O_filter_float_class of float_class
(*
filter float by class
*)
| O_plus
(*
*)
| O_minus
(*
*)
| O_mult
(*
*
*)
| O_div
(*
/
*)
| O_mod
(*
% where the remainder can be negative, following C
*)
| O_ediv
(*
euclidian division
*)
| O_erem
(*
remainder for euclidian division
*)
| O_pow
(*
power
*)
| O_bit_and
(*
&
*)
| O_bit_or
(*
|
*)
| O_bit_xor
(*
^
*)
| O_bit_rshift
(*
>>
*)
| O_bit_lshift
(*
<<
*)
| O_concat
(*
concatenation of arrays and strings
*)
| O_convex_join
(*
convex join of arithmetic expressions
*)
| O_float_class of float_class

Stack variables

type MopsaLib.var_kind +=

| V_stack_var of MopsaLib.callstack * MopsaLib.var

This vkind is used to attach the callstack to local variables

val mk_stack_var : MopsaLib.callstack -> MopsaLib.var -> MopsaLib.var

Create a stack variable

Universal functions

type fundec = {

fun_orig_name : string;
(*
original name of the function
*)
fun_uniq_name : string;
(*
unique name of the function
*)
fun_range : MopsaLib.range;
(*
function range
*)
fun_parameters : MopsaLib.var list;
(*
list of parameters
*)
fun_locvars : MopsaLib.var list;
(*
list of local variables
*)
mutable fun_body : MopsaLib.stmt;
(*
body of the function
*)
fun_return_type : MopsaLib.typ option;
(*
return type
*)
fun_return_var : MopsaLib.var option;
(*
variable storing the return value
*)

}

Function definition

type fun_builtin = {

name : string;
args : MopsaLib.typ option list;
output : MopsaLib.typ;

}

type fun_expr =

| User_defined of fundec
| Builtin of fun_builtin

val compare_fun_expr : fun_expr -> fun_expr -> int

Universal program

type u_program = {

universal_gvars : MopsaLib.var list;
universal_fundecs : fundec list;
universal_main : MopsaLib.stmt;

}

type MopsaLib.prog_kind +=

| P_universal of u_program

module UProgramKey : sig ... end

val u_program_ctx : 
  ('a, u_program) Mopsa_analyzer__Framework__Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

val set_u_program : 
  u_program ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow

Set the C program in the flow

val get_u_program : 'a Mopsa_analyzer.MopsaLib.Flow.flow -> u_program

Get the C program from the flow

Universal expressions

type MopsaLib.expr_kind +=

| E_function of fun_expr
| E_call of MopsaLib.expr * MopsaLib.expr list
(*
List of arguments
*)
| E_array of MopsaLib.expr list
| E_subscript of MopsaLib.expr * MopsaLib.expr
| E_len of MopsaLib.expr

Universal statements

type MopsaLib.stmt_kind +=

| S_expression of MopsaLib.expr
(*
Expression statement, useful for calling functions without a return value
*)
| S_if of MopsaLib.expr * MopsaLib.stmt * MopsaLib.stmt
(*
else branch
*)
| S_return of MopsaLib.expr option
(*
Function return with an optional return expression
*)
| S_while of MopsaLib.expr * MopsaLib.stmt
(*
loop body
*)
| S_break
(*
Loop break
*)
| S_continue
(*
Loop continue
*)
| S_unit_tests of (string * MopsaLib.stmt) list
(*
list of unit tests and their names
*)
| S_assert of MopsaLib.expr
(*
Unit tests assertions
*)
| S_satisfy of MopsaLib.expr
(*
Unit tests satisfiability check
*)
| S_print_state
(*
Print the abstract flow map at current location
*)
| S_print_expr of MopsaLib.expr list
(*
Pretty print the values of expressions
*)
| S_free of MopsaLib.addr
(*
Release a heap address
*)

Utility functions

val is_universal_type : MopsaLib.typ -> bool

val mk_int : 
  ?esynthetic:bool ->
  int ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_z : 
  ?esynthetic:bool ->
  Z.t ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_float : 
  ?esynthetic:bool ->
  ?prec:float_prec ->
  float ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_int_interval : 
  ?esynthetic:bool ->
  int ->
  int ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_int_general_interval : 
  ?esynthetic:bool ->
  Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t ->
  Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_z_interval : 
  ?esynthetic:bool ->
  Z.t ->
  Z.t ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_float_interval : 
  ?esynthetic:bool ->
  ?prec:float_prec ->
  float ->
  float ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_string : 
  ?esynthetic:bool ->
  ?etyp:MopsaLib.typ ->
  string ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_in : 
  ?esynthetic:bool ->
  ?strict:bool ->
  ?left_strict:bool ->
  ?right_strict:bool ->
  ?etyp:MopsaLib.typ ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_zero : 
  ?esynthetic:bool ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_one : 
  ?esynthetic:bool ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_minus_one : 
  ?esynthetic:bool ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val universal_constants_range : MopsaLib.range

val zero : MopsaLib.expr

val one : MopsaLib.expr

val minus_one : MopsaLib.expr

val of_z : 
  ?esynthetic:bool ->
  Z.t ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val of_int : 
  ?esynthetic:bool ->
  int ->
  ?typ:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val add : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val sub : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mul : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val div : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val ediv : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val _mod_ : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val erem : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?typ:Framework.Core.Ast.Typ.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val succ : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val pred : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_succ : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_pred : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val eq : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val ne : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val lt : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val le : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val gt : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val ge : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_eq : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_ne : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_lt : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_le : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_gt : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_ge : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val log_or : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val log_and : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val log_xor : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_log_or : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_log_and : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_log_xor : 
  ?esynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  ?etyp:MopsaLib.typ ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val float_class : ?valid:bool -> ?inf:bool -> ?nan:bool -> unit -> float_class

val inv_float_class : float_class -> float_class

val float_valid : float_class

val float_inf : float_class

val float_nan : float_class

val mk_float_class : 
  ?esynthetic:bool ->
  float_class ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_filter_float_class : 
  ?esynthetic:bool ->
  float_class ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_unit : 
  ?esynthetic:bool ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_bool : 
  ?esynthetic:bool ->
  bool ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_true : 
  ?esynthetic:bool ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_false : 
  ?esynthetic:bool ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val is_int_type : MopsaLib.typ -> bool

val is_float_type : MopsaLib.typ -> bool

val is_numeric_type : MopsaLib.typ -> bool

val is_math_type : MopsaLib.typ -> bool

val is_predicate_op : MopsaLib.operator -> bool

val mk_assert : 
  ?ssynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_satisfy : 
  ?ssynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_block : 
  ?ssynthetic:bool ->
  MopsaLib.stmt list ->
  ?vars:Framework.Core.Ast.Var.var list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_nop : 
  ?ssynthetic:bool ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_if : 
  ?ssynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.stmt ->
  MopsaLib.stmt ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_while : 
  ?ssynthetic:bool ->
  MopsaLib.expr ->
  MopsaLib.stmt ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_call : 
  ?esynthetic:bool ->
  fundec ->
  MopsaLib.expr list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.expr

val mk_expr_stmt : 
  ?ssynthetic:bool ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_free : 
  ?ssynthetic:bool ->
  MopsaLib.addr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_remove_addr : 
  ?ssynthetic:bool ->
  Framework.Core.Ast.Addr.addr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_invalidate_addr : 
  ?ssynthetic:bool ->
  Framework.Core.Ast.Addr.addr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_rename_addr : 
  ?ssynthetic:bool ->
  Framework.Core.Ast.Addr.addr ->
  Framework.Core.Ast.Addr.addr ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_expand_addr : 
  Framework.Core.Ast.Addr.addr ->
  Framework.Core.Ast.Addr.addr list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val mk_fold_addr : 
  Framework.Core.Ast.Addr.addr ->
  Framework.Core.Ast.Addr.addr list ->
  Mopsa_utils.Core.Location.range ->
  MopsaLib.stmt

val expr_to_const : MopsaLib.expr -> MopsaLib.constant option

val expr_to_z : MopsaLib.expr -> Z.t option

module Addr : sig ... end

module AddrSet : sig ... end