[pulse] Vector iterator model

Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array.

Reviewed By: ezgicicek

Differential Revision: D21043304

fbshipit-source-id: db3be49ce

infer/src/pulse/PulseModels.ml

@@ -349,31 +349,88 @@ module StdFunction = struct
           ~formals_opt:None astate
 end
 
-module StdVector = struct
-  let internal_array =
+module GenericArrayBackedCollection = struct
+  let field =
     Fieldname.make
-      (Typ.CStruct (QualifiedCppName.of_list ["std"; "vector"]))
+      (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"]))
       "__infer_model_backing_array"
 
 
-  let internal_array_access = HilExp.Access.FieldAccess internal_array
+  let access = HilExp.Access.FieldAccess field
+
+  let eval location collection astate =
+    PulseOperations.eval_access location collection access astate
+
+
+  let eval_element location internal_array index astate =
+    PulseOperations.eval_access location internal_array (ArrayAccess (Typ.void, index)) astate
+
+
+  let element location collection index astate =
+    let* astate, internal_array = eval location collection astate in
+    eval_element location internal_array index astate
+end
+
+module GenericArrayBackedCollectionIterator = struct
+  let internal_pointer =
+    Fieldname.make
+      (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"]))
+      "__infer_model_backing_pointer"
+
 
-  let to_internal_array location vector astate =
-    PulseOperations.eval_access location vector internal_array_access astate
+  let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer
 
+  let to_internal_pointer location iterator astate =
+    PulseOperations.eval_access location iterator internal_pointer_access astate
 
-  let element_of_internal_array location vector index astate =
-    let* astate, vector_internal_array = to_internal_array location vector astate in
-    PulseOperations.eval_access location vector_internal_array
-      (ArrayAccess (Typ.void, index))
+
+  let constructor ~desc this init : model =
+   fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in
+    let* astate =
+      PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field
+        ~obj:(arr_addr, event :: arr_hist)
+        astate
+    in
+    let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in
+    PulseOperations.write_field location ~ref:this internal_pointer
+      ~obj:(p_addr, event :: p_hist)
       astate
+    >>| ExecutionDomain.continue >>| List.return
 
 
+  let operator_star ~desc iter ~caller_summary:_ ~callee_procname:_ location ~ret astate =
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let* astate, iter_index = to_internal_pointer location iter astate in
+    let+ astate, (elem_val, elem_hist) =
+      GenericArrayBackedCollection.element location iter (fst iter_index) astate
+    in
+    let astate = PulseOperations.write_id (fst ret) (elem_val, event :: elem_hist) astate in
+    [ExecutionDomain.ContinueProgram astate]
+
+
+  let operator_plus_plus ~desc iter ~caller_summary:_ ~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 = to_internal_pointer location iter astate in
+    let* astate, element =
+      GenericArrayBackedCollection.element location iter (fst current_index) astate
+    in
+    (* Iterator is invalid if the value it points to is invalid *)
+    let* astate, _ = PulseOperations.eval_access location element Dereference astate in
+    PulseOperations.write_field location ~ref:iter internal_pointer
+      ~obj:(index_next, [event])
+      astate
+    >>| ExecutionDomain.continue >>| List.return
+end
+
+module StdVector = struct
   let reallocate_internal_array trace vector vector_f location astate =
-    let* astate, array_address = to_internal_array location vector astate in
+    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.havoc_field location vector internal_array trace
+    >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace
 
 
   let invalidate_references vector_f vector : model =
@@ -391,11 +448,33 @@ module StdVector = struct
   let at ~desc vector index : model =
    fun ~caller_summary:_ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in
+    let+ astate, (addr, hist) =
+      GenericArrayBackedCollection.element location vector (fst index) astate
+    in
     let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in
     [ExecutionDomain.ContinueProgram astate]
 
 
+  let vector_begin vector iter : model =
+   fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
+    let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in
+    let index_zero = AbstractValue.mk_fresh () in
+    let astate =
+      PulseArithmetic.and_eq_int (Immediate {location; history= []}) index_zero IntLit.zero astate
+    in
+    let* astate, ((arr_addr, hist) as arr) =
+      GenericArrayBackedCollection.eval location vector astate
+    in
+    let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in
+    PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
+      ~obj:(arr_addr, event :: hist)
+      astate
+    >>= PulseOperations.write_field location ~ref:iter
+          GenericArrayBackedCollectionIterator.internal_pointer
+          ~obj:(index_zero, [event])
+    >>| ExecutionDomain.continue >>| List.return
+
+
   let reserve vector : model =
    fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
@@ -422,7 +501,7 @@ module JavaCollection = struct
    fun ~caller_summary:_ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in
     let* astate, ((old_addr, old_hist) as old_elem) =
-      StdVector.element_of_internal_array location coll (fst index) astate
+      GenericArrayBackedCollection.element location coll (fst index) astate
     in
     let+ astate =
       PulseOperations.write_deref location ~ref:new_elem
@@ -497,10 +576,25 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "integral_constant" < any_typ &+ capt_int
         >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
         <>--> Misc.return_int
+      ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload
+        $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
+      ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
+      ; -"std" &:: "__wrap_iter" &:: "operator++" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_plus_plus ~desc:"iterator operator++"
+      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "__normal_iterator" <>$ capt_arg_payload
+        $+ capt_arg_payload
+        $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
+      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator*" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
+      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator++" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_plus_plus ~desc:"iterator operator++"
       ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload
         $+...$--> StdVector.invalidate_references Assign
       ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload
         $--> StdVector.at ~desc:"std::vector::at()"
+      ; -"std" &:: "vector" &:: "begin" <>$ capt_arg_payload $+ capt_arg_payload
+        $--> StdVector.vector_begin
       ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload
         $--> StdVector.invalidate_references Clear
       ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload

infer/src/pulse/PulseOperations.ml

@@ -214,12 +214,12 @@ let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
   write_access location addr_trace_ref Dereference addr_trace_obj astate
 
 
-let write_field location addr_trace_ref field addr_trace_obj astate =
+let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate =
   write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate
 
 
 let havoc_field location addr_trace field trace_obj astate =
-  write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate
+  write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate
 
 
 let allocate procname location addr_trace astate =

infer/src/pulse/PulseOperations.mli

@@ -61,6 +61,15 @@ val realloc_pvar : Pvar.t -> Location.t -> t -> t
 
 val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
+val write_field :
+     Location.t
+  -> ref:AbstractValue.t * ValueHistory.t
+  -> Fieldname.t
+  -> obj:AbstractValue.t * ValueHistory.t
+  -> t
+  -> t access_result
+(** write the edge [ref --.field--> obj] *)
+
 val write_deref :
      Location.t
   -> ref:AbstractValue.t * ValueHistory.t

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

@@ -30,7 +30,7 @@ codetoanalyze/cpp/impurity/unmodeled.cpp, output_stream_impure, 0, IMPURE_FUNCTI
 codetoanalyze/cpp/impurity/unmodeled.cpp, random_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function random_impure,call to skipped function rand occurs here]
 codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` modified here]
 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,call to skipped function std::vector<int,std::allocator<int>>::begin occurs 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>>::begin occurs here,call to skipped function std::vector<int,std::allocator<int>>::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,call to skipped function std::vector<A,std::allocator<A>>::begin occurs here,call to skipped function std::vector<A,std::allocator<A>>::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_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, 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]

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

@@ -87,3 +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 `vec` declared here,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_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,parameter `vec` of iterator_next_after_emplace_bad,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,parameter `vec` of iterator_next_after_emplace_loop_bad,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,parameter `vec` of iterator_read_after_emplace_bad,passed as argument to `iterator operator*` (modelled),return from call to `iterator operator*` (modelled),invalid access occurs here]

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

@@ -0,0 +1,66 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <iostream>
+#include <vector>
+
+void iterator_read_after_emplace_bad(std::vector<int>& vec) {
+  auto iter = vec.begin();
+  vec.emplace(iter, 4);
+  std::cout << *iter << '\n';
+}
+
+void iterator_next_after_emplace_bad(std::vector<int>& vec) {
+  auto iter = vec.begin();
+  vec.emplace(iter, 4);
+  ++iter;
+  std::cout << *iter << '\n';
+}
+
+void another_iterator_ok(std::vector<int>& vec) {
+  auto iter = vec.begin();
+  vec.emplace(iter, 4);
+  auto another_iter = vec.begin();
+  std::cout << *another_iter << '\n';
+  ++another_iter;
+  std::cout << *another_iter << '\n';
+}
+
+void read_iterator_loop_ok(std::vector<int>& vec) {
+  int sum = 0;
+  for (auto iter = vec.begin(); iter != vec.end(); ++iter) {
+    sum += *iter;
+  }
+}
+
+void iterator_next_after_emplace_loop_bad(std::vector<int>& vec) {
+  int sum = 0;
+  for (auto iter = vec.begin(); iter != vec.end(); ++iter) {
+    int elem = *iter;
+    sum += elem;
+    if (elem < 0)
+      vec.emplace(iter, -elem);
+  }
+}
+
+void iterator_after_push_back_loop_bad(std::vector<int>& vec_other) {
+  std::vector<int> vec(2);
+  auto iter_begin = vec.begin();
+  auto iter_end = vec.end();
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+  int sum = 0;
+  for (auto iter = iter_begin; iter != iter_end; ++iter) {
+    sum += *iter;
+  }
+}
+
+void FN_iterator_empty_vector_read_bad() {
+  std::vector<int> vec = {};
+  auto iter = vec.begin();
+  std::cout << *iter << '\n';
+}