[pulse] invalidate vector backing array correctly

Summary:
We were invalidating "*(vec.__infer_backing_array)" instead of the
address of the field itself.

Reviewed By: ezgicicek

Differential Revision: D21280357

fbshipit-source-id: 48b984800

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]

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
 
 

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

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]