[pulse] Model stack as a map from addresses of variables

Summary:
When we create Dereference edge, we also create TakeAddress back edge. This causes false positives for stack variables. When we write to a stack variable and then take its address, the resulting address is the one from the back edge of the written value. See example `push_back_value_ok`. To solve this issue, this diff changes stack to denote a map from address of variables rather than from variables.
We still have issue for fields, see example, FP_push_back_value_field_ok. To solve this, we probably need to remove back edges.

Reviewed By: jvillard

Differential Revision: D13432415

fbshipit-source-id: 9254a1a6d

infer/src/checkers/PulseDomain.ml

@@ -214,7 +214,7 @@ end = struct
   let fold = Graph.fold
 end
 
-(** Stacks: map variables to values.
+(** Stacks: map addresses of variables to values.
 
     This is defined as an abstract domain but the domain operations are mostly meaningless on their
     own. It so happens that the join on abstract states uses the join of stacks provided by this
@@ -572,9 +572,19 @@ module Operations = struct
             walk actor ~on_last addr' path astate )
 
 
-  let write_var var addr astate =
+  let write_var var new_addr astate =
+    let astate, var_address_of =
+      match Stack.find_opt var astate.stack with
+      | Some addr ->
+          (astate, addr)
+      | None ->
+          let addr = AbstractAddress.mk_fresh () in
           let stack = Stack.add var addr astate.stack in
-    {astate with stack}
+          ({astate with stack}, addr)
+    in
+    (* Update heap with var_address_of -*-> new_addr *)
+    let heap = Memory.add_edge var_address_of HilExp.Access.Dereference new_addr astate.heap in
+    {astate with heap}
 
 
   let rec to_accesses location access_expr astate =
@@ -606,7 +616,7 @@ module Operations = struct
     match (on_last, access_list) with
     | `Overwrite new_addr, [] ->
         Ok (write_var access_var new_addr astate, new_addr)
-    | `Access, _ | `Overwrite _, _ :: _ ->
+    | `Access, _ | `Overwrite _, _ :: _ -> (
         let astate, base_addr =
           match Stack.find_opt access_var astate.stack with
           | Some addr ->
@@ -616,8 +626,12 @@ module Operations = struct
               let stack = Stack.add access_var addr astate.stack in
               ({astate with stack}, addr)
         in
+        match access_list with
+        | [HilExp.Access.TakeAddress] ->
+            Ok (astate, base_addr)
+        | _ ->
             let actor = {access_expr; location} in
-        walk actor ~on_last base_addr access_list astate
+            walk actor ~on_last base_addr (HilExp.Access.Dereference :: access_list) astate )
 
 
   (** Use the stack and heap to walk the access path represented by the given expression down to an
@@ -662,19 +676,10 @@ module Operations = struct
     {astate with heap= Memory.invalidate address actor astate.heap}
 
 
-  let havoc_var var astate =
-    {astate with stack= Stack.add var (AbstractAddress.mk_fresh ()) astate.stack}
-
+  let havoc_var var astate = write_var var (AbstractAddress.mk_fresh ()) astate
 
   let havoc location (access_expr : HilExp.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
+    overwrite_address astate access_expr (AbstractAddress.mk_fresh ()) location >>| fst
 
 
   let write location access_expr addr astate =

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

@@ -20,6 +20,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 204, 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 64, column 5 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 126, column 5 here,accessed `&(this->x)` here]
 codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::assign(vec, ..)` at line 83, column 3 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::clear(vec, ..)` at line 77, 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]

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

@@ -109,3 +109,21 @@ void FN_emplace_back_bad(std::vector<int>& vec) {
                        // (T37883260)
   std::cout << *elt << "\n";
 }
+
+void f(int&);
+
+void push_back_value_ok(std::vector<int>& vec) {
+  int x = vec[0];
+  vec.push_back(7);
+  f(x);
+}
+
+struct VectorA {
+  int x;
+
+  void FP_push_back_value_field_ok(std::vector<int>& vec) {
+    x = vec[0];
+    vec.push_back(7);
+    f(x);
+  }
+};