[biabduction] specialise java models without non-determinism

Summary:
Dynamic dispatch in java requires specialisation of models. Models do not have a CFG, nor attributes, in the capture DB, so the solution til now was to get those from the summary of the model.

Each code path (CFG, attributes) could introduce non-determinism by allowing summaries to mask functions in the capture DB, and doing so depending on race conditions of the analysis (whether a summary has been written or not), as well as by the fact that CFGs from the capture DB are not pre-analysed, while summary CFGs are.

This diff eliminates both code path usages in specialisation by strictly separating functions into captured functions and models. Other summaries are never consulted, and thus cannot introduce non-determinism through timing.

NB model specialisation for clang models has been disabled in the past.

Reviewed By: da319

Differential Revision: D29915082

fbshipit-source-id: 313a60e17

infer/src/absint/AnalysisCallbacks.ml

@@ -9,11 +9,10 @@ open! IStd
 module L = Logging
 
 type callbacks =
-  { get_proc_desc_f: Procname.t -> Procdesc.t option
+  { html_debug_new_node_session_f:
-  ; html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
-  ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }
+  ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
 
 let callbacks_ref : callbacks option ref = ref None
 
@@ -27,10 +26,8 @@ let get_callbacks () =
       L.die InternalError "Callbacks not set"
 
 
-let get_proc_desc proc_name = (get_callbacks ()).get_proc_desc_f proc_name
-
 let html_debug_new_node_session ?kind ~pp_name node ~f =
   (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f
 
 
-let proc_resolve_attributes proc_name = (get_callbacks ()).proc_resolve_attributes_f proc_name
+let get_model_proc_desc proc_name = (get_callbacks ()).get_model_proc_desc_f proc_name

infer/src/absint/AnalysisCallbacks.mli

@@ -9,8 +9,8 @@ open! IStd
 
 (** {2 Analysis API} *)
 
-val get_proc_desc : Procname.t -> Procdesc.t option
+val get_model_proc_desc : Procname.t -> Procdesc.t option
-(** set to [Ondemand.get_proc_desc] *)
+(** get the preanalysed procdesc of a model; raises if procname given is not a biabduction model *)
 
 val html_debug_new_node_session :
      ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
@@ -20,20 +20,16 @@ val html_debug_new_node_session :
   -> 'a
 (** set to [NodePrinter.with_session] *)
 
-val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
-(** set to [Summary.OnDisk.proc_resolve_attributes] *)
-
 (** {2 Callbacks management}*)
 
 (** These callbacks are used to break the dependency cycles between some modules. Specifically, we
     put here functions needed for the analysis that depend on modules higher up the dependency graph
     than this library but whose type does not. *)
 type callbacks =
-  { get_proc_desc_f: Procname.t -> Procdesc.t option
+  { html_debug_new_node_session_f:
-  ; html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
-  ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }
+  ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
 
 val set_callbacks : callbacks -> unit
 (** make sure this is called before starting any actual analysis *)

infer/src/backend/CallbackOfChecker.ml

@@ -11,9 +11,8 @@ open! IStd
    crash) *)
 let () =
   AnalysisCallbacks.set_callbacks
-    { get_proc_desc_f= Ondemand.get_proc_desc
+    { html_debug_new_node_session_f= NodePrinter.with_session
-    ; html_debug_new_node_session_f= NodePrinter.with_session
+    ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc }
-    ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes }
 
 
 let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary

infer/src/backend/Summary.ml

@@ -261,6 +261,13 @@ module OnDisk = struct
         load_summary_to_spec_table proc_name
 
 
+  let get_model_proc_desc model_name =
+    if not (BiabductionModels.mem model_name) then
+      Logging.die InternalError "Requested summary of model that couldn't be found: %a@\n"
+        Procname.pp model_name
+    else Option.map (get model_name) ~f:(fun (s : full_summary) -> s.proc_desc)
+
+
   (** Try to find the attributes for a defined proc. First look at specs (to get attributes computed
       by analysis) then look at the attributes table. If no attributes can be found, return None. *)
   let proc_resolve_attributes proc_name =

infer/src/backend/Summary.mli

@@ -99,4 +99,6 @@ module OnDisk : sig
 
   val pp_specs_from_config : Format.formatter -> unit
   (** pretty print all stored summaries *)
+
+  val get_model_proc_desc : Procname.t -> Procdesc.t option
 end

infer/src/backend/ondemand.mli

@@ -9,9 +9,6 @@ open! IStd
 
 (** Module for on-demand analysis. *)
 
-val get_proc_desc : Procname.t -> Procdesc.t option
-(** Find a proc desc for the procedure, perhaps loading it from disk. *)
-
 val analyze_proc_name : Exe_env.t -> caller_summary:Summary.t -> Procname.t -> Summary.t option
 (** [analyze_proc_name exe_env ~caller_summary callee_pname] performs an on-demand analysis of
     [callee_pname] triggered during the analysis of [caller_summary] *)

infer/src/biabduction/SymExec.ml

@@ -590,6 +590,17 @@ type resolve_and_analyze_result =
   ; resolved_procdesc_opt: Procdesc.t option
   ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option }
 
