[inferbo] Differentiate proof obligations by allocsites

Summary:
This diff differentiates proof obligations by allocsites.  Sizes and
offsets of arrays were joined when making proof obligations.

Reviewed By: mbouaziz

Differential Revision: D14163149

fbshipit-source-id: cb6608c16

infer/src/bufferoverrun/arrayBlk.ml

@@ -287,8 +287,6 @@ let offsetof = join_itv ~f:ArrInfo.offsetof
 
 let sizeof = join_itv ~f:ArrInfo.sizeof
 
-let sizeof_byte = join_itv ~f:ArrInfo.byte_size
-
 let plus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr
 
 let minus_offset : t -> Itv.t -> t = fun arr i -> map (fun a -> ArrInfo.minus_offset a i) arr

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -212,44 +212,54 @@ module Exec = struct
 end
 
 module Check = struct
-  let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
-      ~latest_prune location cond_set =
+  let check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces
+      ~last_included ~latest_prune location cond_set =
     match (size, idx) with
     | NonBottom length, NonBottom idx ->
-        let offset =
-          match ArrayBlk.offsetof (Dom.Val.get_array_blk arr) with
-          | Bottom ->
-              (* Java's collection has no offset. *)
-              Itv.ItvPure.zero
-          | NonBottom offset ->
-              offset
-        in
-        let arr_traces = Dom.Val.get_traces arr in
         PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp
           ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces ~latest_prune cond_set
     | _ ->
         cond_set
 
 
+  let log_array_access allocsite size offset idx =
+    L.(debug BufferOverrun Verbose)
+      "@[<v 2>Add condition :@,array: %a@,  size: %a@,  idx: %a + %a@,@]@." Allocsite.pp allocsite
+      Itv.pp size Itv.ItvPure.pp offset Itv.pp idx
+
+
+  let offsetof arr_info =
+    match ArrayBlk.ArrInfo.offsetof arr_info with
+    | Bottom ->
+        (* Java's collection has no offset. *)
+        Itv.ItvPure.zero
+    | NonBottom offset ->
+        offset
+
+
   let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included ~latest_prune location
       cond_set =
-    let arr_blk = Dom.Val.get_array_blk arr in
-    let size = ArrayBlk.sizeof arr_blk in
-    let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
-    let idx_itv = Dom.Val.get_itv idx in
     let idx_traces = Dom.Val.get_traces idx in
-    let idx = if is_plus then idx_itv else Itv.neg idx_itv in
+    let idx =
+      let idx_itv = Dom.Val.get_itv idx in
+      if is_plus then idx_itv else Itv.neg idx_itv
+    in
+    let arr_traces = Dom.Val.get_traces arr in
+    let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
     let idx_sym_exp =
       let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in
       Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp ->
           let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in
           op idx_sym_exp offset_sym_exp )
     in
-    L.(debug BufferOverrun Verbose)
-      "@[<v 2>Add condition :@,array: %a@,  idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
-      (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
-    check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
-      ~latest_prune location cond_set
+    let array_access1 allocsite arr_info acc =
+      let size = ArrayBlk.ArrInfo.sizeof arr_info in
+      let offset = offsetof arr_info in
+      log_array_access allocsite size offset idx ;
+      check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces
+        ~last_included ~latest_prune location acc
+    in
+    ArrayBlk.fold array_access1 (Dom.Val.get_array_blk arr) cond_set
 
 
   let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set =
@@ -264,17 +274,22 @@ module Check = struct
       location cond_set
 
 
-  let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included location cond_set =
-    let arr_blk = Dom.Val.get_array_blk arr in
-    let size = ArrayBlk.sizeof_byte arr_blk in
-    let idx_itv = Dom.Val.get_itv idx in
+  let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included ~latest_prune location cond_set
+      =
     let idx_traces = Dom.Val.get_traces idx in
-    let idx = if is_plus then idx_itv else Itv.neg idx_itv in
-    L.(debug BufferOverrun Verbose)
-      "@[<v 2>Add condition :@,array: %a@,  idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
-      (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
-    check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
-      ~last_included location cond_set
+    let idx =
+      let idx_itv = Dom.Val.get_itv idx in
+      if is_plus then idx_itv else Itv.neg idx_itv
+    in
+    let arr_traces = Dom.Val.get_traces arr in
+    let array_access_byte1 allocsite arr_info acc =
+      let size = ArrayBlk.ArrInfo.byte_size arr_info in
+      let offset = offsetof arr_info in
+      log_array_access allocsite size offset idx ;
+      check_access ~size ~idx ~offset ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr_traces
+        ~idx_traces ~last_included ~latest_prune location acc
+    in
+    ArrayBlk.fold array_access_byte1 (Dom.Val.get_array_blk arr) cond_set
 
 
   let lindex_byte integer_type_widths ~array_exp ~byte_index_exp ~last_included mem location

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

@@ -101,7 +101,7 @@ codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_b
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
-codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]
+codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: 5]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_1_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]
@@ -287,6 +287,8 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0]
+codetoanalyze/c/bufferoverrun/trivial.c, differentiate_array_info_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
+codetoanalyze/c/bufferoverrun/trivial.c, differentiate_array_info_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10]
 codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/trivial.c

@@ -17,3 +17,27 @@ void malloc_zero_Bad() {
   x = malloc(0);
   x = malloc(1);
 }
+
+int unknown_function();
+
+void differentiate_array_info_Good() {
+  int* p;
+  if (unknown_function()) {
+    p = (int*)malloc(sizeof(int) * 5);
+  } else {
+    p = (int*)malloc(sizeof(int) * 10);
+    p = p + 5;
+  }
+  p[4] = 0;
+}
+
+void differentiate_array_info_Bad() {
+  int* p;
+  if (unknown_function()) {
+    p = (int*)malloc(sizeof(int) * 5);
+  } else {
+    p = (int*)malloc(sizeof(int) * 10);
+    p = p + 5;
+  }
+  p[5] = 0;
+}