[pulse] Memory leak check

Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.

Reviewed By: jvillard

Differential Revision: D20444097

fbshipit-source-id: 33b6b25a2

infer/man/man1/infer-full.txt

@@ -470,6 +470,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),

infer/man/man1/infer-report.txt

@@ -201,6 +201,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),

infer/man/man1/infer.txt

@@ -470,6 +470,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_MEMORY_LEAK (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default),

infer/src/base/IssueType.ml

@@ -406,6 +406,8 @@ let precondition_not_met = register_from_string "PRECONDITION_NOT_MET"
 
 let premature_nil_termination = register_from_string "PREMATURE_NIL_TERMINATION_ARGUMENT"
 
+let pulse_memory_leak = register_from_string ~enabled:false "PULSE_MEMORY_LEAK"
+
 let pure_function = register_from_string "PURE_FUNCTION"
 
 let quandary_taint_error = register_from_string "QUANDARY_TAINT_ERROR"

infer/src/base/IssueType.mli

@@ -264,6 +264,8 @@ val precondition_not_met : t
 
 val premature_nil_termination : t
 
+val pulse_memory_leak : t
+
 val pure_function : t
 
 val quandary_taint_error : t

infer/src/pulse/Pulse.ml

@@ -167,7 +167,8 @@ module PulseTransferFunctions = struct
         dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate
         |> check_error summary
     | Metadata (ExitScope (vars, location)) ->
-        [PulseOperations.remove_vars vars location astate]
+        let astate = PulseOperations.remove_vars vars location astate in
+        [check_error summary astate]
     | Metadata (VariableLifetimeBegins (pvar, _, location)) ->
         [PulseOperations.realloc_pvar pvar location astate]
     | Metadata (Abstract _ | Nullify _ | Skip) ->

infer/src/pulse/PulseAbductiveDomain.ml

@@ -27,6 +27,12 @@ module type BaseDomainSig = sig
   val filter_addr : f:(AbstractValue.t -> bool) -> t -> t
   (**filter both heap and attrs *)
 
+  val partition_addr :
+       f:(AbstractValue.t -> bool)
+    -> t
+    -> (BaseMemory.t * BaseAddressAttributes.t) * (BaseMemory.t * BaseAddressAttributes.t)
+  (**partition both heap and attrs *)
+
   val pp : F.formatter -> t -> unit
 end
 
@@ -54,6 +60,14 @@ module BaseDomainCommon = struct
     let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in
     let attrs' = BaseAddressAttributes.filter (fun address _ -> f address) foot.attrs in
     update ~heap:heap' ~attrs:attrs' foot
+
+
+  let partition_addr ~f foot =
+    let heap_yes, heap_no = BaseMemory.partition (fun address _ -> f address) foot.heap in
+    let attrs_yes, attrs_no =
+      BaseAddressAttributes.partition (fun address _ -> f address) foot.attrs
+    in
+    ((heap_yes, attrs_yes), (heap_no, attrs_no))
 end
 
 (** represents the post abstract state at each program point *)
@@ -324,11 +338,15 @@ let discard_unreachable ({pre; post} as astate) =
   in
   let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
   let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
-  let post_new =
+  let (heap_new, attrs_new), (_, attrs_unreachable) =
-    Domain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
+    Domain.partition_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
   in
+  let post_new = Domain.update ~heap:heap_new ~attrs:attrs_new post in
+  let 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, attrs_unreachable)
 
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
@@ -399,7 +417,9 @@ module PrePost = struct
 
 
   let of_post pdesc astate =
-    filter_for_summary astate |> discard_unreachable |> invalidate_locals pdesc
+    let domain = filter_for_summary astate in
+    let domain, _ = discard_unreachable domain in
+    invalidate_locals pdesc domain
 
 
   (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call

infer/src/pulse/PulseAbductiveDomain.mli

@@ -6,6 +6,7 @@
  *)
 open! IStd
 open PulseBasicInterface
+module BaseAddressAttributes = PulseBaseAddressAttributes
 module BaseDomain = PulseBaseDomain
 module BaseMemory = PulseBaseMemory
 module BaseStack = PulseBaseStack
@@ -103,9 +104,9 @@ end
 
 module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t
 
-val discard_unreachable : t -> t
+val discard_unreachable : t -> t * BaseAddressAttributes.t
-(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
+(** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it
-    keep its size down *)
+    smaller, and retuns the new state and the attributes of discarded addresses *)
 
 val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -45,6 +45,8 @@ let empty = Graph.empty
 
 let filter = Graph.filter
 
+let partition = Graph.partition
+
 let pp = Graph.pp
 
 let invalidate (address, history) invalidation location memory =

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -14,6 +14,8 @@ val empty : t
 
 val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t
 
+val partition : (AbstractValue.t -> Attributes.t -> bool) -> t -> t * t
+
 val find_opt : AbstractValue.t -> t -> Attributes.t option
 
 val add_one : AbstractValue.t -> Attribute.t -> t -> t

infer/src/pulse/PulseDiagnostic.ml

