package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install

Dune Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (2)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/mopsa.mopsa_c_parser/Mopsa_c_parser/C_AST/index.html

Module Mopsa_c_parser.C_ASTSource

C_AST - Simpler C AST

Provides a simpler version of the AST converted from Clang.

The goal of this AST is to:

  • be independent from Clang's version
  • support linking of several translation units into a single AST
  • only support C for now

Unique identifiers (for variables and functions).

Sourcemodule UidMap : sig ... end
Sourcemodule UidSet : sig ... end
Sourcemodule StringMap : sig ... end
module RangeMap : sig ... end

Source locations.

Comments in file.

preprocessor macros

Sourcetype character_kind = Clang_AST.character_kind
Sourcetype target_info = Clang_AST.target_info

Operators

Sourcetype binary_arithmetic =
  1. | ADD
    (*
    *)
  2. | SUB
    (*
    *)
  3. | MUL
    (*

    *

    *)
  4. | DIV
    (*

    /

    *)
  5. | MOD
    (*

    %

    *)
  6. | LEFT_SHIFT
    (*

    <<

    *)
  7. | RIGHT_SHIFT
    (*

    >>

    *)
  8. | BIT_AND
    (*

    &

    *)
  9. | BIT_OR
    (*

    |

    *)
  10. | BIT_XOR
    (*

    ^

    *)
Sourcetype binary_logical =
  1. | LESS
    (*

    <

    *)
  2. | LESS_EQUAL
    (*

    <=

    *)
  3. | GREATER
    (*

    >

    *)
  4. | GREATER_EQUAL
    (*

    >=

    *)
  5. | EQUAL
    (*

    ==

    *)
  6. | NOT_EQUAL
    (*

    !=

    *)
  7. | LOGICAL_AND
    (*

    &&

    *)
  8. | LOGICAL_OR
    (*

    ||

    *)
Sourcetype binary_operator =
  1. | O_arithmetic of binary_arithmetic
  2. | O_logical of binary_logical
Sourcetype unary_operator =
  1. | NEG
    (*
    *)
  2. | BIT_NOT
    (*

    ~

    *)
  3. | LOGICAL_NOT
    (*

    !

    *)
