package mopsa

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

Variables

The type var represents variables in Mopsa. In addition to a unique string name and a type, a variable is decorated with an extensible type var_kind that allows annotating the variable with extra information that is specific to its language.

New kinds of variables can be added by extending var_kind with a new variant. For example, for some toy language Toy in which variables, in addition to a name and a type, have an initial value, a new variable kind can be created with

type var_kind += V_toy of expr

This new variable kind needs to be registered

let () = register_var {
    compare = (fun next v1 v2 ->
        match vkind v1, vkind v2 with
        | V_toy init1, V_toy init2 -> compare_expr init1 init2
        | _ -> next v1 v2
      );
    print = (fun fmt next v ->
        match vkind v with
        | V_toy v -> Format.pp_print_string fmt v.vname
        | _ -> next fmt v
      );
  }

Another property of variables is their access mode. When a variable represents a single dimension in the concrete, assignments on this variable are performed with strong updates, i.e. the update destroys the previous value.

On the other hand, when an abstract domain summarizes the value of several concrete dimensions into a single variable, only weak updates can be performed to preserve the value of unmodified concrete dimensions.

val print_uniq_with_uid : bool Stdlib.ref

Access modes

type var_kind = ..

Extensible kind of variables

type mode =
  1. | WEAK
    (*

    Weak updates are used when the variable summarizes several concrete dimensions

    *)
  2. | STRONG
    (*

    Strong updates are used when the variable represents a single concrete dimension

    *)

Access mode of a variable

val pp_mode : Stdlib.Format.formatter -> mode -> unit

Pretty-print an access mode

val compare_mode : mode -> mode -> int

Compare two access modes

Variables

type var = {
  1. vname : string;
    (*

    unique name of the variable

    *)
  2. vkind : var_kind;
    (*

    kind the variable

    *)
  3. vtyp : Typ.typ;
    (*

    type of the variable

    *)
  4. vmode : mode;
    (*

    access mode of the variable

    *)
  5. vsemantic : Semantic.semantic;
    (*

    semantic of the variable

    *)
}

Variables

val vname : var -> string

Accessor function to the fields of a variable

val vkind : var -> var_kind
val vtyp : var -> Typ.typ
val vmode : var -> mode
val vsemantic : var -> Semantic.semantic
val mkv : string -> var_kind -> ?mode:mode -> ?semantic:Semantic.semantic -> Typ.typ -> var

Create a variable with a unique name, a kind, a type and an access mode (STRONG if not given)

val pp_var : Stdlib.Format.formatter -> var -> unit

Pretty-print a variable

val compare_var : var -> var -> int

Total order between variables

Registration

val register_var : var Mopsa_utils.TypeExt.info -> unit

Register a new kind of variables

val register_var_compare : var Mopsa_utils.TypeExt.compare -> unit

Register a new variable comparison

val register_var_pp : var Mopsa_utils.TypeExt.print -> unit

Register a new variable pretty-printer

Common variables

type var_kind +=
  1. | V_uniq of string * int
    (*

    Unique ID

    *)
  2. | V_tmp of int
    (*

    Unique ID

    *)
  3. | V_var_attr of var * string
    (*

    Attribute

    *)
  4. | V_range_attr of Mopsa_utils.Location.range * string
    (*

    Attribute

    *)
val mk_uniq_var : string -> int -> ?mode:mode -> Typ.typ -> var

Create a unique variable

val mk_fresh_uniq_var : string -> ?mode:mode -> Typ.typ -> unit -> var

Create a fresh variable with a fresh ID

val mktmp : ?typ:Typ.typ -> ?mode:mode -> unit -> var

Create a fresh temporary variable

val mk_attr_var : var -> string -> ?mode:mode -> ?semantic:Semantic.semantic -> Typ.typ -> var

mk_attr_var v a t creates a variable representing an attribute a of another variable v

val mk_range_attr_var : Mopsa_utils.Location.range -> string -> ?mode:mode -> ?semantic:Semantic.semantic -> Typ.typ -> var

mk_range_attr_var r a t creates a variable representing an attribute a of a program location r

Containers for variables

module VarSet : Mopsa_utils.SetExtSig.S with type elt = var

Sets of variables

module VarMap : Mopsa_utils.MapExtSig.S with type key = var

Maps of variables

Deprecated

val start_vcounter_at : int -> unit
val get_vcounter_val : unit -> int
val get_orig_vname : var -> string
val set_orig_vname : string -> var -> var
OCaml

Innovation. Community. Security.