@@ -15,12 +15,13 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 let get_location = function
   | AccessToInvalidAddress {access_trace} ->
       Trace.get_outer_location access_trace
-  | StackVariableAddressEscape {location} ->
+  | MemoryLeak {location} | StackVariableAddressEscape {location} ->
       location
 
 
@@ -66,6 +67,20 @@ let get_message = function
       F.asprintf "%a%a" pp_access_trace access_trace
         (pp_invalidation_trace invalidation_line invalidation)
         invalidation_trace
+  | MemoryLeak {location; allocation_trace} ->
+      let allocation_line =
+        let {Location.line; _} = Trace.get_outer_location allocation_trace in
+        line
+      in
+      let pp_allocation_trace fmt (trace : Trace.t) =
+        match trace with
+        | Immediate _ ->
+            F.fprintf fmt "by call to `malloc()`"
+        | ViaCall {f; _} ->
+            F.fprintf fmt "by call to %a" CallEvent.describe f
+      in
+      F.asprintf "memory dynamically allocated at line %d %a, is not reachable after %a"
+        allocation_line pp_allocation_trace allocation_trace Location.pp location
   | StackVariableAddressEscape {variable; _} ->
       let pp_var f var =
         if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@@ -95,6 +110,13 @@ let get_trace = function
            ~pp_immediate:(fun fmt -> F.pp_print_string fmt "invalid access occurs here")
            access_trace
       @@ []
+  | MemoryLeak {allocation_trace} ->
+      let access_start_location = Trace.get_start_location allocation_trace in
+      add_errlog_header ~title:"allocation part of the trace starts here" access_start_location
+      @@ Trace.add_to_errlog ~nesting:0
+           ~pp_immediate:(fun fmt -> F.pp_print_string fmt "allocation occurs here")
+           allocation_trace
+      @@ []
   | StackVariableAddressEscape {history; location; _} ->
       ValueHistory.add_to_errlog ~nesting:0 history
       @@
@@ -105,5 +127,7 @@ let get_trace = function
 let get_issue_type = function
   | AccessToInvalidAddress {invalidation; _} ->
       Invalidation.issue_type_of_cause invalidation
+  | MemoryLeak _ ->
+      IssueType.pulse_memory_leak
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape

infer/src/pulse/PulseDiagnostic.mli

@@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
+  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 val get_message : t -> string

infer/src/pulse/PulseOperations.ml

@@ -468,6 +468,29 @@ 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_attrs location =
+  let check_memory_leak _ attributes result =
+    let allocated_not_freed_opt =
+      Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
+        ~f:(fun acc attr ->
+          match (attr : Attribute.t) with
+          | Allocated trace ->
+              (Some trace, snd acc)
+          | Invalid (CFree, _) ->
+              (fst acc, true)
+          | _ ->
+              acc )
+    in
+    match allocated_not_freed_opt with
+    | Some trace, false ->
+        (* allocated but not freed *)
+        Error (Diagnostic.MemoryLeak {location; allocation_trace= trace})
+    | _ ->
+        result
+  in
+  PulseBaseAddressAttributes.fold check_memory_leak unreachable_attrs (Ok ())
+
+
 let remove_vars vars location astate =
   let astate =
     List.fold vars ~init:astate ~f:(fun astate var ->
@@ -485,7 +508,11 @@ let remove_vars vars location astate =
             astate )
   in
   let astate' = Stack.remove_vars vars astate in
-  if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate'
+  if phys_equal astate' astate then Ok astate
+  else
+    let astate, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in
+    let+ () = check_memory_leak_unreachable unreachable_attrs location in
+    astate
 
 
 let is_ptr_to_const formal_typ_opt =

infer/src/pulse/PulseOperations.mli

@@ -99,7 +99,7 @@ val shallow_copy :
   -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** returns the address of a new cell with the same edges as the original *)
 
-val remove_vars : Var.t list -> Location.t -> t -> t
+val remove_vars : Var.t list -> Location.t -> t -> t access_result
 
 val check_address_escape :
   Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -0,0 +1,3 @@
+codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocation occurs here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here]

infer/tests/codetoanalyze/c/pulse/memory_leak.c

@@ -6,9 +6,7 @@
  */
 #include <stdlib.h>
 
-void malloc_no_free_bad() { // TODO implement the check
+void malloc_no_free_bad() { int* p = malloc(sizeof(p)); }
-  int* p = malloc(sizeof(p));
-}
 
 int* malloc_returned_ok() {
   int* p = malloc(sizeof(p));
@@ -20,3 +18,17 @@ void malloc_then_free_ok() {
   *p = 5;
   free(p);
 }
+
+int* create_p() {
+  int* p = malloc(sizeof(p));
+  return p;
+}
+
+void malloc_interproc_no_free_bad() { int* p = create_p(); }
+
+void malloc_interproc_no_free_bad2() {
+  int* p = malloc(sizeof(p));
+  int z = 3;
+  int y = 4;
+  int* q = p;
+}