package mopsa

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

AST of the C language.

Types

type c_typedef = {
  1. c_typedef_org_name : string;
    (*

    name as in source

    *)
  2. c_typedef_unique_name : string;
    (*

    unique name

    *)
  3. mutable c_typedef_def : Mopsa.typ;
    (*

    declaration

    *)
  4. c_typedef_range : Mopsa.Location.range;
    (*

    declaration location

    *)
}

Type definition.

and c_record_kind =
  1. | C_struct
  2. | C_union
    (*

    Whether a record is struct or union.

    *)
and c_record_type = {
  1. c_record_kind : c_record_kind;
  2. c_record_org_name : string;
    (*

    name as in source, may be empty

    *)
  3. c_record_unique_name : string;
    (*

    unique, non-empty name

    *)
  4. c_record_defined : bool;
    (*

    false if only declared

    *)
  5. c_record_sizeof : Z.t;
    (*

    size of record, in bytes

    *)
  6. c_record_alignof : Z.t;
    (*

    alignment, in bytes

    *)
  7. mutable c_record_fields : c_record_field list;
  8. c_record_range : Mopsa.Location.range;
    (*

    declaration location

    *)
}

Struct or union type.

and c_record_field = {
  1. c_field_org_name : string;
    (*

    may be empty for anonymous or padding fields

    *)
  2. c_field_name : string;
    (*

    non-empty name

    *)
  3. c_field_offset : int;
  4. c_field_bit_offset : int;
  5. c_field_type : Mopsa.typ;
  6. c_field_range : Mopsa.Location.range;
    (*

    declaration location

    *)
  7. c_field_index : int;
}

Struct or union field.

and c_enum_type = {
  1. c_enum_org_name : string;
    (*

    name as in source, may be empty

    *)
  2. c_enum_unique_name : string;
    (*

    unique, non-empty name

    *)
  3. c_enum_defined : bool;
    (*

    false if only declared

    *)
  4. c_enum_values : c_enum_value list;
  5. c_enum_integer_type : c_integer_type;
  6. c_enum_range : Mopsa.Location.range;
    (*

    declaration location

    *)
}

Enumerated type.

and c_enum_value = {
  1. c_enum_val_org_name : string;
    (*

    name as in source

    *)
  2. c_enum_val_unique_name : string;
    (*

    unique name

    *)
  3. c_enum_val_value : Z.t;
  4. c_enum_val_range : Mopsa.range;
}

A possible value in an enumerated type.

and c_integer_type =
  1. | C_signed_char
  2. | C_unsigned_char
  3. | C_signed_short
  4. | C_unsigned_short
  5. | C_signed_int
  6. | C_unsigned_int
  7. | C_signed_long
  8. | C_unsigned_long
  9. | C_signed_long_long
  10. | C_unsigned_long_long
  11. | C_signed_int128
  12. | C_unsigned_int128
    (*

    Integer types.

    *)
and c_float_type =
  1. | C_float
  2. | C_double
  3. | C_long_double
  4. | C_float128
    (*

    Floating-point types.

    *)
and c_array_length =
  1. | C_array_no_length
  2. | C_array_length_cst of Z.t
  3. | C_array_length_expr of Mopsa.expr
    (*

    Cases of arrays length.

    *)
and c_qual = {
  1. c_qual_is_const : bool;
  2. c_qual_is_volatile : bool;
  3. c_qual_is_restrict : bool;
}

Type qualifiers.

and c_function_type = {
  1. c_ftype_return : Mopsa.typ;
  2. c_ftype_params : Mopsa.typ list;
  3. c_ftype_variadic : bool;
}

Function type.

