[inferbo] Initialize array member in class

Reviewed By: mbouaziz

Differential Revision: D7053775

fbshipit-source-id: c451d46

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -82,7 +82,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
 
 
   let malloc size_exp =
-    let exec {pname; ret; node; location} mem =
+    let exec {pname; ret; node; location; tenv} mem =
       match ret with
       | Some (id, _) ->
           let typ, stride, length0 = get_malloc_info size_exp in
@@ -94,6 +94,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
           in
           mem |> Dom.Mem.add_stack (Loc.of_id id) v
           |> set_uninitialized node typ (Dom.Val.get_array_locs v)
+          |> BoUtils.Exec.init_array_fields tenv pname node typ (Dom.Val.get_array_locs v)
       | _ ->
           L.(debug BufferOverrun Verbose)
             "/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ;

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -43,6 +43,9 @@ module type S = sig
       decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int
       -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:counter
       -> new_alloc_num:counter -> Dom.Mem.astate -> Dom.Mem.astate
+
+    val init_array_fields :
+      Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> Dom.Mem.astate -> Dom.Mem.astate
   end
 
   module Check : sig
@@ -125,6 +128,37 @@ module Make (CFG : ProcCfg.S) = struct
         let mem = Dom.Mem.add_heap loc arr mem in
         let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num alloc_num) in
         decl_sym_val pname tenv node location ~depth deref_loc typ mem
+
+
+    let init_array_fields tenv pname node typ locs mem =
+      let rec init_field locs dimension (mem, inst_num) (field_name, field_typ, _) =
+        let field_loc = PowLoc.append_field locs ~fn:field_name in
+        let mem =
+          match field_typ.Typ.desc with
+          | Tarray (typ, Some length, stride) ->
+              let length = Itv.of_int_lit length in
+              let stride = Option.map stride ~f:IntLit.to_int in
+              let v =
+                Sem.eval_array_alloc pname node typ ?stride Itv.zero length inst_num dimension
+              in
+              Dom.Mem.strong_update_heap field_loc v mem
+          | _ ->
+              init_fields field_typ field_loc dimension mem
+        in
+        (mem, inst_num + 1)
+      and init_fields typ locs dimension mem =
+        match typ.Typ.desc with
+        | Tstruct typename -> (
+          match Tenv.lookup tenv typename with
+          | Some str ->
+              List.fold ~f:(init_field locs (dimension + 1)) ~init:(mem, 1) str.Typ.Struct.fields
+              |> fst
+          | None ->
+              mem )
+        | _ ->
+            mem
+      in
+      init_fields typ locs 1 mem
   end
 
   module Check = struct

infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

@@ -37,3 +37,30 @@ void access_after_new_Bad() {
   my_class* x = new my_class();
   x->access_nth(15);
 }
+
+#include <stdlib.h>
+
+class my_class2 {
+ public:
+  int a[5];
+};
+
+void array_member_malloc_Good() {
+  my_class2* x = (my_class2*)malloc(sizeof(my_class2));
+  x->a[0] = 0;
+}
+
+void array_member_malloc_Bad() {
+  my_class2* x = (my_class2*)malloc(sizeof(my_class2));
+  x->a[10] = 0;
+}
+
+class my_class3 {
+ public:
+  my_class2 b;
+};
+
+void array_member_malloc2_Bad() {
+  my_class3* x = (my_class3*)malloc(sizeof(my_class3));
+  x->b.a[10] = 0;
+}

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

@@ -1,4 +1,6 @@
 codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [15, 15] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/class.cpp:28:34 by call `my_class_access_nth()` ]
+codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]
+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/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]