Add basic support for on-demand for the core Infer analysis.

Reviewed By: @jvillard

Differential Revision: D2507560

fb-gh-sync-id: 0dead86

infer/src/backend/fork.ml

@@ -277,24 +277,42 @@ end = struct
         ignore (Gc.create_alarm SymOp.check_wallclock_alarm)
   end
 
+  let current_timeouts = ref []
+
   let exe_timeout iterations f x =
-    try
+    let restore_timeout () =
+      match !current_timeouts with
+      | prev_iterations :: _ ->
+          set_alarm prev_iterations
+      | [] ->
+          () in
+    let unwind () =
+      let pop () = match !current_timeouts with
+        | _ :: l -> current_timeouts := l
+        | [] -> () in
+      unset_alarm ();
+      SymOp.unset_alarm ();
+      pop () in
+    let before () =
+      current_timeouts := iterations :: !current_timeouts;
       set_iterations iterations;
       set_alarm (get_timeout_seconds ());
-      SymOp.set_alarm ();
+      SymOp.set_alarm () in
+    let after () =
+      unwind ();
+      restore_timeout () in
+    try
+      before ();
       let res = f x in
-      unset_alarm ();
+      after ();
-      SymOp.unset_alarm ();
       Some res
     with
     | Timeout_exe kind ->
-        unset_alarm ();
+        after ();
-        SymOp.unset_alarm ();
         Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_kind kind;
         None
     | exe ->
-        unset_alarm ();
+        after ();
-        SymOp.unset_alarm ();
         raise exe
 end
 
@@ -321,6 +339,18 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
       (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) &&
     (Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0
      || not (proc_is_up_to_date call_graph pname)) in
+  let filter_out_ondemand pname =
+    if !Config.ondemand_enabled then
+      try
+        let cfg = Exe_env.get_cfg exe_env pname in
+        match Cfg.Procdesc.find_from_name cfg pname with
+        | Some pdesc ->
+            not (Ondemand.procedure_should_be_analyzed pdesc pname)
+        | None ->
+            false
+      with Not_found -> false
+    else
+      false in
   let process_one_proc pname (calls: Cg.in_out_calls) =
     DB.current_source :=
       (Specs.get_summary_unsafe "main_algorithm" pname)
@@ -333,7 +363,8 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
           (Specs.pp_summary pe_text whole_seconds)
           (Specs.get_summary_unsafe "main_algorithm" pname)
       end;
-    if filter_out call_graph pname
+    if filter_out call_graph pname ||
+       filter_out_ondemand pname
     then
       post_process_procs exe_env [pname]
     else
@@ -357,7 +388,8 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit =
       with Not_found -> (* no analyzable procs *)
         L.err "Error: can't analyze any procs. Printing current spec table@\n@[<v>%a@]@."
           (Specs.pp_spec_table pe_text false) ();
-        raise (Failure "Stopping")
+        if !Config.ondemand_enabled then wpnames_todo := WeightedPnameSet.empty
+        else raise (Failure "Stopping")
     end
   done
 

infer/src/backend/interproc.ml

@@ -1245,8 +1245,35 @@ let do_analysis exe_env =
     if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children)
     else if !Config.only_nospecs then filter_nospecs
     else (fun _ -> true) in
-  list_iter (fun x -> if filter x then init_proc x) procs_and_defined_children;
+  list_iter
-  Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out
+    (fun ((pn, _) as x) ->
+       let should_init () =
+         not !Config.ondemand_enabled ||
+         Specs.get_summary pn = None in
+       if filter x &&
+          should_init ()
+       then init_proc x)
+    procs_and_defined_children;
+
+  let callbacks =
+    let get_proc_desc proc_name =
+      let callee_cfg = Exe_env.get_cfg exe_env proc_name in
+      Cfg.Procdesc.find_from_name callee_cfg proc_name in
+    let analyze_ondemand proc_name =
+      let saved_footprint = !Config.footprint in
+      let _summaryfp = analyze_proc exe_env proc_name in
+      let cg = Cg.create () in
+      Cg.add_node cg proc_name;
+      perform_transition exe_env cg proc_name;
+      let _summaryre = analyze_proc exe_env proc_name in
+      Config.footprint := saved_footprint;
+      () in
+    { Ondemand.analyze_ondemand; get_proc_desc; } in
+
+  Ondemand.set_callbacks callbacks;
+  Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out;
+  Ondemand.unset_callbacks ()
+
 
 let visited_and_total_nodes cfg =
   let all_nodes =
@@ -1283,7 +1310,8 @@ let print_stats_cfg proc_shadowed proc_is_active cfg =
   let num_timeout = ref 0 in
   let compute_stats_proc proc_desc =
     let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
-    if proc_shadowed proc_desc then
+    if proc_shadowed proc_desc ||
+       Specs.get_summary proc_name = None then
       L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name
     else
       let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in

infer/src/backend/ondemand.ml

@@ -15,21 +15,29 @@ open Utils
 
 let trace = false
 
-let () = Config.ondemand_enabled := Config.from_env_variable "INFER_ONDEMAND"
+let () = Config.ondemand_enabled :=
+    Config.from_env_variable "INFER_ONDEMAND" &&
+    not Config.analyze_models
 
 let across_files () = true
 
-type analyze_proc = Procname.t -> unit
+type analyze_ondemand = Procname.t -> unit
 
 type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
 
-let analyze_proc_fun = ref None
+type callbacks =
+  {
+    analyze_ondemand : analyze_ondemand;
+    get_proc_desc : get_proc_desc;
+  }
 
