[pulse] Model placement new

Summary: Modeling `placement new`

Reviewed By: jvillard

Differential Revision: D10451539

fbshipit-source-id: 43be005e4

infer/src/checkers/Pulse.ml

@@ -66,8 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | None ->
         exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc (fst ret)
     | Some model ->
-        PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+        model call_loc ~ret ~actuals astate
-        >>= model call_loc ~ret ~actuals
 
 
   let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)

infer/src/checkers/PulseModels.ml

@@ -19,11 +19,31 @@ type model = exec_fun
 module Cplusplus = struct
   let delete : model =
    fun location ~ret:_ ~actuals astate ->
+    PulseDomain.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
+    >>= fun astate ->
     match actuals with
     | [AccessExpression deleted_access] ->
         PulseDomain.invalidate location deleted_access astate
     | _ ->
         Ok astate
+
+
+  let placement_new : model =
+   fun location ~ret ~actuals astate ->
+    match List.rev actuals with
+    | HilExp.AccessExpression expr :: other_actuals ->
+        let new_address = PulseDomain.AbstractAddress.mk_fresh () in
+        PulseDomain.write location expr new_address astate
+        >>= PulseDomain.write location (Base ret) new_address
+        >>= PulseDomain.read_all location
+              (List.concat_map other_actuals ~f:HilExp.get_access_exprs)
+    | _ :: other_actuals ->
+        PulseDomain.read_all location
+          (List.concat_map other_actuals ~f:HilExp.get_access_exprs)
+          astate
+        >>= PulseDomain.write location (Base ret) (PulseDomain.AbstractAddress.mk_fresh ())
+    | _ ->
+        Ok astate
 end
 
 module StdVector = struct
@@ -66,7 +86,10 @@ module ProcNameDispatcher = struct
 end
 
 let builtins_dispatcher =
-  let builtins = [(BuiltinDecl.__delete, Cplusplus.delete)] in
+  let builtins =
+    [ (BuiltinDecl.__delete, Cplusplus.delete)
+    ; (BuiltinDecl.__placement_new, Cplusplus.placement_new) ]
+  in
   let builtins_map =
     Hashtbl.create
       ( module struct

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

@@ -19,12 +19,11 @@ 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_aliasing1_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `alias` 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, FN_placement_new_aliasing2_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `alias` 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, basic_placement_new_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `tptr` here,accessed `ptr` 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]