[pulse] Revise F14 iterator operator++ model as unknown call

Summary:
This diff revises the F14 iterator's `operator++` model as unknown call, so that the iterator points
to a different value after `++`. Before this diff, the semantics was `skip`, which introduced a FP
of use after delete because the iterator pointed to the same element in the loop deleting elements.

Reviewed By: rgrig

Differential Revision: D52659360

fbshipit-source-id: adcf71792f8835688cc1a9f3f72dec51d9786a1c

infer/src/pulse/PulseModelsCpp.ml

@@ -1032,8 +1032,9 @@ let map_matchers =
         ; -"folly" <>:: "f14" <>:: "detail" <>:: it &:: "operator*" <>$ capt_arg_payload
           $--> GenericMapCollection.iterator_star
                  (Format.asprintf "folly::f14::detail::%s::operator*" it)
-        ; -"folly" <>:: "f14" <>:: "detail" <>:: it &:: "operator++" <>$ any_arg
-          $+...$--> Basic.skip |> with_non_disj ] )
+        ; -"folly" <>:: "f14" <>:: "detail" <>:: it &:: "operator++"
+          &++> Basic.unknown_call "folly::f14::detail::it::operator++"
+          |> with_non_disj ] )
   in
   let folly_concurrent_hash_map_matchers =
     (* We ignore all [folly::ConcurrentHashMap] methods as of now, because the summaries from the

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

@@ -210,13 +210,11 @@ codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_big_find_arrow_ba
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_big_find_star_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_big_find_star_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_big_find_star_bad,in call to `folly::F14FastMap::find` (modelled),in call to `folly::f14::detail::VectorContainerIterator::operator*` (modelled),assigned,when calling `BigPoint::BigPoint` here,parameter `__param_0` of BigPoint::BigPoint,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_begin_bad, 3, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_begin_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_begin_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_cbegin_bad, 3, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_cbegin_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_cbegin_bad,in call to `folly::F14FastMap::cbegin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_iterator_increment_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_iterator_increment_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_iterator_increment_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, iterator_copy_constructor_bad, 4, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of iterator_copy_constructor_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of iterator_copy_constructor_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, iterator_copy_operator_equal_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of iterator_copy_operator_equal_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of iterator_copy_operator_equal_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator=` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, reserve_operator_bracket_ok_FP, 4, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, use_emplace_iterator_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of use_emplace_iterator_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::emplace` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, known_existing_map_key_literal_ok_FP, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of known_existing_map_key_literal_ok_FP,was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,parameter `map` of known_existing_map_key_literal_ok_FP,in call to `folly::F14FastMap::at` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_stability.cpp, delete_in_loop_ok_FP, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of delete_in_loop_ok_FP,assigned,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator*` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `map` of delete_in_loop_ok_FP,assigned,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator*` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_assign_struct_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `BigPoint::operator=` here,parameter `this` of BigPoint::operator=,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_operation_struct_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `operator+` here,parameter `a` of operator+,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_function_call_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `mul` here,parameter `a` of mul,invalid access occurs here]

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

@@ -223,13 +223,11 @@ codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_big_find_arrow_ba
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_big_find_star_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_big_find_star_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_big_find_star_bad,in call to `folly::F14FastMap::find` (modelled),in call to `folly::f14::detail::VectorContainerIterator::VectorContainerIterator` (modelled),in call to `folly::f14::detail::VectorContainerIterator::operator*` (modelled),assigned,when calling `BigPoint::BigPoint` here,parameter `__param_0` of BigPoint::BigPoint,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_begin_bad, 3, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_begin_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_begin_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_cbegin_bad, 3, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_cbegin_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_cbegin_bad,in call to `folly::F14FastMap::cbegin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_stability.cpp, folly_fastmap_iterator_increment_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of folly_fastmap_iterator_increment_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of folly_fastmap_iterator_increment_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, iterator_copy_constructor_bad, 4, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of iterator_copy_constructor_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of iterator_copy_constructor_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, iterator_copy_operator_equal_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of iterator_copy_operator_equal_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,parameter `map` of iterator_copy_operator_equal_bad,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator=` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, reserve_operator_bracket_ok_FP, 4, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, use_emplace_iterator_bad, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of use_emplace_iterator_bad,was potentially invalidated by `folly::F14FastMap::clear`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::emplace` (modelled),variable `C++ temporary` accessed here,in call to `std::pair<folly::f14::detail::ValueContainerIterator<std::pair<int const ,int>*>,_Bool>::pair`,macro expanded here,parameter `__param_0` of std::pair<folly::f14::detail::ValueContainerIterator<std::pair<int const ,int>*>,_Bool>::pair,in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),return from call to `std::pair<folly::f14::detail::ValueContainerIterator<std::pair<int const ,int>*>,_Bool>::pair`,in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator->` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, known_existing_map_key_literal_ok_FP, 5, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of known_existing_map_key_literal_ok_FP,was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,parameter `map` of known_existing_map_key_literal_ok_FP,in call to `folly::F14FastMap::at` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_stability.cpp, delete_in_loop_ok_FP, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `map` of delete_in_loop_ok_FP,assigned,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator*` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `map` of delete_in_loop_ok_FP,assigned,in call to `folly::F14FastMap::begin` (modelled),in call to `folly::f14::detail::ValueContainerIterator::ValueContainerIterator` (modelled),in call to `folly::f14::detail::ValueContainerIterator::operator*` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_assign_struct_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `BigPoint::operator=` here,parameter `this` of BigPoint::operator=,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_operation_struct_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `operator+` here,parameter `a` of operator+,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_stability.cpp, unsafe_function_call_bad, 1, PULSE_REFERENCE_STABILITY, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),was potentially invalidated by `folly::F14FastMap::operator[]`,use-after-lifetime part of the trace starts here,in call to `folly::F14FastMap::operator[]` (modelled),when calling `mul` here,parameter `a` of mul,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/reference_stability.cpp

@@ -646,7 +646,7 @@ void folly_fastmap_cbegin_bad(folly::F14FastMap<int, int>& map) {
   const auto keyCopy = it->first;
 }
 
-void folly_fastmap_iterator_increment_bad(folly::F14FastMap<int, int>& map) {
+void folly_fastmap_iterator_increment_bad_FN(folly::F14FastMap<int, int>& map) {
   auto it = map.begin();
   ++it;
   const auto& valueRef = it->second;
@@ -746,8 +746,7 @@ void known_existing_map_key_literal_ok_FP(folly::F14FastMap<int, int>& map) {
   const auto valueCopy = valueRef;
 }
 
-// False positive for USE_AFTER_DELETE.
-void delete_in_loop_ok_FP(folly::F14FastMap<int, int*>& map) {
+void delete_in_loop_ok(folly::F14FastMap<int, int*>& map) {
   for (auto& it : map) {
     delete it.second;
   }