[pulse] Allow taking address of a field of an invalid object

Summary:
It's ok to take an address of a field / array access of an invalid object.
This diff calculates the inner most dereference for an access expression starting with `&` and does not report on the dereference even if the address is invalid.

Reviewed By: jvillard

Differential Revision: D13450758

fbshipit-source-id: 18c038701

infer/src/checkers/PulseDomain.ml

@@ -548,28 +548,38 @@ 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 ~on_last addr path astate =
+  let rec walk ~dereference_to_ignore actor ~on_last addr path astate =
+    let check_addr_access_optional actor addr astate =
+      match dereference_to_ignore with
+      | Some 0 ->
+          Ok astate
+      | _ ->
+          check_addr_access actor addr astate
+    in
     match (path, on_last) with
     | [], `Access ->
         Ok (astate, addr)
     | [], `Overwrite _ ->
         L.die InternalError "Cannot overwrite last address in empty path"
     | [a], `Overwrite new_addr ->
-        check_addr_access actor addr astate
+        check_addr_access_optional actor addr astate
         >>| fun astate ->
         let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in
         ({astate with heap}, new_addr)
     | a :: path, _ -> (
-        check_addr_access actor addr astate
+        check_addr_access_optional actor addr astate
         >>= fun astate ->
+        let dereference_to_ignore =
+          Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore
+        in
         match Memory.find_edge_opt addr a astate.heap with
         | None ->
             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 ~on_last addr' path astate
+            walk ~dereference_to_ignore actor ~on_last addr' path astate
         | Some addr' ->
-            walk actor ~on_last addr' path astate )
+            walk ~dereference_to_ignore actor ~on_last addr' path astate )
 
 
   let write_var var new_addr astate =
@@ -587,6 +597,21 @@ module Operations = struct
     {astate with heap}
 
 
+  let ends_with_addressof = function HilExp.AccessExpression.AddressOf _ -> true | _ -> false
+
+  let last_dereference access_list =
+    let rec last_dereference_inner access_list index result =
+      match access_list with
+      | [] ->
+          result
+      | HilExp.Access.Dereference :: rest ->
+          last_dereference_inner rest (index + 1) (Some index)
+      | _ :: rest ->
+          last_dereference_inner rest (index + 1) result
+    in
+    last_dereference_inner access_list 0 None
+
+
   let rec to_accesses location access_expr astate =
     let exception Failed_fold of Diagnostic.t in
     try
@@ -609,6 +634,9 @@ module Operations = struct
   and walk_access_expr ~on_last astate access_expr location =
     to_accesses location access_expr astate
     >>= fun (astate, (access_var, _), access_list) ->
+    let dereference_to_ignore =
+      if ends_with_addressof access_expr then last_dereference access_list else None
+    in
     if Config.write_html then
       L.d_printfln "Accessing %a -> [%a]" Var.pp access_var
         (Pp.seq ~sep:"," Memory.Access.pp)
@@ -631,7 +659,9 @@ module Operations = struct
             Ok (astate, base_addr)
         | _ ->
             let actor = {access_expr; location} in
-            walk actor ~on_last base_addr (HilExp.Access.Dereference :: access_list) astate )
+            walk ~dereference_to_ignore 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

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

@@ -13,11 +13,11 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_D
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 142, column 3 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 148, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 150, column 3 here,accessed `alias` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 156, column 3 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 159, column 3 here,accessed `alias` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 165, column 3 here,accessed `alias` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71, column 3 here,accessed `*(s.f)` here]
-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_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 210, 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]

infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp

@@ -135,6 +135,12 @@ S* destruct_pointer_contents_then_placement_new1_ok(S* s) {
   return s;
 }
 
+S* destruct_pointer_contents_then_placement_new2_ok(S* s) {
+  s->~S();
+  new (&(s->f)) S(1);
+  return s;
+}
+
 S* placement_new_aliasing1_bad() {
   S* s = new S(1);
   s->~S();