[ondemand] more deterministic mutual recursion

Summary:
The main source of non-determinism in infer comes from mutual recursion: the analysis will start from somewhere in the cycle and produce different results depending on where it started. This is (worse) because we stop at the first recursive call and return an empty summary for that one, which makes the place where we start in the cycle all the more important.

Restart the analysis from a predictable place (the smallest procedure) when a mutual recursion cycle is detected so that we always(?) get the same result. If the recursive structure is complex it may restart a bunch of times but it should always eventually terminate since we must pick a smaller procedure each time (assuming analysing a procedure will always generate the same recursive ondemand requests every time, *cough* that might be a problem...).

Reviewed By: skcho

Differential Revision:
D63633971

Privacy Context Container: L1208441

fbshipit-source-id: b4cae047d0275907bcdf0ac2c626828bd9aa80dc

infer/man/man1/infer-analyze.txt

@@ -267,6 +267,16 @@ OPTIONS
        --objc-block-execution-macro string
            Macro for executing Objective-C blocks safely.
 
+       --ondemand-recursion-restart-limit int
+           In order to make the analysis of mutual recursion cycles
+           deterministic in their output, the analysis of a cycle of mutually
+           recursive functions may restart the analysis of the entire cycle
+           from a deterministic place. If the graph of mutual recursion is
+           more complex than a simple cycle this could potentially result in
+           many restarts before finding the "right" procedure from which to
+           start. This limits the number of restarts before we give up and
+           analyze the cycle as-is instead.
+
        --no-parameter-not-null-checked
            Deactivates: parameter-not-null-checked checker: An
            Objective-C-specific analysis to detect when a block parameter is

infer/man/man1/infer-full.txt

@@ -1313,6 +1313,17 @@ OPTIONS
            compiler does. (Conversely: --no-objc-synthesize-dealloc)
            See also infer-capture(1).
 
+       --ondemand-recursion-restart-limit int
+           In order to make the analysis of mutual recursion cycles
+           deterministic in their output, the analysis of a cycle of mutually
+           recursive functions may restart the analysis of the entire cycle
+           from a deterministic place. If the graph of mutual recursion is
+           more complex than a simple cycle this could potentially result in
+           many restarts before finding the "right" procedure from which to
+           start. This limits the number of restarts before we give up and
+           analyze the cycle as-is instead.
+           See also infer-analyze(1).
+
        --no-parameter-not-null-checked
            Deactivates: parameter-not-null-checked checker: An
            Objective-C-specific analysis to detect when a block parameter is

infer/man/man1/infer.txt

@@ -1313,6 +1313,17 @@ OPTIONS
            compiler does. (Conversely: --no-objc-synthesize-dealloc)
            See also infer-capture(1).
 
+       --ondemand-recursion-restart-limit int
+           In order to make the analysis of mutual recursion cycles
+           deterministic in their output, the analysis of a cycle of mutually
+           recursive functions may restart the analysis of the entire cycle
+           from a deterministic place. If the graph of mutual recursion is
+           more complex than a simple cycle this could potentially result in
+           many restarts before finding the "right" procedure from which to
+           start. This limits the number of restarts before we give up and
+           analyze the cycle as-is instead.
+           See also infer-analyze(1).
+
        --no-parameter-not-null-checked
            Deactivates: parameter-not-null-checked checker: An
            Objective-C-specific analysis to detect when a block parameter is

infer/src/absint/AbstractInterpreter.ml

