From 3f969414fea491ba76dcee886eee416920c9832b Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 19 Oct 2018 01:23:33 -0700 Subject: [PATCH] [inferbo] Check integer overflow when really need Summary: It avoids checking integer overflow when it definitely cannot happen. For example, it does not check integer overflow of addition when one of parameters is a negative number, or underflow of subtraction when its first parameter is a positive number. Reviewed By: mbouaziz Differential Revision: D10446161 fbshipit-source-id: b8c86e1b2 --- .../bufferOverrunProofObligations.ml | 36 +++++++++++-- infer/src/bufferoverrun/itv.ml | 2 + infer/src/bufferoverrun/itv.mli | 6 +++ .../codetoanalyze/c/bufferoverrun/arith.c | 50 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 5 +- .../codetoanalyze/java/performance/issues.exp | 1 - 6 files changed, 93 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 81904885c..eb53761a7 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -364,7 +364,31 @@ module BinaryOperationCondition = struct equal_binop binop Mult && (ItvPure.is_one lhs || ItvPure.is_one rhs) - let check {binop; typ; integer_widths; lhs; rhs} = + let should_check {binop; typ; lhs; rhs} = + let cannot_underflow, cannot_overflow = + match (binop, Typ.ikind_is_unsigned typ) with + | Plus, true -> + (true, false) + | Minus, true -> + (false, true) + | Mult, true -> + (true, false) + | Plus, false -> + ( ItvPure.is_ge_zero lhs || ItvPure.is_ge_zero rhs + , ItvPure.is_le_zero lhs || ItvPure.is_le_zero rhs ) + | Minus, false -> + ( ItvPure.is_ge_zero lhs || ItvPure.is_le_zero rhs + , ItvPure.is_le_mone lhs || ItvPure.is_ge_zero rhs ) + | Mult, false -> + ( (ItvPure.is_ge_zero lhs && ItvPure.is_ge_zero rhs) + || (ItvPure.is_le_zero lhs && ItvPure.is_le_zero rhs) + , (ItvPure.is_ge_zero lhs && ItvPure.is_le_zero rhs) + || (ItvPure.is_le_zero lhs && ItvPure.is_ge_zero rhs) ) + in + (not cannot_underflow, not cannot_overflow) + + + let check ({binop; typ; integer_widths; lhs; rhs} as c) = if is_mult_one binop lhs rhs then {report_issue_type= None; propagate= false} else let v = @@ -381,18 +405,20 @@ module BinaryOperationCondition = struct let lb, ub = Typ.range_of_ikind integer_widths typ in (Bound.of_big_int lb, Bound.of_big_int ub) in + let check_underflow, check_overflow = should_check c in if (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *) - Bound.le v_ub typ_ub && Bound.le typ_lb v_lb + ((not check_underflow) || Bound.le typ_lb v_lb) + && ((not check_overflow) || Bound.le v_ub typ_ub) then {report_issue_type= None; propagate= false} else if (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *) - Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb + (check_underflow && Bound.lt v_ub typ_lb) || (check_overflow && Bound.lt typ_ub v_lb) then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false} else if (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *) - (Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb) - || (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub) + (check_underflow && Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb) + || (check_overflow && Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub) then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false} else let is_symbolic = ItvPure.is_symbolic v in diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 8e01d737d..1a8cd63cf 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -580,6 +580,8 @@ module ItvPure = struct let is_le_zero : t -> bool = fun (_, ub) -> Bound.le ub Bound.zero + let is_le_mone : t -> bool = fun (_, ub) -> Bound.le ub Bound.mone + let range : t -> ItvRange.t = fun (lb, ub) -> ItvRange.of_bounds ~lb ~ub let neg : t -> t = diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 5a98987c6..6309ca853 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -100,6 +100,12 @@ module ItvPure : sig val is_one : t -> bool + val is_ge_zero : t -> bool + + val is_le_zero : t -> bool + + val is_le_mone : t -> bool + val ( <= ) : lhs:t -> rhs:t -> bool val have_similar_bounds : t -> t -> bool diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 51ec561c5..c8fe89d31 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -190,3 +190,53 @@ void muliply_two_Bad() { uint64_t x = unknown_uint(); uint64_t y = x * 2; } + +void minus_one_Good() { + uint64_t x = unknown_uint(); + if (x > 0) { + uint64_t y = x - 1; + } +} + +void minus_one_Bad() { + uint64_t x = unknown_uint(); + if (x >= 0) { + uint64_t y = x - 1; + } +} + +int64_t unknown_int(); + +void plus_one_Good() { + int64_t x = unknown_int(); + if (x < INT64_MAX) { + int64_t y = x + 1; + } +} + +void plus_one_Bad() { + int64_t x = unknown_int(); + if (x <= INT64_MAX) { + int64_t y = x + 1; + } +} + +void minus_minimum_Good() { + int64_t x = -1; + int64_t y = x - INT64_MIN; +} + +void minus_minimum_Bad() { + int64_t x = 0; + int64_t y = x - INT64_MIN; +} + +void mult_minimum_Good() { + int64_t x = 1; + int64_t y = x * INT64_MIN; +} + +void mult_minimum_Bad() { + int64_t x = -1; + int64_t y = x * INT64_MIN; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index f97d79a1c..7c4c48427 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -5,16 +5,19 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (0 - -9223372036854775808):signed64] +codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] * 2):unsigned64] +codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-1 * -9223372036854775808):signed64] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19] +codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ] -codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([1, +oo] - 1):signed32] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3fc5ff5bf..ed61d19d5 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -96,7 +96,6 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: j,Assignment,Assignment,Assignment,Assignment,Binop: ([-oo, 9] + 1):signed32] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1]