[SIL][HIL] distinguish auxiliary instructions as `Metadata`

Summary:
Bundle all non-semantic-bearing instructions into a `Metadata _`
instruction in SIL.

- On a documentation level this makes clearer the distinction between
instructions that encode the semantics of the program and those that are
just hints for the various backend analysis.

- This makes it easier to add more of these auxiliary instructions in
the future. For example, the next diff introduces a new `Skip` auxiliary
instruction to replace the hacky `ExitScope([], Location.dummy)`.

- It also makes it easier to surface all current and future such
auxiliary instructions to HIL as the datatype for these syntactic hints
can be shared between SIL and HIL. This diff brings `Nullify` and
`Abstract` to HIL for free.

Reviewed By: ngorogiannis

Differential Revision: D14827674

fbshipit-source-id: f68fe2110

infer/src/IR/HilInstr.ml

@@ -22,7 +22,7 @@ type t =
   | Assign of HilExp.AccessExpression.t * HilExp.t * Location.t
   | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
   | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t
-  | ExitScope of Var.t list * Location.t
+  | Metadata of Sil.instr_metadata
 [@@deriving compare]
 
 let pp fmt = function
@@ -35,11 +35,11 @@ let pp fmt = function
       let pp_ret fmt = F.fprintf fmt "%a := " AccessPath.pp_base in
       let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in
       F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret pp_call call pp_actuals actuals Location.pp loc
-  | ExitScope (vars, loc) ->
+  | Metadata instr_metadata ->
-      F.fprintf fmt "exit scope(%a) [%a]" (Pp.seq ~sep:"; " Var.pp) vars Location.pp loc
+      Sil.pp_instr_metadata Pp.text fmt instr_metadata
 
 
-type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t | Ignore
+type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t
 
 (** convert an SIL instruction into an HIL instruction. The [f_resolve_id] function should map an
    SSA temporary variable to the access path it represents. Evaluating the HIL instruction should
@@ -121,8 +121,5 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) =
       let hil_exp = exp_of_sil exp (Typ.mk (Tint IBool)) in
       let branch = if true_branch then `Then else `Else in
       Instr (Assume (hil_exp, branch, if_kind, loc))