@@ -621,6 +621,7 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
           post
       | Error (exn, backtrace, instr) ->
           ( match exn with
+          | RecursiveCycleException.RecursiveCycle _
           | RestartSchedulerException.ProcnameAlreadyLocked _
           | MissingDependencyException.MissingDependencyException
           | Timer.Timeout _ ->

infer/src/absint/RecursiveCycleException.ml

@@ -0,0 +1,9 @@
+(*
+ * 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
+
+exception RecursiveCycle of {recursive: SpecializedProcname.t; ttl: int}

infer/src/backend/ondemand.ml

@@ -35,6 +35,11 @@ module ActiveProcedures : sig
   val remove : active -> unit
 
   val get_all : unit -> active list
+
+  val get_cycle_start : active -> active * int * active
+  (** given a target where we detected a recursive call, i.e. that already belongs to the queue,
+      return a triple of where the cycle starts, the length of the cycle, and the first procedure we
+      started to analyze *)
 end = struct
   type active = SpecializedProcname.t
 
@@ -65,6 +70,18 @@ end = struct
 
 
   let get_all () = AnalysisTargets.keys currently_analyzed
+
+  let get_cycle_start recursive =
+    let all = get_all () in
+    (* there is always one target in the queue since [recursive] is in the queue *)
+    let first_active = List.hd_exn all in
+    let cycle =
+      List.drop_while all ~f:(fun target -> not (SpecializedProcname.equal target recursive))
+    in
+    let cycle_length = List.length cycle in
+    (* there is always one target in the cycle which is the previous call to [recursive] *)
+    let cycle_start = List.min_elt ~compare:SpecializedProcname.compare cycle |> Option.value_exn in
+    (cycle_start, cycle_length, first_active)
 end
 
 (** an alternative mean of "cutting" recursion cycles used when replaying a previous analysis: times
@@ -257,6 +274,7 @@ let run_proc_analysis exe_env tenv analysis_req specialization_context ?caller_p
     let backtrace = Printexc.get_backtrace () in
     IExn.reraise_if exn ~f:(fun () ->
         match exn with
+        | RecursiveCycleException.RecursiveCycle _
         | RestartSchedulerException.ProcnameAlreadyLocked _
         | MissingDependencyException.MissingDependencyException ->
             decr nesting ;
@@ -405,17 +423,44 @@ let double_lock_for_restart ~lazy_payloads analysis_req callee_pname specializat
         `NoSummary )
 
 
-let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t) ~specialization
-    ?caller_summary ?(from_file_analysis = false) callee_pname : _ AnalysisResult.t =
+let analysis_result_of_option opt = Result.of_option opt ~error:AnalysisResult.AnalysisFailed
+
+(** track how many times we restarted the analysis of the current dependency chain to make the
+    analysis of mutual recursion cycles deterministic *)
+let number_of_recursion_restarts = ref 0
+
+let rec analyze_callee_can_raise_recursion exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
+    ~specialization ?caller_summary ?(from_file_analysis = false) callee_pname : _ AnalysisResult.t
+    =
   match detect_mutual_recursion_cycle ~caller_summary ~callee:callee_pname specialization with
-  | `InMutualRecursionCycle | `ReplayCycleCut ->
+  | `InMutualRecursionCycle ->
+      let target = {SpecializedProcname.proc_name= callee_pname; specialization} in
+      let cycle_start, cycle_length, first_active = ActiveProcedures.get_cycle_start target in
+      if
+        !number_of_recursion_restarts > Config.ondemand_recursion_restart_limit
+        || SpecializedProcname.equal cycle_start target
+      then (
+        register_callee ~cycle_detected:true ?caller_summary callee_pname ;
+        if Config.trace_ondemand then
+          L.progress "Closed the cycle finishing in recursive call to %a@." Procname.pp callee_pname ;
+        Error MutualRecursionCycle )
+      else (
+        if Config.trace_ondemand then
+          L.progress "Found cycle at %a, first_active= %a; restarting from %a@\nactives: %a@."
+            Procname.pp callee_pname Procname.pp first_active.proc_name Procname.pp
+            cycle_start.proc_name
+            (Pp.seq ~sep:"," SpecializedProcname.pp)
+            (ActiveProcedures.get_all ()) ;
+        (* we want the exception to pop back up to the beginning of the cycle, so we set [ttl= cycle_length] *)
+        incr number_of_recursion_restarts ;
+        raise (RecursiveCycleException.RecursiveCycle {recursive= cycle_start; ttl= cycle_length}) )
+  | `ReplayCycleCut ->
       register_callee ~cycle_detected:true ?caller_summary callee_pname ;
+      if Config.trace_ondemand then
+        L.progress "Closed the cycle finishing in recursive call to %a@." Procname.pp callee_pname ;
       Error MutualRecursionCycle
   | `NotInMutualRecursionCycle -> (
       register_callee ~cycle_detected:false ?caller_summary callee_pname ;
-      let analysis_result_of_option opt =
-        Result.of_option opt ~error:AnalysisResult.AnalysisFailed
-      in
       if is_in_block_list callee_pname then Error InBlockList
       else
         let analyze_callee_aux specialization_context =
@@ -480,6 +525,36 @@ let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
             Error UnknownProcedure )
 
 
+and on_recursive_cycle exe_env ~lazy_payloads analysis_req ?caller_summary:_ ?from_file_analysis
+    ~ttl (cycle_start : SpecializedProcname.t) callee_pname =
+  if ttl > 0 then
+    raise (RecursiveCycleException.RecursiveCycle {recursive= cycle_start; ttl= ttl - 1}) ;
+  analyze_callee exe_env ~lazy_payloads analysis_req ~specialization:cycle_start.specialization
+    ?from_file_analysis cycle_start.proc_name
+  |> ignore ;
+  (* TODO: register caller -> callee relationship, possibly *)
+  Summary.OnDisk.get ~lazy_payloads analysis_req callee_pname |> analysis_result_of_option
+
+
+and analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_summary
+    ?from_file_analysis callee_pname =
+  try
+    analyze_callee_can_raise_recursion exe_env ~lazy_payloads analysis_req ~specialization
+      ?caller_summary ?from_file_analysis callee_pname
+  with RecursiveCycleException.RecursiveCycle {recursive; ttl} ->
+    on_recursive_cycle ~lazy_payloads exe_env analysis_req recursive ~ttl callee_pname
+
+
+let analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_summary
+    ?from_file_analysis callee_pname =
+  (* If [caller_summary] is set then we are analyzing a dependency of another procedure, so we
+     should keep counting restarts within that dependency chain (or cycle). If it's not set then
+     this is a "toplevel" analysis of [callee_pname] so we start fresh. *)
+  if Option.is_none caller_summary then number_of_recursion_restarts := 0 ;
+  analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_summary
+    ?from_file_analysis callee_pname
+
+
 let analyze_proc_name exe_env analysis_req ?specialization ~caller_summary callee_pname =
   analyze_callee ~lazy_payloads:false ~specialization exe_env analysis_req ~caller_summary
     callee_pname

infer/src/base/Config.ml

@@ -2250,6 +2250,17 @@ and objc_synthesize_dealloc =
      classes corresponding to what the compiler does."
 
 
+and ondemand_recursion_restart_limit =
+  CLOpt.mk_int ~long:"ondemand-recursion-restart-limit" ~default:100
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "In order to make the analysis of mutual recursion cycles deterministic in their output, the \
+     analysis of a cycle of mutually recursive functions may restart the analysis of the entire \
+     cycle from a deterministic place. If the graph of mutual recursion is more complex than a \
+     simple cycle this could potentially result in many restarts before finding the \"right\" \
+     procedure from which to start. This limits the number of restarts before we give up and \
+     analyze the cycle as-is instead."
+
+
 and oom_threshold =
   CLOpt.mk_int_opt ~long:"oom-threshold"
     "Available memory threshold (in MB) below which multi-worker scheduling throttles back work. \
@@ -4359,14 +4370,16 @@ and no_translate_libs = not !headers
 
 and nullable_annotation = !nullable_annotation
 
-and only_cheap_debug = !only_cheap_debug
-
-and oom_threshold = !oom_threshold
-
 and objc_block_execution_macro = !objc_block_execution_macro
 
 and objc_synthesize_dealloc = !objc_synthesize_dealloc
 
+and ondemand_recursion_restart_limit = !ondemand_recursion_restart_limit
+
+and only_cheap_debug = !only_cheap_debug
+
+and oom_threshold = !oom_threshold
+
 and pmd_xml = !pmd_xml
 
 and preanalysis_html = !preanalysis_html

infer/src/base/Config.mli

@@ -562,14 +562,16 @@ val no_translate_libs : bool
 
 val nullable_annotation : string option
 
-val only_cheap_debug : bool
-
-val oom_threshold : int option
-
 val objc_block_execution_macro : string option
 
 val objc_synthesize_dealloc : bool
 
+val ondemand_recursion_restart_limit : int
+
+val only_cheap_debug : bool
+
+val oom_threshold : int option
+
 val pmd_xml : bool
 
 val preanalysis_html : bool

infer/src/biabduction/Exceptions.ml

@@ -184,7 +184,7 @@ let print_exception_html s exn =
 (** Return true if the exception is not serious and should be handled in timeout mode *)
 let handle_exception exn =
   match exn with
-  | RestartSchedulerException.ProcnameAlreadyLocked _ ->
+  | RecursiveCycleException.RecursiveCycle _ | RestartSchedulerException.ProcnameAlreadyLocked _ ->
       false
   | _ ->
       let error = recognize_exception exn in