Module IR.Sil

module F = Stdlib.Format

Programs and Types

type if_kind =
| Ik_bexp

boolean expressions, and exp ? exp : exp

| Ik_dowhile
| Ik_for
| Ik_if
| Ik_land_lor

obtained from translation of && or ||

| Ik_while
| Ik_switch

Kind of prune instruction

val compare_if_kind : if_kind -> if_kind -> int
val equal_if_kind : if_kind -> if_kind -> bool
type instr_metadata =
| Abstract of IBase.Location.t

a good place to apply abstraction, mostly used in the biabduction analysis

| CatchEntry of {
try_id : int;
loc : IBase.Location.t;
}

entry of C++ catch blocks

| ExitScope of Var.t list * IBase.Location.t

remove temporaries and dead program variables

| Nullify of Pvar.t * IBase.Location.t

nullify stack variable

| Skip

no-op

| TryEntry of {
try_id : int;
loc : IBase.Location.t;
}

entry of C++ try block

| TryExit of {
try_id : int;
loc : IBase.Location.t;
}

exit of C++ try block

| VariableLifetimeBegins of Pvar.t * Typ.t * IBase.Location.t

stack variable declared

val compare_instr_metadata : instr_metadata -> instr_metadata -> int
type instr =
| Load of {
id : Ident.t;
e : Exp.t;
root_typ : Typ.t;
typ : Typ.t;
loc : IBase.Location.t;
}

Load a value from the heap into an identifier.

id = *exp:typ(root_typ) where

  • exp is an expression denoting a heap address
  • typ is typ of exp and id
  • root_typ is the root type of exp

The root_typ is deprecated: it is broken in C/C++. We are removing root_typ in the future, so please use typ instead.

| Store of {
e1 : Exp.t;
root_typ : Typ.t;
typ : Typ.t;
e2 : Exp.t;
loc : IBase.Location.t;
}

Store the value of an expression into the heap.

*exp1:typ(root_typ) = exp2 where

  • exp1 is an expression denoting a heap address
  • typ is typ of *exp1 and exp2
  • root_typ is the root type of exp1
  • exp2 is the expression whose value is stored.

The root_typ is deprecated: it is broken in C/C++. We are removing root_typ in the future, so please use typ instead.

| Prune of Exp.t * IBase.Location.t * bool * if_kind

prune the state based on exp=1, the boolean indicates whether true branch

| Call of Ident.t * Typ.t * Exp.t * (Exp.t * Typ.t) list * IBase.Location.t * CallFlags.t

Call ((ret_id, ret_typ), e_fun, arg_ts, loc, call_flags) represents an instruction ret_id = e_fun(arg_ts);

| Metadata of instr_metadata

hints about the program that are not strictly needed to understand its semantics, for instance information about its original syntactic structure

An instruction.

val compare_instr : instr -> instr -> int
val equal_instr : instr -> instr -> bool
val skip_instr : instr
val instr_is_auxiliary : instr -> bool

Check if an instruction is auxiliary, or if it comes from source instructions.

val location_of_instr : instr -> IBase.Location.t

Get the location of the instruction

val exps_of_instr : instr -> Exp.t list

get the expressions occurring in the instruction

val if_kind_to_string : if_kind -> string

Pretty print an if_kind

val pp_instr_metadata : IStdlib.Pp.env -> F.formatter -> instr_metadata -> unit
val pp_instr : print_types:bool -> IStdlib.Pp.env -> F.formatter -> instr -> unit

Pretty print an instruction.

val d_instr : instr -> unit

Dump an instruction.