Bypass the interprocedural algorithm in Fork with ondemand, and replace it with a simple iteration.

Reviewed By: jberdine

Differential Revision: D2965853

fb-gh-sync-id: b75b874
shipit-source-id: b75b874

infer/src/backend/fork.ml

@@ -255,7 +255,7 @@ let filter_max exe_env filter set priority_set =
 (** Main algorithm responsible for driving the analysis of an Exe_env (set of procedures).
     The algorithm computes dependencies between procedures,
     propagates results, and handles fixpoints in the call graph. *)
-let main_algorithm exe_env analyze_proc filter_out process_result : unit =
+let main_algorithm exe_env analyze_proc process_result : unit =
   let call_graph = Exe_env.get_cg exe_env in
   let filter_initial (pname, _) =
     let summary = Specs.get_summary_unsafe "main_algorithm" pname in
@@ -286,14 +286,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 exe_env pname
-    then
-      post_process_procs exe_env [pname]
-    else
-      begin
     Specs.update_dependency_map pname;
-        process_result exe_env elem (analyze_proc exe_env pname);
+    process_result exe_env elem (analyze_proc exe_env pname) in
-      end in
   while not (WeightedPnameSet.is_empty !G.wpnames_todo) do
     begin
       if !trace then begin
@@ -318,16 +312,13 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
 
 type process_result = Exe_env.t -> WeightedPname.t -> Specs.summary -> unit
 
-type filter_out = Exe_env.t -> Procname.t -> bool
-
 (** Execute [analyze_proc] respecting dependencies between procedures,
-    and apply [process_result] to the result of the analysis.
+    and apply [process_result] to the result of the analysis. *)
-    If [filter_out] returns true, don't analyze the procedure. *)
 let interprocedural_algorithm
     (exe_env: Exe_env.t)
     (_analyze_proc: analyze_proc)
     (_process_result: process_result)
-    (filter_out: filter_out) : unit =
+  : unit =
   let analyze_proc exe_env pname = (* wrap _analyze_proc and handle exceptions *)
     let log_error_and_continue exn kind =
       Reporting.log_error pname exn;
@@ -357,4 +348,4 @@ let interprocedural_algorithm
         let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in
         Reporting.log_error pname exn';
         post_process_procs exe_env [pname] in
-  main_algorithm exe_env analyze_proc filter_out process_result
+  main_algorithm exe_env analyze_proc process_result

infer/src/backend/fork.mli

@@ -29,9 +29,6 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
 
 type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit
 
-type filter_out = Exe_env.t -> Procname.t -> bool
-
 (** Execute [analyze_proc] respecting dependencies between procedures,
-    and apply [process_result] to the result of the analysis.
+    and apply [process_result] to the result of the analysis. *)
-    If [filter_out] returns true, don't analyze the procedure. *)
+val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> unit
-val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> filter_out -> unit

infer/src/backend/inferanalyze.ml

@@ -391,7 +391,6 @@ module Simulator = struct (** Simulate the analysis only *)
     let timestamp = max 1 (prev_summary.Specs.timestamp) in
     { prev_summary with Specs.timestamp = timestamp }
 
-  let filter_out _ _ = false
 end
 
 let analyze exe_env =
@@ -412,7 +411,6 @@ let analyze exe_env =
         exe_env
         Simulator.analyze_proc
         Simulator.process_result
-        Simulator.filter_out
     end
   else (* full analysis *)
     begin

infer/src/backend/interproc.ml

@@ -1179,9 +1179,27 @@ let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary
   let procs_done = Fork.procs_become_done call_graph proc_name in
   Fork.post_process_procs exe_env procs_done
 
-let filter_out_ondemand exe_env proc_name =
+let analyze_proc_for_ondemand exe_env proc_name =
-  let to_analyze =
+  let saved_footprint = !Config.footprint in
-    if !Config.ondemand_enabled then
+  Config.footprint := true;
+  let summaryfp = analyze_proc exe_env proc_name in
+  Specs.add_summary proc_name summaryfp;
+  let cg = Cg.create () in
+  Cg.add_defined_node cg proc_name;
+  perform_transition exe_env cg proc_name;
+  Config.footprint := false;
+  let summaryre = analyze_proc exe_env proc_name in
+  Specs.add_summary proc_name summaryre;
+  Config.footprint := saved_footprint
+
+let interprocedural_algorithm_ondemand exe_env : unit =
+  let call_graph = Exe_env.get_cg exe_env in
+  let filter_initial proc_name =
+    let summary = Specs.get_summary_unsafe "main_algorithm" proc_name in
+    Specs.get_timestamp summary = 0 in
+  let procs_to_analyze =
+    IList.filter filter_initial (Cg.get_defined_nodes call_graph) in
+  let to_analyze proc_name =
     try
       let cfg = Exe_env.get_cfg exe_env proc_name in
       match Cfg.Procdesc.find_from_name cfg proc_name with