type Mopsa.typ +=
  1. | T_c_void
    (*

    Void type.

    *)
  2. | T_c_bool
  3. | T_c_integer of c_integer_type
  4. | T_c_float of c_float_type
  5. | T_c_pointer of Mopsa.typ
    (*

    Scalar types.

    *)
  6. | T_c_array of Mopsa.typ * c_array_length
    (*

    Arrays.

    *)
  7. | T_c_bitfield of Mopsa.typ * int
    (*

    Bitfields, with bit-width, only used in struct.

    *)
  8. | T_c_function of c_function_type option
    (*

    Function, with or without a prototype

    *)
  9. | T_c_builtin_fn
    (*

    Built-in functions

    *)
  10. | T_c_typedef of c_typedef
    (*

    Typedefs

    *)
  11. | T_c_record of c_record_type
    (*

    struct and union

    *)
  12. | T_c_enum of c_enum_type
    (*

    enums

    *)
  13. | T_c_qualified of c_qual * Mopsa.typ
    (*

    Qualified type.

    *)
  14. | T_c_block_object of Mopsa.typ
    (*

    Type of block objects.

    *)

Function descriptor

***********************

type c_fundec = {
  1. mutable c_func_uid : int;
    (*

    unique identifier

    *)
  2. mutable c_func_org_name : string;
    (*

    original name

    *)
  3. mutable c_func_unique_name : string;
    (*

    unique name for globals and statics

    *)
  4. c_func_is_static : bool;
  5. mutable c_func_return : Mopsa.typ;
    (*

    type of returned value

    *)
  6. mutable c_func_parameters : Mopsa.var list;
    (*

    function parameters

    *)
  7. mutable c_func_body : Mopsa.stmt option;
    (*

    function body

    *)
  8. mutable c_func_static_vars : Mopsa.var list;
    (*

    static variables declared in the function

    *)
  9. mutable c_func_local_vars : Mopsa.var list;
    (*

    local variables declared in the function (excluding parameters)

    *)
  10. mutable c_func_variadic : bool;
    (*

    whether the has a variable number of arguments

    *)
  11. mutable c_func_range : Mopsa.range;
    (*

    location range of the declaration

    *)
  12. mutable c_func_name_range : Mopsa.range;
    (*

    location range of the name in the declaration

    *)
  13. mutable c_func_stub : Stubs.Ast.stub_func option;
    (*

    stub comment

    *)
}

Function descriptor.

C variables

type c_var_scope =
  1. | Variable_global
    (*

    global shared among translation units

    *)
  2. | Variable_extern
    (*

    declared but not defined

    *)
  3. | Variable_local of c_fundec
    (*

    local to a function

    *)
  4. | Variable_parameter of c_fundec
    (*

    formal argument

    *)
  5. | Variable_file_static of string
    (*

    restricted to a translation unit

    *)
  6. | Variable_func_static of c_fundec
    (*

    restricted to a function

    *)
val pp_scope : Format.formatter -> c_var_scope -> unit
type c_var_init =
  1. | C_init_expr of Mopsa.expr
  2. | C_init_list of c_var_init list * c_var_init option
    (*

    filler

    *)
  3. | C_init_implicit of Mopsa.typ

Variable initialization.

type cvar = {
  1. cvar_scope : c_var_scope;
    (*

    life-time scope of the variable

    *)
  2. cvar_range : Mopsa.range;
    (*

    declaration range

    *)
  3. cvar_uid : int;
  4. cvar_orig_name : string;
  5. cvar_uniq_name : string;
}
type Mopsa.var_kind +=
  1. | V_cvar of cvar
    (*

    C variable

    *)

C expressions

type Mopsa.operator +=
  1. | O_c_and
  2. | O_c_or
type c_inc_location =
  1. | PRE
  2. | POST
    (*

    Whether an incrementation is performed before (PRE) or after (POST) the expression value is used

    *)
type c_inc_direction =
  1. | INC
  2. | DEC
    (*

    Whether an incrementation is ++ or --

    *)
type c_character_kind =
  1. | C_char_ascii
  2. | C_char_wide
  3. | C_char_utf8
  4. | C_char_utf16
  5. | C_char_utf32
  6. | C_char_unevaluated
