[pulse] refactor check whether an address is allocated but not freed

Summary:
More straightforward (and better asymptotic complexity, not that it
matters) that way. Also log when a leak is found in the debug html.

Reviewed By: ezgicicek

Differential Revision: D28536443

fbshipit-source-id: 08c329100

infer/src/pulse/PulseAbductiveDomain.ml

@@ -603,29 +603,26 @@ let skipped_calls_match_pattern astate =
 
 
 let check_memory_leaks unreachable_addrs astate =
-  let check_memory_leak attributes =
+  let check_memory_leak addr attributes =
     let allocated_not_freed_opt =
-      Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
+      let allocated = Attributes.get_allocation attributes in
-        ~f:(fun acc attr ->
+      if Option.is_some allocated then
-          match (attr : Attribute.t) with
+        match Attributes.get_invalid attributes with Some (CFree, _) -> None | _ -> allocated
-          | Allocated (procname, trace) ->
+      else None
-              (Some (procname, trace), snd acc)
-          | Invalid (CFree, _) ->
-              (fst acc, true)
-          | _ ->
-              acc )
     in
     match allocated_not_freed_opt with
-    | Some (procname, trace), false ->
+    | None ->
-        (* allocated but not freed *)
-        Error (procname, trace)
-    | _ ->
         Ok ()
+    | Some (procname, trace) ->
+        (* allocated but not freed => leak *)
+        L.d_printfln ~color:Red "LEAK: unreachable address %a was allocated by %a" AbstractValue.pp
+          addr Procname.pp procname ;
+        Error (procname, trace)
   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
+          check_memory_leak addr unreachable_attrs
       | None ->
           Ok () )