[pulse] collect garbage (unreachable) heap parts from time to time

Summary:
It's useful to keep the size of states down, especially when humans are
trying to read it. It will also help keep the size of summaries down in
the inter-procedural pulse.

Reviewed By: mbouaziz

Differential Revision: D14258486

fbshipit-source-id: 45ebcac67

infer/src/checkers/PulseDomain.ml

@@ -88,6 +88,8 @@ module Memory : sig
 
   val empty : t
 
+  val filter : (AbstractAddress.t -> cell -> bool) -> t -> t
+
   val find_opt : AbstractAddress.t -> t -> cell option
 
   val for_all : (AbstractAddress.t -> cell -> bool) -> t -> bool
@@ -212,6 +214,8 @@ end = struct
   let find_opt = Graph.find_opt
 
   let for_all = Graph.for_all
+
+  let filter = Graph.filter
 end
 
 (** Stacks: map addresses of variables to values and initialisation location.
@@ -297,3 +301,62 @@ let widen ~prev:_ ~next:_ ~num_iters:_ =
 
 let pp fmt {heap; stack} =
   F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@]}" Memory.pp heap Stack.pp stack
+
+
+module GraphGC : sig
+  val minimize : t -> t
+  (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable
+     from the stack variables, then removes all the unused addresses from the heap *)
+end = struct
+  module AddressSet = PrettyPrintable.MakePPSet (AbstractAddress)
+
+  let visit address visited =
+    if AddressSet.mem address visited then `AlreadyVisited
+    else
+      let visited = AddressSet.add address visited in
+      `NotAlreadyVisited visited
+
+
+  let rec visit_address astate address visited =
+    match visit address visited with
+    | `AlreadyVisited ->
+        visited
+    | `NotAlreadyVisited visited -> (
+      match Memory.find_opt address astate.heap with
+      | None ->
+          visited
+      | Some (edges, attrs) ->
+          visit_edges astate ~edges visited |> visit_attributes astate attrs )
+
+
+  and visit_edges ~edges astate visited =
+    Memory.Edges.fold
+      (fun _access (address, _trace) visited -> visit_address astate address visited)
+      edges visited
+
+
+  and visit_attributes astate attrs visited =
+    Attributes.fold
+      (fun attr visited ->
+        match attr with
+        | Attribute.Invalid _ | Attribute.AddressOfCppTemporary _ | Attribute.StdVectorReserve ->
+            visited
+        | Attribute.Closure (_, captured) ->
+            List.fold captured ~init:visited ~f:(fun visited (address, _) ->
+                visit_address astate address visited ) )
+      attrs visited
+
+
+  let visit_stack astate visited =
+    Stack.fold
+      (fun _var (address, _loc) visited -> visit_address astate address visited)
+      astate.stack visited
+
+
+  let minimize astate =
+    let visited = visit_stack astate AddressSet.empty in
+    let heap = Memory.filter (fun address _ -> AddressSet.mem address visited) astate.heap in
+    if phys_equal heap astate.heap then astate else {astate with heap}
+end
+
+include GraphGC

infer/src/checkers/PulseDomain.mli

@@ -83,3 +83,5 @@ type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 val initial : t
 
 include AbstractDomain.S with type t := t
+
+val minimize : t -> t

infer/src/checkers/PulseOperations.ml

@@ -278,8 +278,9 @@ let remove_vars vars astate =
         | _ ->
             heap )
   in
-  let stack = List.fold ~f:(fun stack var -> Stack.remove var stack) ~init:astate.stack vars in
-  if phys_equal stack astate.stack && phys_equal heap astate.heap then astate else {stack; heap}
+  let stack = Stack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars var)) astate.stack in
+  if phys_equal stack astate.stack && phys_equal heap astate.heap then astate
+  else PulseDomain.minimize {stack; heap}
 
 
 let record_var_decl_location location var astate =

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

@@ -25,13 +25,14 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 125 here,accessed `&(this->x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 84 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 78 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 134 here,accessed `&(this->x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 93 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 87 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace_back(vec, ..)` at line 108 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace(vec, ..)` at line 102 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 96 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 72 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 90 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace_back(vec, ..)` at line 117 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace(vec, ..)` at line 111 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 105 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 74 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 81 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 99 here,accessed `*(elt)` here]

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -67,6 +67,15 @@ void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
   std::cout << *elt << "\n";
 }
 
+void push_back_loop_bad(std::vector<int>& vec_other) {
+  std::vector<int> vec(2);
+  int* elt = &vec[1];
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+  std::cout << *elt << "\n";
+}
+
 void reserve_bad(std::vector<int>& vec) {
   int* elt = &vec[1];
   vec.reserve(vec.size() + 1);