[pulse] Invalidate addresses for destructors

Summary:
Invalidating addresses for destructors to catch use after destructor errors.
To pass ownership tests for use after destructor errors, we still need to:
(1) fix pointer arithmetic false positives
(2) add model for placement new to fix false positives
(3) add model for operator= to fix false positives
(4) support inter-procedural analysis for destructor_order_bad test

Reviewed By: jvillard

Differential Revision: D10450912

fbshipit-source-id: 2d9b1ee68

infer/src/checkers/Pulse.ml

@@ -30,6 +30,29 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = Summary.t
 
+  let is_destructor = function
+    | Typ.Procname.ObjC_Cpp clang_pname ->
+        Typ.Procname.ObjC_Cpp.is_destructor clang_pname
+        && not
+             (* Our frontend generates synthetic inner destructors to model invocation of base class
+           destructors correctly; see D5834555/D7189239 *)
+             (Typ.Procname.ObjC_Cpp.is_inner_destructor clang_pname)
+    | _ ->
+        false
+
+
+  let exec_call _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate =
+    match call with
+    | Direct callee_pname when is_destructor callee_pname -> (
+      match actuals with
+      | [AccessExpression destroyed_access] ->
+          PulseDomain.invalidate call_loc destroyed_access astate
+      | _ ->
+          Ok astate )
+    | _ ->
+        PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+
+
   let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate =
     let model =
       match call with
@@ -41,9 +64,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     match model with
     | None ->
-        PulseDomain.havoc (fst ret) astate |> Result.return
+        exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc (fst ret)
     | Some model ->
-        model call_loc ~ret ~actuals astate
+        PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+        >>= model call_loc ~ret ~actuals
 
 
   let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
@@ -65,9 +89,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Assume (condition, _, _, loc) ->
         PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary
     | Call (ret, call, actuals, flags, loc) ->
-        PulseDomain.read_all loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
-        >>= dispatch_call ret call actuals flags loc
-        |> check_error summary
+        dispatch_call ret call actuals flags loc astate |> check_error summary
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"

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

@@ -1,5 +1,11 @@
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.str)` here]
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.a.str)` here]
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `s.i` here]
 codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
 codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
+codetoanalyze/cpp/ownership/basics.cpp, pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `a` here,accessed `a` here]
+codetoanalyze/cpp/ownership/basics.cpp, struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a)` here]
+codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
 codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `x` here,accessed `x` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
@@ -13,5 +19,14 @@ codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad,
 codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing1_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing2_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, destruct_pointer_contents_then_placement_new1_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, placement_new_non_var_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `m.s` here,accessed `m.s` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `*(s.f)` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(c)` here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `result` here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(x).__internal_array[_]` here,accessed `*(y)` here]