Module Ast.ExprSource

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.

Sourcetype expr_kind = ..

Extensible type of expression kinds

Sourcetype 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

Sourceval compare_expr : expr -> expr -> int

compare_expr e1 e2 implements a total order between expressions

Sourceval pp_expr : Stdlib.Format.formatter -> expr -> unit

pp_expr fmt e pretty-prints expression e with format fmt

Sourceval ekind : expr -> expr_kind

Get the kind of an expression

Sourceval etyp : expr -> Typ.typ

Get the type of an expression

Get the location of an expression

Get the translation map of an expression

Sourceval ehistory : expr -> expr list

Get the evaluation history of an expression

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

Construct an expression

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

Add a translation of an expression

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

Get all translations of an expression

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

Get the translation of an expression into a given semantic

Sourceval get_expr_history : expr -> expr list

Get the evaluation history of an expression

Sourceval get_orig_expr : expr -> expr

Get the original form of an expression

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

Get the ancestor expression verifying a predicate

Registration

Sourceval 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

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

register_expr_compare compare registers a new expression comparison

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

register_expr_compare compare registers a new expression printer

Some common expressions

Variable expressions

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

    optional access mode overloading the variable's access mode

    *)

Variables

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

Create a variable expression

Sourceval weaken_var_expr : expr -> expr

Change the access mode of a variable expression to WEAK

Sourceval strongify_var_expr : expr -> expr

Change the access mode of a variable expression to STRONG

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

Get the overloaded access mode of a variable

Heap addresses expressions

Sourcetype 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

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

Create an address expression

Create an allocation expression

Sourceval weaken_addr_expr : expr -> expr

Change the access mode of an address expression to WEAK

Sourceval strongify_addr_expr : expr -> expr

Change the access mode of an address expression to STRONG

Constant expressions

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

Constants

Create a constant expression

Create ⊤ expression of a given type

Unary expressions

Sourcetype 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

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

    second operand

    *)

Binary operator expressions

Create a binary operator expression

Sourceval negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

Sets of expression

Maps of expressions