package mopsa

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

Expressions

This module allows adding new expressions to the extensible Mopsa AST.

New expressions are added by extending the type expr_kind. For example, to add an expression for subscript access to arrays

type expr_kind += E_array_subscript of expr * expr

New expressions need to be registered using register_expr as follows:

let () = register_expr {
    compare = (fun next e1 e2 ->
        match ekind e1, ekind e2 with
        | E_array_subscript(a1,i1), E_array_subscript(a2,i2) ->
          Compare.pair compare_expr compare_expr (a1,i1) (a2,i2)
        | _ -> next e1 e2
      );
    print = (fun next fmt e ->
        match ekind e with
        | E_array_subscript(a,i) -> 
          Format.fprintf fmt "%a[%a]"
            pp_expr a
            pp_expr i
        | _ -> next fmt e
      );
  }

Registered expressions can be compare using function compare_expr and printed using the function pp_expr.

type expr_kind = ..

Extensible type of expression kinds

type expr = {
  1. ekind : expr_kind;
    (*

    kind of the expression

    *)
  2. etyp : Typ.typ;
    (*

    type of the expression

    *)
  3. erange : Mopsa_utils.Location.range;
    (*

    location range of the expression

    *)
  4. etrans : expr Semantic.SemanticMap.t;
    (*

    translations of the expression into other semantics

    *)
  5. ehistory : expr list;
    (*

    History of preceding evaluations of the expression

    *)
}

Expressions

val compare_expr : expr -> expr -> int

compare_expr e1 e2 implements a total order between expressions

val pp_expr : Format.formatter -> expr -> unit

pp_expr fmt e pretty-prints expression e with format fmt

val ekind : expr -> expr_kind

Get the kind of an expression

val etyp : expr -> Typ.typ

Get the type of an expression

Get the location of an expression

Get the translation map of an expression

val ehistory : expr -> expr list

Get the evaluation history of an expression

val mk_expr : ?etyp:Typ.typ -> ?etrans:expr Semantic.SemanticMap.t -> ?ehistory:expr list -> expr_kind -> Mopsa_utils.Location.range -> expr

Construct an expression

val add_expr_translation : Semantic.semantic -> expr -> expr -> expr

Add a translation of an expression

val get_expr_translations : expr -> expr Semantic.SemanticMap.t

Get all translations of an expression

val get_expr_translation : Semantic.semantic -> expr -> expr

Get the translation of an expression into a given semantic

val get_expr_history : expr -> expr list

Get the evaluation history of an expression

val get_orig_expr : expr -> expr

Get the original form of an expression

val find_expr_ancestor : (expr -> bool) -> expr -> expr

Get the ancestor expression verifying a predicate

Registration

val register_expr : expr Mopsa_utils.TypeExt.info -> unit

register_expr info registers new expressions with their comparison function info.compare and pretty-printer info.print

val register_expr_compare : expr Mopsa_utils.TypeExt.compare -> unit

register_expr_compare compare registers a new expression comparison

val register_expr_pp : expr Mopsa_utils.TypeExt.print -> unit

register_expr_compare compare registers a new expression printer

Some common expressions

Variable expressions

type expr_kind +=
  1. | E_var of Var.var * Var.mode option
    (*

    optional access mode overloading the variable's access mode

    *)

Variables

val mk_var : Var.var -> ?mode:Var.mode option -> Mopsa_utils.Location.range -> expr

Create a variable expression

val weaken_var_expr : expr -> expr

Change the access mode of a variable expression to WEAK

val strongify_var_expr : expr -> expr

Change the access mode of a variable expression to STRONG

val var_mode : Var.var -> Var.mode option -> Var.mode

Get the overloaded access mode of a variable

Heap addresses expressions

type expr_kind +=
  1. | E_addr of Addr.addr * Var.mode option
    (*

    optional access mode overloading the address access mode

    *)
  2. | E_alloc_addr of Addr.addr_kind * Var.mode

Heap addresses

val mk_addr : Addr.addr -> ?etyp:Typ.typ -> ?mode:Var.mode option -> Mopsa_utils.Location.range -> expr

Create an address expression

val mk_alloc_addr : ?mode:Var.mode -> Addr.addr_kind -> Mopsa_utils.Location.range -> expr

Create an allocation expression

val weaken_addr_expr : expr -> expr

Change the access mode of an address expression to WEAK

val strongify_addr_expr : expr -> expr

Change the access mode of an address expression to STRONG

Constant expressions

type expr_kind +=
  1. | E_constant of Constant.constant

Constants

val mk_constant : ?etyp:Typ.typ -> Constant.constant -> Mopsa_utils.Location.range -> expr

Create a constant expression

Create ⊤ expression of a given type

Unary expressions

type expr_kind +=
  1. | E_unop of Operator.operator * expr
    (*

    operand

    *)

Unary operator expressions

Create a unary operator expression

mk_not e range returns the negation of expression e using the operator Operator.O_log_not

Binary expressions

type expr_kind +=
  1. | E_binop of Operator.operator * expr * expr
    (*

    second operand

    *)

Binary operator expressions

Create a binary operator expression

val negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

Sets of expression

Maps of expressions

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