From 75a068b6020baaa6343ed0224abbe14349071875 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 24 May 2021 05:05:43 -0700 Subject: [PATCH] [pulse] delay leak reporting until summary is created Summary: This is needed for the next diff. It was a bit annoying to report leaks in two different places, now it's just in one. Reviewed By: skcho Differential Revision: D28576768 fbshipit-source-id: 4f23b43cb --- infer/src/pulse/Pulse.ml | 9 ++++----- infer/src/pulse/PulseAbductiveDomain.ml | 16 +++++++++++++--- infer/src/pulse/PulseAbductiveDomain.mli | 6 ++---- infer/src/pulse/PulseAttribute.ml | 16 +++++++++++++++- infer/src/pulse/PulseAttribute.mli | 5 +++++ infer/src/pulse/PulseBaseAddressAttributes.ml | 2 ++ infer/src/pulse/PulseBaseAddressAttributes.mli | 2 ++ infer/src/pulse/PulseOperations.ml | 17 +++++++++-------- infer/src/pulse/PulseOperations.mli | 2 +- infer/tests/codetoanalyze/c/pulse/issues.exp | 3 +-- .../tests/codetoanalyze/c/pulse/issues.exp-isl | 3 +-- 11 files changed, 55 insertions(+), 26 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index e211c33ae..2fd669ccb 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -400,17 +400,16 @@ module PulseTransferFunctions = struct |> 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) -> - match astate with + List.map astates ~f:(fun (exec_state : Domain.t) -> + match exec_state with | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ | LatentInvalidAccess _ -> - [astate] + exec_state | ContinueProgram astate -> - PulseOperations.remove_vars vars location astate - |> PulseReport.report_result tenv proc_desc err_log location ) + ContinueProgram (PulseOperations.remove_vars vars location astate) ) in if Procname.is_java (Procdesc.get_proc_name proc_desc) then remove_vars vars [ContinueProgram astate] diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index cc9d4cc9c..b70ff6b61 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -313,6 +313,10 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.mark_as_end_of_collection addr) + let add_unreachable_at addr location astate = + map_post_attrs astate ~f:(BaseAddressAttributes.add_unreachable_at addr location) + + let replace_must_be_valid_reason reason addr astate = match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with | Some (trace, _reason) -> @@ -627,7 +631,10 @@ let check_memory_leaks unreachable_addrs astate = Container.exists ~iter:(fun seq ~f -> Seq.iter f seq) unreachable_addrs ~f:(AbstractValue.equal addr_canon) - then Error (procname, trace) + then + (* if the address became unreachable at a known point use that location *) + let location = Attributes.get_unreachable_at attributes in + Error (location, procname, trace) else ( L.debug Analysis Quiet "HUH? Address %a was going to leak but is equal to %a which is live; not raising an \ @@ -657,6 +664,7 @@ let discard_unreachable_ ~for_summary ({pre; post} as astate) = post_addresses in let post_new, dead_addresses = + (* keep attributes of dead addresses unless we are creating a summary *) PostDomain.filter_addr_with_discarded_addrs ~heap_only:(not for_summary) ~f:(fun address -> AbstractValue.Set.mem address pre_addresses @@ -979,8 +987,10 @@ let summary_of_post tenv pdesc location astate = match check_memory_leaks (Caml.List.to_seq dead_addresses) astate_before_filter with | Ok () -> Ok (invalidate_locals pdesc astate) - | Error (proc_name, trace) -> - Error (`MemoryLeak (astate, proc_name, trace, location)) ) + | Error (unreachable_location, proc_name, trace) -> + Error + (`MemoryLeak + (astate, proc_name, trace, Option.value unreachable_location ~default: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 af5ecc87f..873e8703a 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -144,6 +144,8 @@ module AddressAttributes : sig val std_vector_reserve : AbstractValue.t -> t -> t + val add_unreachable_at : AbstractValue.t -> Location.t -> t -> t + val find_opt : AbstractValue.t -> t -> Attributes.t option val check_valid_isl : @@ -158,10 +160,6 @@ val is_local : Var.t -> t -> bool val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option -val check_memory_leaks : AbstractValue.t Seq.t -> t -> (unit, Procname.t * Trace.t) result -(** [check_memory_leaks unreachable_addrs astate] is an [Error (proc_name, trace)] if one of the - addresses in [unreachable_addrs] was allocated by [proc_name] *) - val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller and return the new state *) diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 668c990f9..54103557c 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -37,6 +37,7 @@ module Attribute = struct | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized + | UnreachableAt of Location.t | WrittenTo of Trace.t [@@deriving compare, variants] @@ -93,6 +94,8 @@ module Attribute = struct let uninitialized_rank = Variants.to_rank Uninitialized + let unreachable_at_rank = Variants.to_rank (UnreachableAt Location.dummy) + let must_be_initialized_rank = Variants.to_rank (MustBeInitialized dummy_trace) let pp f attribute = @@ -133,6 +136,8 @@ module Attribute = struct F.pp_print_string f "std::vector::reserve()" | Uninitialized -> F.pp_print_string f "Uninitialized" + | UnreachableAt location -> + F.fprintf f "UnreachableAt(%a)" Location.pp location | WrittenTo trace -> F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace @@ -149,12 +154,13 @@ module Attribute = struct | EndOfCollection | StdVectorReserve | Uninitialized + | UnreachableAt _ | WrittenTo _ -> false let is_suitable_for_post = function - | MustBeInitialized _ | MustBeValid _ -> + | MustBeInitialized _ | MustBeValid _ | UnreachableAt _ -> false | Invalid _ | Allocated _ @@ -203,6 +209,7 @@ module Attribute = struct | DynamicType _ | EndOfCollection | StdVectorReserve + | UnreachableAt _ | Uninitialized ) as attr -> attr end @@ -288,6 +295,13 @@ module Attributes = struct trace ) + let get_unreachable_at attrs = + Set.find_rank attrs Attribute.unreachable_at_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.UnreachableAt location) = attr in + location ) + + let isl_subset callee_attrs caller_attrs = Set.for_all callee_attrs ~f:(fun attr1 -> Set.for_all caller_attrs ~f:(fun attr2 -> Attribute.isl_subset attr1 attr2) ) diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 200bb239a..3f702fa92 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -24,6 +24,9 @@ type t = | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized + | UnreachableAt of Location.t + (** temporary marker to remember where a variable became unreachable; helps with accurately + reporting leaks *) | WrittenTo of Trace.t [@@deriving compare] @@ -62,6 +65,8 @@ module Attributes : sig val get_must_be_initialized : t -> Trace.t option + val get_unreachable_at : t -> Location.t option + val isl_subset : t -> t -> bool (** check whether for each attr in the second list, there exists a corresponding attr in the first according to {!Attributes.isl_equiv}. *) diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 0653619f6..36d6712de 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -152,6 +152,8 @@ let get_dynamic_type attrs v = get_attribute Attributes.get_dynamic_type v attrs let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory +let add_unreachable_at address location memory = add_one address (UnreachableAt location) memory + let is_end_of_collection address attrs = Graph.find_opt address attrs |> Option.exists ~f:Attributes.is_end_of_collection diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 9f0b522c1..78845a342 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -60,6 +60,8 @@ val mark_as_end_of_collection : AbstractValue.t -> t -> t val is_end_of_collection : AbstractValue.t -> t -> bool +val add_unreachable_at : AbstractValue.t -> Location.t -> t -> t + val pp : F.formatter -> t -> unit val remove_allocation_attr : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 776201807..4fe8397d0 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -627,7 +627,7 @@ let filter_live_addresses ~is_dead_root potential_leak_addrs astate = !potential_leaks -let detect_leaks location ~dead_roots astate = +let mark_potential_leaks location ~dead_roots astate = let is_dead_root var = List.mem ~equal:Var.equal dead_roots var in (* only consider locations that could actually cause a leak if unreachable *) let allocated_reachable_from_dead_root = @@ -638,16 +638,17 @@ let detect_leaks location ~dead_roots astate = in match filter_live_addresses ~is_dead_root allocated_reachable_from_dead_root astate with | exception NoLeak -> - Ok () + astate | potential_leaks -> - AbductiveDomain.check_memory_leaks (AbstractValue.Set.to_seq potential_leaks) astate - |> Result.map_error ~f:(fun (procname, allocation_trace) -> - AccessResult.ReportableError - {astate; diagnostic= MemoryLeak {procname; allocation_trace; location}} ) + (* delay reporting leak as to avoid false positives we need to massage the state some more; + TODO: this can make use miss reporting memory leaks if another error is found *) + AbstractValue.Set.fold + (fun addr astate -> AddressAttributes.add_unreachable_at addr location astate) + potential_leaks astate -let remove_vars vars location astate : t AccessResult.t = - let+ () = detect_leaks location ~dead_roots:vars astate in +let remove_vars vars location astate = + let astate = mark_potential_leaks location ~dead_roots:vars astate in (* remember addresses that will marked invalid later *) let astate = List.fold vars ~init:astate ~f:(fun astate var -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 03355dfaf..790f05652 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -256,7 +256,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 : 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/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 60e5faaa0..b3f7dbf2c 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -28,8 +28,7 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_ codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` 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, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] -codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable 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, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl index 1f2facd07..434478473 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl @@ -28,8 +28,7 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_ codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` 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, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] -codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable 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,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]