[pulse] Model std::vector::reserve to invalidate references to elements

Summary: Similarly as `std::vector::push_back`, `std::vector::reserve` can invalidate the references to elements if the new size is bigger than the existing one. More info on `std::vector::reserve`: https://en.cppreference.com/w/cpp/container/vector/reserve

Reviewed By: jvillard

Differential Revision: D13340324

fbshipit-source-id: bf99b6923

infer/src/checkers/PulseInvalidation.ml

@@ -7,12 +7,21 @@
 open! IStd
 module F = Format
 
+type std_vector_function = PushBack | Reserve [@@deriving compare]
+
+let std_vector_function_pp f = function
+  | PushBack ->
+      F.fprintf f "std::vector::push_back"
+  | Reserve ->
+      F.fprintf f "std::vector::reserve"
+
+
 type t =
   | CFree of AccessExpression.t * Location.t
   | CppDelete of AccessExpression.t * Location.t
   | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t
   | Nullptr
-  | StdVectorPushBack of AccessExpression.t * Location.t
+  | StdVector of std_vector_function * AccessExpression.t * Location.t
 [@@deriving compare]
 
 let issue_type_of_cause = function
@@ -24,7 +33,7 @@ let issue_type_of_cause = function
       IssueType.use_after_destructor
   | Nullptr ->
       IssueType.null_dereference
-  | StdVectorPushBack _ ->
+  | StdVector _ ->
       IssueType.vector_invalidation
 
 
@@ -32,7 +41,7 @@ let get_location = function
   | CFree (_, location)
   | CppDelete (_, location)
   | CppDestructor (_, _, location)
-  | StdVectorPushBack (_, location) ->
+  | StdVector (_, _, location) ->
       Some location
   | Nullptr ->
       None
@@ -50,6 +59,6 @@ let pp f = function
         AccessExpression.pp access_expr Location.pp location
   | Nullptr ->
       F.fprintf f "null pointer"
-  | StdVectorPushBack (access_expr, location) ->
+  | StdVector (std_vector_f, access_expr, location) ->
-      F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a"
+      F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" std_vector_function_pp
-        AccessExpression.pp access_expr Location.pp location
+        std_vector_f AccessExpression.pp access_expr Location.pp location

infer/src/checkers/PulseInvalidation.mli

@@ -6,12 +6,14 @@
  *)
 open! IStd
 
+type std_vector_function = PushBack | Reserve [@@deriving compare]
+
 type t =
   | CFree of AccessExpression.t * Location.t
   | CppDelete of AccessExpression.t * Location.t
   | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t
   | Nullptr
-  | StdVectorPushBack of AccessExpression.t * Location.t
+  | StdVector of std_vector_function * AccessExpression.t * Location.t
 [@@deriving compare]
 
 val issue_type_of_cause : t -> IssueType.t

infer/src/checkers/PulseModels.ml

@@ -86,6 +86,15 @@ module StdVector = struct
     AccessExpression.(array_offset (dereference (to_internal_array vector)) Typ.void [])
 
 
+  let reallocate_internal_array vector vector_f location astate =
+    let array = to_internal_array vector in
+    (* all elements should be invalidated *)
+    let array_elements = deref_internal_array vector in
+    let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in
+    PulseDomain.invalidate invalidation location array_elements astate
+    >>= PulseDomain.havoc location array
+
+
   let at : model =
    fun location ~ret ~actuals astate ->
     match actuals with
@@ -100,7 +109,8 @@ module StdVector = struct
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        PulseDomain.StdVector.mark_reserved location vector astate
+        reallocate_internal_array vector Reserve location astate
+        >>= PulseDomain.StdVector.mark_reserved location vector
     | _ ->
         Ok astate
 
@@ -117,12 +127,7 @@ module StdVector = struct
           Ok astate
         else
           (* simulate a re-allocation of the underlying array every time an element is added *)
-          let array = to_internal_array vector in
+          reallocate_internal_array vector PushBack location astate
-          (* all elements should be invalidated *)
-          let array_elements = deref_internal_array vector in
-          let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in
-          PulseDomain.invalidate invalidation location array_elements astate
-          >>= PulseDomain.havoc location array
     | _ ->
         Ok astate
 end

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

@@ -20,3 +20,4 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AF
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 71, column 3 here,accessed `*(elt)` here]

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -65,3 +65,9 @@ void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
   }
   std::cout << *elt << "\n";
 }
+
+void reserve_bad(std::vector<int>& vec) {
+  int* elt = &vec[1];
+  vec.reserve(vec.size() + 1);
+  std::cout << *elt << "\n";
+}