diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 22ccadece..7a3ea1f92 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -541,6 +541,7 @@ OPTIONS MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 851b6889d..f3b5826f0 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -218,6 +218,7 @@ OPTIONS MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 0c81d300f..3d7a1ae49 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -541,6 +541,7 @@ OPTIONS MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NIL_MESSAGING_TO_NON_POD (disabled by default), NULLPTR_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), OPTIONAL_EMPTY_ACCESS (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index a7ef49cb1..2c924f8de 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -799,6 +799,11 @@ let nullptr_dereference = ~user_documentation:[%blob "../../documentation/issues/NULLPTR_DEREFERENCE.md"] +let nil_messaging_to_non_pod = + register ~enabled:false ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse + ~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)." + + let optional_empty_access = register ~id:"OPTIONAL_EMPTY_ACCESS" Error Pulse ~user_documentation:[%blob "../../documentation/issues/OPTIONAL_EMPTY_ACCESS.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 0dd06689a..f93edf6e9 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -276,6 +276,8 @@ val multiple_weakself : t val mutable_local_variable_in_component_file : t +val nil_messaging_to_non_pod : t + val null_dereference : t val nullptr_dereference : t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index ccc9a1c58..b99f60ffb 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -163,7 +163,8 @@ module Stack = struct let post_attrs = if Config.pulse_isl then let access_trace = Trace.Immediate {location; history= []} in - BaseAddressAttributes.add_one addr (MustBeValid access_trace) + BaseAddressAttributes.add_one addr + (MustBeValid (access_trace, None)) (astate.post :> base_domain).attrs else (astate.post :> base_domain).attrs in @@ -242,7 +243,7 @@ module AddressAttributes = struct let check_valid access_trace addr astate = let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *) - abduce_attribute addr (MustBeValid access_trace) astate + abduce_attribute addr (MustBeValid (access_trace, None)) astate let check_initialized access_trace addr astate = @@ -312,6 +313,14 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.mark_as_end_of_collection addr) + let replace_must_be_valid_reason reason addr astate = + match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with + | Some (trace, _reason) -> + abduce_attribute addr (MustBeValid (trace, Some reason)) astate + | None -> + astate + + let is_end_of_collection addr astate = BaseAddressAttributes.is_end_of_collection addr (astate.post :> base_domain).attrs @@ -353,7 +362,7 @@ module AddressAttributes = struct BaseAddressAttributes.get_must_be_valid_or_allocated_isl addr (astate.post :> BaseDomain.t).attrs with - | None -> + | None, reason -> let null_astates = if PathCondition.is_known_not_equal_zero astate.path_condition addr then [] else @@ -369,7 +378,7 @@ module AddressAttributes = struct else let valid_astate = let abdalloc = Attribute.ISLAbduced access_trace in - let valid_attr = Attribute.MustBeValid access_trace in + let valid_attr = Attribute.MustBeValid (access_trace, reason) in add_one addr abdalloc astate |> abduce_attribute addr valid_attr |> abduce_attribute addr abdalloc in @@ -381,7 +390,7 @@ module AddressAttributes = struct [Ok valid_astate; Error (`ISLError invalid_free)] in not_null_astates @ null_astates - | Some _ -> + | Some _, _ -> [Ok astate] ) | Some (invalidation, invalidation_trace) -> [Error (`InvalidAccess (invalidation, invalidation_trace, astate))] @@ -457,7 +466,9 @@ let rec set_uninitialized_post tenv src typ location ?(fields_prefix = RevList.e let stack, addr = add_edge_on_src src location stack in let attrs = if Config.pulse_isl then - BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs + BaseAddressAttributes.add_one addr + (MustBeValid (Immediate {location; history= []}, None)) + attrs else attrs in let attrs = BaseAddressAttributes.add_one addr Uninitialized attrs in @@ -541,7 +552,9 @@ let mk_initial tenv proc_desc = if Config.pulse_isl then List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs ~f:(fun attrs (_, _, (addr, _)) -> - BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs ) + BaseAddressAttributes.add_one addr + (MustBeValid (Immediate {location; history= []}, None)) + attrs ) else (PreDomain.empty :> base_domain).attrs in let pre = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index d92eea3de..f41cb9e16 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -141,6 +141,8 @@ module AddressAttributes : sig val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + val replace_must_be_valid_reason : Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t + val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t @@ -190,7 +192,10 @@ val summary_of_post : Tenv.t -> Procdesc.t -> t - -> (summary, [> `PotentialInvalidAccessSummary of summary * AbstractValue.t * Trace.t]) result + -> ( summary + , [> `PotentialInvalidAccessSummary of + summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] ) + result SatUnsat.t (** trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state *) @@ -204,7 +209,10 @@ val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Locat val incorporate_new_eqs : PathCondition.new_eqs -> t - -> (t, [> `PotentialInvalidAccess of t * AbstractValue.t * Trace.t]) result + -> ( t + , [> `PotentialInvalidAccess of + t * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] ) + result (** Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x] and [y] being allocated separately. In those cases, the resulting path condition is diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml index cf810b266..5cae8a51e 100644 --- a/infer/src/pulse/PulseAccessResult.ml +++ b/infer/src/pulse/PulseAccessResult.ml @@ -10,9 +10,14 @@ open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain type 'astate error = - | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccess of + { astate: 'astate + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | PotentialInvalidAccessSummary of - {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate @@ -22,8 +27,11 @@ type 'a t = ('a, AbductiveDomain.t) base_t type 'astate abductive_error = [ `ISLError of 'astate - | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t - | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ] + | `PotentialInvalidAccess of + 'astate * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) + | `PotentialInvalidAccessSummary of + AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) + ] let of_abductive_error = function | `ISLError astate -> @@ -43,6 +51,10 @@ let of_abductive_access_result access_trace abductive_result = { astate ; diagnostic= AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} } + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace + ; must_be_valid_reason= None } } | (`ISLError _ | `PotentialInvalidAccess _ | `PotentialInvalidAccessSummary _) as error -> of_abductive_error error ) diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli index 0784f954f..08839c87e 100644 --- a/infer/src/pulse/PulseAccessResult.mli +++ b/infer/src/pulse/PulseAccessResult.mli @@ -10,9 +10,14 @@ open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain type 'astate error = - | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccess of + { astate: 'astate + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | PotentialInvalidAccessSummary of - {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate @@ -24,8 +29,11 @@ type 'a t = ('a, AbductiveDomain.t) base_t circular dependency. *) type 'astate abductive_error = [ `ISLError of 'astate - | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t - | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ] + | `PotentialInvalidAccess of + 'astate * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) + | `PotentialInvalidAccessSummary of + AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) + ] val of_abductive_error : 'astate abductive_error -> 'astate error diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 77edc9c78..3c6fd5a91 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -34,7 +34,7 @@ module Attribute = struct | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t | MustBeInitialized of Trace.t - | MustBeValid of Trace.t + | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized | WrittenTo of Trace.t @@ -63,7 +63,7 @@ module Attribute = struct Variants.to_rank (Invalid (Invalidation.ConstantDereference IntLit.zero, dummy_trace)) - let must_be_valid_rank = Variants.to_rank (MustBeValid dummy_trace) + let must_be_valid_rank = Variants.to_rank (MustBeValid (dummy_trace, None)) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve @@ -125,8 +125,10 @@ module Attribute = struct F.fprintf f "MustBeInitialized %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "read")) trace - | MustBeValid trace -> - F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace + | MustBeValid (trace, reason) -> + F.fprintf f "MustBeValid %a (%a)" + (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) + trace Invalidation.pp_must_be_valid_reason reason | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" | Uninitialized -> @@ -148,8 +150,8 @@ module Attributes = struct let get_must_be_valid attrs = Set.find_rank attrs Attribute.must_be_valid_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.MustBeValid action) = attr in - action ) + let[@warning "-8"] (Attribute.MustBeValid (trace, reason)) = attr in + (trace, reason) ) let get_written_to attrs = @@ -294,8 +296,8 @@ let map_trace ~f = function ISLAbduced (f trace) | Invalid (invalidation, trace) -> Invalid (invalidation, f trace) - | MustBeValid trace -> - MustBeValid (f trace) + | MustBeValid (trace, reason) -> + MustBeValid (f trace, reason) | WrittenTo trace -> WrittenTo (f trace) | MustBeInitialized trace -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 614c64779..818716550 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -21,7 +21,7 @@ type t = | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t (** The allocation is abduced so as the analysis could run normally *) | MustBeInitialized of Trace.t - | MustBeValid of Trace.t + | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized | WrittenTo of Trace.t @@ -53,7 +53,7 @@ module Attributes : sig val get_isl_abduced : t -> Trace.t option - val get_must_be_valid : t -> Trace.t option + val get_must_be_valid : t -> (Trace.t * Invalidation.must_be_valid_reason option) option val get_written_to : t -> Trace.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 3075bc19e..8aba651d6 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -116,8 +116,8 @@ let remove_isl_abduced_attr address memory = let remove_must_be_valid_attr address memory = match get_attribute Attributes.get_must_be_valid address memory with - | Some trace -> - remove_one address (Attribute.MustBeValid trace) memory + | Some (trace, reason) -> + remove_one address (Attribute.MustBeValid (trace, reason)) memory | None -> memory @@ -136,14 +136,14 @@ let get_must_be_valid = get_attribute Attributes.get_must_be_valid let get_must_be_valid_or_allocated_isl address attrs = match get_must_be_valid address attrs with - | Some trace -> - Some trace + | Some (trace, reason) -> + (Some trace, reason) | None -> ( match get_attribute Attributes.get_allocation address attrs with | Some (_, trace) -> - Some trace + (Some trace, None) | None -> - get_attribute Attributes.get_isl_abduced address attrs ) + (get_attribute Attributes.get_isl_abduced address attrs, None) ) let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 800917f55..c9d71726b 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -37,9 +37,11 @@ val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option -val get_must_be_valid : AbstractValue.t -> t -> Trace.t option +val get_must_be_valid : + AbstractValue.t -> t -> (Trace.t * Invalidation.must_be_valid_reason option) option -val get_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> Trace.t option +val get_must_be_valid_or_allocated_isl : + AbstractValue.t -> t -> Trace.t option * Invalidation.must_be_valid_reason option val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index ce583b473..54c6b242e 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -173,7 +173,8 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state { calling_context ; invalidation ; invalidation_trace - ; access_trace= must_be_valid } + ; access_trace= fst must_be_valid + ; must_be_valid_reason= snd must_be_valid } ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) ) | ISLLatentMemoryError astate -> map_call_result ~is_isl_error_prepost:true diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 2002790a7..c905b32bb 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -16,7 +16,8 @@ type access_to_invalid_address = { calling_context: (CallEvent.t * Location.t) list ; invalidation: Invalidation.t ; invalidation_trace: Trace.t - ; access_trace: Trace.t } + ; access_trace: Trace.t + ; must_be_valid_reason: Invalidation.must_be_valid_reason option } [@@deriving compare, equal] type read_uninitialized_value = {calling_context: (CallEvent.t * Location.t) list; trace: Trace.t} @@ -257,8 +258,8 @@ let get_trace = function let get_issue_type = function - | AccessToInvalidAddress {invalidation; _} -> - Invalidation.issue_type_of_cause invalidation + | AccessToInvalidAddress {invalidation; must_be_valid_reason} -> + Invalidation.issue_type_of_cause invalidation must_be_valid_reason | MemoryLeak _ -> IssueType.pulse_memory_leak | ReadUninitializedValue _ -> diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 98d5df530..86e4146ed 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -21,7 +21,8 @@ type access_to_invalid_address = further assumptions *) ; access_trace: Trace.t (** assuming we are in the calling context, the trace leads to an access to the value - invalidated in [invalidation_trace] without further assumptions *) } + invalidated in [invalidation_trace] without further assumptions *) + ; must_be_valid_reason: Invalidation.must_be_valid_reason option } [@@deriving compare, equal, yojson_of] type read_uninitialized_value = diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 0b4057cc4..afe83e96a 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -23,7 +23,7 @@ type 'abductive_domain_t base_t = | LatentInvalidAccess of { astate: AbductiveDomain.summary ; address: AbstractValue.t - ; must_be_valid: (Trace.t[@yojson.opaque]) + ; must_be_valid: (Trace.t * Invalidation.must_be_valid_reason option[@yojson.opaque]) ; calling_context: ((CallEvent.t * Location.t) list[@yojson.opaque]) } | ISLLatentMemoryError of AbductiveDomain.summary [@@deriving equal, compare, yojson_of] diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index b880f3a2a..2a721ec32 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -21,7 +21,7 @@ type 'abductive_domain_t base_t = | LatentInvalidAccess of { astate: AbductiveDomain.summary ; address: AbstractValue.t - ; must_be_valid: Trace.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option ; calling_context: (CallEvent.t * Location.t) list } (** if [address] is ever observed to be invalid then there is an invalid access because it [must_be_valid] *) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index a23e089a1..736abe8dd 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -620,7 +620,7 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with | None -> astate_result - | Some callee_access_trace -> + | Some (callee_access_trace, must_be_valid_reason) -> let access_trace = mk_access_trace callee_access_trace in AddressAttributes.check_valid access_trace addr_caller astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> @@ -628,7 +628,11 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call AccessResult.ReportableError { diagnostic= Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace + ; must_be_valid_reason } ; astate } ) in match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with @@ -678,7 +682,11 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location (AccessResult.ReportableError { diagnostic= Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace + ; must_be_valid_reason= None } ; astate }) ) ) ) invalid_addr_callers (Ok astate) diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 07bb84ccb..401a6f408 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -52,11 +52,25 @@ type t = | JavaIterator of java_iterator_function [@@deriving compare, equal] -let issue_type_of_cause = function +type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal] + +let pp_must_be_valid_reason f = function + | None -> + F.fprintf f "None" + | Some SelfOfNonPODReturnMethod -> + F.fprintf f "SelfOfNonPODReturnMethod" + + +let issue_type_of_cause invalidation must_be_valid_reason = + match invalidation with | CFree -> IssueType.use_after_free - | ConstantDereference i when IntLit.iszero i -> - IssueType.nullptr_dereference + | ConstantDereference i when IntLit.iszero i -> ( + match must_be_valid_reason with + | None -> + IssueType.nullptr_dereference + | Some SelfOfNonPODReturnMethod -> + IssueType.nil_messaging_to_non_pod ) | ConstantDereference _ -> IssueType.constant_address_dereference | CppDelete -> diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index ed251346c..40ee97f07 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -38,6 +38,10 @@ val isl_equiv : t -> t -> bool val pp : F.formatter -> t -> unit -val issue_type_of_cause : t -> IssueType.t - val describe : F.formatter -> t -> unit + +type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal] + +val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit + +val issue_type_of_cause : t -> must_be_valid_reason option -> IssueType.t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 180e051cd..61bebb23f 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -681,7 +681,11 @@ module GenericArrayBackedCollectionIterator = struct (ReportableError { diagnostic= Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace} + { calling_context= [] + ; invalidation= EndIterator + ; invalidation_trace + ; access_trace + ; must_be_valid_reason= None } ; astate }) else Ok astate in diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 71e3dcd5c..4a4516395 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -8,6 +8,7 @@ open! IStd open PulseDomainInterface open PulseOperations.Import +open PulseBasicInterface let mk_objc_self_pvar proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in @@ -104,10 +105,38 @@ let append_objc_actual_self_positive procdesc self_actual astate = Ok astate +let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = + let location = Procdesc.get_loc proc_desc in + let self = mk_objc_self_pvar proc_desc in + let proc_name = Procdesc.get_proc_name proc_desc in + match (astate, proc_name) with + | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} + when not (Procdesc.is_ret_type_pod proc_desc) -> + let result = + (* add reason for must be valid to be because the return type is non pod *) + let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in + let astate = + AddressAttributes.replace_must_be_valid_reason Invalidation.SelfOfNonPODReturnMethod + (fst value) astate + in + astate + in + PulseReport.report_result tenv proc_desc err_log result + | ContinueProgram _, _ + | ExitProgram _, _ + | AbortProgram _, _ + | LatentAbortProgram _, _ + | LatentInvalidAccess _, _ + | ISLLatentMemoryError _, _ -> + [astate] + + let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ~initial_astate ~posts = - mk_objc_method_nil_summary tenv proc_desc initial_astate - |> Option.value_map ~default:posts ~f:(function result -> - let nil_summary = PulseReport.report_result tenv proc_desc err_log result in - let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in - nil_summary @ posts ) + match mk_objc_method_nil_summary tenv proc_desc initial_astate with + | None -> + List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts + | Some result -> + let nil_summary = PulseReport.report_result tenv proc_desc err_log result in + let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in + nil_summary @ posts diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 28ebf5983..06081e153 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -23,14 +23,19 @@ module Import = struct | LatentInvalidAccess of { astate: AbductiveDomain.summary ; address: AbstractValue.t - ; must_be_valid: Trace.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option ; calling_context: (CallEvent.t * Location.t) list } | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = - | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccess of + { astate: 'astate + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | PotentialInvalidAccessSummary of - {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate @@ -52,7 +57,11 @@ let check_addr_access access_mode location (address, history) astate = ReportableError { diagnostic= Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace + ; must_be_valid_reason= None } ; astate } ) in match access_mode with diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 7d6130180..5b01ff1aa 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -30,14 +30,19 @@ module Import : sig | LatentInvalidAccess of { astate: AbductiveDomain.summary ; address: AbstractValue.t - ; must_be_valid: Trace.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option ; calling_context: (CallEvent.t * Location.t) list } | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = - | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccess of + { astate: 'astate + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | PotentialInvalidAccessSummary of - {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 6ae7dd9c5..b0bd6039a 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -87,7 +87,8 @@ let report_summary_error tenv proc_desc err_log { calling_context= [] ; invalidation= ConstantDereference IntLit.zero ; invalidation_trace= Immediate {location= Procdesc.get_loc proc_desc; history= []} - ; access_trace= must_be_valid }) ; + ; access_trace= fst must_be_valid + ; must_be_valid_reason= snd must_be_valid }) ; LatentInvalidAccess {astate; address; must_be_valid; calling_context= []} | ISLError astate -> ISLLatentMemoryError astate diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index fe2bc0701..3a61a563a 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -45,7 +45,8 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc err_log { calling_context= [] ; invalidation ; invalidation_trace - ; access_trace= must_be_valid } + ; access_trace= fst must_be_valid + ; must_be_valid_reason= snd must_be_valid } ; astate }) |> Option.some ) ) (* already a summary but need to reconstruct the variants to make the type system happy :( *) diff --git a/infer/tests/codetoanalyze/objcpp/pulse/Makefile b/infer/tests/codetoanalyze/objcpp/pulse/Makefile index bb7bed24d..61bc2c31b 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/Makefile +++ b/infer/tests/codetoanalyze/objcpp/pulse/Makefile @@ -10,7 +10,8 @@ INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ --pulse-model-alloc-pattern "AB[IF].*Create.*" \ --pulse-model-release-pattern "ABFRelease" \ --pulse-model-transfer-ownership "abf::BridgingRelease" \ ---pulse-model-transfer-ownership "ABFBridgingRelease" +--pulse-model-transfer-ownership "ABFBridgingRelease" \ +--pulse-report-latent-issues INFERPRINT_OPTIONS = --issues-tests diff --git a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm index 4871d920a..ef7b7ebcf 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm +++ b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm @@ -92,6 +92,25 @@ std::shared_ptr testNonPODTraceBad() { return result; } +std::shared_ptr testCallMethodReturnsnonPODLatent(bool b) { + SomeObject* obj; + if (b) { + obj = nil; + } else { + obj = [SomeObject new]; + } + std::shared_ptr d = [obj returnsnonPOD]; // UB if obj nil + return d; +} + +std::shared_ptr testCallMethodReturnsnonPODLatentBad(bool b) { + return testCallMethodReturnsnonPODLatent(true); +} + +std::shared_ptr testCallMethodReturnsnonPODLatentOk(bool b) { + return testCallMethodReturnsnonPODLatent(false); +} + int testAccessPropertyAccessorOk() { SomeObject* obj = nil; return obj.x; // calls property accessor method diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 8ec1aa23d..2a0bcdfd7 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,8 +1,10 @@ codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `SomeObject.returnsNil` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `SomeObject.returnsNil`,return from call to `SomeObject.returnsNil`,passed as argument to `SomeObject.get`,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `SomeObject.returnsNil` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `SomeObject.returnsNil`,return from call to `SomeObject.returnsNil`,passed as argument to `SomeObject.get`,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,passed as argument to `SomeObject.getXPtr`,return from call to `SomeObject.getXPtr`,assigned,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest.deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]