[Bufferoverrun] set uninitialized values in array as top

Summary: uninitialized value in array should not be bottom

Reviewed By: mbouaziz

Differential Revision: D4953174

fbshipit-source-id: 7b6471c

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -49,10 +49,19 @@ struct
     = fun pname ret params node mem ->
       match ret with
       | Some (id, _) ->
+          let set_uninitialized typ loc mem =
+            match typ with
+            | Typ.Tint _
+            | Typ.Tfloat _ ->
+                Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem
+            | _ -> mem
+          in
           let (typ, size) = get_malloc_info (List.hd_exn params |> fst) in
           let size = Sem.eval size mem (CFG.loc node) |> Dom.Val.get_itv in
           let v = Sem.eval_array_alloc pname node typ Itv.zero size 0 1 in
-          Dom.Mem.add_stack (Loc.of_id id) v mem
+          mem
+          |> Dom.Mem.add_stack (Loc.of_id id) v
+          |> set_uninitialized typ (Dom.Val.get_array_locs v)
       | _ -> mem
 
   let model_realloc

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -243,8 +243,11 @@ struct
   let get_array_blk : t -> ArrayBlk.astate
     = fun x -> x.arrayblk
 
+  let get_array_locs : t -> PowLoc.t
+    = fun x -> ArrayBlk.get_pow_loc x.arrayblk
+
   let get_all_locs : t -> PowLoc.t
-    = fun x -> ArrayBlk.get_pow_loc x.arrayblk |> PowLoc.join x.powloc
+    = fun x -> PowLoc.join x.powloc (get_array_locs x)
 
   let top_itv : t
     = { bot with itv = Itv.top }

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

@@ -8,4 +8,4 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offse
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
-codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:18:10]
+codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10]

infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c

@@ -10,11 +10,9 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-char* safealloc(int n);
-
 void while_loop() {
   int i = 0;
-  char* a = safealloc(10);
+  char* a = malloc(10);
   while (*(a + i) && i < 10) /* BUG */
     a[i++] = 1; /* SAFE */
 }