[pulse] add model for `std::vector::reserve` using additional memory attribute

Summary:
Whenever `vec.reserve(n)` is called, remember that the vector is
"reserved". When doing `vec.push_back(x)` on a reserved vector, assume
enough size has been reserved in advance and do not invalidate the
underlying array.

This gets rid of false positives.

Reviewed By: mbouaziz

Differential Revision: D12939837

fbshipit-source-id: ce6354fc5

infer/src/checkers/PulseDomain.ml

@@ -156,14 +156,22 @@ module AttributesDomain : sig
 
   val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option
   (** None denotes a valid location *)
+
+  val std_vector_reserve : AbstractAddress.t -> astate -> astate
+
+  val is_std_vector_reserved : AbstractAddress.t -> astate -> bool
 end = struct
   module Attribute = struct
     (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more
        efficient (only need to look at the first element in the set of attributes to know if an
        address is invalid) *)
-    type t = Invalid of Invalidation.t [@@deriving compare]
+    type t = Invalid of Invalidation.t | StdVectorReserve [@@deriving compare]
 
-    let pp f = function Invalid invalidation -> Invalidation.pp f invalidation
+    let pp f = function
+      | Invalid invalidation ->
+          Invalidation.pp f invalidation
+      | StdVectorReserve ->
+          F.pp_print_string f "std::vector::reserve()"
   end
 
   module Attributes = AbstractDomain.FiniteSet (Attribute)
@@ -190,7 +198,17 @@ end = struct
        an address is invalid or not. *)
     find_opt address attribute_map
     |> Option.bind ~f:Attributes.min_elt_opt
-    |> Option.map ~f:(function Attribute.Invalid invalidation -> invalidation)
+    |> Option.bind ~f:(function Attribute.Invalid invalidation -> Some invalidation | _ -> None)
+
+
+  let std_vector_reserve address attribute_map =
+    add_attribute address Attribute.StdVectorReserve attribute_map
+
+
+  let is_std_vector_reserved address attribute_map =
+    find_opt address attribute_map
+    |> Option.value_map ~default:false ~f:(fun attributes ->
+           Attributes.mem Attribute.StdVectorReserve attributes )
 end
 
 (** the domain *)
@@ -622,5 +640,20 @@ module Operations = struct
     check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
 end
 
+module StdVector = struct
+  open Result.Monad_infix
+
+  let is_reserved location vector_access_expr astate =
+    Operations.read location vector_access_expr astate
+    >>| fun (astate, addr) ->
+    (astate, AttributesDomain.is_std_vector_reserved addr astate.attributes)
+
+
+  let mark_reserved location vector_access_expr astate =
+    Operations.read location vector_access_expr astate
+    >>| fun (astate, addr) ->
+    {astate with attributes= AttributesDomain.std_vector_reserve addr astate.attributes}
+end
+
 include Domain
 include Operations

infer/src/checkers/PulseDomain.mli

@@ -35,6 +35,12 @@ end
 
 type 'a access_result = ('a, Diagnostic.t) result
 
+module StdVector : sig
+  val is_reserved : Location.t -> AccessExpression.t -> t -> (t * bool) access_result
+
+  val mark_reserved : Location.t -> AccessExpression.t -> t -> t access_result
+end
+
 val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) access_result
 
 val read_all : Location.t -> AccessExpression.t list -> t -> t access_result

infer/src/checkers/PulseModels.ml

@@ -96,16 +96,33 @@ module StdVector = struct
         Ok (PulseDomain.havoc_var (fst ret) astate)
 
 
+  let reserve : model =
+   fun location ~ret:_ ~actuals astate ->
+    match actuals with
+    | [AccessExpression vector; _value] ->
+        PulseDomain.StdVector.mark_reserved location vector astate
+    | _ ->
+        Ok astate
+
+
   let push_back : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        let array = to_internal_array vector in
+        PulseDomain.StdVector.is_reserved location vector astate
-        (* all elements should be invalidated *)
+        >>= fun (astate, is_reserved) ->
-        let array_elements = deref_internal_array vector in
+        if is_reserved then
-        let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in
+          (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
-        PulseDomain.invalidate invalidation location array_elements astate
+             (a perfect analysis would also make sure we don't exceed the reserved size) *)
-        >>= PulseDomain.havoc location array
+          Ok astate
+        else
+          (* simulate a re-allocation of the underlying array every time an element is added *)
+          let array = to_internal_array vector in
+          (* 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
@@ -115,7 +132,8 @@ module ProcNameDispatcher = struct
     let open ProcnameDispatcher.ProcName in
     make_dispatcher
       [ -"std" &:: "vector" &:: "operator[]" &--> StdVector.at
-      ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back ]
+      ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back
+      ; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve ]
 end
 
 let builtins_dispatcher =

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

@@ -17,8 +17,6 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
-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 55, column 5 here,accessed `*(elt)` here]
+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, FP_reserve_then_push_back_loop_ok, 7, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 46, column 5 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 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]

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

@@ -31,14 +31,23 @@ void push_back_in_loop_ok(std::vector<int>& vec, std::vector<int>& vec_other) {
   }
 }
 
-void FP_reserve_then_push_back_ok(std::vector<int>& vec) {
+void reserve_then_push_back_ok(std::vector<int>& vec) {
   vec.reserve(vec.size() + 1);
   int* elt = &vec[1];
   vec.push_back(42);
   std::cout << *elt << "\n";
 }
 
-void FP_reserve_then_push_back_loop_ok(std::vector<int>& vec,
+void FN_reserve_too_small_bad() {
+  std::vector<int> vec;
+  vec.reserve(1);
+  vec.push_back(32);
+  int* elt = &vec[0];
+  vec.push_back(52);
+  std::cout << *elt << "\n";
+}
+
+void reserve_then_push_back_loop_ok(std::vector<int>& vec,
                                     std::vector<int>& vec_other) {
   vec.reserve(vec.size() + vec_other.size());
   int* elt = &vec[1];