package mopsa

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

Module Lang.Ast

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_FLOAT16
    (*

    half precision

    *)
  6. | F_REAL
    (*

    no rounding, abstracted as double

    *)
type MopsaLib.typ +=
  1. | T_int
    (*

    Mathematical integers with arbitrary precision.

    *)
  2. | T_float of float_prec
    (*

    Floating-point real numbers.

    *)
  3. | T_string
    (*

    Strings.

    *)
  4. | T_array of MopsaLib.typ
    (*

    Array of typ

    *)
  5. | T_unit
    (*

    Unit type

    *)
  6. | 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 +=
  1. | C_unit
  2. | C_int of Z.t
    (*

    Integer numbers, with arbitrary precision.

    *)
  3. | C_float of float
    (*

    Floating-point numbers.

    *)
  4. | C_string of string
    (*

    String constants.

    *)
  5. | C_int_interval of Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t * Mopsa_analyzer.MopsaLib.ItvUtils.IntBound.t
    (*

    Integer ranges.

    *)
  6. | 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 MopsaLib.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

Stack variables

This vkind is used to attach the callstack to local variables

Create a stack variable

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 : MopsaLib.range;
    (*

    function range

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

    list of parameters

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

    list of local variables

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

    body of the function

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

    return type

    *)
  8. fun_return_var : MopsaLib.var option;
    (*

    variable storing the return value

    *)
}

Function definition

type fun_builtin = {
  1. name : string;
  2. args : MopsaLib.typ option list;
  3. output : MopsaLib.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 : MopsaLib.var list;
  2. universal_fundecs : fundec list;
  3. universal_main : MopsaLib.stmt;
}
type MopsaLib.prog_kind +=
  1. | 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

Set the C program in the flow

Get the C program from the flow

Universal expressions

type MopsaLib.expr_kind +=
  1. | E_function of fun_expr
  2. | E_call of MopsaLib.expr * MopsaLib.expr list
    (*

    List of arguments

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

Universal statements

type MopsaLib.stmt_kind +=
  1. | S_expression of MopsaLib.expr
    (*

    Expression statement, useful for calling functions without a return value

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

    else branch

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

    Function return with an optional return expression

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

    loop body

    *)
  5. | S_break
    (*

    Loop break

    *)
  6. | S_continue
    (*

    Loop continue

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

    list of unit tests and their names

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

    Unit tests assertions

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

    Unit tests satisfiability check

    *)
  10. | S_print_state
    (*

    Print the abstract flow map at current location

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

    Pretty print the values of expressions

    *)
  12. | 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_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 _mod_ : ?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 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_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 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