Module `Ast.Expr`Source

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

ekind : expr_kind;
(*
kind of the expression
*)
etyp : Typ.typ;
(*
type of the expression
*)
erange : Mopsa_utils.Location.range;
(*
location range of the expression
*)
etrans : expr Semantic.SemanticMap.t;
(*
translations of the expression into other semantics
*)
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

Sourceval erange : expr -> Mopsa_utils.Location.range

Get the location of an expression

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

Get the translation map of an expression

Sourceval ehistory : expr -> expr list

Get the evaluation history of an expression

Source

val 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 +=

| E_var of Var.var * Var.mode option
(*
optional access mode overloading the variable's access mode
*)

Variables

Source

val 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 +=

| E_addr of Addr.addr * Var.mode option
(*
optional access mode overloading the address access mode
*)
| E_alloc_addr of Addr.addr_kind * Var.mode

Heap addresses

Source

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

Create an address expression

Source

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

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

| E_constant of Constant.constant

Constants

Source

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

Create a constant expression

Sourceval mk_top : Typ.typ -> Mopsa_utils.Location.range -> expr

Create ⊤ expression of a given type

Unary expressions

Sourcetype expr_kind +=

| E_unop of Operator.operator * expr
(*
operand
*)

Unary operator expressions

Source

val mk_unop : 
  ?etyp:Typ.typ ->
  Operator.operator ->
  expr ->
  Mopsa_utils.Location.range ->
  expr

Create a unary operator expression

Sourceval mk_not : expr -> Mopsa_utils.Location.range -> expr

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

Binary expressions

Sourcetype expr_kind +=

| E_binop of Operator.operator * expr * expr
(*
second operand
*)

Binary operator expressions

Source

val mk_binop : 
  ?etyp:Typ.typ ->
  expr ->
  Operator.operator ->
  expr ->
  Mopsa_utils.Location.range ->
  expr

Create a binary operator expression

Sourceval negate_expr : expr -> expr

Return the negation of an expression

Expressions containers

module ExprSet : Mopsa_utils.SetExtSig.S with type elt = expr

Sets of expression

module ExprMap : Mopsa_utils.MapExtSig.S with type key = expr

Maps of expressions

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ast/Ast/Expr/index.html

Module `Ast.Expr`Source

Registration

Some common expressions

Variable expressions

Heap addresses expressions

Constant expressions

Unary expressions

Binary expressions

Expressions containers

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ast/Ast/Expr/index.html

Module Ast.ExprSource

Registration

Some common expressions

Variable expressions

Heap addresses expressions

Constant expressions

Unary expressions

Binary expressions

Expressions containers

Module `Ast.Expr`Source