[pulse] Model for iterator operator--

Summary: Currently we get false positive if we apply `operator--` to the `end()` iterator. To solve this, we model iterator `operator--` not to raise an error for the `EndIterator` invalidation, but to create a fresh element in the underlying array.

Reviewed By: ezgicicek

Differential Revision: D21476353

fbshipit-source-id: 5c722372e

infer/src/pulse/PulseAbductiveDomain.ml

@@ -225,6 +225,10 @@ module AddressAttributes = struct
     BaseAddressAttributes.is_std_vector_reserved addr (astate.post :> base_domain).attrs
 
 
+  let is_end_iterator addr astate =
+    BaseAddressAttributes.is_end_iterator addr (astate.post :> base_domain).attrs
+
+
   let abduce_and_add value attrs astate =
     Attributes.fold attrs ~init:astate ~f:(fun astate attr ->
         let astate =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -130,6 +130,8 @@ module AddressAttributes : sig
 
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
+  val is_end_iterator : AbstractValue.t -> t -> bool
+
   val is_std_vector_reserved : AbstractValue.t -> t -> bool
 
   val std_vector_reserve : AbstractValue.t -> t -> t

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -94,6 +94,11 @@ let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
 let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory
 
+let is_end_iterator address attrs =
+  let invalid_attrs = get_attribute Attributes.get_invalid address attrs in
+  match invalid_attrs with Some (EndIterator, _) -> true | _ -> false
+
+
 let is_std_vector_reserved address attrs =
   Graph.find_opt address attrs
   |> Option.value_map ~default:false ~f:Attributes.is_std_vector_reserved

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -30,6 +30,8 @@ val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) resul
 
 val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
+val is_end_iterator : AbstractValue.t -> t -> bool
+
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option

infer/src/pulse/PulseModels.ml

@@ -383,10 +383,14 @@ module GenericArrayBackedCollectionIterator = struct
 
   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
+    let+ astate, index = PulseOperations.eval_access location pointer Dereference astate in
+    (astate, pointer, index)
+
+
+  let to_elem_pointed_by_iterator location iterator index astate =
     (* 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* astate = PulseOperations.check_addr_access location index astate in
+    GenericArrayBackedCollection.element location iterator (fst index) astate
 
 
   let construct location event ~init ~ref astate =
@@ -408,26 +412,25 @@ 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, _, index, hist = to_internal_pointer_deref location iter astate in
-    let+ astate, (elem, _) = GenericArrayBackedCollection.element location iter index astate in
-    let astate = PulseOperations.write_id (fst ret) (elem, event :: hist) astate in
+    let* astate, pointer, index = to_internal_pointer_deref location iter astate in
+    let+ astate, (elem, _) = to_elem_pointed_by_iterator location iter index astate in
+    let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in
     [ExecutionDomain.ContinueProgram astate]
 
 
-  let operator_plus_plus ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
+  let operator_step step ~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, pointer, current_index_addr, hist =
-      to_internal_pointer_deref location iter astate
-    in
-    let* astate, element =
-      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, event :: hist) Dereference astate
-    in
-    PulseOperations.write_deref location ~ref:pointer ~obj:(index_next, event :: hist) astate
+    let index_new = AbstractValue.mk_fresh () in
+    let* astate, pointer, current_index = to_internal_pointer_deref location iter astate in
+    let* astate =
+      match (step, AddressAttributes.is_end_iterator (fst current_index) astate) with
+      | `MinusMinus, true ->
+          Ok astate
+      | _ ->
+          let* astate, _ = to_elem_pointed_by_iterator location iter current_index astate in
+          Ok astate
+    in
+    PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate
     >>| ExecutionDomain.continue >>| List.return
 end
 
@@ -682,14 +685,22 @@ module ProcNameDispatcher = struct
       ; -"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++"
+        $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
+               ~desc:"iterator operator++"
+      ; -"std" &:: "__wrap_iter" &:: "operator--" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
+               ~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++"
+        $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
+               ~desc:"iterator operator++"
+      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator--" <>$ capt_arg_payload
+        $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
+               ~desc:"iterator operator--"
       ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload
         $+...$--> StdVector.invalidate_references Assign
       ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload

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

@@ -91,4 +91,5 @@ codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad,
 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_prev_after_emplace_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_prev_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_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

@@ -71,6 +71,26 @@ void iterator_end_read_bad() {
   std::cout << *iter << '\n';
 }
 
+void iterator_end_prev_read_ok() {
+  std::vector<int> vec = {1, 2};
+  auto iter = vec.end();
+  std::cout << *(--iter) << '\n';
+}
+
+void iterator_prev_after_emplace_bad(std::vector<int>& vec) {
+  auto iter = vec.begin();
+  ++iter;
+  vec.emplace(iter, 4);
+  --iter;
+  std::cout << *iter << '\n';
+}
+
+void FN_iterator_begin_prev_read_bad() {
+  std::vector<int> vec = {1, 2};
+  auto iter = vec.begin();
+  std::cout << *(--iter) << '\n';
+}
+
 bool for_each_ok(std::vector<int>& vec, bool b) {
   int res = 0;
   for (const auto& elem : vec) {