@@ -1190,14 +1208,25 @@ let filter_out_ondemand exe_env proc_name =
             if !Config.reactive_mode
             then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
             else true in
+          if
             reactive_changed && (* in reactive mode, only analyze changed procedures *)
             Ondemand.procedure_should_be_analyzed pdesc proc_name
-        | None ->
+          then
-            true
+            Some pdesc
-      with Not_found -> true
           else
-      true in
+            None
-  not to_analyze
+      | None ->
+          None
+    with Not_found ->
+      None in
+  let process_one_proc proc_name =
+    match to_analyze proc_name with
+    | Some pdesc ->
+        Ondemand.do_analysis ~propagate_exceptions:false pdesc proc_name
+    | None ->
+        () in
+  IList.iter process_one_proc procs_to_analyze
+
 
 (** Perform the analysis of an exe_env *)
 let do_analysis exe_env =
@@ -1238,24 +1267,18 @@ let do_analysis exe_env =
       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
+      analyze_proc_for_ondemand exe_env proc_name in
-      Config.footprint := true;
-      let summaryfp = analyze_proc exe_env proc_name in
-      Specs.add_summary proc_name summaryfp;
-      let cg = Cg.create () in
-      Cg.add_defined_node cg proc_name;
-      perform_transition exe_env cg proc_name;
-      Config.footprint := false;
-      let summaryre = analyze_proc exe_env proc_name in
-      Specs.add_summary proc_name summaryre;
-      Config.footprint := saved_footprint;
-      () in
     { Ondemand.analyze_ondemand; get_proc_desc; } in
 
+  if !Config.ondemand_enabled
+  then
+    begin
       Ondemand.set_callbacks callbacks;
-  Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out_ondemand;
+      interprocedural_algorithm_ondemand exe_env;
       Ondemand.unset_callbacks ()
-
+    end
+  else
+    Fork.interprocedural_algorithm exe_env analyze_proc process_result
 
 let visited_and_total_nodes cfg =
   let all_nodes =

infer/src/backend/ondemand.ml

@@ -98,7 +98,8 @@ type global_state =
   }
 
 let save_global_state () =
-  Timeout.suspend_existing_timeout ();
+  Timeout.suspend_existing_timeout
+    ~keep_symop_total:false; (* use a new global counter for the callee *)
   {
     abs_val = !Config.abs_val;
     abstraction_rules = Abs.get_current_rules ();
@@ -121,7 +122,7 @@ let restore_global_state st =
   State.restore_state st.symexec_state;
   Timeout.resume_previous_timeout ()
 
-let do_analysis curr_pdesc callee_pname =
+let do_analysis ~propagate_exceptions curr_pdesc callee_pname =
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
 
   let really_do_analysis analyze_proc =
@@ -159,20 +160,42 @@ let do_analysis curr_pdesc callee_pname =
       Specs.add_summary callee_pname summary';
       Checkers.ST.store_summary callee_pname in
 
+    let log_error_and_continue exn kind =
+      Reporting.log_error callee_pname exn;
+      let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_pname in
+      let timestamp = max 1 (prev_summary.Specs.timestamp) in
+      let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in
+      let payload =
+        { prev_summary.Specs.payload with Specs.preposts = Some []; } in
+      let new_summary =
+        { prev_summary with Specs.stats; payload; timestamp; } in
+      Specs.add_summary callee_pname new_summary in
+
     let old_state = save_global_state () in
     preprocess ();
     try
       analyze_proc callee_pname;
       postprocess ();
       restore_global_state old_state;
-    with e ->
+    with exn ->
       L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@."
         Procname.pp callee_pname
-        (Printexc.to_string e)
+        (Printexc.to_string exn)
         (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000))
         (Printexc.get_backtrace ());
       restore_global_state old_state;
