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
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