[inferbo] Avoid precision-losing pruning

Summary:
In this diff, it avoids a precision-losing pruning, which was needed
to keep effects of assume commands.

```
unsigned int c = a + b; // (1)
if (c > 0) { // (2)
  char result[c];
  result[c - 1] = 0; // (4)
}
```

For example, in the example, `c` is assigned by `[a+b,a+b]` at (1),
then it tried to prune the lower bound of `c` to 1 at (2) while losing
precision, in order to say `c - 1` at (4) is safe in terms of integer
underflow.  Instead, it could not say that `c - 1` is smaller than `c`
in the buffer access, because the former is analyzed to `[0,a+b-1]` and
the latter `[1,a+b]` at (4).

Now, the situation has changed.  By adopting conditional proof
obligation (D13749914), the FP of integer overflow can be suppressed
without the precision-losing pruning.

Reviewed By: mbouaziz

Differential Revision: D14122770

fbshipit-source-id: 634744e99

infer/src/bufferoverrun/bounds.ml

@@ -558,7 +558,7 @@ module Bound = struct
 
 
   let overapprox_min original_b1 b2 =
-    let rec overapprox_min b1 b2 =
+    let overapprox_min b1 b2 =
       exact_min b1 b2 ~otherwise:(fun b1 b2 ->
           match (b1, b2) with
           | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1)
@@ -607,17 +607,9 @@ module Bound = struct
               let v = if Z.leq vmin vmeet && Z.leq vmeet vmax then vmeet else vmax in
               let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in
               mk_MinMax (c1, sign1, minmax1, d, s1)
-          | _ -> (
-            match big_int_ub b2 with
-            | Some v2 when not (is_const b2) ->
-                overapprox_min b1 (Linear (v2, SymLinear.zero))
-            | _ -> (
-              match big_int_ub b1 with
-              | Some v1 when not (is_const b1) ->
-                  overapprox_min (Linear (v1, SymLinear.zero)) b2
-              | _ ->
-                  (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *)
-                  original_b1 ) ) )
+          | _ ->
+              (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *)
+              original_b1 )
     in
     overapprox_min original_b1 b2
 

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

@@ -260,7 +260,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALW
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
-codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_Good_FP, 0, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,<Offset trace>,Parameter `a`,Assignment,<Length trace>,Parameter `a`,Assignment,Array declaration,Array access: Offset: [0, 29] Size: [1, 30] by call to `null_pruning_symbols` ]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `a`,Assignment,<Length trace>,Parameter `a`,Assignment,Array declaration,Array access: Offset: [-1, 9] Size: [0, 10] by call to `null_pruning_symbols` ]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `a`,Assignment,Binary operation: ([0, 10] - 1):unsigned32 by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -182,4 +182,18 @@ void null_pruning_symbols(unsigned int a, unsigned int b) {
   }
 }
 
-void call_null_pruning_symbols_Good_FP() { null_pruning_symbols(10, 20); }
+void call_null_pruning_symbols_1_Good() { null_pruning_symbols(10, 20); }
+
+void call_null_pruning_symbols_2_Good() { null_pruning_symbols(0, 0); }
+
+int unknown_function();
+
+void call_null_pruning_symbols_3_Good_FP() {
+  unsigned int c;
+  if (unknown_function()) {
+    c = 0;
+  } else {
+    c = 10;
+  }
+  null_pruning_symbols(c, 0);
+}