[pulse] havoc vector array on push_back

Summary:
Turns out once a vector array became invalid it stayed that way, instead
of the vector getting a new valid internal array.

Reviewed By: skcho

Differential Revision: D10853532

fbshipit-source-id: f6f22407f

infer/src/checkers/Pulse.ml

@@ -66,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     match model with
     | None ->
-        exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc (fst ret)
+        exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc_var (fst ret)
     | Some model ->
         model call_loc ~ret ~actuals astate
 
@@ -76,28 +76,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     match instr with
     | Assign (lhs_access, rhs_exp, loc) ->
         (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *)
-        let rhs_result =
+        let result =
           match rhs_exp with
           | AccessExpression rhs_access ->
               PulseDomain.read loc rhs_access astate
+              >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate
           | Constant (Cint address) when IntLit.iszero address ->
-              Ok (astate, PulseDomain.AbstractAddress.nullptr)
+              PulseDomain.write loc lhs_access PulseDomain.AbstractAddress.nullptr astate
           | _ ->
               PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate
-              >>= fun astate ->
-              Ok
-                ( astate
-                , (* TODO: we could avoid creating and recording a fresh location whenever
-                       [lhs_access] is not already present in the state so that we keep its
-                       evaluation lazy, which would have the same semantic result but won't make the
-                       state grow needlessly in case we never need that value again. We would just
-                       need to add a function {!PulseDomain.freshen access_expr} that does the lazy
-                       refreshing and use it instead of {!PulseDomain.write} below in this case. *)
-                  PulseDomain.AbstractAddress.mk_fresh () )
+              >>= PulseDomain.havoc loc lhs_access
         in
-        Result.bind rhs_result ~f:(fun (astate, rhs_value) ->
-            PulseDomain.write loc lhs_access rhs_value astate )
-        |> check_error summary
+        check_error summary result
     | Assume (condition, _, _, loc) ->
         PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary
     | Call (ret, call, actuals, flags, loc) ->

infer/src/checkers/PulseDomain.ml

@@ -440,13 +440,13 @@ module Operations = struct
    and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it
    is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each
    address reached is valid. *)
-  let rec walk actor ~overwrite_last addr path astate =
-    match (path, overwrite_last) with
-    | [], None ->
+  let rec walk actor ~on_last addr path astate =
+    match (path, on_last) with
+    | [], `Access ->
         Ok (astate, addr)
-    | [], Some _ ->
+    | [], `Overwrite _ ->
         L.die InternalError "Cannot overwrite last address in empty path"
-    | [a], Some new_addr ->
+    | [a], `Overwrite new_addr ->
         check_addr_access actor addr astate
         >>| fun astate ->
         let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in
@@ -459,24 +459,24 @@ module Operations = struct
             let addr' = AbstractAddress.mk_fresh () in
             let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in
             let astate = {astate with heap} in
-            walk actor ~overwrite_last addr' path astate
+            walk actor ~on_last addr' path astate
         | Some addr' ->
-            walk actor ~overwrite_last addr' path astate )
+            walk actor ~on_last addr' path astate )
 
 
   (** add addresses to the state to give a address to the destination of the given access path *)
-  let walk_access_expr ?overwrite_last astate access_expr location =
+  let walk_access_expr ~on_last astate access_expr location =
     let (access_var, _), access_list = AccessExpression.to_accesses access_expr in
     if Config.write_html then
       L.d_strln
         (F.asprintf "Accessing %a -> [%a]" Var.pp access_var
            (Pp.seq ~sep:"," AccessExpression.Access.pp)
            access_list) ;
-    match (overwrite_last, access_list) with
-    | Some new_addr, [] ->
+    match (on_last, access_list) with
+    | `Overwrite new_addr, [] ->
         let stack = AliasingDomain.add access_var new_addr astate.stack in
         Ok ({astate with stack}, new_addr)
-    | None, _ | Some _, _ :: _ ->
+    | `Access, _ | `Overwrite _, _ :: _ ->
         let astate, base_addr =
           match AliasingDomain.find_opt access_var astate.stack with
           | Some addr ->
@@ -487,7 +487,7 @@ module Operations = struct
               ({astate with stack}, addr)
         in
         let actor = {access_expr; location} in
-        walk actor ~overwrite_last base_addr access_list astate
+        walk actor ~on_last base_addr access_list astate
 
 
   (** Use the stack and heap to walk the access path represented by the given expression down to an
@@ -495,7 +495,7 @@ module Operations = struct
 
     Return an error state if it traverses some known invalid address or if the end destination is
     known to be invalid. *)
-  let materialize_address astate access_expr = walk_access_expr astate access_expr
+  let materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr
 
   (** Use the stack and heap to walk the access path represented by the given expression down to an
     abstract address representing what the expression points to, and replace that with the given
@@ -503,7 +503,7 @@ module Operations = struct
 
     Return an error state if it traverses some known invalid address. *)
   let overwrite_address astate access_expr new_addr =
