diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 58954264a..903ea68d8 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -322,7 +322,9 @@ module StdBasicString = struct let call_event = ValueHistory.Call {f= model; location; in_call= []} in let* astate, (string_addr, string_hist) = to_internal_string location this_hist astate in let string_addr_hist = (string_addr, call_event :: string_hist) in - let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in + let* astate = + PulseOperations.invalidate_access location CppDelete string_addr_hist Dereference astate + in let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in [ExecutionDomain.ContinueProgram astate] end @@ -433,7 +435,8 @@ module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate - >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address + >>= PulseOperations.invalidate_access location (StdVector vector_f) vector + GenericArrayBackedCollection.access >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace @@ -523,7 +526,7 @@ module JavaCollection = struct PulseOperations.write_deref location ~ref:new_elem ~obj:(old_addr, ValueHistory.Assignment location :: old_hist) astate - >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem + >>= PulseOperations.invalidate_access location (StdVector Assign) old_elem Dereference in let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in [ExecutionDomain.ContinueProgram astate] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 49a603a1c..58d52f00b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -232,8 +232,8 @@ let invalidate location cause addr_trace astate = >>| AddressAttributes.invalidate addr_trace cause location -let invalidate_deref location cause ref_addr_hist astate = - let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist Dereference astate in +let invalidate_access location cause ref_addr_hist access astate = + let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist access astate in invalidate location cause (addr_obj, snd ref_addr_hist) astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index dcf77d612..a8383324c 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -86,9 +86,14 @@ val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t val remove_allocation_attr : AbstractValue.t -> t -> t -val invalidate_deref : - Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result -(** record that what the address points to is invalid *) +val invalidate_access : + Location.t + -> Invalidation.t + -> AbstractValue.t * ValueHistory.t + -> BaseMemory.Access.t + -> t + -> t access_result +(** record that what the address points via the access to is invalid *) val invalidate_array_elements : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 6a726c298..b98cfa6dd 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -87,7 +87,7 @@ codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucke codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] -codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),passed as argument to `iterator operator*` (modelled),return from call to `iterator operator*` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `iter_begin` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator constructor` (modelled),return from call to `iterator constructor` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_bad, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),passed as argument to `iterator operator*` (modelled),return from call to `iterator operator*` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::begin()` (modelled),return from call to `std::vector::begin()` (modelled),invalid access occurs here]