Module Lang.AstSource

Abstract Syntax Tree extension for the simple Universal language.

Universal types

Sourcetype float_prec =
  1. | F_SINGLE
    (*

    IEEE single-precision 32-bit

    *)
  2. | F_DOUBLE
    (*

    IEEE double-precision 64-bit

    *)
  3. | F_LONG_DOUBLE
    (*

    extended precision, abstracted as double

    *)
  4. | F_FLOAT128
    (*

    quadruple precision, abstracted as double

    *)
  5. | F_REAL
    (*

    no rounding, abstracted as double

    *)
Sourcetype Mopsa.typ +=
  1. | T_bool
    (*

    Boolean

    *)
  2. | T_int
    (*

    Mathematical integers with arbitrary precision.

    *)
  3. | T_float of float_prec
    (*

    Floating-point real numbers.

    *)
  4. | T_string
    (*

    Strings.

    *)
  5. | T_array of Mopsa.typ
    (*

    Array of typ

    *)
  6. | T_unit
    (*

    Unit type

    *)
  7. | T_char
Sourceval pp_float_prec : Stdlib.Format.formatter -> float_prec -> unit
Sourceval pp_float_op : string -> string -> Stdlib.Format.formatter -> float_prec -> unit

Universal constants

Sourcetype Mopsa.constant +=
  1. | C_unit
  2. | C_bool of bool
  3. | C_int of Z.t
    (*

    Integer numbers, with arbitrary precision.

    *)
  4. | C_float of float
    (*

    Floating-point numbers.

    *)
  5. | C_string of string
    (*

    String constants.

    *)
  6. | C_int_interval of Mopsa.ItvUtils.IntBound.t * Mopsa.ItvUtils.IntBound.t
    (*

    Integer ranges.

    *)
  7. | C_float_interval of float * float
    (*

    Float ranges.

    *)

Constants.

Universal operators

Sourcetype float_class = {
  1. float_valid : bool;
  2. float_inf : bool;
  3. float_nan : bool;
}
Sourceval pp_float_class : Stdlib.Format.formatter -> float_class -> unit
Sourcetype Mopsa.operator +=
  1. | O_sqrt
    (*

    square root

    *)
  2. | O_abs
    (*

    absolute value

    *)
  3. | O_bit_invert
    (*

    bitwise ~

    *)
  4. | O_wrap of Z.t * Z.t
    (*

    wrap

    *)
  5. | O_filter_float_class of float_class
    (*

    filter float by class

    *)
  6. | O_plus
    (*
    *)
  7. | O_minus
    (*
    *)
  8. | O_mult
    (*

    *

    *)
  9. | O_div
    (*

    /

    *)
  10. | O_mod
    (*

    % where the remainder can be negative, following C

    *)
  11. | O_ediv
    (*

    euclidian division

    *)
  12. | O_erem
    (*

    remainder for euclidian division

    *)
  13. | O_pow
    (*

    power

    *)
  14. | O_bit_and
    (*

    &

    *)
  15. | O_bit_or
    (*

    |

    *)
  16. | O_bit_xor
    (*

    ^

    *)
  17. | O_bit_rshift
    (*

    >>

    *)
  18. | O_bit_lshift
    (*

    <<

    *)
  19. | O_concat
    (*

    concatenation of arrays and strings

    *)
  20. | O_convex_join
    (*

    convex join of arithmetic expressions

    *)
  21. | O_float_class of float_class

Universal functions

Sourcetype fundec = {
  1. fun_orig_name : string;
    (*

    original name of the function

    *)
  2. fun_uniq_name : string;
    (*

    unique name of the function

    *)
  3. fun_range : Mopsa.range;
    (*

    function range

    *)
  4. fun_parameters : Mopsa.var list;
    (*

    list of parameters

    *)
  5. fun_locvars : Mopsa.var list;
    (*

    list of local variables

    *)
  6. mutable fun_body : Mopsa.stmt;
    (*

    body of the function

    *)
  7. fun_return_type : Mopsa.typ option;
    (*

    return type

    *)
  8. fun_return_var : Mopsa.var;
    (*

    variable storing the return value

    *)
}

Function definition

Sourcetype fun_builtin = {
  1. name : string;
  2. args : Mopsa.typ option list;
  3. output : Mopsa.typ;
}
Sourcetype fun_expr =
  1. | User_defined of fundec
  2. | Builtin of fun_builtin
Sourceval compare_fun_expr : fun_expr -> fun_expr -> int

Universal program

Sourcetype u_program = {
  1. universal_gvars : Mopsa.var list;
  2. universal_fundecs : fundec list;
  3. universal_main : Mopsa.stmt;
}
Sourcetype Mopsa.prog_kind +=
  1. | 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 +=
  1. | E_function of fun_expr
  2. | E_call of Mopsa.expr * Mopsa.expr list
    (*

    List of arguments

    *)
  3. | E_array of Mopsa.expr list
  4. | E_subscript of Mopsa.expr * Mopsa.expr
  5. | E_len of Mopsa.expr

Universal statements

Sourcetype Mopsa.stmt_kind +=
  1. | S_expression of Mopsa.expr
    (*

    Expression statement, useful for calling functions without a return value

    *)
  2. | S_if of Mopsa.expr * Mopsa.stmt * Mopsa.stmt
    (*

    else branch

    *)
  3. | S_return of Mopsa.expr option
    (*

    Function return with an optional return expression

    *)
  4. | S_while of Mopsa.expr * Mopsa.stmt
    (*

    loop body

    *)
  5. | S_break
    (*

    Loop break

    *)
  6. | S_continue
    (*

    Loop continue

    *)
  7. | S_unit_tests of (string * Mopsa.stmt) list
    (*

    list of unit tests and their names

    *)
  8. | S_assert of Mopsa.expr
    (*

    Unit tests assertions

    *)
  9. | S_satisfy of Mopsa.expr
    (*

    Unit tests satisfiability check

    *)
  10. | S_print_state
    (*

    Print the abstract flow map at current location

    *)
  11. | S_print_expr of Mopsa.expr list
    (*

    Pretty print the values of expressions

    *)
  12. | S_free of Mopsa.addr
    (*

    Release a heap address

    *)

Utility functions

Sourceval is_universal_type : Mopsa.typ -> bool
Sourceval mk_float : ?prec:float_prec -> float -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_int_interval : int -> int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_z_interval : Z.t -> Z.t -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_float_interval : ?prec:float_prec -> float -> float -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_string : ?etyp:Mopsa.typ -> string -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval 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 universal_constants_range : Mopsa.range
Sourceval zero : Mopsa.expr
Sourceval minus_one : Mopsa.expr
Sourceval _mod_ : Mopsa.expr -> Mopsa.expr -> ?typ:Ast.Typ.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
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_block : Mopsa.stmt list -> ?vars:Ast.Var.var 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