From 8575596dbf68f1fbb713ed043ecbb6115426552b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 24 Oct 2024 03:26:30 -0700 Subject: [PATCH] [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 | 10 +++ infer/man/man1/infer-full.txt | 11 +++ infer/man/man1/infer.txt | 11 +++ infer/src/absint/AbstractInterpreter.ml | 1 + infer/src/absint/RecursiveCycleException.ml | 9 +++ infer/src/backend/ondemand.ml | 87 +++++++++++++++++++-- infer/src/base/Config.ml | 21 ++++- infer/src/base/Config.mli | 10 ++- infer/src/biabduction/Exceptions.ml | 2 +- 9 files changed, 147 insertions(+), 15 deletions(-) create mode 100644 infer/src/absint/RecursiveCycleException.ml diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 61922650dea..219e01fd004 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 3099c33f514..3ad1d6ac4d7 100644 --- a/infer/man/man1/infer-full.txt +++ b/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 diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 0201c9db34a..8f712ad813a 100644 --- a/infer/man/man1/infer.txt +++ b/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 diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 71a62731dd7..7d8619dea35 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 _ -> diff --git a/infer/src/absint/RecursiveCycleException.ml b/infer/src/absint/RecursiveCycleException.ml new file mode 100644 index 00000000000..4fd69610e8a --- /dev/null +++ b/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} diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 6b122b5c878..d24f2597516 100644 --- a/infer/src/backend/ondemand.ml +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index efb998e4fee..cd5dac898a6 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b794d73c84e..23deebb9383 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index 5aa015f044d..c8aa2e07aa8 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/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