[infer][backend] More functions from the Specs module taking a summary as parameter

Summary: These functions are also called when the summary is guaranteed to exist. Enforcing this within the API

Reviewed By: cristianoc

Differential Revision: D4126839

fbshipit-source-id: 305b484

infer/src/backend/interproc.ml

@@ -529,9 +529,9 @@ let forward_tabulate tenv pdesc wl source =
 
   let print_node_preamble curr_node session pathset_todo =
     let log_string proc_name =
-      let phase_string =
-        if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE" in
       let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
+      let phase_string =
+        if Specs.get_phase summary == Specs.FOOTPRINT then "FP" else "RE" in
       let timestamp = Specs.get_timestamp summary in
       F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in
     L.d_strln ("**** " ^ (log_string pname) ^ " " ^
@@ -987,10 +987,10 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p
     [go ()] was interrupted by and exception. *)
 let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) source
   : exe_phase =
+  let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
   let start_node = Cfg.Procdesc.get_start_node pdesc in
 
   let check_recursion_level () =
-    let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
     let recursion_level = Specs.get_timestamp summary in
     if recursion_level > Config.max_recursion then
       begin
@@ -1097,7 +1097,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
       specs, Specs.RE_EXECUTION in
     go, get_results in
 
-  match Specs.get_phase pname with
+  match Specs.get_phase summary with
   | Specs.FOOTPRINT ->
       compute_footprint ()
   | Specs.RE_EXECUTION ->
@@ -1394,8 +1394,10 @@ let perform_transition exe_env tenv proc_name source =
         L.err "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt;
         [] in
     transition_footprint_re_exe tenv proc_name joined_pres in
-  if Specs.get_phase proc_name == Specs.FOOTPRINT
-  then transition ()
+  match Specs.get_summary proc_name with
+  | Some summary when Specs.get_phase summary == Specs.FOOTPRINT ->
+      transition ()
+  | _ -> ()
 
 
 let interprocedural_algorithm exe_env : unit =

infer/src/backend/specs.ml

@@ -675,10 +675,10 @@ let pdesc_resolve_attributes proc_desc =
       (* this should not happen *)
       assert false
 
-let get_origin proc_name =
+let is_model proc_name =
   match get_summary_origin proc_name with
-  | Some (_, origin) -> origin
-  | None -> DB.Res_dir
+  | None -> false
+  | Some (_, origin) -> origin = DB.Models
 
 let summary_exists proc_name =
   match get_summary proc_name with
@@ -707,15 +707,11 @@ let get_attributes summary =
   summary.attributes
 
 (** Get the flag with the given key for the procedure, if any *)
-(* TODO get_flag should get a summary as parameter *)
-let get_flag proc_name key =
-  match get_summary proc_name with
-  | None -> None
-  | Some summary ->
-      let proc_flags = summary.attributes.ProcAttributes.proc_flags in
-      try
-        Some (Hashtbl.find proc_flags key)
-      with Not_found -> None
+let get_flag summary key =
+  let proc_flags = summary.attributes.ProcAttributes.proc_flags in
+  try
+    Some (Hashtbl.find proc_flags key)
+  with Not_found -> None
 
 (** Return the specs and parameters for the proc in the spec table *)
 let get_specs_formals proc_name =
@@ -732,10 +728,8 @@ let get_specs proc_name =
   fst (get_specs_formals proc_name)
 
 (** Return the current phase for the proc *)
-let get_phase proc_name =
-  match get_summary_origin proc_name with
-  | None -> raise (Failure ("Specs.get_phase: " ^ (Procname.to_string proc_name) ^ " Not_found"))
-  | Some (summary, _) -> summary.phase
+let get_phase summary =
+  summary.phase
 
 (** Set the current status for the proc *)
 let set_status proc_name status =

infer/src/backend/specs.mli

@@ -159,6 +159,12 @@ val clear_spec_tbl : unit -> unit
 (** Dump a spec *)
 val d_spec : 'a spec -> unit
 
+(** Returns true if the procedure is a model *)
+val is_model: Procname.t -> bool
+
+(** Return the summary option for the procedure name *)
+val get_summary : Procname.t -> summary option
+
 (** Get the procedure name *)
 val get_proc_name : summary -> Procname.t
 
@@ -172,13 +178,10 @@ val get_ret_type : summary -> Typ.t
 val get_formals : summary -> (Mangled.t * Typ.t) list
 
 (** Get the flag with the given key for the procedure, if any *)
-val get_flag : Procname.t -> string -> string option
+val get_flag : summary -> string -> string option
 
 (** Return the current phase for the proc *)
-val get_phase : Procname.t -> phase
-
-(** Return the origin of the spec file *)
-val get_origin: Procname.t -> DB.origin
+val get_phase : summary -> phase
 
 (** Return the signature of a procedure declaration as a string *)
 val get_signature : summary -> string
