diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index a7a6a3290..8a8e2da66 100644 --- a/infer/src/backend/interproc.ml +++ b/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 = diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 6f0c7520f..0c7a379d6 100644 --- a/infer/src/backend/specs.ml +++ b/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 = diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 253df11ea..f325042aa 100644 --- a/infer/src/backend/specs.mli +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 9697ee2db..3be7a0b42 100644 --- a/infer/src/backend/symExec.ml +++ b/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 diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 7196a43da..4a97e0bd2 100644 --- a/infer/src/backend/tabulation.ml +++ b/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))