eliminating dead stores created by copy-propagation

Reviewed By: jberdine

Differential Revision: D3471323

fbshipit-source-id: 10431be

infer/src/IR/Sil.re

@@ -524,6 +524,8 @@ type stackop =
 /** An instruction. */
 type instr =
   /** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] */
+  /* note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire
+     `Letderef` instruction may be eliminated by copy-propagation */
   | Letderef of Ident.t exp Typ.t Location.t
   /** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] */
   | Set of exp Typ.t exp Location.t

infer/src/IR/Sil.rei

@@ -267,6 +267,8 @@ type stackop =
 /** An instruction. */
 type instr =
   /** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] */
+  /* note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire
+     `Letderef` instruction may be eliminated by copy-propagation */
   | Letderef of Ident.t exp Typ.t Location.t
   /** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] */
   | Set of exp Typ.t exp Location.t

infer/src/backend/iList.ml

@@ -118,6 +118,20 @@ let map_changed (f : 'a -> 'a) l =
   then rev l'
   else l
 
+(** like filter, but returns the original list if unchanged *)
+let filter_changed (f : 'a -> bool) l =
+  let l', changed =
+    fold_left
+      (fun (l_acc, changed) e ->
+         if f e
+         then e :: l_acc, changed
+         else l_acc, true)
+      ([], false)
+      l in
+  if changed
+  then rev l'
+  else l
+
 (** tail-recursive variant of List.mapi *)
 let mapi f l =
   let i = ref 0 in

infer/src/backend/iList.mli

@@ -48,6 +48,9 @@ val map : ('a -> 'b) -> 'a list -> 'b list
 (** like map, but returns the original list if unchanged *)
 val map_changed : ('a -> 'a) -> 'a list -> 'a list
 
+(** like filter, but returns the original list if unchanged *)
+val filter_changed : ('a -> bool) -> 'a list -> 'a list
+
 (** tail-recursive variant of List.mapi *)
 val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
 

infer/src/backend/preanal.ml

@@ -91,7 +91,7 @@ let add_abstraction_instructions pdesc =
     if node_requires_abstraction node then Node.append_instrs node [Sil.Abstract loc] in
   Cfg.Procdesc.iter_nodes do_node pdesc
 
-module BackwardCfg = ProcCfg.Backward(ProcCfg.Exceptional)
+module BackwardCfg = ProcCfg.OneInstrPerNode(ProcCfg.Backward(ProcCfg.Exceptional))
 
 module LivenessAnalysis =
   AbstractInterpreter.Make
@@ -115,9 +115,10 @@ module NullifyTransferFunctions = struct
   module CFG = ProcCfg.Exceptional
   type extras = LivenessAnalysis.inv_map
 
-  let postprocess ((reaching_defs, _) as astate) node_id { ProcData.extras; } =
+  let postprocess ((reaching_defs, _) as astate) node { ProcData.extras; } =
+    let node_id =  (CFG.underlying_id node), ProcCfg.Node_index in
     match LivenessAnalysis.extract_state node_id extras with
-    (* note: because the analysis backward, post and pre are reversed *)
+    (* note: because the analysis is backward, post and pre are reversed *)
     | Some { AbstractInterpreter.post = live_before; pre = live_after; } ->
         let to_nullify = VarDomain.diff (VarDomain.union live_before reaching_defs) live_after in
         let reaching_defs' = VarDomain.diff reaching_defs to_nullify in
@@ -150,7 +151,7 @@ module NullifyTransferFunctions = struct
       | Sil.Nullify _ ->
           failwith "Should not add nullify instructions before running nullify analysis!" in
     if is_last_instr_in_node instr node
-    then postprocess astate' (CFG.id node) extras
+    then postprocess astate' node extras
     else astate'
 end
 
@@ -159,16 +160,32 @@ module NullifyAnalysis =
     (Scheduler.ReversePostorder (ProcCfg.Exceptional))
     (NullifyTransferFunctions)
 
-let add_nullify_instrs pdesc tenv =
-  let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
-  let proc_data_no_extras = ProcData.make_default pdesc tenv in
-  let liveness_inv_map = LivenessAnalysis.exec_cfg liveness_proc_cfg proc_data_no_extras in
+(** remove dead stores whose lhs is a frontend-created temporary variable. these dead stores are
+    created by copy-propagation *)
+let remove_dead_frontend_stores pdesc liveness_inv_map =
+  let is_live var instr_id liveness_inv_map =
+    match LivenessAnalysis.extract_pre instr_id liveness_inv_map with
+    | Some pre -> VarDomain.mem var pre
+    | None -> true in
+  let is_used_store (instr, instr_id_opt) =
+    match instr, instr_id_opt with
+    | Sil.Letderef (id, _, _, _), Some instr_id when not (Ident.is_none id) ->
+        is_live (Var.of_id id) instr_id liveness_inv_map
+    | _ -> true in
+  let node_remove_dead_stores node =
+    let instr_nodes = BackwardCfg.instr_ids node in
+    let instr_nodes' = IList.filter_changed is_used_store instr_nodes in
+    if instr_nodes' != instr_nodes
+    then
+      Cfg.Node.replace_instrs node (IList.rev_map fst instr_nodes') in
+  Cfg.Procdesc.iter_nodes node_remove_dead_stores pdesc
 
+let add_nullify_instrs pdesc tenv liveness_inv_map =
   let address_taken_vars =
     if Procname.is_java (Cfg.Procdesc.get_proc_name pdesc)
     then AddressTaken.Domain.empty (* can't take the address of a variable in Java *)
     else
-      match AddressTaken.Analyzer.compute_post proc_data_no_extras with
+      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) with
       | Some post -> post
       | None -> AddressTaken.Domain.empty in
 
@@ -270,8 +287,16 @@ let do_copy_propagation pdesc tenv =
        then Cfg.Node.replace_instrs node (IList.rev instrs))
     (Cfg.Procdesc.get_nodes pdesc)
 
+let do_liveness pdesc tenv =
+  let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
+  LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv)
+
 let doit pdesc cg tenv =
   if Config.copy_propagation then do_copy_propagation pdesc tenv;
-  add_nullify_instrs pdesc tenv;
-  if not Config.lazy_dynamic_dispatch then add_dispatch_calls pdesc cg tenv;
+  let liveness_inv_map = do_liveness pdesc tenv in
+  if not (Config.lazy_dynamic_dispatch) && Config.copy_propagation
+  then remove_dead_frontend_stores pdesc liveness_inv_map;
+  add_nullify_instrs pdesc tenv liveness_inv_map;
+  if not Config.lazy_dynamic_dispatch
+  then add_dispatch_calls pdesc cg tenv;
   add_abstraction_instructions pdesc;

infer/src/checkers/procCfg.ml

@@ -23,6 +23,7 @@ module type Node = sig
 
   val kind : t -> Cfg.Node.nodekind
   val id : t -> id
+  val underlying_id : t -> Cfg.Node.id
   val id_compare : id -> id -> int
   val pp_id : F.formatter -> id -> unit
 end
@@ -33,6 +34,7 @@ module DefaultNode = struct
 
   let kind = Cfg.Node.get_kind
   let id = Cfg.Node.get_id
+  let underlying_id = id
   let id_compare = Cfg.Node.id_compare
   let pp_id = Cfg.Node.pp_id
 end
@@ -43,7 +45,9 @@ module InstrNode = struct
 
   let kind = Cfg.Node.get_kind
 
-  let id t = Cfg.Node.get_id t, Node_index
+  let underlying_id t = Cfg.Node.get_id t
+
+  let id t = underlying_id t, Node_index
 
   let index_compare index1 index2 = match index1, index2 with
     | Node_index, Node_index -> 0

infer/src/checkers/procCfg.mli

@@ -19,6 +19,7 @@ module type Node = sig
 
   val kind : t -> Cfg.Node.nodekind
   val id : t -> id
+  val underlying_id : t -> Cfg.Node.id
   val id_compare : id -> id -> int
   val pp_id : Format.formatter -> id -> unit
 end

infer/src/unit/procCfgTests.ml

@@ -84,14 +84,19 @@ let tests =
         | _ -> assert_failure "Expected exactly two instructions with correct indices"
       end;
       let backward_node_id, _ = BackwardInstrCfg.id n1 in
-      match BackwardInstrCfg.instr_ids n1 with
-      | [ (instr1, Some (id1, ProcCfg.Instr_index 1));
-          (instr2, Some (id2, ProcCfg.Instr_index 0)); ] ->
-          assert_bool "First instr should be dummy_instr2" (instr1 == dummy_instr2);
-          assert_bool "Second instr should be dummy_instr1" (instr2 == dummy_instr1);
-          assert_bool "id1 should be id of underlying node" (id1 == backward_node_id);
-          assert_bool "id2 should be id of underlying node" (id2 == backward_node_id);
-      | _ -> assert_failure "Expected exactly two instructions with correct indices" in
+      begin
+        match BackwardInstrCfg.instr_ids n1 with
+        | [ (instr1, Some (id1, ProcCfg.Instr_index 1));
+            (instr2, Some (id2, ProcCfg.Instr_index 0)); ] ->
+            assert_bool "First instr should be dummy_instr2" (instr1 == dummy_instr2);
+            assert_bool "Second instr should be dummy_instr1" (instr2 == dummy_instr1);
+            assert_bool "id1 should be id of underlying node" (id1 == backward_node_id);
+            assert_bool "id2 should be id of underlying node" (id2 == backward_node_id);
+        | _ -> assert_failure "Expected exactly two instructions with correct indices"
+      end;
+      assert_bool
+        "underlying_id should return id of underlying CFG type"
+        (BackwardInstrCfg.underlying_id n1 = BackwardCfg.id n1) in
     "instr_test">::instr_test_ in
 
   let graph_tests = [

infer/src/unit/schedulerTests.ml

@@ -22,6 +22,7 @@ module MockNode = struct
   let instr_ids _ = []
   let to_instr_nodes _ = assert false
   let id n = n
+  let underlying_id _ = assert false
   let kind _ = Cfg.Node.Stmt_node ""
   let id_compare = int_compare
   let pp_id fmt i =