Module IR.Sil

The Smallfoot Intermediate Language

module F = Stdlib.Format

Programs and Types

type if_kind =
  1. | Ik_bexp
    (*

    boolean expressions, and exp ? exp : exp

    *)
  2. | Ik_compexch
    (*

    used in atomic compare exchange expressions

    *)
  3. | Ik_dowhile
  4. | Ik_for
  5. | Ik_if
  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
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. | ExitScope of Var.t list * IBase.Location.t
    (*

    remove temporaries and dead program variables

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

    nullify stack variable

    *)
  5. | Skip
    (*

    no-op

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

    entry of C++ try block

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

    exit of C++ try block

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