[multicore][pulse] do not die on specialisation timing out

Summary: There are a few reasons for which analysis may fail (timeout, restart) which are not errors deserving a crash.

Reviewed By: jvillard

Differential Revision:
D68094473

Privacy Context Container: L1208441

fbshipit-source-id: f017a983dccd5e1e9a982798f2a6173d2ed4d679

infer/src/absint/AnalysisResult.ml

@@ -13,3 +13,5 @@ type no_summary = AnalysisFailed | InBlockList | MutualRecursionCycle | UnknownP
 type 'a t = ('a, no_summary) result
 
 let to_option = function Ok x -> Some x | Error _ -> None
+
+let of_option = function Some v -> Ok v | None -> Error AnalysisFailed

infer/src/absint/AnalysisResult.mli

@@ -13,3 +13,5 @@ type no_summary = AnalysisFailed | InBlockList | MutualRecursionCycle | UnknownP
 type 'a t = ('a, no_summary) result
 
 val to_option : 'a t -> 'a option
+
+val of_option : 'a option -> ('a, no_summary) result

infer/src/absint/InterproceduralAnalysis.ml

@@ -29,5 +29,4 @@ let bind_payload_opt analysis_data ~f =
     analyze_dependency=
       (fun ?specialization proc_name ->
         analysis_data.analyze_dependency ?specialization proc_name
-        |> Result.bind ~f:(fun payload ->
-               f payload |> Result.of_option ~error:AnalysisResult.AnalysisFailed ) ) }
+        |> Result.bind ~f:(fun payload -> f payload |> AnalysisResult.of_option) ) }

infer/src/backend/CallbackOfChecker.ml

@@ -11,15 +11,13 @@ open! IStd
    crash) *)
 let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session}
 
-let analysis_result_of_option opt = Result.of_option opt ~error:AnalysisResult.AnalysisFailed
-
 let mk_interprocedural_t analysis_req ~f_analyze_dep ~get_payload
     {Callbacks.exe_env; proc_desc; summary= {Summary.stats; proc_name; err_log} as caller_summary}
     ?(tenv = Exe_env.get_proc_tenv exe_env proc_name) () =
   let analyze_dependency ?specialization proc_name =
     Ondemand.analyze_proc_name exe_env analysis_req ?specialization ~caller_summary proc_name
     |> Result.bind ~f:(fun {Summary.payloads} ->
-           f_analyze_dep (get_payload payloads) |> analysis_result_of_option )
+           f_analyze_dep (get_payload payloads) |> AnalysisResult.of_option )
   in
   let stats = ref stats in
   let update_stats ?add_symops ?failure_kind () =
@@ -98,7 +96,7 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s
       (Payloads.analysis_request_of_field payload_field)
       proc_name
     |> Result.bind ~f:(fun {Summary.payloads; _} ->
-           Field.get payload_field payloads |> ILazy.force_option |> analysis_result_of_option )
+           Field.get payload_field payloads |> ILazy.force_option |> AnalysisResult.of_option )
   in
   checker
     {InterproceduralAnalysis.procedures; source_file; file_exe_env= exe_env; analyze_file_dependency}

infer/src/backend/ondemand.ml

@@ -427,8 +427,6 @@ let double_lock_for_restart ~lazy_payloads analysis_req callee_pname specializat
         `NoSummary )
 
 
-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 = DLS.new_key (fun () -> 0)
@@ -520,15 +518,15 @@ let rec analyze_callee_can_raise_recursion exe_env ~lazy_payloads (analysis_req
         | `SummaryReady summary ->
             Ok summary
         | `ComputeDefaultSummary ->
-            analyze_callee_aux None |> analysis_result_of_option
+            analyze_callee_aux None |> AnalysisResult.of_option
         | `ComputeDefaultSummaryThenSpecialize specialization ->
             (* recursive call so that we detect mutual recursion on the unspecialized summary *)
             analyze_callee exe_env ~lazy_payloads analysis_req ~specialization:None ?caller_summary
               ~from_file_analysis callee_pname
             |> Result.bind ~f:(fun summary ->
-                   analyze_callee_aux (Some (summary, specialization)) |> analysis_result_of_option )
+                   analyze_callee_aux (Some (summary, specialization)) |> AnalysisResult.of_option )
         | `AddNewSpecialization (summary, specialization) ->
-            analyze_callee_aux (Some (summary, specialization)) |> analysis_result_of_option
+            analyze_callee_aux (Some (summary, specialization)) |> AnalysisResult.of_option
         | `UnknownProcedure ->
             Error UnknownProcedure )
 
@@ -541,7 +539,7 @@ and on_recursive_cycle exe_env ~lazy_payloads analysis_req ?caller_summary:_ ?fr
     ?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
+  Summary.OnDisk.get ~lazy_payloads analysis_req callee_pname |> AnalysisResult.of_option
 
 
 and analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_summary

infer/src/pulse/PulseCallOperations.ml

@@ -947,9 +947,8 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
                            exec_state ) )
                 in
                 case_if_specialization_is_impossible res
-            | Error ((AnalysisFailed | InBlockList | UnknownProcedure) as no_summary) ->
-                L.die InternalError "No summary found by specialization: %a"
-                  AnalysisResult.pp_no_summary no_summary
+            | Error (AnalysisFailed | InBlockList | UnknownProcedure) ->
+                case_if_specialization_is_impossible res
             | Ok (summary, is_pulse_specialization_limit_not_reached) ->
                 let already_given = Specialization.Pulse.Set.add specialization already_given in
                 iter_call ~max_iteration ~nth_iteration:(nth_iteration + 1)