-      raise e in
+      if propagate_exceptions
+      then
+        raise exn
+      else
+        match exn with
+        | Analysis_failure_exe kind ->
+            (* in production mode, log the timeout/crash and continue with the summary we had before
+               the failure occurred *)
+            log_error_and_continue exn kind
+        | _ ->
+            (* this happens with assert false or some other unrecognized exception *)
+            log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in
 
   match !callbacks_ref with
   | Some callbacks

infer/src/backend/ondemand.mli

@@ -25,7 +25,7 @@ type callbacks =
 (** do_analysis curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pname. *)
-val do_analysis : Cfg.Procdesc.t -> Procname.t -> unit
+val do_analysis : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit
 
 val one_cluster_per_procedure : unit -> bool
 

infer/src/backend/symExec.ml

@@ -1092,7 +1092,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
         resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in
       let exec_one_pname pname =
         if !Config.ondemand_enabled then
-          Ondemand.do_analysis pdesc pname;
+          Ondemand.do_analysis ~propagate_exceptions:true pdesc pname;
         let exec_skip_call ret_type =
           skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in
         match Specs.get_summary pname with
@@ -1118,7 +1118,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
         | resolved_pname :: _ -> resolved_pname
         | [] -> fn in
       if !Config.ondemand_enabled then
-        Ondemand.do_analysis pdesc resolved_pname;
+        Ondemand.do_analysis ~propagate_exceptions:true pdesc resolved_pname;
       let callee_pdesc_opt = Cfg.Procdesc.find_from_name cfg resolved_pname in
       let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in
       let sentinel_result =

infer/src/backend/timeout.ml

@@ -65,9 +65,9 @@ let get_seconds_remaining () =
   | Config.Win32 ->
       SymOp.get_remaining_wallclock_time ()
 
-let get_current_status () =
+let get_current_status ~keep_symop_total =
   let seconds_remaining = get_seconds_remaining () in
