From 16cb07698e390d52b0d8d1179bb56fa72f0ce6f6 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 6 May 2021 07:45:37 -0700 Subject: [PATCH] [pulse] no longer drop attributes of dead addresses Summary: When garbage-collecting addresses we would also remove their attributes. But even though the addresses are no longer allocated in the heap, they might show up in the formula and so we need to remember facts about them. This forces us to detect leaks closer to the point where addresses are deleted from the heap, in AbductiveDomain.ml. This is a nice refactoring in itself: doing so fixes some other FNs where we sometimes missed leak detection on dead addresses. This also makes it unecessary to simplify InstanceOf eagerly when variables get out of scope. Some new {folly,std}::optionals false positives that either are similar to existing ones or involve unmodelled smart pointers. Reviewed By: da319 Differential Revision: D28126103 fbshipit-source-id: e3a903282 --- infer/src/pulse/Pulse.ml | 21 +++-- infer/src/pulse/PulseAbductiveDomain.ml | 94 ++++++++++++++----- infer/src/pulse/PulseAbductiveDomain.mli | 21 +++-- infer/src/pulse/PulseAccessResult.ml | 8 ++ infer/src/pulse/PulseAccessResult.mli | 19 +++- infer/src/pulse/PulseCallOperations.ml | 21 +++-- infer/src/pulse/PulseFormula.mli | 7 -- infer/src/pulse/PulseModels.ml | 6 +- infer/src/pulse/PulseObjectiveCSummary.ml | 7 +- infer/src/pulse/PulseOperations.ml | 48 +--------- infer/src/pulse/PulseOperations.mli | 3 +- infer/src/pulse/PulsePathCondition.ml | 5 - infer/src/pulse/PulsePathCondition.mli | 2 - infer/src/pulse/PulseReport.ml | 41 ++++---- infer/src/pulse/PulseReport.mli | 9 +- infer/src/pulse/PulseSummary.ml | 14 ++- infer/src/pulse/PulseSummary.mli | 9 +- infer/tests/codetoanalyze/c/pulse/issues.exp | 6 +- .../tests/codetoanalyze/c/pulse/memory_leak.c | 2 + infer/tests/codetoanalyze/c/pulse/nullptr.c | 8 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 + .../codetoanalyze/cpp/pulse/optional.cpp | 8 +- .../tests/codetoanalyze/objc/pulse/issues.exp | 16 ++-- .../codetoanalyze/objcpp/pulse/issues.exp | 2 +- 24 files changed, 221 insertions(+), 160 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index ca42e830c..f45089917 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -206,7 +206,7 @@ module PulseTransferFunctions = struct | Error _ as err -> Some err | Ok exec_state -> - PulseSummary.force_exit_program tenv proc_desc err_log exec_state + PulseSummary.force_exit_program tenv proc_desc err_log call_loc exec_state |> Option.map ~f:(fun exec_state -> Ok exec_state) ) else exec_states_res @@ -258,7 +258,7 @@ module PulseTransferFunctions = struct [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate - |> PulseReport.report_exec_results tenv proc_desc err_log ) + |> PulseReport.report_exec_results tenv proc_desc err_log location ) in let dynamic_types_unreachable = PulseOperations.get_dynamic_type_unreachable_values vars astate @@ -296,7 +296,7 @@ module PulseTransferFunctions = struct [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate) ] in - PulseReport.report_results tenv proc_desc err_log result + PulseReport.report_results tenv proc_desc err_log loc result in let set_global_astates = match rhs_exp with @@ -369,7 +369,7 @@ module PulseTransferFunctions = struct | _ -> astates in - PulseReport.report_results tenv proc_desc err_log result + PulseReport.report_results tenv proc_desc err_log loc result | Prune (condition, loc, _is_then_branch, _if_kind) -> (let<*> astate = PulseOperations.prune loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then @@ -378,10 +378,10 @@ module PulseTransferFunctions = struct else (* [condition] is true or unknown value: go into the branch *) [Ok (ContinueProgram astate)]) - |> PulseReport.report_exec_results tenv proc_desc err_log + |> PulseReport.report_exec_results tenv proc_desc err_log loc | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate - |> PulseReport.report_exec_results tenv proc_desc err_log + |> PulseReport.report_exec_results tenv proc_desc err_log loc | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = List.concat_map astates ~f:(fun (astate : Domain.t) -> @@ -393,8 +393,7 @@ module PulseTransferFunctions = struct | LatentInvalidAccess _ -> [astate] | ContinueProgram astate -> - PulseOperations.remove_vars tenv vars location astate - |> PulseReport.report_result tenv proc_desc err_log ) + [ContinueProgram (PulseOperations.remove_vars vars location astate)] ) in if Procname.is_java (Procdesc.get_proc_name proc_desc) then remove_vars vars [ContinueProgram astate] @@ -461,7 +460,11 @@ let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data let updated_posts = PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts in - let summary = PulseSummary.of_posts tenv proc_desc err_log updated_posts in + let summary = + PulseSummary.of_posts tenv proc_desc err_log + (Procdesc.get_exit_node proc_desc |> Procdesc.Node.get_loc) + updated_posts + in report_topl_errors proc_desc err_log summary ; Some summary ) | None -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 699211ca3..027ad24ea 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -35,7 +35,7 @@ module type BaseDomainSig_ = sig (** filter both heap and attrs *) val filter_addr_with_discarded_addrs : - f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list + heap_only:bool -> f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list (** compute new state containing only reachable addresses in its heap and attributes, as well as the list of discarded unreachable addresses *) @@ -76,10 +76,11 @@ end = struct update ~heap:heap' ~attrs:attrs' foot - let filter_addr_with_discarded_addrs ~f foot = + let filter_addr_with_discarded_addrs ~heap_only ~f foot = let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in let attrs', discarded_addresses = - BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs + if heap_only then (foot.attrs, []) + else BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs in (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses) @@ -130,16 +131,6 @@ let leq ~lhs ~rhs = let initialize address astate = {astate with post= PostDomain.initialize address astate.post} -let simplify_instanceof tenv astate = - let attrs = (astate.post :> BaseDomain.t).attrs in - let path_condition = - PathCondition.simplify_instanceof tenv - ~get_dynamic_type:(BaseAddressAttributes.get_dynamic_type attrs) - astate.path_condition - in - {astate with path_condition} - - module Stack = struct let is_abducible astate var = (* HACK: formals are pre-registered in the initial state *) @@ -613,14 +604,42 @@ let skipped_calls_match_pattern astate = astate.skipped_calls ) -let discard_unreachable ({pre; post} as astate) = +let check_memory_leaks unreachable_addrs astate = + let check_memory_leak attributes = + let allocated_not_freed_opt = + Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) + ~f:(fun acc attr -> + match (attr : Attribute.t) with + | Allocated (procname, trace) -> + (Some (procname, trace), snd acc) + | Invalid (CFree, _) -> + (fst acc, true) + | _ -> + acc ) + in + match allocated_not_freed_opt with + | Some (procname, trace), false -> + (* allocated but not freed *) + Error (procname, trace) + | _ -> + Ok () + in + List.fold_result unreachable_addrs ~init:() ~f:(fun () addr -> + match AddressAttributes.find_opt addr astate with + | Some unreachable_attrs -> + check_memory_leak unreachable_attrs + | None -> + Ok () ) + + +let discard_unreachable_ ~for_summary ({pre; post} as astate) = let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in let pre_new = PreDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre in let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in - let post_new, discard_addresses = - PostDomain.filter_addr_with_discarded_addrs + let post_new, dead_addresses = + PostDomain.filter_addr_with_discarded_addrs ~heap_only:(not for_summary) ~f:(fun address -> AbstractValue.Set.mem address pre_addresses || AbstractValue.Set.mem address post_addresses ) @@ -631,7 +650,25 @@ let discard_unreachable ({pre; post} as astate) = if phys_equal pre_new pre && phys_equal post_new post then astate else {astate with pre= pre_new; post= post_new} in - (astate, pre_addresses, post_addresses, discard_addresses) + (astate, pre_addresses, post_addresses, dead_addresses) + + +(* exported in .mli *) +let discard_unreachable astate = + let astate, _pre_addresses, _post_addresses, _dead_addresses = + discard_unreachable_ ~for_summary:false astate + in + (* NOTE: [_dead_addresses] is always the empty list when [for_summary] is [false] *) + astate + + +let get_unreachable_attributes {post} = + let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in + BaseAddressAttributes.fold + (fun address _ dead_addresses -> + if AbstractValue.Set.mem address post_addresses then dead_addresses + else address :: dead_addresses ) + (post :> BaseDomain.t).attrs [] let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) @@ -875,7 +912,9 @@ let filter_for_summary tenv proc_name astate0 = this. *) let astate = restore_formals_for_summary astate_before_filter in let astate = {astate with topl= PulseTopl.filter_for_summary astate.path_condition astate.topl} in - let astate, pre_live_addresses, post_live_addresses, _ = discard_unreachable astate in + let astate, pre_live_addresses, post_live_addresses, dead_addresses = + discard_unreachable_ ~for_summary:true astate + in let can_be_pruned = if PatternMatch.is_entry_point proc_name then (* report all latent issues at entry points *) @@ -889,10 +928,12 @@ let filter_for_summary tenv proc_name astate0 = (BaseAddressAttributes.get_dynamic_type (astate_before_filter.post :> BaseDomain.t).attrs) ~can_be_pruned ~keep:live_addresses astate.path_condition in - ({astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}, new_eqs) + ( {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl} + , dead_addresses + , new_eqs ) -let summary_of_post tenv pdesc astate = +let summary_of_post tenv pdesc location astate = let open SatUnsat.Import in (* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then canonicalize *before* garbage collecting unused addresses in case we detect any last-minute @@ -905,13 +946,20 @@ let summary_of_post tenv pdesc astate = let* () = if is_unsat then Unsat else Sat () in let astate = {astate with path_condition} in let* astate, error = incorporate_new_eqs astate new_eqs in - let* astate, new_eqs = filter_for_summary tenv (Procdesc.get_proc_name pdesc) astate in + let astate_before_filter = astate in + let* astate, dead_addresses, new_eqs = + filter_for_summary tenv (Procdesc.get_proc_name pdesc) astate + in let+ astate, error = match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error) in match error with - | None -> - Ok (invalidate_locals pdesc astate) + | None -> ( + match check_memory_leaks dead_addresses astate_before_filter with + | Ok () -> + Ok (invalidate_locals pdesc astate) + | Error (proc_name, trace) -> + Error (`MemoryLeak (astate, proc_name, trace, location)) ) | Some (address, must_be_valid) -> Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid)) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index b5b8edc27..7bec085b0 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -57,8 +57,6 @@ val get_pre : t -> BaseDomain.t val get_post : t -> BaseDomain.t -val simplify_instanceof : Tenv.t -> t -> t - (** stack operations like {!BaseStack} but that also take care of propagating facts to the precondition *) module Stack : sig @@ -158,10 +156,11 @@ val is_local : Var.t -> t -> bool val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option -val discard_unreachable : t -> t * AbstractValue.Set.t * AbstractValue.Set.t * AbstractValue.t list -(** garbage collect unreachable addresses in the state to make it smaller and return the new state, - the live pre addresses, the live post addresses, and the discarded addresses that used to have - attributes attached *) +val discard_unreachable : t -> t +(** garbage collect unreachable addresses in the state to make it smaller and return the new state *) + +val get_unreachable_attributes : t -> AbstractValue.t list +(** collect the addresses that have attributes but are unreachable in the current post-condition *) val add_skipped_call : Procname.t -> Trace.t -> t -> t @@ -181,14 +180,16 @@ val skipped_calls_match_pattern : summary -> bool val summary_of_post : Tenv.t -> Procdesc.t + -> Location.t -> t -> ( summary - , [> `PotentialInvalidAccessSummary of - summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] ) + , [> `MemoryLeak of summary * Procname.t * Trace.t * Location.t + | `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 *) +(** Trim the state down to just the procedure's interface (formals and globals), and simplify and + normalize the state. *) val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t (** directly set the edges for the given address, bypassing abduction altogether *) diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml index 5cae8a51e..93095e072 100644 --- a/infer/src/pulse/PulseAccessResult.ml +++ b/infer/src/pulse/PulseAccessResult.ml @@ -19,6 +19,7 @@ type 'astate error = ; address: AbstractValue.t ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t} | ISLError of 'astate type ('a, 'astate) base_t = ('a, 'astate error) result @@ -33,6 +34,13 @@ type 'astate abductive_error = AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] +let ignore_memory_leaks = function + | Ok astate | Error (`MemoryLeak (astate, _, _, _)) -> + Ok astate + | Error #abductive_error as result -> + result + + let of_abductive_error = function | `ISLError astate -> ISLError astate diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli index 08839c87e..75a53d6f6 100644 --- a/infer/src/pulse/PulseAccessResult.mli +++ b/infer/src/pulse/PulseAccessResult.mli @@ -19,6 +19,7 @@ type 'astate error = ; address: AbstractValue.t ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t} | ISLError of 'astate type ('a, 'astate) base_t = ('a, 'astate error) result @@ -26,7 +27,10 @@ type ('a, 'astate) base_t = ('a, 'astate error) result type 'a t = ('a, AbductiveDomain.t) base_t (** Intermediate datatype since {!AbductiveDomain} cannot refer to this module without creating a - circular dependency. *) + circular dependency. + + Purposefully omits [`MemoryLeak] errors as it's a good idea to double-check if you really want + to report a leak. *) type 'astate abductive_error = [ `ISLError of 'astate | `PotentialInvalidAccess of @@ -35,11 +39,18 @@ type 'astate abductive_error = AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] -val of_abductive_error : 'astate abductive_error -> 'astate error +val of_abductive_error : [< 'astate abductive_error] -> 'astate error -val of_abductive_result : ('a, 'astate abductive_error) result -> ('a, 'astate) base_t +val of_abductive_result : ('a, [< 'astate abductive_error]) result -> ('a, 'astate) base_t val of_abductive_access_result : Trace.t - -> ('a, [`InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result + -> ('a, [< `InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result -> ('a, 'astate) base_t + +val ignore_memory_leaks : + ( AbductiveDomain.summary + , [< `MemoryLeak of AbductiveDomain.summary * Procname.t * Trace.t * Location.t + | AbductiveDomain.summary abductive_error ] ) + result + -> (AbductiveDomain.summary, [> AbductiveDomain.summary abductive_error]) result diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index c9b400c8f..f0e882f64 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -117,8 +117,10 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state (astate :> AbductiveDomain.t) ~f:(fun subst astate -> let* astate_summary_result = - AbductiveDomain.summary_of_post tenv caller_proc_desc astate - >>| AccessResult.of_abductive_result + ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate + >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result + :> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t + ) in match astate_summary_result with | Error _ as error -> @@ -140,11 +142,9 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state | `DelayReport latent_issue -> Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) | `ReportNow -> - Sat - (Error - (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)})) + Sat (Error (ReportableErrorSummary {diagnostic; astate= astate_summary})) | `ISLDelay astate -> - Sat (Error (ISLError (astate :> AbductiveDomain.t))) ) + Sat (Error (ISLError astate)) ) | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> ( match AbstractValue.Map.find_opt address_callee subst with | None -> @@ -167,7 +167,7 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state | Some (invalidation, invalidation_trace) -> Sat (Error - (ReportableError + (ReportableErrorSummary { diagnostic= AccessToInvalidAddress { calling_context @@ -175,13 +175,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ; invalidation_trace ; access_trace= fst must_be_valid ; must_be_valid_reason= snd must_be_valid } - ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) ) + ; astate= astate_summary })) ) ) ) ) | ISLLatentMemoryError astate -> map_call_result ~is_isl_error_prepost:true (astate :> AbductiveDomain.t) ~f:(fun _subst astate -> - AbductiveDomain.summary_of_post tenv caller_proc_desc astate - >>| AccessResult.of_abductive_result + ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate + >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result + :> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t ) >>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) ) diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index cc028d81a..eea52e431 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -77,10 +77,3 @@ val has_no_assumptions : t -> bool val get_var_repr : t -> Var.t -> Var.t (** get the canonical representative for the variable according to the equality relation *) - -(** Module for reasoning about dynamic types. **) -module DynamicTypes : sig - val simplify : Tenv.t -> get_dynamic_type:(Var.t -> Typ.t option) -> t -> t - (** Simplifies [IsInstanceOf(var, typ)] predicate when dynamic type information is available in - state. **) -end diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 7387dc326..751b9e295 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -49,10 +49,12 @@ module Misc = struct let early_exit : model = - fun {analysis_data= {tenv; proc_desc}} astate -> + fun {analysis_data= {tenv; proc_desc}; location} astate -> let open SatUnsat.Import in match - AbductiveDomain.summary_of_post tenv proc_desc astate >>| AccessResult.of_abductive_result + ( AbductiveDomain.summary_of_post tenv proc_desc location astate + >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result + :> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t ) with | Unsat -> [] diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 3a3bbfa28..e3a753432 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -85,7 +85,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in PulseArithmetic.prune_positive (fst value) astate in - PulseReport.report_result tenv proc_desc err_log result + PulseReport.report_result tenv proc_desc err_log location result | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ @@ -120,7 +120,7 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo in astate in - PulseReport.report_result tenv proc_desc err_log result + PulseReport.report_result tenv proc_desc err_log location result | ContinueProgram _, _ | ExitProgram _, _ | AbortProgram _, _ @@ -136,6 +136,7 @@ let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} | 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 location = Procdesc.get_loc proc_desc in + let nil_summary = PulseReport.report_result tenv proc_desc err_log location 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 2910e5550..3bf8a864f 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -37,6 +37,7 @@ module Import = struct ; address: AbstractValue.t ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t} | ISLError of 'astate include IResult.Let_syntax @@ -512,37 +513,6 @@ let mark_address_of_stack_variable history variable location address astate = AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate -let check_memory_leak_unreachable unreachable_addrs location astate = - let check_memory_leak result attributes = - let allocated_not_freed_opt = - Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) - ~f:(fun acc attr -> - match (attr : Attribute.t) with - | Allocated (procname, trace) -> - (Some (procname, trace), snd acc) - | Invalid (CFree, _) -> - (fst acc, true) - | _ -> - acc ) - in - match allocated_not_freed_opt with - | Some (procname, trace), false -> - (* allocated but not freed *) - Error - (ReportableError - { diagnostic= Diagnostic.MemoryLeak {procname; location; allocation_trace= trace} - ; astate }) - | _ -> - result - in - List.fold unreachable_addrs ~init:(Ok ()) ~f:(fun res addr -> - match AbductiveDomain.AddressAttributes.find_opt addr astate with - | Some unreachable_attrs -> - check_memory_leak res unreachable_attrs - | None -> - res ) - - let get_dynamic_type_unreachable_values vars astate = (* For each unreachable address we find a root variable for it; if there is more than one, it doesn't matter which *) @@ -553,7 +523,7 @@ let get_dynamic_type_unreachable_values vars astate = astate None in let astate' = Stack.remove_vars vars astate in - let _, _, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in + let unreachable_addrs = AbductiveDomain.get_unreachable_attributes astate' in let res = List.fold unreachable_addrs ~init:[] ~f:(fun res addr -> (let open IOption.Let_syntax in @@ -566,13 +536,9 @@ let get_dynamic_type_unreachable_values vars astate = List.map ~f:(fun (var, _, typ) -> (var, typ)) res -let remove_vars tenv vars location orig_astate = +let remove_vars vars location orig_astate = let astate = - (* Simplification of [IsInstanceOf(var, typ)] term is necessary here, as a variable can die before - the normalization function is called. This could cause [IsInstanceOf(var, typ)] terms that - reference dead vars to be collected before they are evaluated to detect a contradiction *) - List.fold vars ~init:(AbductiveDomain.simplify_instanceof tenv orig_astate) - ~f:(fun astate var -> + List.fold vars ~init:orig_astate ~f:(fun astate var -> match Stack.find_opt var astate with | Some (address, history) -> let astate = @@ -587,11 +553,7 @@ let remove_vars tenv vars location orig_astate = astate ) in let astate' = Stack.remove_vars vars astate in - if phys_equal astate' astate then Ok astate - else - let astate, _, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in - let+ () = check_memory_leak_unreachable unreachable_addrs location orig_astate in - astate + if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate' let get_captured_actuals location ~captured_vars ~actual_closure astate = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index bfd63fec8..7804404a8 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -44,6 +44,7 @@ module Import : sig ; address: AbstractValue.t ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t} | ISLError of 'astate (** {2 Monadic syntax} *) @@ -219,7 +220,7 @@ val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) lis (** Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available *) -val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t AccessResult.t +val remove_vars : Var.t list -> Location.t -> t -> t val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index f38f342f5..0da486144 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -121,11 +121,6 @@ let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi = if (fst result).is_unsat then Unsat else Sat result -let simplify_instanceof tenv ~get_dynamic_type phi = - let formula = Formula.DynamicTypes.simplify tenv ~get_dynamic_type phi.formula in - {phi with formula} - - let subst_find_or_new subst addr_callee = match AbstractValue.Map.find_opt addr_callee subst with | None -> diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index c2bfb5c8c..62d3c6faa 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -45,8 +45,6 @@ val simplify : in [keep] as possible, and tries to eliminate variables not in [can_be_pruned] from the "pruned" part of the formula *) -val simplify_instanceof : Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t - val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index b0bd6039a..b06d3104f 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -47,33 +47,37 @@ let is_suppressed tenv proc_desc diagnostic astate = false -let summary_of_error_post tenv proc_desc mk_error astate = - match AbductiveDomain.summary_of_post tenv proc_desc astate with - | Sat (Ok astate) -> +let summary_of_error_post tenv proc_desc location mk_error astate = + match AbductiveDomain.summary_of_post tenv proc_desc location astate with + | Sat (Ok astate) | Sat (Error (`MemoryLeak (astate, _, _, _))) -> + (* ignore potential memory leaks: error'ing in the middle of a function will typically produce + spurious leaks *) Sat (mk_error astate) - | Sat (Error error) -> + | Sat (Error (`PotentialInvalidAccessSummary (summary, addr, trace))) -> (* ignore the error we wanted to report (with [mk_error]): the abstract state contained a potential error already so report [error] instead *) - Sat (AccessResult.of_abductive_error error) + Sat (AccessResult.of_abductive_error (`PotentialInvalidAccessSummary (summary, addr, trace))) | Unsat -> Unsat -let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) : +let summary_error_of_error tenv proc_desc location (error : AbductiveDomain.t AccessResult.error) : AbductiveDomain.summary AccessResult.error SatUnsat.t = match error with | PotentialInvalidAccessSummary {astate; address; must_be_valid} -> Sat (PotentialInvalidAccessSummary {astate; address; must_be_valid}) | PotentialInvalidAccess {astate; address; must_be_valid} -> - summary_of_error_post tenv proc_desc + summary_of_error_post tenv proc_desc location (fun astate -> PotentialInvalidAccess {astate; address; must_be_valid}) astate | ReportableError {astate; diagnostic} -> - summary_of_error_post tenv proc_desc + summary_of_error_post tenv proc_desc location (fun astate -> ReportableError {astate; diagnostic}) astate + | ReportableErrorSummary {astate; diagnostic} -> + Sat (ReportableErrorSummary {astate; diagnostic}) | ISLError astate -> - summary_of_error_post tenv proc_desc (fun astate -> ISLError astate) astate + summary_of_error_post tenv proc_desc location (fun astate -> ISLError astate) astate let report_summary_error tenv proc_desc err_log @@ -92,7 +96,7 @@ let report_summary_error tenv proc_desc err_log LatentInvalidAccess {astate; address; must_be_valid; calling_context= []} | ISLError astate -> ISLLatentMemoryError astate - | ReportableError {astate; diagnostic} -> ( + | ReportableError {astate; diagnostic} | ReportableErrorSummary {astate; diagnostic} -> ( match LatentIssue.should_report astate diagnostic with | `ReportNow -> if not (is_suppressed tenv proc_desc diagnostic astate) then @@ -103,30 +107,33 @@ let report_summary_error tenv proc_desc err_log LatentAbortProgram {astate; latent_issue} ) -let report_error tenv proc_desc err_log (access_error : AbductiveDomain.t AccessResult.error) = +let report_error tenv proc_desc err_log location + (access_error : AbductiveDomain.t AccessResult.error) = let open SatUnsat.Import in - summary_error_of_error tenv proc_desc access_error >>| report_summary_error tenv proc_desc err_log + summary_error_of_error tenv proc_desc location access_error + >>| report_summary_error tenv proc_desc err_log -let report_exec_results tenv proc_desc err_log results = +let report_exec_results tenv proc_desc err_log location results = List.filter_map results ~f:(fun exec_result -> match exec_result with | Ok post -> Some post | Error error -> ( - match report_error tenv proc_desc err_log error with + match report_error tenv proc_desc err_log location error with | Unsat -> None | Sat exec_state -> Some exec_state ) ) -let report_results tenv proc_desc err_log results = +let report_results tenv proc_desc err_log location results = let open IResult.Let_syntax in List.map results ~f:(fun result -> let+ astate = result in ExecutionDomain.ContinueProgram astate ) - |> report_exec_results tenv proc_desc err_log + |> report_exec_results tenv proc_desc err_log location -let report_result tenv proc_desc err_log result = report_results tenv proc_desc err_log [result] +let report_result tenv proc_desc err_log location result = + report_results tenv proc_desc err_log location [result] diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index 4b77fcf3a..c7d0b3b1d 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -9,7 +9,12 @@ open! IStd open PulseDomainInterface val report_result : - Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list + Tenv.t + -> Procdesc.t + -> Errlog.t + -> Location.t + -> AbductiveDomain.t AccessResult.t + -> ExecutionDomain.t list val report_summary_error : Tenv.t @@ -22,6 +27,7 @@ val report_results : Tenv.t -> Procdesc.t -> Errlog.t + -> Location.t -> AbductiveDomain.t AccessResult.t list -> ExecutionDomain.t list @@ -29,5 +35,6 @@ val report_exec_results : Tenv.t -> Procdesc.t -> Errlog.t + -> Location.t -> ExecutionDomain.t AccessResult.t list -> ExecutionDomain.t list diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index 3a61a563a..f52a12a7f 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -21,15 +21,19 @@ let pp fmt summary = F.close_box () -let exec_summary_of_post_common tenv ~continue_program proc_desc err_log +let exec_summary_of_post_common tenv ~continue_program proc_desc err_log location (exec_astate : ExecutionDomain.t) : _ ExecutionDomain.base_t option = match exec_astate with | ContinueProgram astate -> ( - match AbductiveDomain.summary_of_post tenv proc_desc astate with + match AbductiveDomain.summary_of_post tenv proc_desc location astate with | Unsat -> None | Sat (Ok astate) -> Some (continue_program astate) + | Sat (Error (`MemoryLeak (astate, procname, allocation_trace, location))) -> + Some + (PulseReport.report_summary_error tenv proc_desc err_log + (ReportableError {astate; diagnostic= MemoryLeak {procname; allocation_trace; location}})) | Sat (Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))) -> ( match AbductiveDomain.find_post_cell_opt address (astate :> AbductiveDomain.t) @@ -67,8 +71,8 @@ let force_exit_program tenv proc_desc err_log post = ExitProgram astate ) -let of_posts tenv proc_desc err_log posts = +let of_posts tenv proc_desc err_log location posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ; - exec_summary_of_post_common tenv proc_desc err_log exec_state ~continue_program:(fun astate -> - ContinueProgram astate ) ) + exec_summary_of_post_common tenv proc_desc err_log location exec_state + ~continue_program:(fun astate -> ContinueProgram astate) ) diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index c283e4aad..734d505d0 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -10,9 +10,14 @@ open PulseDomainInterface type t = ExecutionDomain.summary list [@@deriving yojson_of] -val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t list -> t +val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> Location.t -> ExecutionDomain.t list -> t val force_exit_program : - Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option + Tenv.t + -> Procdesc.t + -> Errlog.t + -> Location.t + -> ExecutionDomain.t + -> _ ExecutionDomain.base_t option val pp : Format.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 1551ea6ea..2077e7c30 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -9,14 +9,18 @@ codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, NULLPTR_DEREFERENCE, n codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/latent.c, main, 3, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/latent.c, manifest_use_after_free, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] +codetoanalyze/c/pulse/memory_leak.c, malloc_formal_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 5, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, create_null_path2_latent, 8, NULLPTR_DEREFERENCE, 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,parameter `p` of create_null_path2_latent,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c index a568be0d1..25d285a9f 100644 --- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c +++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c @@ -34,3 +34,5 @@ void malloc_interproc_no_free_bad2() { int y = 4; int* q = p; } + +void malloc_formal_leak_bad(int* x) { x = (int*)malloc(sizeof(int*)); } diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 9f2774357..ab4cd7b0d 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -25,7 +25,7 @@ void call_create_null_path_then_deref_unconditionally_ok(int* p) { *p = 52; } -void create_null_path2_ok(int* p) { +void create_null_path2_latent(int* p) { int* q = NULL; if (p) { *p = 32; @@ -115,3 +115,9 @@ void bug_with_allocation_bad(int* x) { int* y = NULL; *y = 42; } + +void null_alias_bad(int* x) { + int* y = NULL; + x = (int*)malloc(sizeof(int*)); + *x = 42; +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 4d2f32733..0dd961058 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -54,6 +54,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, US codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, NULLPTR_DEREFERENCE, 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,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, NULLPTR_DEREFERENCE, 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,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference2_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `test_after_dereference2_latent` here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] @@ -63,6 +64,9 @@ codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, FP_smart_pointer, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Node::getShared` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Node::getShared`,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,return from call to `Node::getShared`,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, FP_std_value_or_check_value_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, FP_value_or_check_value_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,passed as argument to `folly::Optional::operator=`,parameter `other` of folly::Optional::operator=,passed as argument to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp index 8299405d7..028045697 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp @@ -185,9 +185,7 @@ int value_or_check_empty_ok() { return -1; } -// missing a more precise model for constructing an optional from a -// value, which could cause an FP but doesn't at the moment -int value_or_check_value_ok() { +int FP_value_or_check_value_ok() { folly::Optional foo{5}; int x = foo.value_or(0); if (x != 5) { @@ -306,7 +304,7 @@ int std_value_or_check_empty_ok() { return -1; } -int std_value_or_check_value_ok() { +int FP_std_value_or_check_value_ok() { std::optional foo{5}; int x = foo.value_or(0); if (x != 5) { @@ -400,7 +398,7 @@ struct Node { } }; -int smart_pointer(const Node& node) { +int FP_smart_pointer(const Node& node) { if (node.getShared().has_value()) { return *(node.getShared().value()); } diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 1e87eba8f..5b4fd0b1c 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,12 +1,12 @@ -codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `BufferContainer2.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `BufferContainer2.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MallocInObjC.m, leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.call_no_bridge_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `MemoryLeaks.ret_no_bridge` here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_mutable_leak_bad:, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_with_rect_leak_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 6, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.call_no_bridge_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `MemoryLeaks.ret_no_bridge` here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_mutable_leak_bad:, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_with_rect_leak_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 7, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here] codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 3567ad5d6..236b8b653 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,4 +1,4 @@ -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/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 2, 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, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]