-  | ExitScope (vars, loc) ->
+  | Metadata metadata ->
-      Instr (ExitScope (vars, loc))
+      Instr (Metadata metadata)
-  | Abstract _ | Nullify _ ->
-      (* these don't seem useful for most analyses. can translate them later if we want to *)
-      Ignore

infer/src/IR/HilInstr.mli

@@ -20,7 +20,7 @@ type t =
       (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *)
   | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t
       (** Var to hold the return, call expression, formals *)
-  | ExitScope of Var.t list * Location.t
+  | Metadata of Sil.instr_metadata  (** see {!Sil.instr_metadata} *)
 [@@deriving compare]
 
 val pp : F.formatter -> t -> unit
@@ -29,7 +29,6 @@ val pp : F.formatter -> t -> unit
 type translation =
   | Instr of t  (** HIL instruction to execute *)
   | Bind of Var.t * HilExp.AccessExpression.t  (** add binding to identifier map *)
-  | Ignore  (** no-op *)
 
 val of_sil :
      include_array_indexes:bool

infer/src/IR/Procdesc.ml

@@ -187,7 +187,7 @@ module Node = struct
 
   (** Get the source location of the last instruction in the node *)
   let get_last_loc n =
-    n |> get_instrs |> Instrs.last |> Option.value_map ~f:Sil.instr_get_loc ~default:n.loc
+    n |> get_instrs |> Instrs.last |> Option.value_map ~f:Sil.location_of_instr ~default:n.loc
 
 
   let find_in_node_or_preds =
@@ -360,26 +360,17 @@ module Node = struct
   (** simple key for a node: just look at the instructions *)
   let simple_key node =
     let add_instr instr =
-      if Sil.instr_is_auxiliary instr then None
-      else
-        let instr_key =
       match instr with
       | Sil.Load _ ->
-              1
+          Some 1
       | Sil.Store _ ->
-              2
+          Some 2
       | Sil.Prune _ ->
-              3
+          Some 3
       | Sil.Call _ ->
-              4
+          Some 4
-          | Sil.Nullify _ ->
+      | Sil.Metadata _ ->
-              5
+          None
-          | Sil.Abstract _ ->
-              6
-          | Sil.ExitScope _ ->
-              7
-        in
-        Some instr_key
     in
     get_instrs node
     |> IContainer.rev_filter_map_to_list ~fold:Instrs.fold ~f:add_instr

infer/src/IR/Sil.ml

@@ -26,6 +26,13 @@ type if_kind =
   | Ik_switch
 [@@deriving compare]
 
+type instr_metadata =
+  | Abstract of Location.t
+      (** a good place to apply abstraction, mostly used in the biabduction analysis *)
+  | ExitScope of Var.t list * Location.t  (** remove temporaries and dead program variables *)
+  | Nullify of Pvar.t * Location.t  (** nullify stack variable *)
+[@@deriving compare]
+
 (** An instruction. *)
 type instr =
   (* Note for frontend writers:
@@ -33,34 +40,41 @@ type instr =
      `Load` instruction may be eliminated by copy-propagation. *)
   | Load of Ident.t * Exp.t * Typ.t * Location.t
       (** Load a value from the heap into an identifier.
+
           [x = *lexp:typ] where
-            [lexp] is an expression denoting a heap address
+
-            [typ] is the root type of [lexp]. *)
+          - [lexp] is an expression denoting a heap address
+
+          - [typ] is the root type of [lexp]. *)
   | Store of Exp.t * Typ.t * Exp.t * Location.t
       (** Store the value of an expression into the heap.
+
           [*lexp1:typ = exp2] where
-            [lexp1] is an expression denoting a heap address
+
-            [typ] is the root type of [lexp1]
+          - [lexp1] is an expression denoting a heap address
-            [exp2] is the expression whose value is store. *)
+
+          - [typ] is the root type of [lexp1]
+
+          - [exp2] is the expression whose value is store. *)
   | Prune of Exp.t * 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 * 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);] *)
-  | Nullify of Pvar.t * Location.t  (** nullify stack variable *)
+  | Metadata of instr_metadata
-  | Abstract of Location.t  (** apply abstraction *)
+      (** hints about the program that are not strictly needed to understand its semantics, for
-  | ExitScope of Var.t list * Location.t  (** remove temporaries and dead program variables *)
+          instance information about its original syntactic structure *)
 [@@deriving compare]
 
 let equal_instr = [%compare.equal: instr]
 
-let skip_instr = ExitScope ([], Location.dummy)
+let skip_instr = Metadata (ExitScope ([], Location.dummy))
 
 (** Check if an instruction is auxiliary, or if it comes from source instructions. *)
 let instr_is_auxiliary = function
   | Load _ | Store _ | Prune _ | Call _ ->
       false
-  | Nullify _ | Abstract _ | ExitScope _ ->
+  | Metadata _ ->
       true
 
 
@@ -325,20 +339,30 @@ let d_offset_list (offl : offset list) = L.d_pp_with_pe pp_offset_list offl
 
 let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t
 
+let location_of_instr_metadata = function
+  | Abstract loc | ExitScope (_, loc) | Nullify (_, loc) ->
+      loc
+
+
 (** Get the location of the instruction *)
-let instr_get_loc = function
+let location_of_instr = function
-  | Load (_, _, _, loc)
+  | Load (_, _, _, loc) | Store (_, _, _, loc) | Prune (_, loc, _, _) | Call (_, _, _, loc, _) ->
-  | Store (_, _, _, loc)
-  | Prune (_, loc, _, _)
-  | Call (_, _, _, loc, _)
-  | Nullify (_, loc)
-  | Abstract loc
-  | ExitScope (_, loc) ->
       loc
+  | Metadata metadata ->
+      location_of_instr_metadata metadata
+
+
+let exps_of_instr_metadata = function
+  | Abstract _ ->
+      []
+  | ExitScope (vars, _) ->
+      List.map ~f:Var.to_exp vars
+  | Nullify (pvar, _) ->
+      [Exp.Lvar pvar]
 
 
 (** get the expressions occurring in the instruction *)
