From 05ec029e504d1c20c863e42b8121c85c868406ff Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 8 Jan 2019 18:49:17 -0800 Subject: [PATCH] [inferbo] Suppress intended integer overflow Summary: It suppresses intended integer overflows that generate hash values or random numbers. For judging that the intention of integer overflow, it applies a heuristics: checking if traces of issues include a whitelisted words, e.g., "rand" or "seed". While we would be able to suppress all integer overflows of unsigned integers since they have defined behaviors, we don't want to miss unintended integer overflows, e.g., that on unsigned index value. Depends on D13595958 Reviewed By: mbouaziz Differential Revision: D13595967 fbshipit-source-id: 8d3aca5a7 --- infer/src/bufferoverrun/absLoc.ml | 7 +++ infer/src/bufferoverrun/bounds.ml | 12 ++++ infer/src/bufferoverrun/bounds.mli | 2 + .../bufferOverrunProofObligations.ml | 24 ++++++-- infer/src/bufferoverrun/bufferOverrunTrace.ml | 23 +++++++ infer/src/bufferoverrun/itv.ml | 2 + infer/src/bufferoverrun/itv.mli | 2 + infer/src/bufferoverrun/symb.ml | 17 ++++++ infer/src/bufferoverrun/symb.mli | 4 ++ .../codetoanalyze/cpp/bufferoverrun/arith.cpp | 60 +++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 3 + 11 files changed, 151 insertions(+), 5 deletions(-) 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]