diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 08330065c..f8b41bba1 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -208,6 +208,10 @@ module Loc = struct Allocsite.represents_multiple_values allocsite | Field (l, _) -> represents_multiple_values l + + + let exists_str ~f l = + Option.exists (get_path l) ~f:(fun path -> Symb.SymbolPath.exists_str_partial ~f path) end module PowLoc = struct @@ -240,6 +244,9 @@ module PowLoc = struct let subst x (eval_locpath : eval_locpath) = fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty + + + let exists_str ~f x = exists (fun l -> Loc.exists_str ~f l) x end let always_strong_update = false diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 3176a413d..df501b046 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -180,6 +180,9 @@ module SymLinear = struct Some (Symb.Symbol.path s1) | _ -> None + + + let exists_str ~f x = M.exists (fun k _ -> Symb.Symbol.exists_str ~f k) x end module Bound = struct @@ -943,6 +946,15 @@ module Bound = struct SymLinear.is_same_symbol se1 se2 | _ -> None + + + let exists_str ~f = function + | MInf | PInf -> + false + | Linear (_, s) -> + SymLinear.exists_str ~f s + | MinMax (_, _, _, _, s) -> + Symb.Symbol.exists_str ~f s end type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 9a7ccd427..e796e0ae7 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -116,6 +116,8 @@ module Bound : sig val simplify_bound_ends_from_paths : t -> t val is_same_symbol : t -> t -> Symb.SymbolPath.t option + + val exists_str : f:(string -> bool) -> t -> bool end type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 161e0ba30..4af9cd88a 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -74,6 +74,8 @@ module ConditionTrace = struct let has_risky ct = ValTrace.Issue.has_risky ct.val_traces + let exists_str ~f ct = ValTrace.Issue.exists_str ~f ct.val_traces + let check ~issue_type_u5 ~issue_type_r2 : _ t0 -> IssueType.t option = fun ct -> if has_risky ct then Some issue_type_r2 @@ -515,8 +517,19 @@ module BinaryOperationCondition = struct (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= NotIssue; propagate= false} + let is_deliberate_integer_overflow = + let whitelist = ["lfsr"; "prng"; "rand"; "seed"] in + let f x = + List.exists whitelist ~f:(fun whitelist -> String.is_substring x ~substring:whitelist) + in + fun {typ; lhs; rhs} ct -> + Typ.ikind_is_unsigned typ + && (ConditionTrace.exists_str ~f ct || ItvPure.exists_str ~f lhs || ItvPure.exists_str ~f rhs) + + + let check ({binop; typ; integer_widths; lhs; rhs} as c) (trace : ConditionTrace.t) = + if is_mult_one binop lhs rhs || is_deliberate_integer_overflow c trace then + {report_issue_type= NotIssue; propagate= false} else let v = match binop with @@ -658,13 +671,14 @@ module Condition = struct BinaryOperationCondition.pp_description ~markup fmt c - let check = function + let check cond trace = + match cond with | AllocSize c -> AllocSizeCondition.check c | ArrayAccess c -> ArrayAccessCondition.check c | BinaryOperation c -> - BinaryOperationCondition.check c + BinaryOperationCondition.check c trace let forget_locs locs x = @@ -750,7 +764,7 @@ module ConditionWithTrace = struct let check cwt = - let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond in + let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond cwt.trace in match report_issue_type with | NotIssue | SymbolicIssue -> checked diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index a57e19f29..76dfd4c32 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -105,6 +105,25 @@ module BoTrace = struct let has_risky = final_exists ~f:(function UnknownFrom _ -> false | RiskyLibCall _ -> true) + let exists_str ~f = + let rec helper = function + | Empty | Final _ -> + false + | Elem {kind= elem; from} -> + ( match elem with + | Assign locs -> + PowLoc.exists_str ~f locs + | Parameter l -> + Loc.exists_str ~f l + | _ -> + false ) + || helper from + | Call {caller; callee} -> + helper caller || helper callee + in + helper + + let final_err_desc = function | UnknownFrom pname_opt -> F.asprintf "Unknown value from: %a" pp_pname_opt pname_opt @@ -187,6 +206,8 @@ module Set = struct let has_risky t = exists BoTrace.has_risky t + let exists_str ~f t = exists (BoTrace.exists_str ~f) t + let make_err_trace depth set tail = if is_empty set then tail else BoTrace.make_err_trace depth (choose_shortest set) tail @@ -232,6 +253,8 @@ module Issue = struct let has_risky = has_common ~f:Set.has_risky + let exists_str ~f = has_common ~f:(Set.exists_str ~f) + let binary_labels = function ArrayAccess -> ("Offset", "Length") | Binop -> ("LHS", "RHS") let pp_elem f = function Alloc -> F.pp_print_string f "Alloc" diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 2913ea7bd..4248354e8 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -50,6 +50,8 @@ module ItvPure = struct let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false + let exists_str ~f (l, u) = Bound.exists_str ~f l || Bound.exists_str ~f u + let ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index a8f3a0928..6ce51a1b9 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -96,6 +96,8 @@ module ItvPure : sig val succ : t -> t val mult : t -> t -> t + + val exists_str : f:(string -> bool) -> t -> bool end include module type of AbstractDomain.BottomLifted (ItvPure) diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index a331d3753..74f57c65a 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -127,6 +127,20 @@ module SymbolPath = struct false | Deref (_, p) | Field (_, p) -> represents_callsite_sound_partial p + + + let rec exists_str_partial ~f = function + | Pvar pvar -> + f (Pvar.to_string pvar) + | Deref (_, x) -> + exists_str_partial ~f x + | Field (fld, x) -> + f (Typ.Fieldname.to_string fld) || exists_str_partial ~f x + | Callsite _ -> + false + + + let exists_str ~f = function Normal p | Offset p | Length p -> exists_str_partial ~f p end module Symbol = struct @@ -195,6 +209,9 @@ module Symbol = struct let assert_bound_end s be = match s with OneValue _ -> () | BoundEnd {bound_end} -> assert (BoundEnd.equal be bound_end) + + + let exists_str ~f = function OneValue {path} | BoundEnd {path} -> SymbolPath.exists_str ~f path end module SymbolSet = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 430761cfa..76c8da320 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -57,6 +57,8 @@ module SymbolPath : sig val represents_multiple_values_sound : partial -> bool val represents_callsite_sound_partial : partial -> bool + + val exists_str_partial : f:(string -> bool) -> partial -> bool end module Symbol : sig @@ -81,6 +83,8 @@ module Symbol : sig val make_onevalue : unsigned:bool -> SymbolPath.t -> t val make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t + + val exists_str : f:(string -> bool) -> t -> bool end module SymbolSet : sig diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp index cd4e31a7d..08777d4e5 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp @@ -4,6 +4,8 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ +#include + void sizeof_bool_Good() { int a[2]; int z = sizeof(bool); // z is 1 (byte) @@ -55,3 +57,61 @@ void bool_overflow2_Good_FP() { a[5] = 0; } } + +class RG { + public: + RG(uint32_t init) { + seed = init; + x = init; + } + + inline uint32_t integer_overflow_rand() { + uint32_t max = 4294967295; + return (seed = seed * max); + } + + inline uint32_t integer_overflow_x() { + uint32_t max = 4294967295; + return (x = x * max); + } + + private: + uint32_t seed; + uint32_t x; +}; + +uint32_t call_integer_overflow_rand_Good() { + RG generator(4294967295); + return generator.integer_overflow_rand(); +} + +uint32_t call_integer_overflow_x_Bad() { + RG generator(4294967295); + return generator.integer_overflow_x(); +} + +struct S_prng_lfsr { + uint32_t prng_lfsr; +}; + +void integer_overflow_field_Good(struct S_prng_lfsr* c) { + c->prng_lfsr = 1; + c->prng_lfsr = 0 - c->prng_lfsr; +} + +struct S_x { + uint32_t x; +}; + +void integer_overflow_field_Bad(struct S_x* c) { + c->x = 1; + c->x = 0 - c->x; +} + +uint32_t integer_overflow_param_1(uint32_t seed) { return seed - 1; } + +void call_integer_overflow_param_1_Good() { integer_overflow_param_1(0); } + +uint32_t integer_overflow_param_2(uint32_t x) { return x - 1; } + +void call_integer_overflow_param_2_Bad() { integer_overflow_param_2(0); } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 70947881d..3c3dcce5a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -8,6 +8,9 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 2, CONDITION_ALWAY codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_param_2_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `x`,Binary operation: (0 - 1):unsigned32 by call to `integer_overflow_param_2` ] +codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_x_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter `init`,Assignment,Call,,Parameter `this->x`,,Assignment,Binary operation: (4294967295 × 4294967295):unsigned32 by call to `RG_integer_overflow_x` ] +codetoanalyze/cpp/bufferoverrun/arith.cpp, integer_overflow_field_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1]