Let on-demand control whether to start at all the analysis of a procedure.

Reviewed By: @dulmarod

Differential Revision: D2507562

infer/src/backend/callbacks.ml

@@ -217,7 +217,11 @@ let iterate_callbacks store_summary call_graph exe_env =
   let reset_summary proc_name =
     let attributes_opt =
       Specs.proc_resolve_attributes proc_name in
-    Specs.reset_summary call_graph proc_name attributes_opt in
+    let should_reset =
+      not !Config.ondemand_enabled ||
+      Specs.get_summary proc_name = None in
+    if should_reset
+    then Specs.reset_summary call_graph proc_name attributes_opt in
 
 
   (* Make sure summaries exists. *)

infer/src/backend/config.ml

@@ -170,6 +170,9 @@ let eradicate = ref false
 (** should the checkers be run? *)
 let checkers_enabled () = not !eradicate
 
+(** flag to activate ondemand mode. *)
+let ondemand_enabled = ref false
+
 (** Flag for footprint discovery mode *)
 let footprint = ref true
 

infer/src/backend/inferanalyze.ml

@@ -780,7 +780,7 @@ let compute_files_changed_map _exe_env (source_dirs : DB.source_dir list) exclud
 let exe_env_from_cluster cluster =
   let _exe_env =
     let active_procs_opt =
-      if Ondemand.enabled ()
+      if !Config.ondemand_enabled
       then None
       else Some (cluster_to_active_procs cluster) in
     Exe_env.create active_procs_opt in
@@ -871,7 +871,7 @@ let () =
     match !cluster_cmdline with
     | None ->
         if !Config.curr_language = Config.C_CPP &&
-           not (Ondemand.enabled ()) then
+           not !Config.ondemand_enabled then
           Objc_preanal.do_objc_preanalysis ();
         L.stdout "Starting analysis (Infer version %s)@." Version.versionString;
     | Some clname -> L.stdout "Cluster %s@." clname in
@@ -905,7 +905,7 @@ let () =
   L.err "Found %d source files in %s@." (list_length source_dirs) !Config.results_dir;
 
   let clusters =
-    if Ondemand.enabled ()
+    if !Config.ondemand_enabled
     then
       compute_ondemand_clusters source_dirs
     else

infer/src/backend/ondemand.ml

@@ -15,7 +15,7 @@ open Utils
 
 let trace = false
 
-let enabled () = false
+let () = Config.ondemand_enabled := Config.from_env_variable "INFER_ONDEMAND"
 
 let across_files () = true
 
@@ -33,7 +33,34 @@ let unset_analyze_prop () =
 
 let nesting = ref 0
 
-let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name =
+let procedure_should_be_analyzed curr_pdesc proc_name =
+  match AttributesTable.load_attributes proc_name with
+  | Some proc_attributes ->
+      let currently_analyzed =
+        Specs.summary_exists proc_name &&
+        Specs.is_active proc_name in
+      let already_analyzed = match Specs.get_summary proc_name with
+        | Some summary ->
+            Specs.get_timestamp summary > 0
+        | None ->
+            false in
+      (* The procedure to be analyzed is in the same file as the current one. *)
+      let same_file proc_attributes =
+        (Cfg.Procdesc.get_loc curr_pdesc).Location.file
+        =
+        proc_attributes.ProcAttributes.loc.Location.file in
+
+      !Config.ondemand_enabled &&
+      proc_attributes.ProcAttributes.is_defined && (* we have the implementation *)
+      not currently_analyzed && (* avoid infinite loops *)
+      not already_analyzed && (* avoid re-analysis of the same procedure *)
+      (across_files () (* whether to push the analysis into other files *)
+       || same_file proc_attributes)
+  | None ->
+      false
+
+let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name =
+  let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
 
   let really_do_analysis analyze_proc proc_desc =
     if trace then L.stderr "[%d] really_do_analysis %a -> %a@."
@@ -73,31 +100,9 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name =
         (Printexc.get_backtrace ());
       raise e in
 
