copy propagation step 1: propagate copies in the CFG

Reviewed By: jberdine

Differential Revision: D3346459

fbshipit-source-id: b69f9af

infer/src/backend/config.ml

@@ -593,6 +593,10 @@ and continue =
     "Continue the capture for the reactive analysis,\
      increasing the changed files/procedures."
 
+and copy_propagation =
+  CLOpt.mk_bool ~deprecated:["copy-propagation"] ~long:"copy-propagation"
+    "Perform copy-propagation on the IR"
+
 and curr_language =
   let var = ref Clang in
   CLOpt.mk_set var Java ~deprecated:["java"] ~long:"java" "Set language to Java" ;
@@ -1306,6 +1310,7 @@ and clang_lang = !clang_lang
 and cluster_cmdline = !cluster
 and code_query = !code_query
 and continue_capture = !continue
+and copy_propagation = !copy_propagation
 and create_harness = !android_harness
 and cxx_experimental = !cxx_experimental
 and debug_mode = !debug

infer/src/backend/config.mli

@@ -151,6 +151,7 @@ val clang_lang : clang_lang
 val cluster_cmdline : string option
 val code_query : string option
 val continue_capture : bool
+val copy_propagation : bool
 val create_harness : bool
 val cxx_experimental : bool
 val debug_mode : bool

infer/src/backend/errdesc.ml

@@ -197,7 +197,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
 (** Find the Letderef instruction used to declare normal variable [id],
     and return the expression dereferenced to initialize [id] *)
 let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp option =
-  let is_infer = Config.analyzer = Some Infer in
+  let is_infer = not (Config.checkers || Config.eradicate) in
   let find_declaration node = function
     | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
         if verbose

infer/src/backend/interproc.ml

@@ -1429,7 +1429,11 @@ let do_analysis exe_env =
     let analyze_ondemand proc_desc =
       let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
       let tenv = Exe_env.get_tenv exe_env proc_name in
-      Preanal.doit proc_desc (Exe_env.get_cg exe_env) tenv;
+      if not (Config.eradicate || Config.checkers)
+      then
+        (* Eradicate and the checkers don't need the Nullify/Remove_temps/Abstract instructions that
+           the preanalysis inserts. *)
+        Preanal.doit proc_desc (Exe_env.get_cg exe_env) tenv;
       let summaryfp =
         Config.run_in_footprint_mode (analyze_proc exe_env) proc_desc in
       Specs.add_summary proc_name summaryfp;

infer/src/backend/preanal.ml

@@ -218,7 +218,60 @@ let add_nullify_instrs pdesc tenv =
     let exit_node = ProcCfg.Exceptional.exit_node nullify_proc_cfg in
     node_add_nullify_instructions exit_node (AddressTaken.Domain.elements address_taken_vars)
 
+module ExceptionalOneInstrPerNodeCfg = ProcCfg.OneInstrPerNode(ProcCfg.Exceptional)
+
+module CopyProp =
+  AbstractInterpreter.Make
+    (ExceptionalOneInstrPerNodeCfg)
+    (Scheduler.ReversePostorder)
+    (CopyPropagation.TransferFunctions)
+
+let do_copy_propagation pdesc tenv =
+  let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in
+  let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) in
+  (** [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some
+      ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an
+      ident. *)
+  let id_sub var_map id =
+    (* [last_id] is the highest identifier in the chain that we've seen so far *)
+    let rec id_sub_inner var_map var last_id =
+      try
+        let var' = CopyPropagation.Domain.find var var_map in
+        let last_id' = match var' with
+          | Var.LogicalVar id -> id
+          | _ -> last_id in
+        id_sub_inner var_map var' last_id'
+      with Not_found ->
+        Sil.Var last_id in
+    id_sub_inner var_map (Var.of_id id) id in
+
+  (** perform copy-propagation on each instruction in [node] *)
+  let rev_transform_node_instrs node =
+    IList.fold_left
+      (fun (instrs, changed) (instr, id_opt) ->
+         match id_opt with
+         | Some id ->
+             begin
+               match CopyProp.extract_pre id copy_prop_inv_map with
+               | Some pre when not (CopyPropagation.Domain.is_empty pre) ->
+                   let instr' = Sil.instr_sub_ids ~sub_id_binders:false (id_sub pre) instr in
+                   instr' :: instrs, changed || instr' != instr
+               | _ ->
+                   instr :: instrs, changed
+             end
+         | None -> instr :: instrs, changed)
+      ([], false)
+      (ExceptionalOneInstrPerNodeCfg.instr_ids node) in
+
+  IList.iter
+    (fun node ->
+       let instrs, changed = rev_transform_node_instrs node in
+       if changed
+       then Cfg.Node.replace_instrs node (IList.rev instrs))
+    (Cfg.Procdesc.get_nodes pdesc)
+
 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;
   add_abstraction_instructions pdesc;

infer/src/checkers/copyPropagation.ml

@@ -13,6 +13,7 @@ module F = Format
 module L = Logging
 
 module Domain = struct
+  include Var.Map
   type astate = Var.t Var.Map.t
 
   let initial = Var.Map.empty

infer/src/checkers/var.ml

@@ -11,12 +11,10 @@ open! Utils
 
 (** Single abstraction for all the kinds of variables in SIL *)
 
-type var =
+type t =
   | ProgramVar of Pvar.t
   | LogicalVar of Ident.t
 
-type t = var
-
 let of_id id =
   LogicalVar id
 
@@ -41,13 +39,13 @@ let pp fmt = function
   | LogicalVar id -> (Ident.pp pe_text) fmt id
 
 module Map = PrettyPrintable.MakePPMap(struct
-    type t = var
+    type nonrec t = t
     let compare = compare
     let pp_key = pp
   end)
 
 module Set = PrettyPrintable.MakePPSet(struct
-    type t = var
+    type nonrec t = t
     let compare = compare
     let pp_element = pp
   end)

infer/src/checkers/var.mli

@@ -9,7 +9,9 @@
 
 (** Single abstraction for all the kinds of variables in SIL *)
 
-type t
+type t = private
+  | ProgramVar of Pvar.t
+  | LogicalVar of Ident.t
 
 val of_id : Ident.t -> t