type Mopsa.constant +=
  1. | C_c_character of Z.t * c_character_kind
    (*

    Constant character

    *)
  2. | C_c_string of string * c_character_kind
    (*

    Constant string literal

    *)
  3. | C_c_invalid
    (*

    Invalid pointer value

    *)
type Mopsa.expr_kind +=
  1. | E_c_conditional of Mopsa.expr * Mopsa.expr * Mopsa.expr
    (*

    else

    *)
  2. | E_c_array_subscript of Mopsa.expr * Mopsa.expr
    (*

    index

    *)
  3. | E_c_member_access of Mopsa.expr * int * string
    (*

    field

    *)
  4. | E_c_function of c_fundec
  5. | E_c_builtin_function of string
  6. | E_c_builtin_call of string * Mopsa.expr list
  7. | E_c_arrow_access of Mopsa.expr * int * string
    (*

    field

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

    rvalue

    *)
  9. | E_c_compound_assign of Mopsa.expr * Mopsa.typ * Mopsa.operator * Mopsa.expr * Mopsa.typ
    (*

    type of the result, before converting back to lvalue type

    *)
  10. | E_c_comma of Mopsa.expr * Mopsa.expr
    (*

    , operator

    *)
  11. | E_c_increment of c_inc_direction * c_inc_location * Mopsa.expr
  12. | E_c_address_of of Mopsa.expr
    (*

    & operator (address of lvalue)

    *)
  13. | E_c_deref of Mopsa.expr
    (*

    * operator (pointer dereference)

    *)
  14. | E_c_cast of Mopsa.expr * bool
    (*

    explicitness

    *)
  15. | E_c_statement of Mopsa.stmt
  16. | E_c_predefined of string
    (*

    predefined identifier

    *)
  17. | E_c_var_args of Mopsa.expr
    (*

    __builtin_va_arg

    *)
  18. | E_c_atomic of int * Mopsa.expr * Mopsa.expr
  19. | E_c_block_object of Mopsa.expr
    (*

    Block objects are useful to distinguish between operations on the block itself and its content. For, expanding the contents of a block will duplicate every cell in the block, while expanding the block object will update the pointers that point to the block.

    *)

Scope update

type c_scope_update = {
  1. c_scope_var_added : Mopsa.var list;
  2. c_scope_var_removed : Mopsa.var list;
}

Scope update information for jump statements

Statements

type Mopsa.stmt_kind +=
  1. | S_c_goto_stab of Mopsa.stmt
    (*

    stabilization point for goto statement

    *)
  2. | S_c_declaration of Mopsa.var * c_var_init option * c_var_scope
    (*

    declaration of a variable

    *)
  3. | S_c_do_while of Mopsa.stmt * Mopsa.expr
    (*

    condition

    *)
  4. | S_c_for of Mopsa.stmt * Mopsa.expr option * Mopsa.expr option * Mopsa.stmt
    (*

    body

    *)
  5. | S_c_return of Mopsa.expr option * c_scope_update
    (*

    return statement

    *)
  6. | S_c_break of c_scope_update
    (*

    break statement

    *)
  7. | S_c_continue of c_scope_update
    (*

    continue statement

    *)
  8. | S_c_goto of string * c_scope_update
    (*

    goto statements.

    *)
  9. | S_c_switch of Mopsa.expr * Mopsa.stmt
    (*

    switch statement.

    *)
  10. | S_c_label of string
    (*

    statement label.

    *)
  11. | S_c_switch_case of Mopsa.expr list * c_scope_update
    (*

    case of a switch statement.

    case a: case b: stmt;

    is represented through S_c_switch_case a; b to factor in some cases

    For integer cases, we use the interval a, b to simplify expressions, similar to the GCC C extension for ranges

    *)
  12. | S_c_switch_default of c_scope_update
    (*

    default case of switch statements.

    *)
  13. | S_c_asm of string
    (*

    inline assembly for now, we keep only a string representation to display warnings; see C_AST.asm_kind for a more usable representation when support is added

    *)
