Module IR.Sil

The Smallfoot Intermediate Language

module F = Stdlib.Format

Programs and Types

type if_kind =
  1. | Ik_bexp of {
    1. terminated : bool;
    }
    (*

    boolean expressions, and exp ? exp : exp

    *)
  2. | Ik_compexch
    (*

    used in atomic compare exchange expressions

    *)
  3. | Ik_dowhile
  4. | Ik_for
  5. | Ik_if of {
    1. terminated : bool;
    }
  6. | Ik_land_lor
    (*

    obtained from translation of && or ||

    *)
  7. | Ik_while
  8. | Ik_switch

Kind of prune instruction

val compare_if_kind : if_kind -> if_kind -> int
val equal_if_kind : if_kind -> if_kind -> bool
val pp_if_kind : F.formatter -> if_kind -> unit
val is_terminated_if_kind : if_kind -> bool

Whether an if_kind has a true terminated field, meaning that the conditional control flow creates a temporary branching in the CFG of the procedure that is closed by a Join node containing an EndBranches instruction. Frontends should try to terminate conditionals (by setting the terminated flag and emitting an EndBranches instruction at the appropriate point) whenever possible so some analyses can detect which instructions are executed under the influence of a conditional more easily.

type instr_metadata =
  1. | Abstract of IBase.Location.t
    (*

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

    *)
  2. | CatchEntry of {
    1. try_id : int;
    2. loc : IBase.Location.t;
    }
    (*

    entry of C++ catch blocks

    *)
  3. | EndBranches
    (*

    the end of a conditional control flow generated by an if statement whose if_kind satisfies is_terminated_if_kind

    *)
  4. | ExitScope of Var.t list * IBase.Location.t
    (*

    remove temporaries and dead program variables

    *)
  5. | Nullify of Pvar.t * IBase.Location.t
    (*

    nullify stack variable

    *)
  6. | Skip
    (*

    no-op

    *)
  7. | TryEntry of {
    1. try_id : int;
    2. loc : IBase.Location.t;
    }
    (*

    entry of C++ try block

    *)
  8. | TryExit of {
    1. try_id : int;
    2. loc : IBase.Location.t;
    }
    (*

    exit of C++ try block

    *)
  9. | VariableLifetimeBegins of {
    1. pvar : Pvar.t;
    2. typ : Typ.t;
    3. loc : IBase.Location.t;
    4. is_cpp_structured_binding : bool;
    }
    (*

    stack variable declared

    *)
val compare_instr_metadata : instr_metadata -> instr_metadata -> int
type instr =
  1. | Load of {
    1. id : Ident.t;
    2. e : Exp.t;
    3. typ : Typ.t;
    4. loc : IBase.Location.t;
    }
    (*

    Load a value from the heap into an identifier.

    id = *e:typ where

    • e is an expression denoting a heap address
    • typ is the type of *e and id.
    *)
  2. | Store of {
    1. e1 : Exp.t;
    2. typ : Typ.t;
    3. e2 : Exp.t;
    4. loc : IBase.Location.t;
    }
    (*

    Store the value of an expression into the heap.

    *e1:typ = e2 where

    • e1 is an expression denoting a heap address
    • typ is the type of *e1 and e2.
    *)
  3. | Prune of Exp.t * IBase.Location.t * bool * if_kind
    (*

    The semantics of Prune (exp, loc, is_then_branch, if_kind) is that it prunes the state (blocks, or diverges) if exp evaluates to 1; the boolean is_then_branch is true if this is the then branch of an if condition, false otherwise (it is meaningless if if_kind is not Ik_if, Ik_bexp, or other if-like cases

    This instruction, together with the CFG structure, is used to encode control-flow with tests in the source program such as if branches and while loops.

    *)
  4. | 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)

    *)
  5. | 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. Syntactic invariants of instructions per-frontend are documented in Checkers.SilValidation, where Clang is the most general validator (that is, it properly subsumes all other validators). These invariants are enforced when --sil-validation is passed.

val compare_instr : instr -> instr -> int
val equal_instr : instr -> instr -> bool
val hash_normalize_instr : instr -> instr
val hash_normalize_instr_opt : instr option -> instr option
val hash_normalize_instr_list : instr list -> instr list
val equal_structural_instr : instr -> instr -> Exp.t IR.Exp.Map.t -> bool * Exp.t IR.Exp.Map.t

Compare instructions from different procedures without considering locs, idents, pvars, or try_ids. The exp_map parameter gives a mapping of names used in the first instr to those used in the second, and the returned exp_map includes any additional mappings inferred from this comparison.

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 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.