diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 17c6abe33..81904885c 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -360,40 +360,46 @@ module BinaryOperationCondition = struct let pp_description = pp + let is_mult_one binop lhs rhs = + equal_binop binop Mult && (ItvPure.is_one lhs || ItvPure.is_one rhs) + + let check {binop; typ; integer_widths; lhs; rhs} = - let v = - match binop with - | Plus -> - ItvPure.plus lhs rhs - | Minus -> - ItvPure.minus lhs rhs - | Mult -> - ItvPure.mult lhs rhs - in - let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in - let typ_lb, typ_ub = - let lb, ub = Typ.range_of_ikind integer_widths typ in - (Bound.of_big_int lb, Bound.of_big_int ub) - 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 - 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 - 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) - then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false} + if is_mult_one binop lhs rhs then {report_issue_type= None; propagate= false} else - let is_symbolic = ItvPure.is_symbolic v in - let report_issue_type = - if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5 + let v = + match binop with + | Plus -> + ItvPure.plus lhs rhs + | Minus -> + ItvPure.minus lhs rhs + | Mult -> + ItvPure.mult lhs rhs in - {report_issue_type; propagate= is_symbolic} + let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in + let typ_lb, typ_ub = + let lb, ub = Typ.range_of_ikind integer_widths typ in + (Bound.of_big_int lb, Bound.of_big_int ub) + 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 + 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 + 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) + then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false} + else + let is_symbolic = ItvPure.is_symbolic v in + let report_issue_type = + if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5 + in + {report_issue_type; propagate= is_symbolic} let make integer_widths bop ~lhs ~rhs = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index fcd6ec2ef..8e01d737d 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -568,6 +568,8 @@ module ItvPure = struct let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u + let is_one : t -> bool = fun (l, u) -> Bound.eq l Bound.one && Bound.eq u Bound.one + let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone let is_false : t -> bool = is_zero diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 655dbf1fd..5a98987c6 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -98,6 +98,8 @@ module ItvPure : sig val is_top : t -> bool + val is_one : 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 0b162e3f2..51ec561c5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -178,3 +178,15 @@ void use_uint64_max_Bad_FN() { uint64_t y = UINT64_MAX - 15; arr[x - y] = 0; } + +uint64_t unknown_uint(); + +void muliply_one_Good() { + uint64_t x = unknown_uint(); + uint64_t y = x * 1; +} + +void muliply_two_Bad() { + uint64_t x = unknown_uint(); + uint64_t y = x * 2; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 68ba155d9..f97d79a1c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -7,6 +7,7 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, I codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] 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, 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]