[pulse] Modeling std::vector::end()

Summary:
It is undefined behavior to dereference end iterator.

To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself.

Reviewed By: ezgicicek

Differential Revision: D21178441

fbshipit-source-id: fd6a94b0b

infer/src/pulse/PulseInvalidation.ml

@@ -45,6 +45,7 @@ type t =
   | CFree
   | ConstantDereference of IntLit.t
   | CppDelete
+  | EndIterator
   | GoneOutOfScope of Pvar.t * Typ.t
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function
@@ -59,6 +60,8 @@ let issue_type_of_cause = function
       IssueType.constant_address_dereference
   | CppDelete ->
       IssueType.use_after_delete
+  | EndIterator ->
+      IssueType.vector_invalidation
   | GoneOutOfScope _ ->
       IssueType.use_after_lifetime
   | JavaIterator _ | StdVector _ ->
@@ -75,6 +78,8 @@ let describe f cause =
       F.fprintf f "is the constant %a" IntLit.pp i
   | CppDelete ->
       F.pp_print_string f "was invalidated by `delete`"
+  | EndIterator ->
+      F.pp_print_string f "is pointed to by the `end()` iterator"
   | GoneOutOfScope (pvar, typ) ->
       let pp_var f pvar =
         if Pvar.is_cpp_temporary pvar then
@@ -96,7 +101,7 @@ let pp f invalidation =
       F.fprintf f "ConstantDereference(%a)" describe invalidation
   | CppDelete ->
       F.fprintf f "CppDelete(%a)" describe invalidation
-  | GoneOutOfScope _ ->
+  | EndIterator | GoneOutOfScope _ ->
       describe f invalidation
   | StdVector _ ->
       F.fprintf f "StdVector(%a)" describe invalidation

infer/src/pulse/PulseInvalidation.mli

@@ -27,6 +27,7 @@ type t =
   | CFree
   | ConstantDereference of IntLit.t
   | CppDelete
+  | EndIterator
   | GoneOutOfScope of Pvar.t * Typ.t
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function

infer/src/pulse/PulseModels.ml

@@ -381,6 +381,14 @@ module GenericArrayBackedCollectionIterator = struct
     PulseOperations.eval_access location iterator internal_pointer_access astate
 
 
+  let to_internal_pointer_deref location iterator astate =
+    let* astate, pointer = to_internal_pointer location iterator astate in
+    let* astate, index = PulseOperations.eval_access location pointer Dereference astate in
+    (* We do not want to create internal array if iterator pointer has an invalid value *)
+    let+ astate = PulseOperations.check_addr_access location index astate in
+    (astate, pointer, fst index, snd pointer)
+
+
   let construct location event ~init ~ref astate =
     let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in
     let* astate =
@@ -400,28 +408,26 @@ module GenericArrayBackedCollectionIterator = struct
 
   let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, (iter_index_addr, iter_index_hist) = to_internal_pointer location iter astate in
+    let* astate, _, index, hist = to_internal_pointer_deref location iter astate in
-    let+ astate, (elem_val, _) =
+    let+ astate, (elem, _) = GenericArrayBackedCollection.element location iter index astate in
-      GenericArrayBackedCollection.element location iter iter_index_addr astate
+    let astate = PulseOperations.write_id (fst ret) (elem, event :: hist) astate in
-    in
-    let astate = PulseOperations.write_id (fst ret) (elem_val, event :: iter_index_hist) astate in
     [ExecutionDomain.ContinueProgram astate]
 
 
   let operator_plus_plus ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let index_next = AbstractValue.mk_fresh () in
-    let* astate, (current_index, current_index_hist) = to_internal_pointer location iter astate in
+    let* astate, pointer, current_index_addr, hist =
+      to_internal_pointer_deref location iter astate
+    in
     let* astate, element =
-      GenericArrayBackedCollection.element location iter current_index astate
+      GenericArrayBackedCollection.element location iter current_index_addr astate
     in
     (* Iterator is invalid if the value it points to is invalid *)
     let* astate, _ =
-      PulseOperations.eval_access location (fst element, current_index_hist) Dereference astate
+      PulseOperations.eval_access location (fst element, event :: hist) Dereference astate
     in
-    PulseOperations.write_field location ~ref:iter internal_pointer
+    PulseOperations.write_deref location ~ref:pointer ~obj:(index_next, event :: hist) astate
-      ~obj:(index_next, event :: current_index_hist)
-      astate
     >>| ExecutionDomain.continue >>| List.return
 end
 
