From 44007f054c6cfc31a33082bc4cc391e933a51394 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 5 Mar 2019 09:34:23 -0800 Subject: [PATCH] [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 | 63 +++++++++++++++++++ infer/src/checkers/PulseDomain.mli | 2 + infer/src/checkers/PulseOperations.ml | 5 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 17 ++--- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 9 +++ 5 files changed, 86 insertions(+), 10 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 1ef108c01..d9c9ae9f0 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 "{@[ heap=@[%a@];@;stack=@[%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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 03ec5191f..07fa7b48c 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/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 diff --git a/infer/src/checkers/PulseOperations.ml b/infer/src/checkers/PulseOperations.ml index 177809163..d6e106a60 100644 --- a/infer/src/checkers/PulseOperations.ml +++ b/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 = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 385b21a16..379f2ef66 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 0d9f9b22f..91e405314 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -67,6 +67,15 @@ void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { std::cout << *elt << "\n"; } +void push_back_loop_bad(std::vector& vec_other) { + std::vector 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& vec) { int* elt = &vec[1]; vec.reserve(vec.size() + 1);