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) {