-    walk_access_expr ~overwrite_last:new_addr astate access_expr
+    walk_access_expr ~on_last:(`Overwrite new_addr) astate access_expr
 
 
   (** Add the given address to the set of know invalid addresses. *)
@@ -511,6 +511,23 @@ module Operations = struct
     {astate with invalids= InvalidAddressesDomain.add address actor astate.invalids}
 
 
+  let havoc_var var astate =
+    if AliasingDomain.mem var astate.stack then
+      {astate with stack= AliasingDomain.remove var astate.stack}
+    else astate
+
+
+  let havoc location (access_expr : AccessExpression.t) astate =
+    match access_expr with
+    | Base (access_var, _) ->
+        havoc_var access_var astate |> Result.return
+    | _ ->
+        walk_access_expr
+          ~on_last:(`Overwrite (AbstractAddress.mk_fresh ()))
+          astate access_expr location
+        >>| fst
+
+
   let read location access_expr astate =
     materialize_address astate access_expr location
     >>= fun (astate, addr) ->
@@ -527,8 +544,6 @@ module Operations = struct
     overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate
 
 
-  let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack}
-
   let invalidate cause location access_expr astate =
     materialize_address astate access_expr location
     >>= fun (astate, addr) ->

infer/src/checkers/PulseDomain.mli

@@ -39,7 +39,9 @@ val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) acce
 
 val read_all : Location.t -> AccessExpression.t list -> t -> t access_result
 
-val havoc : Var.t -> t -> t
+val havoc_var : Var.t -> t -> t
+
+val havoc : Location.t -> AccessExpression.t -> t -> t access_result
 
 val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result
 

infer/src/checkers/PulseModels.ml

@@ -67,7 +67,9 @@ module StdVector = struct
 
   let deref_internal_array vector =
     AccessExpression.ArrayOffset
-      (AccessExpression.FieldOffset (vector, internal_array), Typ.void, [])
+      ( AccessExpression.Dereference (AccessExpression.FieldOffset (vector, internal_array))
+      , Typ.void
+      , [] )
 
 
   let at : model =
@@ -77,16 +79,16 @@ module StdVector = struct
         PulseDomain.read location (deref_internal_array vector) astate
         >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.Base ret) loc astate
     | _ ->
-        Ok (PulseDomain.havoc (fst ret) astate)
+        Ok (PulseDomain.havoc_var (fst ret) astate)
 
 
   let push_back : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        PulseDomain.invalidate
-          (StdVectorPushBack (vector, location))
-          location (deref_internal_array vector) astate
+        let deref_array = deref_internal_array vector in
+        PulseDomain.invalidate (StdVectorPushBack (vector, location)) location deref_array astate
+        >>= PulseDomain.havoc location deref_array
     | _ ->
         Ok astate
 end

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

@@ -9,7 +9,7 @@ codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_b
 codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `v.__internal_array[_]` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `*(v.__internal_array)[_]` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 112, column 5 here,accessed `s` here]
@@ -29,5 +29,9 @@ codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad,
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 186, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` 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, deref_local_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 19, column 3 here,accessed `*(y)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(x, ..)` at line 12, column 3 here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 56, column 5 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_push_back_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 31, column 5 here,accessed `*(vec.__internal_array)[_]` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_loop_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 47, column 5 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 38, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, USE_AFTER_LIFETIME, 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, USE_AFTER_LIFETIME, 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

@@ -7,15 +7,53 @@
 #include <iostream>
 #include <vector>
 
-void deref_vector_element_after_lifetime_bad(std::vector<int>& x) {
-  int* y = &x[1];
-  x.push_back(42);
-  std::cout << *y << "\n";
+void deref_vector_element_after_push_back_bad(std::vector<int>& vec) {
+  int* elt = &vec[1];
+  vec.push_back(42);
+  std::cout << *elt << "\n";
 }
 
-void deref_local_vector_element_after_lifetime_bad() {
-  std::vector<int> x = {0, 0};
-  int* y = &x[1];
-  x.push_back(42);
-  std::cout << *y << "\n";
+void deref_local_vector_element_after_push_back_bad() {
+  std::vector<int> vec = {0, 0};
+  int* elt = &vec[1];
+  vec.push_back(42);
+  std::cout << *elt << "\n";
+}
+
+void two_push_back_ok(std::vector<int>& vec) {
+  vec.push_back(32);
+  vec.push_back(52);
+}
+
+void FP_push_back_in_loop_ok(std::vector<int>& vec,
+                             std::vector<int>& vec_other) {
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+}
+
+void FP_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,
+                                       std::vector<int>& vec_other) {
+  vec.reserve(vec.size() + vec_other.size());
+  int* elt = &vec[1];
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+  std::cout << *elt << "\n";
+}
+
+void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+  std::vector<int> vec(vec_other.size());
+  int* elt = &vec[1];
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+  std::cout << *elt << "\n";
 }