[inferbo] Suppress ALLOC_IS_ZERO for C++'s array object

Reviewed By: mbouaziz

Differential Revision: D14122889

fbshipit-source-id: d0c99a5e6

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -52,7 +52,7 @@ let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = fun
       (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None)
 
 
-let check_alloc_size size_exp {location; integer_type_widths} mem cond_set =
+let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem cond_set =
   let _, _, length0, _ = get_malloc_info size_exp in
   let v_length = Sem.eval integer_type_widths length0 mem in
   match Dom.Val.get_itv v_length with
@@ -61,7 +61,7 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set =
   | NonBottom length ->
       let traces = Dom.Val.get_traces v_length in
       let latest_prune = Dom.Mem.get_latest_prune mem in
-      PO.ConditionSet.add_alloc_size location ~length traces latest_prune cond_set
+      PO.ConditionSet.add_alloc_size location ~can_be_zero ~length traces latest_prune cond_set
 
 
 let fgets str_exp num_exp =
@@ -90,7 +90,7 @@ let fgets str_exp num_exp =
   {exec; check}
 
 
-let malloc size_exp =
+let malloc ~can_be_zero size_exp =
   let exec ({pname; node_hash; location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem
       =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
@@ -114,7 +114,7 @@ let malloc size_exp =
     |> Dom.Mem.add_stack (Loc.of_id id) v
     |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt
     |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length
-  and check = check_alloc_size size_exp in
+  and check = check_alloc_size ~can_be_zero size_exp in
   {exec; check}
 
 
@@ -243,17 +243,17 @@ let realloc src_exp size_exp =
     Option.value_map dyn_length ~default:mem ~f:(fun dyn_length ->
         let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in
         BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem )
-  and check = check_alloc_size size_exp in
+  and check = check_alloc_size ~can_be_zero:false size_exp in
   {exec; check}
 
 
 let placement_new size_exp (src_exp1, t1) src_arg2_opt =
   match (t1.Typ.desc, src_arg2_opt) with
   | Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) ->
-      malloc (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))
+      malloc ~can_be_zero:true (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))
   | Tstruct (CppClass (name, _)), None
     when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->
-      malloc size_exp
+      malloc ~can_be_zero:true size_exp
   | _, _ ->
       let exec {integer_type_widths} ~ret:(id, _) mem =
         let src_exp =
@@ -317,7 +317,7 @@ let inferbo_set_size e1 e2 =
     let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in
     let length = Sem.eval integer_type_widths e2 mem in
     Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem
-  and check = check_alloc_size e2 in
+  and check = check_alloc_size ~can_be_zero:true e2 in
   {exec; check}
 
 
@@ -402,7 +402,7 @@ let set_array_length array length_exp =
         Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem
     | _ ->
         L.(die InternalError) "Unexpected type of first argument for __set_array_length() "
-  and check = check_alloc_size length_exp in
+  and check = check_alloc_size ~can_be_zero:false length_exp in
   {exec; check}
 
 
