[SIL] add `Skip` metadata instruction

Summary: springcleaning2

Reviewed By: ezgicicek

Differential Revision: D14827673

fbshipit-source-id: 0d3cf730b

infer/src/IR/Sil.ml

@@ -31,6 +31,7 @@ type instr_metadata =
       (** 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 *)
+  | Skip  (** no-op *)
 [@@deriving compare]
 
 (** An instruction. *)
@@ -68,7 +69,7 @@ type instr =
 
 let equal_instr = [%compare.equal: instr]
 
-let skip_instr = Metadata (ExitScope ([], Location.dummy))
+let skip_instr = Metadata Skip
 
 (** Check if an instruction is auxiliary, or if it comes from source instructions. *)
 let instr_is_auxiliary = function
@@ -342,6 +343,8 @@ let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp
 let location_of_instr_metadata = function
   | Abstract loc | ExitScope (_, loc) | Nullify (_, loc) ->
       loc
+  | Skip ->
+      Location.dummy
 
 
 (** Get the location of the instruction *)
@@ -359,6 +362,8 @@ let exps_of_instr_metadata = function
       List.map ~f:Var.to_exp vars
   | Nullify (pvar, _) ->
       [Exp.Lvar pvar]
+  | Skip ->
+      []
 
 
 (** get the expressions occurring in the instruction *)
@@ -400,6 +405,8 @@ let pp_instr_metadata pe f = function
       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
+  | Skip ->
+      F.pp_print_string f "SKIP"
 
 
 let pp_instr ~print_types pe0 f instr =
@@ -1304,7 +1311,7 @@ let instr_sub_ids ~sub_id_binders f instr =
       in
       let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars in
       if phys_equal vars vars' then instr else Metadata (ExitScope (vars', loc))
-  | Metadata (Abstract _ | Nullify _) ->
+  | Metadata (Abstract _ | Nullify _ | Skip) ->
       instr
 
 

infer/src/IR/Sil.mli

@@ -29,6 +29,7 @@ type instr_metadata =
       (** 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 *)
+  | Skip  (** no-op *)
 [@@deriving compare]
 
 (** An instruction. *)

infer/src/backend/preanal.ml

@@ -107,7 +107,7 @@ 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 _ | Metadata (Abstract _ | ExitScope _) ->
+      | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _ | Skip) ->
           astate
       | Sil.Metadata (Nullify _) ->
           L.(die InternalError)

infer/src/biabduction/SymExec.ml

@@ -1509,6 +1509,8 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
   | 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_]
+  | Sil.Metadata Skip ->
+      ret_old_path [prop_]
 
 
 and diverge prop path =

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -272,7 +272,7 @@ module TransferFunctions = struct
         Dom.Mem.add_unknown id ~location mem
     | Metadata (ExitScope (dead_vars, _)) ->
         Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem
-    | Metadata (Abstract _ | Nullify _) ->
+    | Metadata (Abstract _ | Nullify _ | Skip) ->
         mem
 
 

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.Metadata (ExitScope _) -> (
+    | Sil.Metadata Skip -> (
       match InstrCFG.Node.kind instr_node with
       | Procdesc.Node.Start_node ->
           CostDomain.unit_cost_atomic_operation
       | _ ->
           CostDomain.zero_record )
-    | Sil.Metadata (Abstract _ | Nullify _) ->
+    | Sil.Metadata (Abstract _ | ExitScope _ | Nullify _) ->
         CostDomain.zero_record
 
 

infer/src/nullsafe/typeCheck.ml

@@ -423,7 +423,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
               TypeState.remove_id id astate
           | Var.ProgramVar _ ->
               astate )
-  | Sil.Metadata (Abstract _ | Nullify _) ->
+  | Sil.Metadata (Abstract _ | Nullify _ | Skip) ->
       typestate
   | Sil.Load (id, e, typ, loc) ->
       typecheck_expr_for_errors typestate e loc ;

infer/src/pulse/Pulse.ml

@@ -157,7 +157,7 @@ module PulseTransferFunctions = struct
     | Metadata (ExitScope (vars, _)) ->
         let post = PulseOperations.remove_vars vars astate in
         [post]
-    | Metadata (Abstract _ | Nullify _) ->
+    | Metadata (Abstract _ | Nullify _ | Skip) ->
         [astate]
 
 

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

@@ -1,4 +1,4 @@
-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_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 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]
@@ -7,7 +7,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ok, 2, USE_AFTE
 codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ptr_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 32 here,accessed `x` here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, FP_may_return_invalid_ptr_ok, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Y))`,assigned to `y`,invalidated by call to `delete y` at line 81 here,accessed `y` here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 37 here,accessed `x` here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 35 here,accessed `*(result)` here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 30 here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []