[inferbo] Simplify realloc model

Summary: It simply resizes the target structure instead of allocating new heap memories and copying values.

Reviewed By: mbouaziz

Differential Revision: D7179353

fbshipit-source-id: 9c20f64

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -110,20 +110,25 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
 
 
   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
+    let exec {ret; location; tenv} mem =
       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
+          let typ, _, length0, dyn_length = get_malloc_info size_exp in
+          let length = Sem.eval length0 mem in
+          let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
+          let v =
+            Sem.eval src_exp mem |> Dom.Val.set_array_size (Dom.Val.get_itv length)
+            |> Dom.Val.set_traces traces
+          in
+          let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
+          Option.value_map dyn_length ~default:mem ~f:(fun dyn_length ->
+              let dyn_length = Dom.Val.get_itv (Sem.eval dyn_length mem) in
+              BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem )
       | _ ->
           mem
-    in
-    {exec; check= malloc_check}
+    and check = check_alloc_size size_exp in
+    {exec; check}
 
 
   let placement_new allocated_mem_exp =

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -48,8 +48,7 @@ module type S = sig
       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
+    val set_dyn_length : Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate
   end
 
   module Check : sig
@@ -171,23 +170,22 @@ module Make (CFG : ProcCfg.S) = struct
       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} -> (
+    let rec set_dyn_length tenv typ locs dyn_length mem =
+      match typ.Typ.desc with
+      | 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 ->
+        | Some {fields} when not (List.is_empty fields)
+          -> (
+            let field_name, field_typ, _ = List.last_exn fields in
+            let field_loc = PowLoc.append_field locs ~fn:field_name in
+            match field_typ.Typ.desc with
+            | Tarray {length= Some length} ->
+                let length = Itv.plus (Itv.of_int_lit length) dyn_length in
+                let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in
+                Dom.Mem.strong_update_heap field_loc v mem
+            | _ ->
+                set_dyn_length tenv field_typ field_loc dyn_length mem )
+        | _ ->
             mem )
       | _ ->
           mem

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

@@ -15,6 +15,7 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt
 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/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, [Offset: [7, 7] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, []

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

@@ -70,3 +70,30 @@ void realloc_struct2_Bad() {
   struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3));
   buf2[buf2[0].s.x].s.x = 0;
 }
+
+struct S4 {
+  int a[3];
+  int c[3];
+  int b[1];
+};
+
+struct S5 {
+ public:
+  int d[3];
+  int f[3];
+  S4 e;
+};
+
+void realloc_flexible_array_Good() {
+  struct S5* buf1 = (struct S5*)malloc(sizeof(struct S5) + 4 * sizeof(int));
+  struct S5* buf2 =
+      (struct S5*)realloc(buf1, sizeof(struct S5) + 9 * sizeof(int));
+  buf2->e.b[7] = 0;
+}
+
+void realloc_flexible_array_Bad() {
+  struct S5* buf1 = (struct S5*)malloc(sizeof(struct S5) + 9 * sizeof(int));
+  struct S5* buf2 =
+      (struct S5*)realloc(buf1, sizeof(struct S5) + 4 * sizeof(int));
+  buf2->e.b[7] = 0;
+}