-let instr_get_exps = function
+let exps_of_instr = function
   | Load (id, e, _, _) ->
       [Exp.Var id; e]
   | Store (e1, _, e2, _) ->
@@ -347,12 +371,8 @@ let instr_get_exps = function
       [cond]
   | Call ((id, _), e, _, _, _) ->
       [e; Exp.Var id]
-  | Nullify (pvar, _) ->
+  | Metadata metadata ->
-      [Exp.Lvar pvar]
+      exps_of_instr_metadata metadata
-  | Abstract _ ->
-      []
-  | ExitScope (vars, _) ->
-      List.map ~f:Var.to_exp vars
 
 
 (** Convert an if_kind to string  *)
@@ -373,7 +393,15 @@ let if_kind_to_string = function
       "switch"
 
 
-(** Pretty print an instruction. *)
+let pp_instr_metadata pe f = function
+  | Abstract loc ->
+      F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc
+  | ExitScope (vars, loc) ->
+      F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc
+  | Nullify (pvar, loc) ->
+      F.fprintf f "NULLIFY(%a); [%a]" (Pvar.pp pe) pvar Location.pp loc
+
+
 let pp_instr ~print_types pe0 f instr =
   let pp_typ = if print_types then Typ.pp_full else Typ.pp in
   color_wrapper pe0 f instr ~f:(fun pe f instr ->
@@ -392,12 +420,8 @@ let pp_instr ~print_types pe0 f instr =
           F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv ~print_types pe) e
             (Pp.comma_seq (pp_exp_typ pe))
             arg_ts CallFlags.pp cf Location.pp loc
-      | Nullify (pvar, loc) ->
+      | Metadata metadata ->
-          F.fprintf f "NULLIFY(%a); [%a]" (Pvar.pp pe) pvar Location.pp loc
+          pp_instr_metadata pe0 f metadata )
-      | Abstract loc ->
-          F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc
-      | ExitScope (vars, loc) ->
-          F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc )
 
 
 let add_with_block_parameters_flag instr =
@@ -1269,7 +1293,7 @@ let instr_sub_ids ~sub_id_binders f instr =
   | Prune (exp, loc, true_branch, if_kind) ->
       let exp' = exp_sub_ids f exp in
       if phys_equal exp' exp then instr else Prune (exp', loc, true_branch, if_kind)
-  | ExitScope (vars, loc) ->
+  | Metadata (ExitScope (vars, loc)) ->
       let sub_var var =
         match var with
         | Var.ProgramVar _ ->
@@ -1279,8 +1303,8 @@ let instr_sub_ids ~sub_id_binders f instr =
             if phys_equal ident ident' then var else Var.of_id ident'
       in
       let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars in
-      if phys_equal vars vars' then instr else ExitScope (vars', loc)
+      if phys_equal vars vars' then instr else Metadata (ExitScope (vars', loc))
-  | Nullify _ | Abstract _ ->
+  | Metadata (Abstract _ | Nullify _) ->
       instr
 
 

infer/src/IR/Sil.mli

@@ -24,6 +24,13 @@ type if_kind =
   | Ik_switch
 [@@deriving compare]
 
+type instr_metadata =
+  | Abstract of Location.t
+      (** a good place to apply abstraction, mostly used in the biabduction analysis *)
+  | ExitScope of Var.t list * Location.t  (** remove temporaries and dead program variables *)
+  | Nullify of Pvar.t * Location.t  (** nullify stack variable *)
+[@@deriving compare]
+
 (** An instruction. *)
 type instr =
   (* Note for frontend writers:
@@ -45,9 +52,9 @@ type instr =
   | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * 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);] *)
-  | Nullify of Pvar.t * Location.t  (** nullify stack variable *)
+  | Metadata of instr_metadata
-  | Abstract of Location.t  (** apply abstraction *)
+      (** hints about the program that are not strictly needed to understand its semantics, for
-  | ExitScope of Var.t list * Location.t  (** remove temporaries and dead program variables *)
+          instance information about its original syntactic structure *)
 [@@deriving compare]
 
 val equal_instr : instr -> instr -> bool
