[preanal] do not rewrite capture db

Summary: There is no reason to write back to the database here, as the resulting procdesc is anyway stored in the summary.  This is a source of non-determinism.

Reviewed By: skcho

Differential Revision: D23500220

fbshipit-source-id: 7434e6239

infer/src/backend/preanal.ml

@@ -301,12 +301,6 @@ module Liveness = struct
     add_nullify_instrs summary tenv liveness_inv_map
 end
 
-module FunctionPointerSubstitution = struct
-  let process proc_desc =
-    let updated = FunctionPointers.substitute_function_pointers proc_desc in
-    if updated then Attributes.store ~proc_desc:(Some proc_desc) (Procdesc.get_attributes proc_desc)
-end
-
 (** pre-analysis to cut control flow after calls to functions whose type indicates they do not
     return *)
 module NoReturn = struct
@@ -376,7 +370,7 @@ let do_preanalysis exe_env pdesc =
   let proc_name = Procdesc.get_proc_name pdesc in
   if Procname.is_java proc_name then InlineJavaSyntheticMethods.process pdesc ;
   if Config.function_pointer_specialization && not (Procname.is_java proc_name) then
-    FunctionPointerSubstitution.process pdesc ;
+    FunctionPointers.substitute pdesc ;
   (* NOTE: It is important that this preanalysis stays before Liveness *)
   if not (Procname.is_java proc_name) then (
     ClosuresSubstitution.process summary ;

infer/src/checkers/functionPointers.ml

@@ -7,13 +7,6 @@
 
 open! IStd
 module F = Format
-
-module Procname = struct
-  type t = Procname.t [@@deriving compare]
-
-  let pp = Procname.pp
-end
-
 module ProcnameSet = AbstractDomain.FiniteSet (Procname)
 module Domain = AbstractDomain.Map (String) (ProcnameSet)
 
@@ -95,7 +88,7 @@ let get_function_pointers proc_desc =
   Analyzer.exec_cfg cfg () ~initial:Domain.empty
 
 
-let substitute_function_pointers proc_desc =
+let substitute proc_desc =
   let function_pointers = get_function_pointers proc_desc in
   let f = substitute_function_ptrs ~function_pointers in
-  Procdesc.replace_instrs proc_desc ~f
+  ignore (Procdesc.replace_instrs proc_desc ~f)

infer/src/checkers/functionPointers.mli

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+val substitute : Procdesc.t -> unit