[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

@@ -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

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;
+}

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]]