@@ -275,15 +282,17 @@ val pp_offset : Pp.env -> F.formatter -> offset -> unit
 val d_offset_list : offset list -> unit
 (** Dump a list of offsets *)
 
-val instr_get_loc : instr -> Location.t
+val location_of_instr : instr -> Location.t
 (** Get the location of the instruction *)
 
-val instr_get_exps : instr -> Exp.t list
+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 : Pp.env -> F.formatter -> instr_metadata -> unit
+
 val pp_instr : print_types:bool -> Pp.env -> F.formatter -> instr -> unit
 (** Pretty print an instruction. *)
 

infer/src/IR/SpecializeProcdesc.ml

@@ -113,7 +113,7 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions =
         Some call_instr
     | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
         Some (Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind))
-    | Sil.Nullify _ | Abstract _ | ExitScope _ ->
+    | Sil.Metadata _ ->
         (* these are generated instructions that will be replaced by the preanalysis *)
         None
   in
@@ -206,7 +206,7 @@ let with_block_args_instrs resolved_pdesc substitutions =
             (Var.of_id id, (Exp.Var id, pvar, typ), Sil.Load (id, Exp.Lvar pvar, typ, loc)) )
         |> List.unzip3
       in
-      let remove_temps_instr = Sil.ExitScope (dead_vars, loc) in
+      let remove_temps_instr = Sil.Metadata (ExitScope (dead_vars, loc)) in
       (block_name, id_exp_typs, load_instrs, remove_temps_instr)
     in
     let convert_generic_call return_ids exp origin_args loc call_flags =
@@ -261,7 +261,7 @@ let with_block_args_instrs resolved_pdesc substitutions =
         convert_generic_call return_ids origin_call_exp origin_args loc call_flags
     | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
         (Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind) :: instrs, id_map)
-    | Sil.Nullify _ | Abstract _ | Sil.ExitScope _ ->
+    | Sil.Metadata _ ->
         (* these are generated instructions that will be replaced by the preanalysis *)
         (instrs, id_map)
   in

infer/src/absint/LowerHil.ml

@@ -68,17 +68,17 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
       HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
     in
     match hil_translation with
-    | Ignore ->
-        (None, bindings)
     | Bind (id, access_path) ->
         (None, Bindings.add id access_path bindings)
-    | Instr (ExitScope (vars, loc)) ->
+    | Instr (Metadata (ExitScope (vars, loc))) ->
         let bindings, vars =
           List.fold vars ~init:(bindings, []) ~f:(fun (bindings, vars) var ->
               let bindings, vars' = Bindings.exit_scope var bindings in
               (bindings, append_bindings vars vars') )
         in
-        let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope (vars, loc)) in
+        let instr =
+          if List.is_empty vars then None else Some (HilInstr.Metadata (ExitScope (vars, loc)))
+        in
         (instr, bindings)
     | Instr instr ->
         (Some instr, bindings)

infer/src/backend/errdesc.ml

@@ -499,7 +499,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
     | None ->
         if verbose then L.d_strln "explain_leak: no current instruction" ;
         value_str_from_pvars_vpath [] vpath
-    | Some (Sil.Nullify (pvar, _)) when check_pvar pvar -> (
+    | Some (Sil.Metadata (Nullify (pvar, _))) when check_pvar pvar -> (
         if verbose then (
           L.d_str "explain_leak: current instruction is Nullify for pvar " ;
           Pvar.d pvar ;
@@ -509,10 +509,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
             Some (DExp.to_string de)
         | _ ->
             None )
-    | Some (Sil.Abstract _) ->
+    | Some (Sil.Metadata (Abstract _)) ->
         if verbose then L.d_strln "explain_leak: current instruction is Abstract" ;
         let get_nullify = function
-          | Sil.Nullify (pvar, _) when check_pvar pvar ->
+          | Sil.Metadata (Nullify (pvar, _)) when check_pvar pvar ->
               if verbose then (
                 L.d_str "explain_leak: found nullify before Abstract for pvar " ;
                 Pvar.d pvar ;

infer/src/backend/preanal.ml

@@ -29,7 +29,7 @@ let add_abstraction_instructions pdesc =
   in
   let do_node node =
     let loc = Node.get_last_loc node in
-    if node_requires_abstraction node then Node.append_instrs node [Sil.Abstract loc]
+    if node_requires_abstraction node then Node.append_instrs node [Sil.Metadata (Abstract loc)]
   in
   Procdesc.iter_nodes do_node pdesc
 
@@ -107,9 +107,9 @@ module NullifyTransferFunctions = struct
           (active_defs, to_nullify)
       | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) ->
           (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify)
-      | Sil.Store _ | Prune _ | ExitScope _ | Abstract _ ->
+      | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _) ->
           astate
-      | Sil.Nullify _ ->
+      | Sil.Metadata (Nullify _) ->
           L.(die InternalError)
             "Should not add nullify instructions before running nullify analysis!"
     in
@@ -141,7 +141,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
   let is_local pvar = not (Pvar.is_return pvar || Pvar.is_global pvar) in
   let prepend_node_nullify_instructions loc pvars instrs =
     List.fold pvars ~init:instrs ~f:(fun instrs pvar ->
-        if is_local pvar then Sil.Nullify (pvar, loc) :: instrs else instrs )
+        if is_local pvar then Sil.Metadata (Nullify (pvar, loc)) :: instrs else instrs )
   in
   let node_deadvars_instruction loc vars =
     let local_vars =
@@ -151,7 +151,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
         | Var.LogicalVar _ ->
             true )
     in