@@ -525,6 +531,8 @@ module StdVector = struct
   let vector_begin vector iter : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in
+    let pointer_hist = event :: snd iter in
+    let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in
     let index_zero = AbstractValue.mk_fresh () in
     let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
     let* astate, ((arr_addr, _) as arr) =
@@ -532,14 +540,36 @@ module StdVector = struct
     in
     let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in
     PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
-      ~obj:(arr_addr, event :: snd iter)
+      ~obj:(arr_addr, pointer_hist) astate
-      astate
     >>= PulseOperations.write_field location ~ref:iter
-          GenericArrayBackedCollectionIterator.internal_pointer
+          GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val
-          ~obj:(index_zero, event :: snd iter)
+    >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist)
     >>| ExecutionDomain.continue >>| List.return
 
 
+  let vector_end vector iter : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in
+    let pointer_addr = AbstractValue.mk_fresh () in
+    let pointer_hist = event :: snd iter in
+    let pointer_val = (pointer_addr, pointer_hist) in
+    let index_last = AbstractValue.mk_fresh () in
+    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval location vector astate in
+    let* astate =
+      PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
+        ~obj:(arr_addr, pointer_hist) astate
+    in
+    let* astate =
+      PulseOperations.write_field location ~ref:iter
+        GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val astate
+    in
+    let* astate =
+      PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_last, pointer_hist) astate
+    in
+    let+ astate = PulseOperations.invalidate location EndIterator (index_last, []) astate in
+    [ExecutionDomain.ContinueProgram astate]
+
+
   let reserve vector : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
@@ -666,6 +696,8 @@ module ProcNameDispatcher = struct
         $--> StdVector.at ~desc:"std::vector::at()"
       ; -"std" &:: "vector" &:: "begin" <>$ capt_arg_payload $+ capt_arg_payload
         $--> StdVector.vector_begin
+      ; -"std" &:: "vector" &:: "end" <>$ capt_arg_payload $+ capt_arg_payload
+        $--> StdVector.vector_end
       ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload
         $--> StdVector.invalidate_references Clear
       ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload

infer/src/pulse/PulseOperations.ml

@@ -16,7 +16,6 @@ type 'a access_result = ('a, Diagnostic.t * t) result
 
 let ok_continue post = Ok [ExecutionDomain.ContinueProgram post]
 
-(** Check that the [address] is not known to be invalid *)
 let check_addr_access location (address, history) astate =
   let access_trace = Trace.Immediate {location; history} in
   AddressAttributes.check_valid access_trace address astate

infer/src/pulse/PulseOperations.mli

@@ -15,6 +15,9 @@ type 'a access_result = ('a, Diagnostic.t * t) result
 
 val ok_continue : t -> (ExecutionDomain.t list, 'a) result
 
+val check_addr_access : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
+(** Check that the [address] is not known to be invalid *)
+
 module Closures : sig
   val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result
   (** assert the validity of the addresses captured by the lambda *)

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

@@ -32,5 +32,5 @@ codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_buc
 codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec` modified here]
 codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` modified here]
 codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec` modified here]
-codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec_other` modified here,parameter `vec` modified here,call to skipped function std::vector<int,std::allocator<int>>::end occurs here]
+codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec` modified here]
-codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` modified here,call to skipped function std::vector<A,std::allocator<A>>::end occurs here]
+codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` modified here]

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

@@ -88,6 +88,7 @@ codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION,
 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),invalid access occurs here]
+codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_end_read_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,is pointed to by the `end()` iterator,use-after-lifetime part of the trace starts here,variable `iter` declared here,passed as argument to `std::vector::end()` (modelled),return from call to `std::vector::end()` (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),invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp

@@ -64,3 +64,26 @@ void FN_iterator_empty_vector_read_bad() {
   auto iter = vec.begin();
   std::cout << *iter << '\n';
 }
+
+void iterator_end_read_bad() {
+  std::vector<int> vec = {1, 2};
+  auto iter = vec.end();
+  std::cout << *iter << '\n';
+}
+
+bool for_each_ok(std::vector<int>& vec, bool b) {
+  int res = 0;
+  for (const auto& elem : vec) {
+    res += 0;
+  }
+  return b;
+}
+
+void call_iterator_loop_ok(bool b) {
+  std::vector<int> vec;
+  bool finished = false;
+  while (!finished) {
+    if (!for_each_ok(vec, b))
+      return;
+  }
+}