@@ -192,9 +195,6 @@ val get_specs_formals : Procname.t -> Prop.normal spec list * (Mangled.t * Typ.t
 (** Get the specs from the payload of the summary. *)
 val get_specs_from_payload : summary -> Prop.normal spec list
 
-(** Return the summary option for the procedure name *)
-val get_summary : Procname.t -> summary option
-
 (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *)
 val get_summary_unsafe : string -> Procname.t -> summary
 

infer/src/backend/symExec.ml

@@ -375,13 +375,13 @@ let check_inherently_dangerous_function caller_pname callee_pname =
         (Localise.desc_inherently_dangerous_function callee_pname) in
     Reporting.log_warning caller_pname exn
 
-let call_should_be_skipped callee_pname summary =
+let call_should_be_skipped callee_summary =
   (* check skip flag *)
-  Specs.get_flag callee_pname proc_flag_skip <> None
+  Specs.get_flag callee_summary proc_flag_skip <> None
   (* skip abstract methods *)
-  || summary.Specs.attributes.ProcAttributes.is_abstract
+  || callee_summary.Specs.attributes.ProcAttributes.is_abstract
   (* treat calls with no specs as skip functions in angelic mode *)
-  || (Config.angelic_execution && Specs.get_specs_from_payload summary == [])
+  || (Config.angelic_execution && Specs.get_specs_from_payload callee_summary == [])
 
 (** In case of constant string dereference, return the result immediately *)
 let check_constant_string_dereference lexp =
@@ -1067,20 +1067,20 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               let exec_skip_call skipped_pname ret_annots ret_type =
                 skip_call norm_prop path skipped_pname ret_annots loc ret_id
                   (Some ret_type) norm_args in
-              let resolved_pname, summary_opt = resolve_and_analyze tenv current_pdesc
+              let resolved_pname, resolved_summary_opt = resolve_and_analyze tenv current_pdesc
                   norm_prop norm_args callee_pname call_flags in
               begin
-                match summary_opt with
+                match resolved_summary_opt with
                 | None ->
                     let ret_typ = Typ.java_proc_return_typ callee_pname_java in
                     let ret_annots = load_ret_annots callee_pname in
                     exec_skip_call resolved_pname ret_annots ret_typ
-                | Some summary when call_should_be_skipped resolved_pname summary ->
-                    let proc_attrs = summary.Specs.attributes in
+                | Some resolved_summary when call_should_be_skipped resolved_summary ->
+                    let proc_attrs = resolved_summary.Specs.attributes in
                     let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                     exec_skip_call resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
-                | Some summary ->
-                    proc_call summary (call_args prop_ callee_pname norm_args ret_id loc)
+                | Some resolved_summary ->
+                    proc_call resolved_summary (call_args prop_ callee_pname norm_args ret_id loc)
               end
           | Java callee_pname_java ->
               do_error_checks tenv (Paths.Path.curr_node path) instr current_pname current_pdesc;
@@ -1098,12 +1098,13 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                     let ret_typ = Typ.java_proc_return_typ callee_pname_java in
                     let ret_annots = load_ret_annots callee_pname in
                     exec_skip_call ret_annots ret_typ
-                | Some summary when call_should_be_skipped pname summary ->
-                    let proc_attrs = summary.Specs.attributes in
+                | Some callee_summary when call_should_be_skipped callee_summary ->
+                    let proc_attrs = callee_summary.Specs.attributes in
                     let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                     exec_skip_call ret_annots proc_attrs.ProcAttributes.ret_type
-                | Some summary ->
-                    proc_call summary (call_args norm_prop pname url_handled_args ret_id loc) in
+                | Some callee_summary ->
+                    let handled_args = call_args norm_prop pname url_handled_args ret_id loc in
+                    proc_call callee_summary handled_args in
               IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames
           | _ -> (* Generic fun call with known name *)
               let (prop_r, n_actual_params) =
@@ -1122,12 +1123,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                     (call_args prop_r callee_pname actual_params ret_id loc)
                 else [(prop_r, path)] in
               let do_call (prop, path) =
-                let summary = Specs.get_summary resolved_pname in
-                let should_skip resolved_pname summary =
-                  match summary with
-                  | None -> true
-                  | Some summary -> call_should_be_skipped resolved_pname summary in
-                if should_skip resolved_pname summary then
+                let resolved_summary_opt = Specs.get_summary resolved_pname in
+                if Option.map_default call_should_be_skipped true resolved_summary_opt then
                   (* If it's an ObjC getter or setter, call the builtin rather than skipping *)
                   let attrs_opt =
                     let attr_opt = Option.map Cfg.Procdesc.get_attributes callee_pdesc_opt in
@@ -1149,7 +1146,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                         current_pdesc callee_pname loc path
                         (sym_exec_objc_accessor objc_property_accessor ret_typ)
                   | None ->
-                      let ret_annots = match summary with
+                      let ret_annots = match resolved_summary_opt with
                         | Some summ ->
                             let ret_annots, _ =
                               summ.Specs.attributes.ProcAttributes.method_annotation in
@@ -1163,7 +1160,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                       skip_call ~is_objc_instance_method prop path resolved_pname ret_annots
                         loc ret_id ret_typ_opt n_actual_params
                 else
-                  proc_call (Option.get summary)
+                  proc_call (Option.get resolved_summary_opt)
                     (call_args prop resolved_pname n_actual_params ret_id loc) in
               IList.flatten (IList.map do_call sentinel_result)
         )
@@ -1540,7 +1537,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
       | _, None -> true
       | _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in
     if is_ignored
-    && Specs.get_flag callee_pname proc_flag_ignore_return = None then
+    && Specs.get_flag summary proc_flag_ignore_return = None then
       let err_desc = Localise.desc_return_value_ignored callee_pname loc in
       let exn = (Exceptions.Return_value_ignored (err_desc, __POS__)) in
       Reporting.log_warning caller_pname exn in

infer/src/backend/tabulation.ml

@@ -664,7 +664,7 @@ let prop_set_exn tenv pname prop se_exn =
 
 (** Include a subtrace for a procedure call if the callee is not a model. *)
 let include_subtrace callee_pname =
-  Specs.get_origin callee_pname <> DB.Models &&
+  not (Specs.is_model callee_pname) &&
   not (AttributesTable.pname_is_cpp_model callee_pname) &&
   not (AttributesTable.is_whitelisted_cpp_method (Procname.to_string callee_pname))