diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 37986b0aa..a41748ee7 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -545,6 +545,16 @@ let get_ret_var pdesc = Pvar.get_ret_pvar (get_proc_name pdesc) let get_ret_param_var pdesc = Pvar.get_ret_param_pvar (get_proc_name pdesc) +let get_ret_type_from_signature pdesc = + if pdesc.attributes.has_added_return_param then + List.last pdesc.attributes.formals + |> Option.value_map + ~f:(fun (_, typ) -> + match typ.Typ.desc with Tptr (t, _) -> t | _ -> pdesc.attributes.ret_type ) + ~default:pdesc.attributes.ret_type + else pdesc.attributes.ret_type + + let get_start_node pdesc = pdesc.start_node (** Return [true] iff the procedure is defined, and not just declared *) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 6e2c00cf4..3f07f47e9 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -271,6 +271,10 @@ val get_ret_var : t -> Pvar.t val get_ret_param_var : t -> Pvar.t +val get_ret_type_from_signature : t -> Typ.t +(** Return the return type from method signature: if the procedure has added return parameter, + return its type *) + val get_start_node : t -> Node.t val get_static_callees : t -> Procname.t list diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index e6f1380ed..1a58bc810 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -57,7 +57,8 @@ let immediate_or_first_call calling_context (trace : Trace.t) = let get_message diagnostic = let pulse_start_msg = "Pulse found a potential" in match diagnostic with - | AccessToInvalidAddress {calling_context; invalidation; invalidation_trace; access_trace} -> ( + | AccessToInvalidAddress + {calling_context; invalidation; invalidation_trace; access_trace; must_be_valid_reason} -> ( let invalidation, invalidation_trace = Trace.get_invalidation access_trace |> Option.value_map @@ -67,6 +68,14 @@ let get_message diagnostic = match invalidation with | ConstantDereference i when IntLit.equal i IntLit.zero -> (* Special error message for nullptr dereference *) + let issue_kind_str = + match must_be_valid_reason with + | Some (Invalidation.SelfOfNonPODReturnMethod non_pod_typ) -> + F.asprintf "undefined behaviour caused by nil messaging of non-pod return type (%a)" + (Typ.pp Pp.text) non_pod_typ + | _ -> + F.sprintf "null pointer dereference" + in let pp_access_trace fmt (trace : Trace.t) = match immediate_or_first_call calling_context trace with | `Immediate -> @@ -78,10 +87,10 @@ let get_message diagnostic = let pp_line fmt line = F.fprintf fmt "on line %d" line in match immediate_or_first_call calling_context trace with | `Immediate -> - F.fprintf fmt "null pointer dereference %a" pp_line line + F.fprintf fmt "%s %a" issue_kind_str pp_line line | `Call f -> - F.fprintf fmt "null pointer dereference %a indirectly during the call to %a" pp_line - line CallEvent.describe f + F.fprintf fmt "%s %a indirectly during the call to %a" issue_kind_str pp_line line + CallEvent.describe f in let invalidation_line = let {Location.line; _} = Trace.get_outer_location invalidation_trace in diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index e53c4821c..2a165f3c0 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -52,7 +52,10 @@ type t = | JavaIterator of java_iterator_function [@@deriving compare, equal] -type must_be_valid_reason = BlockCall | InsertionIntoCollection | SelfOfNonPODReturnMethod +type must_be_valid_reason = + | BlockCall + | InsertionIntoCollection + | SelfOfNonPODReturnMethod of Typ.t [@@deriving compare, equal] let pp_must_be_valid_reason f = function @@ -62,7 +65,7 @@ let pp_must_be_valid_reason f = function F.fprintf f "Block" | Some InsertionIntoCollection -> F.fprintf f "InsertionIntoCollection" - | Some SelfOfNonPODReturnMethod -> + | Some (SelfOfNonPODReturnMethod _) -> F.fprintf f "SelfOfNonPODReturnMethod" @@ -78,7 +81,7 @@ let issue_type_of_cause invalidation must_be_valid_reason = IssueType.nil_block_call | Some InsertionIntoCollection -> IssueType.nil_insertion_into_collection - | Some SelfOfNonPODReturnMethod -> + | Some (SelfOfNonPODReturnMethod _) -> IssueType.nil_messaging_to_non_pod ) | ConstantDereference _ -> IssueType.constant_address_dereference diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 7db7a45e7..554d6974d 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -40,7 +40,10 @@ val pp : F.formatter -> t -> unit val describe : F.formatter -> t -> unit -type must_be_valid_reason = BlockCall | InsertionIntoCollection | SelfOfNonPODReturnMethod +type must_be_valid_reason = + | BlockCall + | InsertionIntoCollection + | SelfOfNonPODReturnMethod of Typ.t [@@deriving compare, equal] val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 9c157d803..07b0dfbeb 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -126,8 +126,9 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo let result = (* add reason for must be valid to be because the return type is non pod *) let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in - AddressAttributes.replace_must_be_valid_reason path SelfOfNonPODReturnMethod (fst value) - astate + AddressAttributes.replace_must_be_valid_reason path + (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc)) + (fst value) astate in PulseReport.report_result tenv proc_desc err_log location result | ContinueProgram _, _