From c91d0a777d9692cf77ec2a287d588a4cdc886b67 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 18 Feb 2019 17:13:09 -0800 Subject: [PATCH] [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 | 16 ++++------------ .../codetoanalyze/c/bufferoverrun/issues.exp | 3 ++- .../c/bufferoverrun/prune_constant.c | 16 +++++++++++++++- 3 files changed, 21 insertions(+), 14 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 84dc7adc2..2162dde3b 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1c30f205f..27bbb732b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [,Call,Assignment,Assignment,,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, [,Call,Assignment,Assignment,,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, [,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,,Parameter `a`,Assignment,,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,,Parameter `a`,Assignment,,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,,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,,Parameter `x`,,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,,Parameter `x`,,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] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index b3317b123..057b4a662 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/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); +}