type c_program = {
  1. c_globals : (Mopsa.var * c_var_init option) list;
    (*

    global variables of the program

    *)
  2. c_functions : c_fundec list;
    (*

    functions of the program

    *)
  3. c_stub_directives : Stubs.Ast.stub_directive list;
    (*

    list of stub directives

    *)
}
type Mopsa.prog_kind +=
  1. | C_program of c_program
module CProgramKey : sig ... end
val c_program_ctx : ('a, c_program) Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

val set_c_program : c_program -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Set the C program in the flow

val get_c_program : 'a Mopsa.Flow.flow -> c_program

Get the C program from the flow

Conversion to/from Clang parser types

val to_clang_float_type : c_float_type -> Mopsa_c_parser.C_AST.float_type
val from_clang_float_type : Mopsa_c_parser.C_AST.float_type -> c_float_type

Target information

module TargetCtx : sig ... end
val remove_c_target_info : 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Sizes and alignments

val sizeof_type_in_target : Mopsa.typ -> Mopsa_c_parser.C_utils.C.target_info -> Z.t

sizeof t computes the size (in bytes) of a C type t

val sizeof_type : Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t
val sizeof_type_in_host : Mopsa.typ -> Z.t

Size (in bytes) of a type, as an expression. Handles variable-length ararys.

val remove_typedef : Mopsa.typ -> Mopsa.typ
val remove_qual : Mopsa.typ -> Mopsa.typ
val remove_typedef_qual : Mopsa.typ -> Mopsa.typ
val is_signed : Mopsa.typ -> bool

is_signed t whether t is signed

val rangeof : Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t * Z.t

range t computes the interval range of type t

val int_rangeof : Mopsa.typ -> 'a Mopsa.Flow.flow -> int * int

range t computes the interval range of type t as integers

wrap_expr e (l,h) expression needed to bring back e in range (l,h)

val is_c_char_type : Mopsa.typ -> bool
val is_c_string_type : Mopsa.typ -> bool
val is_c_int_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is an integer type

val is_c_int_array_type : Mopsa.typ -> bool
val is_c_signed_int_type : Mopsa.typ -> bool
val is_c_bool_type : Mopsa.typ -> bool
val is_c_float_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is a floating point type

val get_c_float_type : Mopsa.typ -> c_float_type
val get_c_float_precision : Mopsa.typ -> Universal.Ast.float_prec

Get the float precision from a C type

val is_c_bitfield : Mopsa.typ -> bool
val is_c_num_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is a numeric type

val is_c_scalar_type : Mopsa.typ -> bool

is_c_scalar_type t tests whether t is a scalar type

val is_c_pointer_type : Mopsa.typ -> bool

is_c_pointer t tests whether t is a pointer

val is_c_void_type : Mopsa.typ -> bool
val is_c_record_type : Mopsa.typ -> bool
val is_c_struct_type : Mopsa.typ -> bool
val is_c_union_type : Mopsa.typ -> bool
val is_c_array_type : Mopsa.typ -> bool
val is_c_function_type : Mopsa.typ -> bool
val pointer_type : Mopsa.typ -> Mopsa.typ

is_scalartype t lifts t to a pointer to t

val under_pointer_type : Mopsa.typ -> Mopsa.typ
val under_array_type : Mopsa.typ -> Mopsa.typ
val under_type : Mopsa.typ -> Mopsa.typ
val void_to_char : Mopsa.typ -> Mopsa.typ
val get_array_constant_length : Mopsa.typ -> Z.t
val align_byte : Mopsa.typ -> int -> int
val is_c_type : Mopsa.typ -> bool
val is_c_function_parameter : Mopsa.var -> bool
val mk_c_member_access_by_name : Mopsa.expr -> string -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_arrow_access_by_name : Mopsa.expr -> string -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_subscript_access : Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_character : char -> Mopsa_utils.Location.range -> Mopsa.typ -> Mopsa.expr
val extract_multibyte_integer : string -> int -> Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t
val mk_c_multibyte_integer : string -> int -> Mopsa.typ -> 'a Mopsa.Flow.flow -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_invalid_pointer : Mopsa_utils.Location.range -> Mopsa.expr
val void : Mopsa.typ
val u8 : Mopsa.typ
val s8 : Mopsa.typ
val s16 : Mopsa.typ
val u16 : Mopsa.typ
val s32 : Mopsa.typ
val u32 : Mopsa.typ
val s64 : Mopsa.typ
val u64 : Mopsa.typ
val ul : Mopsa.typ
val sl : Mopsa.typ
val ull : Mopsa.typ
val sll : Mopsa.typ
val array_type : Mopsa.typ -> Z.t -> Mopsa.typ
val size_type : 'a Mopsa.Flow.flow -> Mopsa.typ
val type_of_string : string -> Mopsa.typ
val is_c_block_object_type : Mopsa.typ -> bool
val to_c_block_object : Mopsa.expr -> Mopsa.expr
val of_c_block_object : Mopsa.expr -> Mopsa.expr
val mk_c_string : ?kind:c_character_kind -> string -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_fun_typ : c_fundec -> Mopsa.typ
val mk_c_builtin_call : string -> Mopsa.expr list -> Ast.Typ.typ -> Mopsa_utils.Location.range -> Mopsa.expr
val mk_c_call_stmt : c_fundec -> Mopsa.expr list -> Mopsa_utils.Location.range -> Mopsa.stmt
val mk_c_declaration : Mopsa.var -> c_var_init option -> c_var_scope -> Mopsa_utils.Location.range -> Mopsa.stmt
val is_c_global_scope : c_var_scope -> bool

Statement comparison *

val compare_c_var_init : c_var_init -> c_var_init -> int
val compare_c_fundec : c_fundec -> c_fundec -> int
val compare_c_var_scope : c_var_scope -> c_var_scope -> int
val compare_c_var_scope_update : c_scope_update -> c_scope_update -> int
val remove_casts : Mopsa.expr -> Mopsa.expr
val c_expr_to_z : Mopsa.expr -> 'a Mopsa.Flow.flow -> Z.t option

Simplify C constant expressions to constants

val is_c_expr_equals_z : Mopsa.expr -> Z.t -> 'a Mopsa.Flow.flow -> bool
val is_c_constant : Mopsa.expr -> 'a Mopsa.Flow.flow -> bool
val is_c_lval : Mopsa.expr -> bool
val is_c_deref : Mopsa.expr -> bool
val get_c_deref_type : Mopsa.expr -> Mopsa.typ
val is_c_variable_length_array_type : Mopsa.typ -> bool

Check if v is declared as a variable length array

val is_c_no_length_array_type : Mopsa.typ -> bool

Check if v is declared as an array without length (as for many auxiliary variables)

val find_c_fundec_by_name : string -> 'a Mopsa.Flow.flow -> c_fundec

Find the definition of a C function

val find_c_fundec_by_uid : int -> 'a Mopsa.Flow.flow -> c_fundec
val assert_valid_string : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a nul-terminated array

val assert_valid_wide_string : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a nul-terminated wide char array

val assert_valid_stream : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a valid stream

val assert_valid_file_descriptor : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a valid file descriptor

val assert_valid_ptr : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer is valid

Randomize an entire array

Randomize a string

Randomize a substring

Randomize a wide substring

Set elements of an array with the same value c

Copy elements of an array

Exit if status is non-zero

val error_error_at_line : Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Exit if status is non-zero

val asprintf_stub : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Eval.eval
val vasprintf_stub : bool -> Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Eval.eval

Stack variables

type Mopsa.var_kind +=
  1. | V_c_stack_var of Mopsa.callstack * Mopsa.var

This vkind is used to attach the callstack to local variables

val mk_stack_var : Mopsa.callstack -> Mopsa.var -> Mopsa.var

Create a stack variable

val var_scope : Mopsa.var -> c_var_scope
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