From c6b2126c3f013f6c4a4fcc6e03c8d037632c26c0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 31 Oct 2018 08:42:33 -0700 Subject: [PATCH] [pulse] forget about addresses that are invalid on only one side of a join Summary: Getting this right will be long and complex so for now the easiest is to underreport and only consider as invalid the addresses we know to be invalid on both sides of a join. In fact the condition for an address to be invalid after a join is more complex than this: it is invalid only if *all* the addresses in its equivalence class as discovered by the join are invalid. Reviewed By: skcho Differential Revision: D12823925 fbshipit-source-id: 2ca109356 --- infer/src/checkers/PulseDomain.ml | 55 ++++++++++++++----- .../tests/codetoanalyze/cpp/pulse/basics.cpp | 8 +-- .../tests/codetoanalyze/cpp/pulse/issues.exp | 17 +----- infer/tests/codetoanalyze/cpp/pulse/join.cpp | 3 +- .../cpp/pulse/use_after_delete.cpp | 12 ++-- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 9 ++- 6 files changed, 60 insertions(+), 44 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 916e1b333..324a1d5df 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -149,14 +149,13 @@ module InvalidAddressesDomain : sig val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option (** None denotes a valid location *) - val map : (AbstractAddress.t -> AbstractAddress.t) -> astate -> astate - (** translate invalid addresses according to the mapping *) + val is_invalid : AbstractAddress.t -> astate -> bool end = struct include AbstractDomain.Map (AbstractAddress) (Invalidation) - let map f invalids = fold (fun key value map -> add (f key) value map) invalids empty - let get_invalidation address invalids = find_opt address invalids + + let is_invalid address invalids = mem address invalids end (** the domain *) @@ -168,7 +167,7 @@ let initial = ; invalids= InvalidAddressesDomain.empty (* TODO: this makes the analysis go a bit overboard with the Nullptr reports. *) - (* (\* always recall that 0 is invalid *\) + (* (* always recall that 0 is invalid *) InvalidAddressesDomain.add AbstractAddress.nullptr Nullptr InvalidAddressesDomain.empty *) } @@ -201,11 +200,7 @@ module Domain : AbstractDomain.S with type astate = t = struct let compare_size _ _ = 0 - let merge ~from ~to_ = - (* building the actual set is only useful to display what equalities where discovered in the - HTML debug output *) - if Config.debug_mode then to_ := Set.union !from !to_ - + let merge ~from ~to_ = to_ := Set.union !from !to_ let pp f x = Set.pp f !x end @@ -290,6 +285,42 @@ module Domain : AbstractDomain.S with type astate = t = struct {subst; astate= {heap; stack; invalids}} + (** compute new set of invalid addresses for a given join state *) + let to_invalids {subst; astate= {invalids= old_invalids}} = + (* iterate over all discovered equivalence classes *) + AddressUF.fold_sets subst ~init:InvalidAddressesDomain.empty + ~f:(fun new_invalids (repr, set) -> + (* Add [repr] as an invalid address if *all* the addresses it represents were known to + be invalid. This is unsound but avoids false positives for now. *) + if + AddressUnionSet.Set.for_all + (fun addr -> InvalidAddressesDomain.is_invalid addr old_invalids) + !set + then + (* join the invalidation reasons for all the invalidations of the representative *) + let reason = + AddressUnionSet.Set.fold + (fun address reason -> + (* this is safe because of [for_all] above *) + let reason' = + Option.value_exn (InvalidAddressesDomain.get_invalidation address old_invalids) + in + match reason with + | None -> + Some reason' + | Some reason -> + Some (Invalidation.join reason reason') ) + !set None + in + InvalidAddressesDomain.add + (repr :> AbstractAddress.t) + ((* safe because [!set] cannot be empty so there is at least one address to join from + *) + Option.value_exn reason) + new_invalids + else new_invalids ) + + let rec normalize state = let one_addr subst addr edges heap_has_converged = Memory.Edges.fold @@ -314,9 +345,7 @@ module Domain : AbstractDomain.S with type astate = t = struct AddressUnionSet.pp set ) ; L.d_decrease_indent () ; let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in - let invalids = - InvalidAddressesDomain.map (to_canonical_address state.subst) state.astate.invalids - in + let invalids = to_invalids state in {heap; stack; invalids} ) else normalize {state with astate= {state.astate with heap}} end diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp index 78e2ce3b0..1fcb3d6ba 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp @@ -14,7 +14,7 @@ struct Aggregate { ~Aggregate() {} }; -void FP_aggregate_reassign_ok() { +void aggregate_reassign_ok() { const int len = 5; Aggregate arr[len]; for (int i = 0; i < len; i++) { @@ -29,7 +29,7 @@ struct AggregateWithConstructedField { std::string str; }; -void FP_aggregate_reassign2_ok() { +void aggregate_reassign2_ok() { AggregateWithConstructedField arr[10]; for (int i = 0; i < 10; i++) { // this is translated as string(&(a.str), "hi"). need to make sure this is @@ -43,7 +43,7 @@ struct NestedAggregate { AggregateWithConstructedField a; }; -void FP_aggregate_reassign3_ok() { +void aggregate_reassign3_ok() { NestedAggregate arr[10]; for (int i = 0; i < 10; i++) { // this is translated as std::basic_string(&(a.str), "hi"). need to make @@ -62,7 +62,7 @@ int multiple_invalidations_branch_bad(int n, int* ptr) { return *ptr; } -int multiple_invalidations_loop_bad(int n, int* ptr) { +int FN_multiple_invalidations_loop_bad(int n, int* ptr) { for (int i = 0; i < n; i++) { if (i == 7) { delete ptr; diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 2b0796cd8..b4d844dad 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,16 +1,6 @@ -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(a)` at line 39, column 3 here,accessed `a.str` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(a)` at line 53, column 3 here,accessed `a.a.str` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(s)` at line 25, column 3 here,accessed `s.i` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 26, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `*(v.__internal_array)[_]` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 112, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 130, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_exit_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 121, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here] @@ -24,9 +14,6 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing2_bad, 5 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 185, column 3 here,accessed `pc->f` 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, column 3 here,accessed `*(x)` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 56, column 5 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_push_back_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 31, column 5 here,accessed `*(vec.__internal_array)[_]` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_loop_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 47, column 5 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 38, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/join.cpp b/infer/tests/codetoanalyze/cpp/pulse/join.cpp index c5f3d57a0..a223c1491 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/join.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/join.cpp @@ -13,7 +13,7 @@ struct list { struct foo* foo; }; -int visit_list(struct list* head, int cond) { +int invalidate_node_alias_bad(struct list* head, int cond) { int* result = 0; struct list* x = head; if (cond) { @@ -23,6 +23,7 @@ int visit_list(struct list* head, int cond) { x = x->next; struct list* y = x->next; result = x->foo->val; + delete result; } return *result; } diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp index 011b6cc9a..7967d3630 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp @@ -51,7 +51,7 @@ void double_delete_bad() { delete s; } -Simple* delete_in_branch_bad(bool b) { +Simple* FN_delete_in_branch_bad(bool b) { auto s = new Simple{1}; if (b) { delete s; @@ -76,7 +76,7 @@ void use_in_branch_bad(bool b) { } } -void delete_in_loop_bad() { +void FN_delete_in_loop_bad() { auto s = new Simple{1}; for (int i = 0; i < 10; i++) { delete s; @@ -90,7 +90,7 @@ void delete_in_loop_ok() { } } -void FP_delete_ref_in_loop_ok(int j, std::vector v) { +void delete_ref_in_loop_ok(int j, std::vector v) { int i = 0; for (int i = 0; i < 10; i++) { auto s = &v[i]; @@ -106,7 +106,7 @@ void use_in_loop_bad() { } } -Simple* FP_gated_delete_abort_ok(bool b) { +Simple* gated_delete_abort_ok(bool b) { auto s = new Simple{1}; if (b) { delete s; @@ -115,7 +115,7 @@ Simple* FP_gated_delete_abort_ok(bool b) { return s; } -Simple* FP_gated_exit_abort_ok(bool b) { +Simple* gated_exit_abort_ok(bool b) { auto s = new Simple{1}; if (b) { delete s; @@ -124,7 +124,7 @@ Simple* FP_gated_exit_abort_ok(bool b) { return s; } -Simple* FP_gated_delete_throw_ok(bool b) { +Simple* gated_delete_throw_ok(bool b) { auto s = new Simple{1}; if (b) { delete s; diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 4b490a092..e653c0e7d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -25,8 +25,7 @@ void two_push_back_ok(std::vector& vec) { vec.push_back(52); } -void FP_push_back_in_loop_ok(std::vector& vec, - std::vector& vec_other) { +void push_back_in_loop_ok(std::vector& vec, std::vector& vec_other) { for (const auto& i : vec_other) { vec.push_back(i); } @@ -39,8 +38,8 @@ void FP_reserve_then_push_back_ok(std::vector& vec) { std::cout << *elt << "\n"; } -void FP_reserve_then_push_back_loop_ok(std::vector& vec, - std::vector& vec_other) { +void reserve_then_push_back_loop_ok(std::vector& vec, + std::vector& vec_other) { vec.reserve(vec.size() + vec_other.size()); int* elt = &vec[1]; for (const auto& i : vec_other) { @@ -49,7 +48,7 @@ void FP_reserve_then_push_back_loop_ok(std::vector& vec, std::cout << *elt << "\n"; } -void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { +void init_fill_then_push_back_loop_ok(std::vector& vec_other) { std::vector vec(vec_other.size()); int* elt = &vec[1]; for (const auto& i : vec_other) {