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]