-    if List.is_empty local_vars then None else Some (Sil.ExitScope (local_vars, loc))
+    if List.is_empty local_vars then None else Some (Sil.Metadata (ExitScope (local_vars, loc)))
   in
   Container.iter nullify_proc_cfg ~fold:ProcCfg.Exceptional.fold_nodes ~f:(fun node ->
       match NullifyAnalysis.extract_post (ProcCfg.Exceptional.Node.id node) nullify_inv_map with

infer/src/biabduction/State.ml

@@ -92,13 +92,13 @@ let get_node () = !gs.last_node
 let get_loc_exn () =
   match !gs.last_instr with
   | Some instr ->
-      Sil.instr_get_loc instr
+      Sil.location_of_instr instr
   | None ->
       get_node_exn () |> Procdesc.Node.get_loc
 
 
 let get_loc () =
-  match !gs.last_instr with Some instr -> Some (Sil.instr_get_loc instr) | None -> None
+  match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None
 
 
 (** normalize the list of instructions by renaming let-bound ids *)

infer/src/biabduction/SymExec.ml

@@ -1480,7 +1480,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
             ; proc_name= callee_pname
             ; loc
             ; exe_env } )
-  | Sil.Nullify (pvar, _) -> (
+  | Sil.Metadata (Nullify (pvar, _)) -> (
       let eprop = Prop.expose prop_ in
       match
         List.partition_tf
@@ -1500,13 +1500,13 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
           L.internal_error "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text)
             pvar ;
           assert false )
-  | Sil.Abstract _ ->
+  | Sil.Metadata (Abstract _) ->
       if Prover.check_inconsistency tenv prop_ then ret_old_path []
       else
         ret_old_path
           [ Abs.remove_redundant_array_elements current_pname tenv
               (Abs.abstract current_pname tenv prop_) ]
-  | Sil.ExitScope (dead_vars, _) ->
+  | Sil.Metadata (ExitScope (dead_vars, _)) ->
       let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in
       ret_old_path [Prop.exist_quantify tenv dead_ids prop_]
 
@@ -1940,7 +1940,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
       | _ ->
           () ) ;
       let node_has_abstraction node =
-        let instr_is_abstraction = function Sil.Abstract _ -> true | _ -> false in
+        let instr_is_abstraction = function Sil.Metadata (Abstract _) -> true | _ -> false in
         Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node)
       in
       let curr_node = State.get_node_exn () in

infer/src/biabduction/interproc.ml

@@ -373,7 +373,7 @@ let do_after_node node = Printer.node_finish_session node
 (** Return the list of normal ids occurring in the instructions *)
 let instrs_get_normal_vars instrs =
   let do_instr res instr =
