Module `Lang.Ast`Source

Abstract Syntax Tree extension for the simple Universal language.

Universal types

Sourcetype 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_REAL
(*
no rounding, abstracted as double
*)

Sourcetype Mopsa.typ +=

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

Sourceval pp_float_prec : Stdlib.Format.formatter -> float_prec -> unit

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

Universal constants

Sourcetype Mopsa.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.ItvUtils.IntBound.t * Mopsa.ItvUtils.IntBound.t
(*
Integer ranges.
*)
| C_float_interval of float * float
(*
Float ranges.
*)

Constants.

Universal operators

Sourcetype float_class = {

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

}

Sourceval pp_float_class : Stdlib.Format.formatter -> float_class -> unit

Sourcetype Mopsa.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

Universal functions

Sourcetype fundec = {

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

}

Function definition

Sourcetype fun_builtin = {

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

}

Sourcetype fun_expr =

| User_defined of fundec
| Builtin of fun_builtin

Sourceval compare_fun_expr : fun_expr -> fun_expr -> int

Universal program

Sourcetype u_program = {

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

}

Sourcetype Mopsa.prog_kind +=

| P_universal of u_program

module UProgramKey : sig ... end

Sourceval u_program_ctx : ('a, u_program) Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

Sourceval set_u_program : u_program -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Set the C program in the flow

Sourceval get_u_program : 'a Mopsa.Flow.flow -> u_program

Get the C program from the flow

Universal expressions

Sourcetype Mopsa.expr_kind +=

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

Universal statements

Sourcetype Mopsa.stmt_kind +=

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

Utility functions

Sourceval is_universal_type : Mopsa.typ -> bool

Sourceval mk_int : int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_z : Z.t -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Source

val mk_float : 
  ?prec:float_prec ->
  float ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_int_interval : 
  int ->
  int ->
  ?typ:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_int_general_interval : 
  Mopsa.ItvUtils.IntBound.t ->
  Mopsa.ItvUtils.IntBound.t ->
  ?typ:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_z_interval : 
  Z.t ->
  Z.t ->
  ?typ:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_float_interval : 
  ?prec:float_prec ->
  float ->
  float ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_string : 
  ?etyp:Mopsa.typ ->
  string ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

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

Sourceval mk_zero : ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_one : ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_minus_one : ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval universal_constants_range : Mopsa.range

Sourceval zero : Mopsa.expr

Sourceval one : Mopsa.expr

Sourceval minus_one : Mopsa.expr

Sourceval of_z : Z.t -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval of_int : int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr

Source

val add : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val sub : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mul : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val div : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val ediv : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val _mod_ : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val erem : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?typ:Ast.Typ.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval succ : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval pred : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_succ : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_pred : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr

Source

val eq : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val ne : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val lt : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val le : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val gt : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val ge : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_eq : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_ne : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_lt : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_le : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_gt : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_ge : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val log_or : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val log_and : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val log_xor : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_log_or : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_log_and : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_log_xor : 
  Mopsa.expr ->
  Mopsa.expr ->
  ?etyp:Mopsa.typ ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

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

Sourceval inv_float_class : float_class -> float_class

Sourceval float_valid : float_class

Sourceval float_inf : float_class

Sourceval float_nan : float_class

Source

val mk_float_class : 
  float_class ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Source

val mk_filter_float_class : 
  float_class ->
  Mopsa.expr ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval mk_unit : Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_bool : bool -> Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_true : Mopsa_utils.Location.range -> Mopsa.expr

Sourceval mk_false : Mopsa_utils.Location.range -> Mopsa.expr

Sourceval is_int_type : Mopsa.typ -> bool

Sourceval is_float_type : Mopsa.typ -> bool

Sourceval is_numeric_type : Mopsa.typ -> bool

Sourceval is_math_type : Mopsa.typ -> bool

Sourceval is_predicate_op : Mopsa.operator -> bool

Sourceval mk_assert : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Sourceval mk_satisfy : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Source

val mk_block : 
  Mopsa.stmt list ->
  ?vars:Ast.Var.var list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Sourceval mk_nop : Mopsa_utils.Location.range -> Mopsa.stmt

Source

val mk_if : 
  Mopsa.expr ->
  Mopsa.stmt ->
  Mopsa.stmt ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_while : 
  Mopsa.expr ->
  Mopsa.stmt ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_call : 
  fundec ->
  Mopsa.expr list ->
  Mopsa_utils.Location.range ->
  Mopsa.expr

Sourceval mk_expr_stmt : Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.stmt

Sourceval mk_free : Mopsa.addr -> Mopsa_utils.Location.range -> Mopsa.stmt

Sourceval mk_remove_addr : Ast.Addr.addr -> Mopsa_utils.Location.range -> Mopsa.stmt

Source

val mk_invalidate_addr : 
  Ast.Addr.addr ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_rename_addr : 
  Ast.Addr.addr ->
  Ast.Addr.addr ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_expand_addr : 
  Ast.Addr.addr ->
  Ast.Addr.addr list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Source

val mk_fold_addr : 
  Ast.Addr.addr ->
  Ast.Addr.addr list ->
  Mopsa_utils.Location.range ->
  Mopsa.stmt

Sourceval expr_to_const : Mopsa.expr -> Mopsa.constant option

Sourceval expr_to_z : Mopsa.expr -> Z.t option

Sourcemodule Addr : sig ... end

Sourcemodule AddrSet : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/lang/Lang/Ast/index.html

Module `Lang.Ast`Source

Universal types

Universal constants

Universal operators

Universal functions

Universal program

Universal expressions

Universal statements

Utility functions

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/lang/Lang/Ast/index.html

Module Lang.AstSource

Universal types

Universal constants

Universal operators

Universal functions

Universal program

Universal expressions

Universal statements

Utility functions

Module `Lang.Ast`Source