package mopsa

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

Statements

This module is responsible for extending the Mopsa AST with new statements. This is done by creating new variant constructor of the extensible type stmt_kind, for instance

type stmt_kind += S_assign of expr * expr

creates a new assignment statement, which needs to be registered

let () = register_stmt {
    compare = (fun next s1 s2 ->
        match skind s1, skind s2 with
        | S_assign(x1,e1), S_assign(x2,e2) ->
          Compare.pair compare_expr compare_expr (x1,e1) (x2,e2)
        | _ -> next s1 s2
      );
    print = (fun next s ->
        match skind s with
        | S_assign(x,e) -> Format.fprintf fmt "%a = %a;" pp_expr x pp_expr e
        | _    -> next fmt s
      );
  }
type stmt_kind = ..

Extensible kinds of statements

type stmt = {
  1. skind : stmt_kind;
    (*

    kind of the statement

    *)
  2. srange : Mopsa_utils.Location.range;
    (*

    location range of the statement

    *)
}

Statements

Create a statement

val skind : stmt -> stmt_kind

Get the kind of a statement

Get the location range of a statement

val compare_stmt : stmt -> stmt -> int

Total order between statements

val pp_stmt : Format.formatter -> stmt -> unit

Pretty-printer of statements

Registration

val register_stmt : stmt Mopsa_utils.TypeExt.info -> unit

register_stmt info registers a new statement by registering its compare function info.compare and pretty-printer info.print

val register_stmt_compare : stmt Mopsa_utils.TypeExt.compare -> unit

Register a comparison function for statements

val register_stmt_pp : stmt Mopsa_utils.TypeExt.print -> unit

Register a pretty-printer function for statements

Blocks

type block = stmt list

Blocks are sequences of statements

val pp_block : Format.formatter -> block -> unit

Pretty-printer for blocks

Common statements

type stmt_kind +=
  1. | S_program of Program.program * string list option
    (*

    Command-line arguments as given to Mopsa after --

    *)

Programs

type stmt_kind +=
  1. | S_assign of Expr.expr * Expr.expr
    (*

    rhs

    *)

Assignments

mk_assign lhs rhs range creates the assignment lhs = rhs;

type stmt_kind +=
  1. | S_assume of Expr.expr
    (*

    condition

    *)

Tests

Create a test statement

type stmt_kind +=
  1. | S_add of Expr.expr
    (*

    Add a dimension to the environment

    *)
  2. | S_remove of Expr.expr
    (*

    Remove a dimension from the environment and invalidate all references to it

    *)
  3. | S_invalidate of Expr.expr
    (*

    Invalidate all references to a dimension without removing it

    *)
  4. | S_rename of Expr.expr * Expr.expr
    (*

    new

    *)
  5. | S_forget of Expr.expr
    (*

    Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed

    *)
  6. | S_project of Expr.expr list
    (*

    Project the environment on the given list of dimensions. All other dimensions are removed

    *)
  7. | S_expand of Expr.expr * Expr.expr list
    (*

    Expand a dimension into a list of other dimensions. The expanded dimension is untouched

    *)
  8. | S_fold of Expr.expr * Expr.expr list
    (*

    Fold a list of dimensions into a single one. The folded dimensions are removed

    *)
  9. | S_block of stmt list * Var.var list
    (*

    local variables declared within the block

    *)
  10. | S_breakpoint of string
    (*

    Trigger a breakpoint

    *)

Dimensions

Utility functions to create various statements for dimension management

val mk_rename_var : Var.var -> Var.var -> Mopsa_utils.Location.range -> stmt
val mk_remove_var : Var.var -> Mopsa_utils.Location.range -> stmt
val mk_invalidate : Expr.expr -> Mopsa_utils.Location.range -> stmt
val mk_invalidate_var : Var.var -> Mopsa_utils.Location.range -> stmt
val mk_add_var : Var.var -> Mopsa_utils.Location.range -> stmt
val mk_project : Expr.expr list -> Mopsa_utils.Location.range -> stmt
val mk_project_vars : Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_forget_var : Var.var -> Mopsa_utils.Location.range -> stmt
val mk_expand : Expr.expr -> Expr.expr list -> Mopsa_utils.Location.range -> stmt
val mk_expand_var : Var.var -> Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_fold_var : Var.var -> Var.var list -> Mopsa_utils.Location.range -> stmt
val mk_breakpoint : string -> Mopsa_utils.Location.range -> stmt

Containers of statements

Sets of statements

Maps of statements

OCaml

Innovation. Community. Security.