-    Sil.instr_get_exps instr
+    Sil.exps_of_instr instr
     |> List.fold_left ~init:res ~f:(fun res e ->
            Exp.free_vars e
            |> Sequence.filter ~f:Ident.is_normal
@@ -559,7 +559,7 @@ let compute_visited vset =
     let lines =
       node_loc.Location.line
       :: IContainer.rev_map_to_list ~fold:Instrs.fold
-           ~f:(fun instr -> (Sil.instr_get_loc instr).Location.line)
+           ~f:(fun instr -> (Sil.location_of_instr instr).Location.line)
            (ProcCfg.Exceptional.instrs n)
     in
     List.remove_consecutive_duplicates ~equal:Int.equal (List.sort ~compare:Int.compare lines)

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -270,9 +270,9 @@ module TransferFunctions = struct
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
         L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ;
         Dom.Mem.add_unknown id ~location mem
-    | ExitScope (dead_vars, _) ->
+    | Metadata (ExitScope (dead_vars, _)) ->
         Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem
-    | Abstract _ | Nullify _ ->
+    | Metadata (Abstract _ | Nullify _) ->
         mem
 
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -120,7 +120,7 @@ let add_unreachable_code (cfg : CFG.t) (node : CFG.Node.t) instr rem_instrs (che
          && ExitStatement.is_end_of_block_or_procedure cfg node rem_instrs ->
       checks
   | _ ->
-      let location = Sil.instr_get_loc instr in
+      let location = Sil.location_of_instr instr in
       let unreachable_statement = UnreachableStatement.{location} in
       {checks with unreachable_statements= unreachable_statement :: checks.unreachable_statements}
 

infer/src/checkers/Ownership.ml

@@ -372,7 +372,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             Domain.remove ret_id_typ astate' )
     | Assume (assume_exp, _, _, loc) ->
         Domain.exp_add_reads assume_exp loc summary astate
-    | ExitScope _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/checkers/Siof.ml

@@ -205,7 +205,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         add_actuals_globals astate pdesc loc actuals
         |> (* make sure it's not Bottom: we made a function call so this needs initialization *)
            at_least_nonbottom
-    | ExitScope _ | Abstract _ | Nullify _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/checkers/addressTaken.ml

@@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               astate_acc
         in
         List.fold ~f:add_actual_by_ref ~init:astate actuals
-    | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | ExitScope _ ->
+    | Sil.Store _ | Load _ | Prune _ | Metadata _ ->
         astate
 
 

infer/src/checkers/cost.ml

@@ -602,13 +602,13 @@ module InstrBasicCost = struct
         CostDomain.zero_record
     | Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
         CostDomain.unit_cost_atomic_operation
-    | Sil.ExitScope _ -> (
+    | Sil.Metadata (ExitScope _) -> (
       match InstrCFG.Node.kind instr_node with
       | Procdesc.Node.Start_node ->
           CostDomain.unit_cost_atomic_operation
       | _ ->
           CostDomain.zero_record )
-    | _ ->
+    | Sil.Metadata (Abstract _ | Nullify _) ->
         CostDomain.zero_record
 
 

infer/src/checkers/functionPointers.ml

@@ -35,7 +35,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Sil.Store (Lvar lhs_pvar, _, Exp.Const (Const.Cfun pn), _) ->
         (* strong update *)
         Domain.add (Pvar.to_string lhs_pvar) (ProcnameSet.singleton pn) astate
-    | Sil.Abstract _ | Call _ | Load _ | Nullify _ | Prune _ | ExitScope _ | Store _ ->
+    | Sil.Load _ | Store _ | Call _ | Prune _ | Metadata _ ->
         astate
 
 

infer/src/checkers/liveness.ml

@@ -157,7 +157,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
         Domain.remove (Var.of_id ret_id) astate
         |> exp_add_live call_exp
         |> add_live_actuals actuals_to_read call_exp
-    | Sil.ExitScope _ | Abstract _ | Nullify _ ->
+    | Sil.Metadata _ ->
         astate
 
 
@@ -185,7 +185,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct
   type extras = ProcData.no_extras
 
   let exec_instr astate _ _ instr =
-    List.fold (Sil.instr_get_exps instr)
+    List.fold (Sil.exps_of_instr instr)
       ~f:(fun acc exp ->
         Exp.fold_captured exp
           ~f:(fun acc exp ->

infer/src/checkers/uninit.ml

@@ -299,7 +299,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         {astate with maybe_uninit_vars}
     | Assume (expr, _, _, loc) ->
         check_hil_expr expr ~loc ; astate
-    | ExitScope _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/concurrency/RacerD.ml

@@ -497,7 +497,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         do_assignment lhs_access_expr rhs_exp loc proc_data astate
     | Assume (assume_exp, _, _, loc) ->
         do_assume assume_exp loc proc_data astate
-    | ExitScope _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/concurrency/starvation.ml

@@ -88,7 +88,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       |> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc)
     in
     match instr with
-    | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | ExitScope _ ->
+    | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ ->
         astate
     | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals ->
         astate

infer/src/labs/ResourceLeaks.ml

@@ -72,7 +72,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Call (_, Indirect _, _, _, _) ->
         (* This should never happen in Java. Fail if it does. *)
         L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr
-    | ExitScope _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/nullsafe/NullabilitySuggest.ml

@@ -112,7 +112,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           | None ->
               astate
         else astate
-    | ExitScope _ ->
+    | Metadata _ ->
         astate
 
 

infer/src/nullsafe/typeCheck.ml

@@ -416,14 +416,14 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
     ignore (typecheck_expr_simple typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1)
   in
   match instr with
-  | Sil.ExitScope (vars, _) ->
+  | Sil.Metadata (ExitScope (vars, _)) ->
       List.fold_right vars ~init:typestate ~f:(fun var astate ->
           match var with
           | Var.LogicalVar id ->
               TypeState.remove_id id astate
           | Var.ProgramVar _ ->
               astate )
-  | Sil.Abstract _ | Sil.Nullify _ ->
+  | Sil.Metadata (Abstract _ | Nullify _) ->
       typestate
   | Sil.Load (id, e, typ, loc) ->
       typecheck_expr_for_errors typestate e loc ;

infer/src/pulse/Pulse.ml

@@ -154,9 +154,11 @@ module PulseTransferFunctions = struct
           dispatch_call summary ret call actuals flags loc astate |> check_error summary
         in
         [post]
-    | ExitScope (vars, _) ->
+    | Metadata (ExitScope (vars, _)) ->
         let post = PulseOperations.remove_vars vars astate in
         [post]
+    | Metadata (Abstract _ | Nullify _) ->
+        [astate]
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"

infer/src/unit/procCfgTests.ml

@@ -17,12 +17,12 @@ let tests =
     Cfg.create_proc_desc cfg
       (ProcAttributes.default (SourceFile.invalid __FILE__) Typ.Procname.empty_block)
   in
-  let dummy_instr1 = Sil.ExitScope ([], Location.dummy) in
+  let dummy_instr1 = Sil.skip_instr in
-  let dummy_instr2 = Sil.Abstract Location.dummy in
+  let dummy_instr2 = Sil.Metadata (Abstract Location.dummy) in
   let dummy_instr3 =
-    Sil.ExitScope ([Var.of_id (Ident.create_fresh Ident.knormal)], Location.dummy)
+    Sil.Metadata (ExitScope ([Var.of_id (Ident.create_fresh Ident.knormal)], Location.dummy))
   in
-  let dummy_instr4 = Sil.ExitScope ([], Location.dummy) in
+  let dummy_instr4 = Sil.skip_instr in
   let instrs1 = [dummy_instr1; dummy_instr2] in
   let instrs2 = [dummy_instr3] in
   let instrs3 = [dummy_instr4] in

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,5 +1,5 @@
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60 here,accessed `*(ptr)` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70 here,accessed `ptr` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here]
 codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `std::function<_fn_>::function(&(lambda),&(0$?%__sil_tmpSIL_materialize_temp__n$8))`,invalidated by destructor call `std::function<_fn_>::~function(lambda)` at line 102 here,accessed `lambda` here]
 codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 30 here,accessed `&(f)` here]
 codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 21 here,accessed `&(f)` here]