Sourcetype explicitness =
  1. | EXPLICIT
  2. | IMPLICIT
    (*

    Whether a cast is explicit (in the source) or implicit (added for implicit conversions

    *)
Sourcetype inc_location =
  1. | PRE
  2. | POST
    (*

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

    *)
Sourcetype inc_direction =
  1. | INC
  2. | DEC
    (*

    Whether an incrementation is ++ or --

    *)

Types

Sourcetype signedness =
  1. | SIGNED
  2. | UNSIGNED
    (*

    Whether an integer type is signed or not.

    *)
Sourcetype integer_type =
  1. | Char of signedness
    (*

    plain 'char', where the signeness is defined by the platform

    *)
  2. | SIGNED_CHAR
  3. | UNSIGNED_CHAR
  4. | SIGNED_SHORT
  5. | UNSIGNED_SHORT
  6. | SIGNED_INT
  7. | UNSIGNED_INT
  8. | SIGNED_LONG
  9. | UNSIGNED_LONG
  10. | SIGNED_LONG_LONG
  11. | UNSIGNED_LONG_LONG
  12. | SIGNED_INT128
  13. | UNSIGNED_INT128
    (*

    Integer types.

    *)
Sourcetype float_type =
  1. | FLOAT
  2. | DOUBLE
  3. | LONG_DOUBLE
  4. | FLOAT128
    (*

    Floating-point types.

    *)
Sourcetype record_kind =
  1. | STRUCT
  2. | UNION
    (*

    Whether a record type is a struct or a union.

    *)
Sourcetype qualifier = {
  1. qual_is_const : bool;
}

Type qualifiers. For now, only 'const' is useful.

Sourcetype typ =
  1. | T_void
    (*

    Void type.

    *)
  2. | T_bool
  3. | T_integer of integer_type
  4. | T_float of float_type
  5. | T_complex of float_type
  6. | T_pointer of type_qual
    (*

    Scalar types.

    *)
  7. | T_array of type_qual * array_length
    (*

    Arrays.

    *)
  8. | T_bitfield of typ * int
    (*

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

    *)
  9. | T_function of function_type option
    (*

    Function, with or without a prototype

    *)
  10. | T_builtin_fn
    (*

    Built-in functions

    *)
  11. | T_typedef of typedef
    (*

    Typedefs

    *)
  12. | T_record of record_type
    (*

    struct and union

    *)
  13. | T_enum of enum_type
    (*

    enums

    *)
  14. | T_vector of vector_type
    (*

    GCC vectors

    *)
  15. | T_unknown_builtin of string
    (*

    unknown builtin

    *)

Types.

Sourceand type_qual = typ * qualifier

Type with qualifier.

Sourceand typedef = {
  1. typedef_org_name : string;
    (*

    name as in source

    *)
  2. mutable typedef_uid : uid;
  3. mutable typedef_unique_name : string;
    (*

    unique name

    *)
  4. mutable typedef_def : type_qual;
    (*

    declaration

    *)
  5. mutable typedef_range : range;
    (*

    declaration location

    *)
  6. mutable typedef_com : comment list;
    (*

    comments associated to the declaration

    *)
}
Sourceand record_type = {
  1. record_kind : record_kind;
  2. record_org_name : string;
    (*

    name as in source, may be empty

    *)
  3. mutable record_uid : uid;
    (*

    unique identifier

    *)
  4. mutable record_unique_name : string;
    (*

    unique, non-empty name

    *)
  5. mutable record_defined : bool;
    (*

    false if only declared

    *)
  6. mutable record_sizeof : Z.t;
    (*

    size of record, in bytes

    *)
  7. mutable record_alignof : Z.t;
    (*

    alignment, in bytes

    *)
  8. mutable record_fields : record_field array;
  9. mutable record_range : range;
    (*

    declaration location

    *)
  10. mutable record_com : comment list;
    (*

    comments associated to the declaration

    *)
}

Struct or union type.

Sourceand record_field = {
  1. field_uid : uid;
    (*

    unique identifier

    *)
  2. field_org_name : string;
    (*

    may be empty for anonymous or padding fields

    *)
  3. field_name : string;
    (*

    non-empty name

    *)
  4. field_offset : int;
  5. field_bit_offset : int;
  6. mutable field_type : type_qual;
  7. field_range : range;
    (*

    declaration location

    *)
  8. field_record : record_type;
  9. field_index : int;
  10. mutable field_com : comment list;
    (*

    comments associated to the declaration

    *)
}

Struct or union field.

Sourceand enum_type = {
  1. enum_org_name : string;
    (*

    name as in source, may be empty

    *)
  2. mutable enum_uid : uid;
    (*

    unoque identifier

    *)
  3. mutable enum_unique_name : string;
    (*

    unique, non-empty name

    *)
  4. mutable enum_defined : bool;
    (*

    false if only declared

    *)
  5. mutable enum_values : enum_value list;
  6. mutable enum_integer_type : integer_type option;
  7. mutable enum_range : range;
    (*

    declaration location

    *)
  8. mutable enum_com : comment list;
    (*

    comments associated to the declaration

    *)
}

Enumerated type.

Sourceand enum_value = {
  1. enum_val_uid : uid;
    (*

    unique identifier

    *)
  2. enum_val_org_name : string;
    (*

    name as in source

    *)
  3. enum_val_unique_name : string;
    (*

    unique name

    *)
  4. enum_val_value : Z.t;
  5. enum_val_enum : enum_type;
  6. enum_val_range : range;
  7. mutable enum_val_com : comment list;
    (*

    comments associated to the declaration

    *)
}

A possible value in an enumerated type.

Sourceand array_length =
  1. | No_length
  2. | Length_cst of Z.t
  3. | Length_expr of expr
    (*

    Length of an array.

    *)
Sourceand function_type = {
  1. mutable ftype_return : type_qual;
  2. mutable ftype_params : type_qual list;
  3. ftype_variadic : bool;
}

Type of functions and prototypes.

Sourceand vector_type = {
  1. vector_type : type_qual;
  2. vector_size : int;
  3. vector_kind : int;
}

GCC vector types.

Variables and functions

Sourceand variable = {
  1. var_uid : uid;
    (*

    unique identifier

    *)
  2. var_org_name : string;
    (*

    original name

    *)
  3. var_unique_name : string;
    (*

    unique name for globals and statics

    *)
  4. mutable var_kind : variable_kind;
    (*

    variable kind and life-time

    *)
  5. mutable var_type : type_qual;
  6. mutable var_init : init option;
  7. mutable var_before_stmts : statement list;
    (*

    statements executed before the declaration of the variable

    *)
  8. mutable var_after_stmts : statement list;
    (*

    statements executed after the declaration of the variable

    *)
  9. mutable var_range : range;
  10. mutable var_com : comment list;
    (*

    comments associated to the declaration

    *)
}
Sourceand variable_kind =
  1. | Variable_global
    (*

    global shared among translation units

    *)
  2. | Variable_extern
    (*

    declared but not defined

    *)
  3. | Variable_local of func
    (*

    local to a function

    *)
  4. | Variable_parameter of func
    (*

    formal argument

    *)
  5. | Variable_file_static of translation_unit
    (*

    restricted to a translation unit

    *)
  6. | Variable_func_static of func
    (*

    restricted to a function

    *)
Sourceand func = {
  1. func_uid : uid;
    (*

    unique identifier

    *)
  2. func_org_name : string;
    (*

    original name

    *)
  3. func_unique_name : string;
    (*

    unique name for globals and statics

    *)
  4. func_is_static : bool;
  5. mutable func_return : type_qual;
    (*

    type of returned value

    *)
  6. mutable func_parameters : variable array;
    (*

    function parameters

    *)
  7. mutable func_body : block option;
    (*

    function body

    *)
  8. mutable func_static_vars : variable list;
    (*

    static variables declared in the function

    *)
  9. mutable func_local_vars : variable list;
    (*

    local variables declared in the function (excluding parameters)

    *)
  10. mutable func_variadic : bool;
    (*

    whether the has a variable number of arguments

    *)
  11. mutable func_range : range;
    (*

    range of the full declaration

    *)
  12. mutable func_name_range : range;
    (*

    range of the name part of the declaration

    *)
  13. mutable func_com : (comment * macro StringMap.t) list;
    (*

    comments associated to the declaration

    *)
}

Statements and expressions

Sourceand statement = statement_kind * range
Sourceand block = {
  1. blk_stmts : statement list;
    (*

    statements in the block

    *)
  2. blk_local_vars : variable list;
    (*

    local variables declared within the block (excluding sub-blocks); these should be deallocated when exiting the block

    *)
}
Sourceand statement_kind =
  1. | S_local_declaration of variable
    (*

    local variable declaration

    *)
  2. | S_expression of expr
    (*

    expression statement

    *)
  3. | S_block of block
    (*

    statement block

    *)
  4. | S_if of expr * block * block
    (*

    else branch

    *)
  5. | S_while of expr * block
    (*

    body

    *)
  6. | S_do_while of block * expr
    (*

    condition

    *)
  7. | S_for of block * expr option * expr option * block
    (*

    body

    *)
  8. | S_jump of jump_kind
    (*

    jump instruction

    *)
  9. | S_target of target_kind
    (*

    target of a jump

    *)
  10. | S_asm of asm_kind
    (*

    asm statement

    *)
Sourceand jump_kind =
  1. | S_goto of string * scope_update
  2. | S_break of scope_update
  3. | S_continue of scope_update
  4. | S_return of expr option * scope_update
  5. | S_switch of expr * block
    (*

    various ways to jump

    *)
Sourceand target_kind =
  1. | S_label of string
  2. | S_case of expr list * scope_update
  3. | S_default of scope_update
    (*

    various targets of jumps

    *)
Sourceand scope_update = {
  1. mutable scope_var_added : variable list;
  2. mutable scope_var_removed : variable list;
}

variables to remove and to add (uninitialized) when jumping into another scope; may be attached to a jump source (break, continue, return, goto) or a jump target (switch case and default), depending on what's more convinient

Sourceand asm_kind = {
  1. asm_style : asm_style;
  2. asm_is_simple : bool;
  3. asm_is_volatile : bool;
  4. asm_body : string;
  5. asm_outputs : asm_output array;
  6. asm_inputs : asm_input array;
  7. asm_clobbers : string array;
  8. asm_labels : string array;
}

and asm statement

Sourceand asm_output = {
  1. asm_output_string : string;
  2. asm_output_expr : expr;
  3. asm_output_constraint : asm_output_constraint;
}
Sourceand asm_input = {
  1. asm_input_string : string;
  2. asm_input_expr : expr;
}
Sourceand asm_output_constraint = Clang_AST.asm_output_constraint
Sourceand expr_kind =
  1. | E_conditional of expr * expr * expr
    (*

    else

    *)
  2. | E_binary_conditional of expr * expr
    (*

    else

    *)
  3. | E_array_subscript of expr * expr
    (*

    index

    *)
  4. | E_member_access of expr * int * string
    (*

    field

    *)
  5. | E_arrow_access of expr * int * string
    (*

    field

    *)
  6. | E_compound_assign of expr * type_qual * binary_arithmetic * expr * type_qual
    (*

    type of the result, before converting back to lvalue type

    *)
  7. | E_binary of binary_operator * expr * expr
    (*

    right argument

    *)
  8. | E_assign of expr * expr
    (*

    rvalue

    *)
  9. | E_comma of expr * expr
    (*

    , operator

    *)
  10. | E_unary of unary_operator * expr
  11. | E_increment of inc_direction * inc_location * expr
  12. | E_address_of of expr
    (*

    & operator (address of lvalue)

    *)
  13. | E_deref of expr
    (*

    * operator (pointer dereference)

    *)
  14. | E_cast of expr * explicitness
  15. | E_call of expr * expr array
    (*

    actual arguments

    *)
  16. | E_character_literal of Z.t * character_kind
    (*

    literal character

    *)
  17. | E_integer_literal of Z.t
    (*

    literal integer

    *)
  18. | E_float_literal of string
    (*

    literal float, in binary string notation

    *)
  19. | E_string_literal of string * character_kind
  20. | E_compound_literal of init
  21. | E_variable of variable
  22. | E_function of func
  23. | E_predefined of string
    (*

    predefined identifier

    *)
  24. | E_statement of block
    (*

    a block of statements viewed as an expression (GCC extension)

    *)
  25. | E_var_args of expr
    (*

    __builtin_va_arg

    *)
  26. | E_atomic of int * expr * expr
  27. | E_convert_vector of expr
  28. | E_vector_element of expr * string
    (*

    accessor

    *)
  29. | E_shuffle_vector of expr array
Sourceand init =
  1. | I_init_expr of expr
  2. | I_init_list of init list * init option
    (*

    filler

    *)
  3. | I_init_implicit of type_qual
Sourceand translation_unit = {
  1. tu_uid : int;
  2. tu_name : string;
  3. tu_range : range;
}
Sourceand project = {
  1. proj_name : string;
    (*

    project name

    *)
  2. proj_tu : translation_unit list;
    (*

    translation units composing the project

    *)
  3. proj_target : target_info;
  4. proj_typedefs : typedef StringMap.t;
    (*

    typedefs, by unique name

    *)
  5. proj_enums : enum_type StringMap.t;
    (*

    enums, by unique name

    *)
  6. proj_records : record_type StringMap.t;
    (*

    records, by unique name

    *)
  7. proj_vars : variable StringMap.t;
    (*

    variables with global lifetime, by unique name

    *)
  8. proj_funcs : func StringMap.t;
    (*

    functions, by unique name

    *)
  9. proj_file_scope_asm : string RangeMap.t;
    (*

    file-scope assembly directives

    *)
  10. proj_files : string list;
    (*

    list of parsed files

    *)
  11. proj_comments : (comment * macro StringMap.t) list RangeMap.t;
    (*

    all comments

    *)
  12. proj_macros : macro StringMap.t;
    (*

    macros, by name

    *)
}

A project is a set of translation units linked together.

Useful definitions

Sourceval no_qual : qualifier

No qualifier.

Sourceval int_type : typ * qualifier
Sourceval bool_type : typ * qualifier
Sourceval void_ptr_type : typ * qualifier
Sourceval uchar_ptr_type : typ * qualifier
Sourceval merge_qualifiers : qualifier -> qualifier -> qualifier
Sourceval resolve_typedef : type_qual -> type_qual

Replace toplevel occurences of typedefs with their definition.

Sourceval as_int_type : type_qual -> integer_type

Interprets the type as an integer type, if possible

Sourceval as_float_type : type_qual -> float_type

Interprets the type as an integer type, if possible

Sourceval type_is_scalar : typ -> bool

Whether a type yields a scalar value.

Variable utilities

Sourceval variable_is_global : variable_kind -> bool

Whether variables of this kind have global lifetime or not.

Sourceval variable_is_static : variable_kind -> bool

Whether variables of this kind are static or not.

Sourceval variable_is_file_static : variable_kind -> bool

Whether variables of this kind are file-level static.

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