Module IR.Exp

The Smallfoot Intermediate Language: Expressions

NOTE: For doing substitutionson expressions, there are some functions in Sil.

module F = Stdlib.Format
type closure = {
  1. name : Procname.t;
  2. captured_vars : (t * Pvar.t * Typ.t * CapturedVar.capture_mode) list;
}
and sizeof_data = {
  1. typ : Typ.t;
  2. nbytes : int option;
  3. dynamic_length : t option;
  4. subtype : Subtype.t;
  5. nullable : bool;
}

This records information about a sizeof(typ) expression.

nbytes represents the result of the evaluation of sizeof(typ) if it is statically known.

If typ is of the form Tarray elt (Some static_length), then dynamic_length is the number of elements of type elt in the array. The dynamic_length, tracked by symbolic execution, may differ from the static_length obtained from the type definition, e.g. when an array is over-allocated.

If typ is a struct type, the dynamic_length is that of the final extensible array, if any.

and t =
  1. | Var of Ident.t
    (*

    Pure variable: it is not an lvalue

    *)
  2. | UnOp of Unop.t * t * Typ.t option
    (*

    Unary operator with type of the result if known

    *)
  3. | BinOp of Binop.t * t * t
    (*

    Binary operator

    *)
  4. | Exn of t
    (*

    Exception

    *)
  5. | Closure of closure
    (*

    Anonymous function

    *)
  6. | Const of Const.t
    (*

    Constants

    *)
  7. | Cast of Typ.t * t
    (*

    Type cast

    *)
  8. | Lvar of Pvar.t
    (*

    The address of a program variable

    *)
  9. | Lfield of t * Fieldname.t * Typ.t
    (*

    A field offset, the type is the surrounding struct type

    *)
  10. | Lindex of t * t
    (*

    An array index offset: exp1[exp2]

    *)
  11. | Sizeof of sizeof_data

Program expressions.

val compare_closure : closure -> closure -> int
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val compare : t -> t -> int
val hash_fold_closure : Ppx_hash_lib.Std.Hash.state -> closure -> Ppx_hash_lib.Std.Hash.state
val hash_closure : closure -> Ppx_hash_lib.Std.Hash.hash_value
val hash_fold_sizeof_data : Ppx_hash_lib.Std.Hash.state -> sizeof_data -> Ppx_hash_lib.Std.Hash.state
val hash_sizeof_data : sizeof_data -> Ppx_hash_lib.Std.Hash.hash_value
val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
val hash : t -> Ppx_hash_lib.Std.Hash.hash_value
val hash_normalize_closure : closure -> closure
val hash_normalize_closure_opt : closure option -> closure option
val hash_normalize_closure_list : closure list -> closure list
val hash_normalize_sizeof_data : sizeof_data -> sizeof_data
val hash_normalize_sizeof_data_opt : sizeof_data option -> sizeof_data option
val hash_normalize_sizeof_data_list : sizeof_data list -> sizeof_data list
val hash_normalize : t -> t
val hash_normalize_opt : t option -> t option
val hash_normalize_list : t list -> t list
val equal : t -> t -> bool

Equality for expressions.

module Set : IStdlib.IStd.Caml.Set.S with type elt = t

Set of expressions.

module Map : IStdlib.IStd.Caml.Map.S with type key = t

Map with expression keys.

module Hash : IStdlib.IStd.Caml.Hashtbl.S with type key = t

Hashtable with expression keys.

val is_null_literal : t -> bool
val is_this : t -> bool

return true if exp is the special this/self expression

val is_zero : t -> bool
val is_const : t -> bool

Utility Functions for Expressions

val texp_to_typ : Typ.t option -> t -> Typ.t

Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception

val root_of_lexp : t -> t

Return the root of lexp.

val get_undefined : bool -> t

Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint

val pointer_arith : t -> bool

Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai only.

val has_local_addr : t -> bool

returns true if the expression operates on address of local variable

val zero : t

Integer constant 0

val null : t

Null constant

val one : t

Integer constant 1

val minus_one : t

Integer constant -1

val int : IntLit.t -> t

Create integer constant

val float : float -> t

Create float constant

val bool : bool -> t

Create integer constant corresponding to the boolean value

val eq : t -> t -> t

Create expression e1 == e2

val ne : t -> t -> t

Create expression e1 != e2

val le : t -> t -> t

Create expression e1 <= e2

val lt : t -> t -> t

Create expression e1 < e2

val free_vars : t -> Ident.t IStdlib.IStd.Sequence.t

all the idents appearing in the expression

val gen_free_vars : t -> (unit, Ident.t) IStdlib.IStd.Sequence.Generator.t
val ident_mem : t -> Ident.t -> bool

true if the identifier appears in the expression

val program_vars : t -> Pvar.t IStdlib.IStd.Sequence.t

all the program variables appearing in the expression

val closures : t -> closure IStdlib.IStd.Sequence.t

all closures appearing in the expression

val fold_captured : f:('a -> t -> 'a) -> t -> 'a -> 'a

Fold over the expressions captured by this expression.

val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F.formatter -> t -> unit
val pp : F.formatter -> t -> unit
val pp_closure : F.formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit

dump an expression.

val pp_texp : IStdlib.Pp.env -> F.formatter -> t -> unit

Pretty print a type.

val pp_texp_full : IStdlib.Pp.env -> F.formatter -> t -> unit

Pretty print a type with all the details.

val d_texp_full : t -> unit

Dump a type expression with all the details.

val d_list : t list -> unit

Dump a list of expressions.

val is_cpp_closure : t -> bool
val zero_of_type : Typ.t -> t option

Returns the zero value of a type, for int, float and ptr types

val zero_of_type_exn : Typ.t -> t
val ignore_cast : t -> t
val ignore_integer_cast : t -> t
val get_java_class_initializer : Tenv.t -> t -> (Procname.t * Pvar.t * Fieldname.t * Typ.t) option

Returns the class initializer of the given expression in Java