[pulse] Clean up placement new model

Summary: Do not create a new location for placement new argument if it already exists.

Reviewed By: jvillard

Differential Revision: D12839942

fbshipit-source-id: 758b67a82

infer/src/checkers/PulseDomain.mli

@@ -11,8 +11,6 @@ module AbstractAddress : sig
   type t = private int [@@deriving compare]
 
   val nullptr : t
-
-  val mk_fresh : unit -> t
 end
 
 type t

infer/src/checkers/PulseModels.ml

@@ -42,18 +42,16 @@ module Cplusplus = struct
 
   let placement_new : model =
    fun location ~ret:(ret_var, _) ~actuals astate ->
+    let read_all args astate =
+      PulseDomain.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
+    in
     match List.rev actuals with
     | HilExp.AccessExpression expr :: other_actuals ->
-        let new_address = PulseDomain.AbstractAddress.mk_fresh () in
+        PulseDomain.read location expr astate
-        PulseDomain.write location expr new_address astate
+        >>= fun (astate, address) ->
-        >>| PulseDomain.write_var ret_var new_address
+        Ok (PulseDomain.write_var ret_var address astate) >>= read_all other_actuals
-        >>= PulseDomain.read_all location
-              (List.concat_map other_actuals ~f:HilExp.get_access_exprs)
     | _ :: other_actuals ->
-        PulseDomain.read_all location
+        read_all other_actuals astate >>| PulseDomain.havoc_var ret_var
-          (List.concat_map other_actuals ~f:HilExp.get_access_exprs)
-          astate
-        >>| PulseDomain.write_var ret_var (PulseDomain.AbstractAddress.mk_fresh ())
     | _ ->
         Ok astate
 end

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

@@ -11,8 +11,9 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destr
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, 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, placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 149, column 3 here,accessed `alias` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, 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_DESTRUCTOR, 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_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, 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_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, 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/use_after_destructor.cpp

@@ -141,6 +141,15 @@ S* placement_new_aliasing2_bad() {
   return alias; // bad, returning freed memory
 }
 
+S* placement_new_aliasing3_bad() {
+  S* s = new S(1);
+  s->~S();
+  S* alias = s;
+  auto alias_placement = new (s) S(2);
+  delete s; // this deletes alias too
+  return alias; // bad, returning freed memory
+}
+
 void placement_new_non_var_ok() {
   struct M {
     S* s;