-  let symop_state = SymOp.save_state () in
+  let symop_state = SymOp.save_state ~keep_symop_total in
   {
     seconds_remaining;
     symop_state;
@@ -97,8 +97,8 @@ let unwind () =
   SymOp.unset_alarm ();
   GlobalState.pop ()
 
-let suspend_existing_timeout () =
+let suspend_existing_timeout ~keep_symop_total =
-  let current_status = get_current_status () in
+  let current_status = get_current_status ~keep_symop_total in
   unset_alarm ();
   GlobalState.push current_status
 
@@ -108,7 +108,7 @@ let resume_previous_timeout () =
 
 let exe_timeout f x =
   let suspend_existing_timeout_and_start_new_one () =
-    suspend_existing_timeout ();
+    suspend_existing_timeout ~keep_symop_total:true;
     set_alarm (get_timeout_seconds ());
     SymOp.set_alarm () in
   try

infer/src/backend/timeout.mli

@@ -16,4 +16,4 @@ val exe_timeout : ('a -> unit) -> 'a -> failure_kind option
 val resume_previous_timeout : unit -> unit
 
 (** Suspend the current timeout. It must be resumed later. *)
-val suspend_existing_timeout : unit -> unit
+val suspend_existing_timeout : keep_symop_total:bool -> unit

infer/src/backend/utils.ml

@@ -320,11 +320,10 @@ module SymOp = struct
       (** Number of symop's *)
       mutable symop_count : int;
 
-      (** Total number of symop's since the beginning *)
+      (** Counter for the total number of symop's.
-      mutable symop_total : int;
+          The new state created when save_state is called shares this counter
-
+          if keep_symop_total is true. Otherwise, a new counter is created. *)
-      (** Time in the beginning *)
+      symop_total : int ref;
-      mutable timer : float;
     }
 
   let initial () : t =
@@ -332,8 +331,7 @@ module SymOp = struct
       alarm_active = false;
       last_wallclock = None;
       symop_count = 0;
-      symop_total = 0;
+      symop_total = ref 0;
-      timer = Unix.gettimeofday ();
     }
 
   (** Global State *)
@@ -343,10 +341,18 @@ module SymOp = struct
   let restore_state state =
     gs := state
 
-  (** Return the old state, and revert the current state to the initial one. *)
+  (** Return the old state, and revert the current state to the initial one.
-  let save_state () =
+      If keep_symop_total is true, share the total counter. *)
+  let save_state ~keep_symop_total =
     let old_state = !gs in
-    gs := initial ();
+    let new_state =
+      let st = initial () in
+      if keep_symop_total
+      then
+        { st with symop_total = old_state.symop_total }
+      else
+        st in
+    gs := new_state;
     old_state
 
   (** handler for the wallclock timeout *)
@@ -382,42 +388,33 @@ module SymOp = struct
 
   (** Return the total number of symop's since the beginning *)
   let get_total () =
-    !gs.symop_total
+    !(!gs.symop_total)
 
   (** Reset the total number of symop's *)
   let reset_total () =
-    !gs.symop_total <- 0
+    !gs.symop_total := 0
 
   (** Count one symop *)
   let pay () =
     !gs.symop_count <- !gs.symop_count + 1;
-    !gs.symop_total <- !gs.symop_total + 1;
+    !gs.symop_total := !(!gs.symop_total) + 1;
     if !gs.symop_count > !timeout_symops &&
        !gs.alarm_active
     then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count));
     check_wallclock_alarm ()
 
-  (** Reset the counters *)
+  (** Reset the counter *)
-  let reset () =
+  let reset_count () =
-    !gs.symop_count <- 0;
+    !gs.symop_count <- 0
-    !gs.timer <- Unix.gettimeofday ()
 
   (** Reset the counter and activate the alarm *)
   let set_alarm () =
-    reset ();
+    reset_count ();
     !gs.alarm_active <- true
 
   (** De-activate the alarm *)
   let unset_alarm () =
     !gs.alarm_active <- false
-
-  let report_stats f symops elapsed =
-    F.fprintf f "SymOp stats -- symops:%d time:%f symops/sec:%f" symops elapsed ((float_of_int symops) /. elapsed)
-
-  (** Report the stats since the last reset *)
-  let report f () =
-    let elapsed = Unix.gettimeofday () -. !gs.timer in
-    report_stats f !gs.symop_count elapsed
 end
 
 (** Check if the lhs is a substring of the rhs. *)

infer/src/backend/utils.mli

@@ -199,17 +199,15 @@ module SymOp : sig
   (** Count one symop *)
   val pay : unit -> unit
 
-  (** Report the stats since the last reset *)
-  val report : Format.formatter -> unit -> unit
-
   (** Reset the total number of symop's *)
   val reset_total : unit -> unit
 
   (** Restore the old state. *)
   val restore_state : t -> unit
 
-  (** Return the old state, and revert the current state to the initial one. *)
+  (** Return the old state, and revert the current state to the initial one.
-  val save_state : unit -> t
+      If keep_symop_total is true, share the total counter. *)
+  val save_state : keep_symop_total:bool -> t
 
   (** Reset the counter and activate the alarm *)
   val set_alarm : unit -> unit

infer/src/checkers/performanceCritical.ml

@@ -156,7 +156,7 @@ let collect_calls tenv caller_pdesc checked_pnames call_summary (pname, _) =
   if Procname.Set.mem pname !checked_pnames then call_summary
   else
     begin
-      Ondemand.do_analysis caller_pdesc pname;
+      Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc pname;
       checked_pnames := Procname.Set.add pname !checked_pnames;
       let call_loc = lookup_location pname in
       let updated_expensive_calls =

infer/src/eradicate/typeCheck.ml

@@ -557,7 +557,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 curr_pdesc callee_pname;
+        Ondemand.do_analysis ~propagate_exceptions:true curr_pdesc callee_pname;
       let callee_attributes =
         match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
         | Some proc_attributes -> proc_attributes

infer/src/java/jMain.ml

@@ -85,7 +85,6 @@ let init_global_state source_file =
   DB.current_source := source_file;
   DB.Results_dir.init ();
   Ident.NameGenerator.reset ();
-  SymOp.reset_total ();
   JContext.reset_exn_node_table ();
   let nLOC = FileLOC.file_get_loc (DB.source_file_to_string source_file) in
   Config.nLOC := nLOC

infer/src/llvm/lMain.ml

@@ -41,7 +41,6 @@ let init_global_state source_filename =
   end;
   DB.Results_dir.init ();
   Ident.NameGenerator.reset ();
-  SymOp.reset_total ();
   Config.nLOC := FileLOC.file_get_loc source_filename
 
 let store_icfg tenv cg cfg =