From 1cbcbe6fb3f0230deaa01dde3dcfef4ff5629f06 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sat, 10 Nov 2018 01:12:15 -0800 Subject: [PATCH] [inferbo] Improve division on constant Reviewed By: mbouaziz, jvillard Differential Revision: D12921835 fbshipit-source-id: 9d0e85696 --- infer/src/bufferoverrun/bounds.ml | 2 ++ .../codetoanalyze/c/bufferoverrun/arith.c | 28 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ .../codetoanalyze/c/performance/issues.exp | 2 -- 4 files changed, 32 insertions(+), 2 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index f90efbdb9..58db2e36f 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -750,6 +750,8 @@ module Bound = struct Some (if NonZeroInt.is_positive n then MInf else PInf) | PInf -> Some (if NonZeroInt.is_positive n then PInf else MInf) + | Linear (c, x') when SymLinear.is_zero x' -> + Some (Linear (Z.(c / (n :> Z.t)), SymLinear.zero)) | Linear (c, x') when NonZeroInt.is_multiple c n -> ( match SymLinear.exact_div_const_exn x' n with | x'' -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 9d5dc0975..6ce024d86 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -307,6 +307,34 @@ void minmax_div_const_Bad(int n) { } } +void div_const_Good() { + int a[3]; + int x = 5 / 2; + a[x] = 0; +} + +void div_const_Bad() { + int a[2]; + int x = 5 / 2; + a[x] = 0; +} + +void div_const2_FP(int n) { + int a[1]; + int x = (n * 2 + 1) / 2; + a[x] = 0; +} + +void minmax_div_const2_Good() { + div_const2(-1); + div_const2(0); +} + +void minmax_div_const2_Bad_FN() { + div_const2(1); + div_const2(-2); +} + uint32_t unknown_nat() { uint32_t x = unknown_function(); if (x >= 0) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 90c4c0a2e..a61f9b80f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -5,6 +5,8 @@ codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index cb9944784..924c2610e 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -167,10 +167,8 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUT codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Binop: (n + [-oo, +oo]):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 15, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Assignment,Binop: ([-oo, +oo] - 1):signed32] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * m.ub + 4 * (1+max(0, m.ub)), degree = 1]