package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

Abstract Syntax Tree extension for the simple Universal language.

Universal types

type 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

    *)
type 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
val pp_float_prec : Format.formatter -> float_prec -> unit
val pp_float_op : string -> string -> Format.formatter -> float_prec -> unit

Universal constants

type 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

type float_class = {
  1. float_valid : bool;
  2. float_inf : bool;
  3. float_nan : bool;
}
val pp_float_class : Format.formatter -> float_class -> unit
type 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

type 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

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

Universal program

type u_program = {
  1. universal_gvars : Mopsa.var list;
  2. universal_fundecs : fundec list;
  3. universal_main : Mopsa.stmt;
}
type Mopsa.prog_kind +=
  1. | P_universal of u_program
module UProgramKey : sig ... end
val u_program_ctx : ('a, u_program) Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

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

Set the C program in the flow

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

Get the C program from the flow

Universal expressions

type 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

type 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

val is_universal_type : Mopsa.typ -> bool
val mk_int : int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_float : ?prec:float_prec -> float -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_int_interval : int -> int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_z_interval : Z.t -> Z.t -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_float_interval : ?prec:float_prec -> float -> float -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_string : ?etyp:Mopsa.typ -> string -> Mopsa_utils.Location.range -> Mopsa.expr
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
val mk_minus_one : ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val universal_constants_range : Mopsa.range
val zero : Mopsa.expr
val one : Mopsa.expr
val minus_one : Mopsa.expr
val of_int : int -> ?typ:Mopsa.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val _mod_ : Mopsa.expr -> Mopsa.expr -> ?typ:Ast.Typ.typ -> Mopsa_utils.Location.range -> Mopsa.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_filter_float_class : float_class -> Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_bool : bool -> Mopsa_utils.Location.range -> Mopsa.expr
val is_int_type : Mopsa.typ -> bool
val is_float_type : Mopsa.typ -> bool
val is_numeric_type : Mopsa.typ -> bool
val is_math_type : Mopsa.typ -> bool
val is_predicate_op : Mopsa.operator -> bool
val mk_block : Mopsa.stmt list -> ?vars:Ast.Var.var list -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_invalidate_addr : Ast.Addr.addr -> Mopsa_utils.Location.range -> Mopsa.stmt
val expr_to_const : Mopsa.expr -> Mopsa.constant option
val expr_to_z : Mopsa.expr -> Z.t option
module Addr : sig ... end
module AddrSet : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct