[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

@@ -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]

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))
 

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 *)
 

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) )

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}. *)

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
 

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

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 ->

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

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]

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]