@@ -503,7 +503,7 @@ end
 module StdBasicString = struct
   (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
   let constructor_from_char_ptr tgt src len =
-    let {exec= malloc_exec; check= malloc_check} = malloc len in
+    let {exec= malloc_exec; check= malloc_check} = malloc ~can_be_zero:true len in
     let exec model_env ~ret:((ret_id, _) as ret) mem =
       let mem = malloc_exec model_env ~ret mem in
       let v = Dom.Mem.find (Loc.of_id ret_id) mem in
@@ -653,7 +653,7 @@ module Collection = struct
     let exec {integer_type_widths} ~ret:_ mem =
       let itr = Sem.eval integer_type_widths rhs_exp mem in
       model_by_value itr lhs_id mem
-    and check = check_alloc_size rhs_exp in
+    and check = check_alloc_size ~can_be_zero:true rhs_exp in
     {exec; check}
 
 
@@ -730,13 +730,13 @@ module Call = struct
       ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255
       ; -"fgets" <>$ capt_exp $+ capt_exp $+...$--> fgets
       ; -"infer_print" <>$ capt_exp $!--> infer_print
-      ; -"malloc" <>$ capt_exp $+...$--> malloc
-      ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc
+      ; -"malloc" <>$ capt_exp $+...$--> malloc ~can_be_zero:false
+      ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc ~can_be_zero:false
       ; -"__new"
         <>$ capt_exp_of_typ (+PatternMatch.implements_collection)
         $+...$--> Collection.new_collection
-      ; -"__new" <>$ capt_exp $+...$--> malloc
-      ; -"__new_array" <>$ capt_exp $+...$--> malloc
+      ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
+      ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; -"__placement_new" <>$ capt_exp $+ capt_arg $+? capt_arg $!--> placement_new
       ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc
       ; -"__get_array_length" <>$ capt_exp $!--> get_array_length

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -103,55 +103,62 @@ type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue
 type checked_condition = {report_issue_type: report_issue_type; propagate: bool}
 
 module AllocSizeCondition = struct
-  type t = ItvPure.t [@@deriving compare]
+  type t = {length: ItvPure.t; can_be_zero: bool} [@@deriving compare]
 
-  let get_symbols = ItvPure.get_symbols
+  let get_symbols {length} = ItvPure.get_symbols length
 
-  let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length
+  let pp fmt {length} = F.fprintf fmt "alloc(%a)" ItvPure.pp length
 
-  let pp_description ~markup fmt length =
+  let pp_description ~markup fmt {length} =
     F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length
 
 
-  let make ~length = if ItvPure.is_invalid length then None else Some length
+  let make ~can_be_zero ~length =
+    if ItvPure.is_invalid length then None else Some {length; can_be_zero}
+
+
+  let have_similar_bounds x y =
+    ItvPure.have_similar_bounds x.length y.length && Bool.equal x.can_be_zero y.can_be_zero
 
-  let have_similar_bounds = ItvPure.have_similar_bounds
 
   let xcompare ~lhs ~rhs =
-    match ItvPure.xcompare ~lhs ~rhs with
-    | `Equal ->
-        `Equal
-    | `NotComparable ->
-        `NotComparable
-    | `LeftSubsumesRight ->
-        `LeftSubsumesRight
-    | `RightSubsumesLeft ->
-        `RightSubsumesLeft
-    | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp ->
-        let lpos = ItvPure.le_sem ItvPure.zero lhs in
-        let rpos = ItvPure.le_sem ItvPure.zero rhs in
-        if not (Boolean.equal lpos rpos) then `NotComparable
-        else if Boolean.is_true lpos then
-          match cmp with
-          | `LeftSmallerThanRight ->
-              `RightSubsumesLeft
-          | `RightSmallerThanLeft ->
-              `LeftSubsumesRight
-        else if Boolean.is_false lpos then
-          match cmp with
-          | `LeftSmallerThanRight ->
-              `LeftSubsumesRight
-          | `RightSmallerThanLeft ->
-              `RightSubsumesLeft
-        else `NotComparable
+    if Bool.equal lhs.can_be_zero rhs.can_be_zero then
+      match ItvPure.xcompare ~lhs:lhs.length ~rhs:rhs.length with
+      | `Equal ->
+          `Equal
+      | `NotComparable ->
+          `NotComparable
+      | `LeftSubsumesRight ->
+          `LeftSubsumesRight
+      | `RightSubsumesLeft ->
+          `RightSubsumesLeft
+      | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp ->
+          let lpos = ItvPure.le_sem ItvPure.zero lhs.length in
+          let rpos = ItvPure.le_sem ItvPure.zero rhs.length in
+          if not (Boolean.equal lpos rpos) then `NotComparable
+          else if Boolean.is_true lpos then
+            match cmp with
+            | `LeftSmallerThanRight ->
+                `RightSubsumesLeft
+            | `RightSmallerThanLeft ->
+                `LeftSubsumesRight
+          else if Boolean.is_false lpos then
+            match cmp with
+            | `LeftSmallerThanRight ->
+                `LeftSubsumesRight
+            | `RightSmallerThanLeft ->
+                `RightSubsumesLeft
+          else `NotComparable
+    else `NotComparable
 
 
   let itv_big = ItvPure.of_int 1_000_000
 
-  let check length =
+  let check {length; can_be_zero} =
     match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with
     | `Equal | `RightSubsumesLeft ->
-        {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false}
+        if can_be_zero then {report_issue_type= NotIssue; propagate= false}
+        else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false}
     | `LeftSmallerThanRight ->
         {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
     | _ -> (
@@ -181,8 +188,12 @@ module AllocSizeCondition = struct
               else {report_issue_type= NotIssue; propagate} ) )
 
 
-  let subst eval_sym length =
-    match ItvPure.subst length eval_sym with NonBottom length -> Some length | Bottom -> None
+  let subst eval_sym {length; can_be_zero} =
+    match ItvPure.subst length eval_sym with
+    | NonBottom length ->
+        Some {length; can_be_zero}
+    | Bottom ->
+        None
 end
 
 module ArrayAccessCondition = struct
@@ -908,8 +919,9 @@ module ConditionSet = struct
          latest_prune condset
 
 
-  let add_alloc_size location ~length val_traces latest_prune condset =
-    AllocSizeCondition.make ~length |> Condition.make_alloc_size
+  let add_alloc_size location ~can_be_zero ~length val_traces latest_prune condset =
+    AllocSizeCondition.make ~can_be_zero ~length
+    |> Condition.make_alloc_size
     |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset
 
 

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -50,6 +50,7 @@ module ConditionSet : sig
 
   val add_alloc_size :
        Location.t
+    -> can_be_zero:bool
     -> length:ItvPure.t
     -> BufferOverrunTrace.Set.t
     -> BufferOverrunDomain.LatestPrune.t

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

@@ -83,6 +83,7 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OV
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 11]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, malloc_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp

@@ -137,3 +137,7 @@ void array_rev_iter_Bad() {
   }
   a[a[0]] = 0;
 }
+
+void malloc_zero_Bad() { int* a = (int*)malloc(sizeof(int) * 0); }
+
+void new_array_zero_Good() { int* a = new int[0]; }

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -61,7 +61,7 @@ class Array {
     a = new ArrayList<>(-1);
   }
 
-  void zero_alloc_Good_FP() {
+  void zero_alloc_Good() {
     a = new ArrayList<>(0);
   }
 

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

@@ -5,6 +5,5 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
-codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.zero_alloc_Good_FP():void, 1, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]