-  let currently_analyzed =
-    Specs.summary_exists proc_name &&
-    Specs.is_active proc_name in
-  let already_analyzed = match Specs.get_summary proc_name with
-    | Some summary ->
-        Specs.get_timestamp summary > 0
-    | None ->
-        false in
-  (* The procedure to be analyzed is in the same file as the current one. *)
-  let same_file proc_attributes =
-    match get_proc_desc curr_pname with
-    | Some curr_pdesc ->
-        (Cfg.Procdesc.get_loc curr_pdesc).Location.file
-        =
-        proc_attributes.ProcAttributes.loc.Location.file
-    | None -> false in
-
-  match !analyze_proc_fun, AttributesTable.load_attributes proc_name with
-  | Some analyze_proc, Some proc_attributes
-    when enabled () &&
-         proc_attributes.ProcAttributes.is_defined && (* we have the implementation *)
-         not currently_analyzed && (* avoid infinite loops *)
-         not already_analyzed && (* avoid re-analysis of the same procedure *)
-         (across_files () (* whether to push the analysis into other files *)
-          || same_file proc_attributes) ->
+  match !analyze_proc_fun with
+  | Some analyze_proc
+    when procedure_should_be_analyzed curr_pdesc proc_name ->
       begin
         match get_proc_desc proc_name with
         | Some proc_desc ->

infer/src/backend/ondemand.mli

@@ -13,13 +13,13 @@ type analyze_proc = Procname.t -> unit
 
 type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
 
-(** do_analysis get_proc_desc curr_pname proc_name
+(** do_analysis get_proc_desc curr_descproc_name
     performs an on-demand analysis of proc_name
-    triggered during the analysis of curr_pname. *)
-val do_analysis : get_proc_desc -> Procname.t -> Procname.t -> unit
+    triggered during the analysis of curr_pdesc. *)
+val do_analysis : get_proc_desc -> Cfg.Procdesc.t -> Procname.t -> unit
 
-(** Check if on-demand is currently active. *)
-val enabled : unit -> bool
+(** Check if the procedure called by the current pdesc needs to be analyzed. *)
+val procedure_should_be_analyzed : Cfg.Procdesc.t -> Procname.t -> bool
 
 (** Mark the return type @Nullable by modifying the spec. *)
 val proc_add_return_nullable : Procname.t -> unit

infer/src/checkers/checkers.ml

@@ -57,7 +57,10 @@ module ST = struct
   let store_summary proc_name =
     Option.may
       (fun summary ->
-         try Specs.store_summary proc_name summary with Sys_error s -> L.err "%s@." s)
+         let summary' =
+           { summary with
+             Specs.timestamp = summary.Specs.timestamp + 1 } in
+         try Specs.store_summary proc_name summary' with Sys_error s -> L.err "%s@." s)
       (Specs.get_summary proc_name)
 
   let report_error

infer/src/checkers/eradicate.ml

@@ -393,9 +393,14 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc =
     | Some pdesc ->
         let idenv_pname = Idenv.create_from_idenv idenv pdesc in
         Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in
+  if not !Config.ondemand_enabled ||
+     Ondemand.procedure_should_be_analyzed proc_desc proc_name
+  then
+    begin
       Ondemand.set_analyze_proc _ondemand;
       Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc;
       Ondemand.unset_analyze_prop ()
+    end
 
 (** Call the given check_return_type at the end of every procedure. *)
 let callback_check_return_type check_return_type all_procs

infer/src/checkers/eradicateChecks.ml

@@ -354,7 +354,7 @@ let check_return_annotation
       if return_not_nullable && Models.Inference.enabled then
         Models.Inference.proc_add_return_nullable curr_pname;
 
-      if return_not_nullable && Ondemand.enabled () then
+      if return_not_nullable && !Config.ondemand_enabled then
         Ondemand.proc_add_return_nullable curr_pname;
 
       if return_not_nullable || return_value_not_present then

infer/src/checkers/typeCheck.ml

@@ -557,8 +557,8 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
       typestate (* skip othe builtins *)
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
     when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None ->
-      if Ondemand.enabled () then
-        Ondemand.do_analysis get_proc_desc curr_pname callee_pname;
+      if !Config.ondemand_enabled then
+        Ondemand.do_analysis get_proc_desc curr_pdesc callee_pname;
       let callee_attributes =
         match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
         | Some proc_attributes -> proc_attributes