+let get_proc_desc proc_name =
+  if BiabductionModels.mem proc_name then AnalysisCallbacks.get_model_proc_desc proc_name
+  else Procdesc.load proc_name
+
+
+let get_attributes proc_name =
+  if BiabductionModels.mem proc_name then
+    AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes
+  else Attributes.load proc_name
+
+
 (** Resolve the procedure name and run the analysis of the resolved procedure if not already
     analyzed *)
 let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv}
@@ -601,15 +612,15 @@ let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc;
        whether the method is defined or generated by the specialization *)
     let analyze_ondemand resolved_pname =
       if Procname.equal resolved_pname callee_proc_name then
-        (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name)
+        (get_proc_desc callee_proc_name, analyze_dependency callee_proc_name)
       else
         (* Create the type specialized procedure description and analyze it directly *)
         let resolved_proc_desc_option =
-          match AnalysisCallbacks.get_proc_desc resolved_pname with
+          match get_proc_desc resolved_pname with
           | Some _ as resolved_proc_desc ->
               resolved_proc_desc
           | None ->
-              let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in
+              let procdesc_opt = get_proc_desc callee_proc_name in
               Option.map procdesc_opt ~f:(fun callee_proc_desc ->
                   (* It is possible that the types of the arguments are not as precise as the type of
                      the objects in the heap, so we should update them to get the best results. *)
@@ -988,7 +999,7 @@ let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv;
 
 
 let is_variadic_procname callee_pname =
-  Option.exists (AnalysisCallbacks.proc_resolve_attributes callee_pname) ~f:(fun proc_attrs ->
+  Option.exists (get_attributes callee_pname) ~f:(fun proc_attrs ->
       proc_attrs.ProcAttributes.is_variadic )
 
 
@@ -1002,9 +1013,7 @@ let resolve_and_analyze_no_dynamic_dispatch {InterproceduralAnalysis.analyze_dep
         callee_pname
   in
   let resolved_summary_opt = analyze_dependency resolved_pname in
-  { resolved_pname
+  {resolved_pname; resolved_procdesc_opt= get_proc_desc resolved_pname; resolved_summary_opt}
-  ; resolved_procdesc_opt= AnalysisCallbacks.get_proc_desc resolved_pname
-  ; resolved_summary_opt }
 
 
 let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname call_flags =
@@ -1556,9 +1565,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
         callee_pname ret_annots loc path_pos
     in
     let callee_loc_opt =
-      Option.map
+      Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (get_attributes callee_pname)
-        ~f:(fun attributes -> attributes.ProcAttributes.loc)
-        (AnalysisCallbacks.proc_resolve_attributes callee_pname)
     in
     let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in
     [(prop_with_undef_attr, skip_path)]
@@ -1600,7 +1607,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po
 
 
 and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as builtin_args) =
-  match AnalysisCallbacks.proc_resolve_attributes proc_name with
+  match get_attributes proc_name with
   | Some callee_attributes -> (
     match callee_attributes.ProcAttributes.sentinel_attr with
     | Some sentinel ->

infer/src/biabduction/Tabulation.ml

@@ -745,9 +745,15 @@ let prop_set_exn tenv pname prop se_exn =
   Prop.normalize tenv (Prop.set prop ~sigma:sigma')
 
 
+let get_attributes proc_name =
+  if BiabductionModels.mem proc_name then
+    AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes
+  else Attributes.load proc_name
+
+
 (** Include a subtrace for a procedure call if the callee is not a model. *)
 let include_subtrace callee_pname =
-  match AnalysisCallbacks.proc_resolve_attributes callee_pname with
+  match get_attributes callee_pname with
   | Some attrs ->
       (not attrs.ProcAttributes.is_biabduction_model)
       && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file

infer/src/unit/analyzerTester.ml

@@ -300,9 +300,8 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) =
 
   let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests =
     AnalysisCallbacks.set_callbacks
-      { get_proc_desc_f= Ondemand.get_proc_desc
+      { html_debug_new_node_session_f= NodePrinter.with_session
-      ; html_debug_new_node_session_f= NodePrinter.with_session
+      ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } ;
-      ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } ;
     let open OUnit2 in
     List.concat_map
       ~f:(fun (name, test_program) ->