-let set_analyze_proc (analyze_proc : analyze_proc) =
+let callbacks_ref = ref None
-  analyze_proc_fun := Some analyze_proc
 
-let unset_analyze_prop () =
+let set_callbacks  (callbacks : callbacks) =
-  analyze_proc_fun := None
+  callbacks_ref := Some callbacks
+
+let unset_callbacks () =
+  callbacks_ref := None
 
 let nesting = ref 0
 
@@ -50,16 +58,20 @@ let procedure_should_be_analyzed curr_pdesc proc_name =
         =
         proc_attributes.ProcAttributes.loc.Location.file in
 
+      let is_harness () =
+        string_contains "InferGeneratedHarness" (Procname.to_simplified_string proc_name) 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 *)
+      (across_files () || (* whether to push the analysis into other files *)
-       || same_file proc_attributes)
+       same_file proc_attributes) &&
+      not (is_harness ()) (* skip harness procedures *)
   | None ->
       false
 
-let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name =
+let do_analysis curr_pdesc proc_name =
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
 
   let really_do_analysis analyze_proc proc_desc =
@@ -100,13 +112,14 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name =
         (Printexc.get_backtrace ());
       raise e in
 
-  match !analyze_proc_fun with
+  match !callbacks_ref with
-  | Some analyze_proc
+  | Some callbacks
     when procedure_should_be_analyzed curr_pdesc proc_name ->
+
       begin
-        match get_proc_desc proc_name with
+        match callbacks.get_proc_desc proc_name with
         | Some proc_desc ->
-            really_do_analysis analyze_proc proc_desc
+            really_do_analysis callbacks.analyze_ondemand proc_desc
         | None -> ()
       end
   | _ ->

infer/src/backend/ondemand.mli

@@ -9,14 +9,20 @@
 
 (** Module for on-demand analysis. *)
 
-type analyze_proc = Procname.t -> unit
+type analyze_ondemand = Procname.t -> unit
 
 type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
 
-(** do_analysis get_proc_desc curr_descproc_name
+type callbacks =
+  {
+    analyze_ondemand : analyze_ondemand;
+    get_proc_desc : get_proc_desc;
+  }
+
+(** do_analysis curr_pdesc proc_name
     performs an on-demand analysis of proc_name
-    triggered during the analysis of curr_pdesc. *)
+    triggered during the analysis of curr_pname. *)
-val do_analysis : get_proc_desc -> Cfg.Procdesc.t -> Procname.t -> unit
+val do_analysis : Cfg.Procdesc.t -> Procname.t -> unit
 
 (** Check if the procedure called by the current pdesc needs to be analyzed. *)
 val procedure_should_be_analyzed : Cfg.Procdesc.t -> Procname.t -> bool
@@ -24,8 +30,8 @@ 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
 
-(** Set the function to be used to perform on-demand analysis. *)
+(** Set the callbacks used to perform on-demand analysis. *)
-val set_analyze_proc : analyze_proc -> unit
+val set_callbacks : callbacks -> unit
 
-(** Unset the function to be used to perform on-demand analysis. *)
+(** Unset the callbacks used to perform on-demand analysis. *)
-val unset_analyze_prop : unit -> unit
+val unset_callbacks : unit -> unit

infer/src/backend/specs.ml

@@ -396,7 +396,7 @@ let describe_status summary =
   ("Status", if summary.status == ACTIVE then "ACTIVE" else "INACTIVE")
 
 let describe_phase summary =
-  ("Phase", if summary.phase == FOOTPRINT then "FOOTRPRINT" else "RE_EXECUTION")
+  ("Phase", if summary.phase == FOOTPRINT then "FOOTPRINT" else "RE_EXECUTION")
 
 (** Return the signature of a procedure declaration as a string *)
 let get_signature summary =

infer/src/backend/symExec.ml

@@ -963,6 +963,10 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
         if call_flags.Sil.cf_virtual then
           resolve_virtual_pname cfg tenv prop_r n_actual_params fn
         else fn in
+
+      if !Config.ondemand_enabled then
+        Ondemand.do_analysis pdesc callee_pname;
+
       let ret_typ_opt =
         match Cfg.Procdesc.find_from_name cfg resolved_pname with
         | None -> None

infer/src/checkers/eradicate.ml

@@ -387,19 +387,22 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc =
       check_extension = false;
       check_ret_type = [];
     } in
-  let _ondemand pname =
+  let callbacks =
-    match get_proc_desc pname with
+    let analyze_ondemand pname =
-    | None -> ()
+      match get_proc_desc pname with
-    | Some pdesc ->
+      | None -> ()
-        let idenv_pname = Idenv.create_from_idenv idenv pdesc in
+      | Some pdesc ->
-        Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in
+          let idenv_pname = Idenv.create_from_idenv idenv pdesc in
+          Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in
+    { Ondemand.analyze_ondemand; get_proc_desc; } in
+
   if not !Config.ondemand_enabled ||
      Ondemand.procedure_should_be_analyzed proc_desc proc_name
   then
     begin
-      Ondemand.set_analyze_proc _ondemand;
+      Ondemand.set_callbacks callbacks;
       Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc;
-      Ondemand.unset_analyze_prop ()
+      Ondemand.unset_callbacks ()
     end
 
 (** Call the given check_return_type at the end of every procedure. *)

infer/src/checkers/typeCheck.ml

@@ -558,7 +558,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
   | 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 !Config.ondemand_enabled then
-        Ondemand.do_analysis get_proc_desc curr_pdesc callee_pname;
+        Ondemand.do_analysis curr_pdesc callee_pname;
       let callee_attributes =
         match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
         | Some proc_attributes -> proc_attributes