From 3ef619ef14ac0737e9d393fe3a7ad746888ef07a Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 23 Feb 2018 19:34:46 -0800
Subject: [PATCH] [inferbo] Add a model for "placement new"

Summary:
The semantics of "placement new" is defined simply as an assignment.
For example, `C* x = new (y) C();` is analyzed as if `C* x = y;`.

Reviewed By: mbouaziz

Differential Revision: D7054007

fbshipit-source-id: 1c6754f
---
 infer/src/bufferoverrun/bufferOverrunModels.ml     | 13 +++++++++++++
 .../codetoanalyze/cpp/bufferoverrun/class.cpp      | 14 ++++++++++++++
 .../codetoanalyze/cpp/bufferoverrun/issues.exp     |  1 +
 3 files changed, 28 insertions(+)

diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 283ffcdfe..31d488ac6 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -105,6 +105,18 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
 
   let realloc = malloc
 
+  let placement_new allocated_mem_exp =
+    let exec {ret} mem =
+      match ret with
+      | Some (id, _) ->
+          let v = Sem.eval allocated_mem_exp mem in
+          Dom.Mem.add_stack (Loc.of_id id) v mem
+      | None ->
+          mem
+    in
+    {exec; check= no_check}
+
+
   let inferbo_min e1 e2 =
     let exec {ret} mem =
       match ret with
@@ -291,6 +303,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
         ; -"malloc" <>$ capt_exp $+...$--> malloc
         ; -"__new" <>$ capt_exp $+...$--> malloc
         ; -"__new_array" <>$ capt_exp $+...$--> malloc
+        ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new
         ; -"realloc" <>$ any_arg $+ capt_exp $+...$--> realloc
         ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length
         ; -"strlen" <>--> by_value Dom.Val.Itv.nat
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
index d938d5777..8ababc705 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
@@ -64,3 +64,17 @@ void array_member_malloc2_Bad() {
   my_class3* x = (my_class3*)malloc(sizeof(my_class3));
   x->b.a[10] = 0;
 }
+
+#include <new>
+
+void placement_new_Good() {
+  char* mem = (char*)malloc(sizeof(my_class2));
+  my_class2* x = new (mem) my_class2();
+  x->a[0] = 0;
+}
+
+void placement_new_Bad() {
+  char* mem = (char*)malloc(sizeof(my_class2));
+  my_class2* x = new (mem) my_class2();
+  x->a[10] = 0;
+}
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index 468bccead..4e36b8848 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -3,6 +3,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_O
 codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]