[pulse] Invalidate object rather than address in destructor call

Summary: We provide an address of an object as a parameter to destructor. When destructor is called the object itself is invalidated, but not the address.

Reviewed By: jvillard

Differential Revision: D12824032

fbshipit-source-id: 516eebcf8

infer/src/checkers/Pulse.ml

@@ -46,9 +46,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Direct callee_pname when is_destructor callee_pname -> (
       match actuals with
       | [AccessExpression destroyed_access] ->
+          let destroyed_object =
+            AccessExpression.normalize (AccessExpression.Dereference destroyed_access)
+          in
           PulseDomain.invalidate
-            (CppDestructor (callee_pname, destroyed_access, call_loc))
-            call_loc destroyed_access astate
+            (CppDestructor (callee_pname, destroyed_object, call_loc))
+            call_loc destroyed_object astate
       | _ ->
           Ok astate )
     | _ ->

infer/tests/codetoanalyze/cpp/pulse/basics.cpp

@@ -73,7 +73,7 @@ int multiple_invalidations_loop_bad(int n, int* ptr) {
   return *ptr;
 }
 
-Aggregate* FP_pointer_arithmetic_ok(Aggregate* a) {
+Aggregate* pointer_arithmetic_ok(Aggregate* a) {
   a->~Aggregate();
   a++;
   return a;

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

@@ -1,13 +1,11 @@
-codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(&(a))` at line 39, column 3 here,accessed `&(a)` here]
-codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(&(a))` at line 53, column 3 here,accessed `&(a)` here]
-codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(&(s))` at line 25, column 3 here,accessed `&(s)` here]
-codetoanalyze/cpp/pulse/basics.cpp, FP_pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(a)` at line 77, column 3 here,accessed `a` here]
-codetoanalyze/cpp/pulse/basics.cpp, FP_struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(&(a))` at line 100, column 3 here,accessed `&(a)` here]
+codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(a)` at line 39, column 3 here,accessed `&(a.str)` here]
+codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(a)` at line 53, column 3 here,accessed `&(a.a.str)` here]
+codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(s)` at line 25, column 3 here,accessed `s.i` here]
+codetoanalyze/cpp/pulse/basics.cpp, FP_struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(a)` at line 100, column 3 here,accessed `&(a)` here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` 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/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/pulse/returns.cpp, returns::return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `returns::S_~S(s)` at line 120, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_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/pulse/use_after_delete.cpp, FP_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]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 130, column 5 here,accessed `s` here]
@@ -20,14 +18,14 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3,
 codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here]
 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 103, column 3 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_basic_placement_new_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(tptr)` at line 118, column 3 here,accessed `ptr` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 162, column 3 here,accessed `&(s)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 34, column 3 here,accessed `&(s)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 54, column 3 here,accessed `&(s)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 162, column 3 here,accessed `&(s)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_placement_new_explicit_destructor_ok, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(*(s))` at line 43, column 5 here,accessed `&(buf)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 34, column 3 here,accessed `&(s)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 54, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 132, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 140, column 3 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `&(s)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 185, column 3 here,accessed `pc->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, 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_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 185, 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, 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]

infer/tests/codetoanalyze/cpp/pulse/returns.cpp

@@ -113,9 +113,8 @@ int* return_deleted_bad() {
   return x;
 }
 
-// this *could* be ok depending on what the destructor does, but there's
-// probably no good reason to do it
-S* return_destructed_pointer_bad() {
+// this *could* be ok depending on what the caller does
+S* return_destructed_pointer_ok() {
   S* s = new S(1);
   s->~S();
   return s;

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

@@ -36,7 +36,7 @@ int FP_reinit_after_explicit_destructor_ok() {
   return *s.f;
 }
 
-void placement_new_explicit_destructor_ok() {
+void FP_placement_new_explicit_destructor_ok() {
   char buf[sizeof(S)];
   {
     S* s = new (buf) S(1);
@@ -112,7 +112,7 @@ class Subclass : virtual POD {
   ~Subclass() { delete f; }
 };
 
-void FP_basic_placement_new_ok() {
+void basic_placement_new_ok() {
   S* ptr = new S(1);
   S* tptr = new (ptr) S(1);
   tptr->~S();