[inferbo] Revise realloc semantics

Summary: It does not only malloc a new heap memory, but also copy its contents.

Reviewed By: mbouaziz

Differential Revision: D7152194

fbshipit-source-id: 58cba5e

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -109,7 +109,22 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
     {exec; check}
 
 
-  let realloc = malloc
+  let realloc src_exp size_exp =
+    let {exec= malloc_exec; check= malloc_check} = malloc size_exp in
+    let exec ({ret; tenv} as model_env) mem =
+      let mem = malloc_exec model_env mem in
+      match ret with
+      | Some (id, _) ->
+          let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
+          let typ, _, _, _ = get_malloc_info size_exp in
+          let tgt_locs = Dom.Val.get_all_locs (Dom.Mem.find_stack (Loc.of_id id) mem) in
+          let src_locs = Dom.Val.get_all_locs (Sem.eval src_exp mem) in
+          BoUtils.Exec.structural_copy tenv typ ~tgt_locs ~src_locs mem
+      | _ ->
+          mem
+    in
+    {exec; check= malloc_check}
+
 
   let placement_new allocated_mem_exp =
     let exec {ret} mem =
@@ -310,7 +325,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
         ; -"__new" <>$ capt_exp $+...$--> malloc
         ; -"__new_array" <>$ capt_exp $+...$--> malloc
         ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new
-        ; -"realloc" <>$ any_arg $+ capt_exp $+...$--> realloc
+        ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc
         ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length
         ; -"strlen" <>--> by_value Dom.Val.Itv.nat
         ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -47,6 +47,9 @@ module type S = sig
     val init_array_fields :
       Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t
       -> Dom.Mem.astate -> Dom.Mem.astate
+
+    val structural_copy :
+      Tenv.t -> Typ.t -> tgt_locs:PowLoc.t -> src_locs:PowLoc.t -> Dom.Mem.astate -> Dom.Mem.astate
   end
 
   module Check : sig
@@ -166,6 +169,28 @@ module Make (CFG : ProcCfg.S) = struct
             mem
       in
       init_fields typ locs 1 ?dyn_length mem
+
+
+    let rec structural_copy tenv typ ~tgt_locs ~src_locs mem =
+      match typ with
+      | {Typ.desc= Tint _} | {Typ.desc= Tfloat _} | {Typ.desc= Tvoid} | {Typ.desc= Tptr _} ->
+          let v = Dom.Mem.find_heap_set src_locs mem in
+          Dom.Mem.strong_update_heap tgt_locs v mem
+      | {Typ.desc= Tarray {elt}} ->
+          let tgt_locs = Dom.Val.get_all_locs (Dom.Mem.find_heap_set tgt_locs mem) in
+          let src_locs = Dom.Val.get_all_locs (Dom.Mem.find_heap_set src_locs mem) in
+          structural_copy tenv elt ~tgt_locs ~src_locs mem
+      | {Typ.desc= Tstruct typename} -> (
+        match Tenv.lookup tenv typename with
+        | Some str ->
+            List.fold str.Typ.Struct.fields ~init:mem ~f:(fun mem (fn, typ, _) ->
+                let tgt_locs = PowLoc.append_field tgt_locs ~fn in
+                let src_locs = PowLoc.append_field src_locs ~fn in
+                structural_copy tenv typ ~tgt_locs ~src_locs mem )
+        | None ->
+            mem )
+      | _ ->
+          mem
   end
 
   module Check = struct

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

@@ -13,6 +13,8 @@ codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5,
 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]]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, []

infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp

@@ -0,0 +1,72 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <cstdlib>
+
+void realloc_Good() {
+  int* buf1 = (int*)malloc(2 * sizeof(int));
+  buf1[0] = 3;
+  int* buf2 = (int*)realloc(buf1, 5 * sizeof(int));
+  buf2[buf2[0]] = 0;
+}
+
+void realloc_Bad() {
+  int* buf1 = (int*)malloc(2 * sizeof(int));
+  buf1[0] = 5;
+  int* buf2 = (int*)realloc(buf1, 5 * sizeof(int));
+  buf2[buf2[0]] = 0;
+}
+
+void realloc_Good_FP() {
+  int* buf1 = (int*)malloc(2 * sizeof(int));
+  for (int i = 0; i < 2; i++) {
+    buf1[i] = 3;
+  }
+  int* buf2 = (int*)realloc(buf1, 5 * sizeof(int));
+  buf2[buf2[0]] = 0;
+}
+
+struct S1 {
+  int x[2];
+};
+
+void realloc_struct1_Good() {
+  struct S1* buf1 = (struct S1*)malloc(2 * sizeof(struct S1));
+  buf1[0].x[0] = 3;
+  struct S1* buf2 = (struct S1*)realloc(buf1, 5 * sizeof(struct S1));
+  buf2[buf2[0].x[0]].x[0] = 0;
+}
+
+void realloc_struct1_Bad_FN() {
+  struct S1* buf1 = (struct S1*)malloc(2 * sizeof(struct S1));
+  buf1[0].x[0] = 5;
+  struct S1* buf2 = (struct S1*)realloc(buf1, 5 * sizeof(struct S1));
+  buf2[buf2[0].x[0]].x[0] = 0;
+}
+
+struct S2 {
+  int x;
+};
+
+struct S3 {
+  struct S2 s;
+};
+
+void realloc_struct2_Good() {
+  struct S3* buf1 = (struct S3*)malloc(2 * sizeof(struct S3));
+  buf1[0].s.x = 3;
+  struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3));
+  buf2[buf2[0].s.x].s.x = 0;
+}
+
+void realloc_struct2_Bad_FN() {
+  struct S3* buf1 = (struct S3*)malloc(2 * sizeof(struct S3));
+  buf1[0].s.x = 5;
+  struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3));
+  buf2[buf2[0].s.x].s.x = 0;
+}