diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index e459e35a7..1feec5b1a 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -298,18 +298,22 @@ module Bound = struct let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s) - let of_path path_of_partial make_symbol ~unsigned partial = - let s = make_symbol ~unsigned (path_of_partial partial) in + let of_path path_of_partial make_symbol ~unsigned ?boolean partial = + let s = make_symbol ~unsigned ?boolean (path_of_partial partial) in of_sym (SymLinear.singleton_one s) let of_normal_path = of_path Symb.SymbolPath.normal - let of_offset_path ~is_void = of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false + let of_offset_path ~is_void = + of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false ~boolean:false - let of_length_path ~is_void = of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true - let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true + let of_length_path ~is_void = + of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~boolean:false + + + let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~boolean:false let is_path_of ~f = function | Linear (n, se) when Z.(equal n zero) -> diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 3fc960667..ed8c995c1 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -35,7 +35,8 @@ module Bound : sig val pinf : t - val of_normal_path : Symb.Symbol.make_t -> unsigned:bool -> Symb.SymbolPath.partial -> t + val of_normal_path : + Symb.Symbol.make_t -> unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t val of_offset_path : is_void:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 7617b78ee..e31ca4a3b 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -424,11 +424,11 @@ module Val = struct let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in TraceSet.singleton location trace in - let itv_val () = + let itv_val ~boolean = let l = Loc.of_path path in let traces = traces_of_loc l in let unsigned = Typ.is_unsigned_int typ in - of_itv ~traces (Itv.of_normal_path ~unsigned path) + of_itv ~traces (Itv.of_normal_path ~unsigned ~boolean path) in let ptr_to_c_array_alloc deref_path size = let allocsite = Allocsite.make_symbol deref_path in @@ -441,8 +441,10 @@ module Val = struct (if may_last_field then ", may_last_field" else "") (if is_java then ", is_java" else "") ; match typ.Typ.desc with + | Tint IBool -> + itv_val ~boolean:true | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ -> - itv_val () + itv_val ~boolean:false | Tptr (elt, _) -> if is_java || SPath.is_this path then let deref_kind = @@ -492,7 +494,7 @@ module Val = struct let length = Itv.of_length_path ~is_void:false path in of_java_array_alloc allocsite ~length ~traces | Some JavaInteger -> - itv_val () + itv_val ~boolean:false | None -> let l = Loc.of_path path in let traces = traces_of_loc l in @@ -611,8 +613,11 @@ module MemPure = struct (fun loc (_, v) acc -> match filter_loc loc with | Some loop_head_loc -> - v |> Val.get_itv |> Itv.range loop_head_loc |> Itv.ItvRange.to_top_lifted_polynomial - |> Polynomials.NonNegativePolynomial.mult acc + let itv = Val.get_itv v in + if Itv.has_only_boolean_symbols itv then acc + else + Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial + |> Polynomials.NonNegativePolynomial.mult acc | None -> acc ) mem Polynomials.NonNegativePolynomial.one diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 4f5616e5c..3f9e66f77 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -414,6 +414,11 @@ module ItvPure = struct fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u) + let has_only_boolean_symbols x = + let symbols = get_symbols x in + (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_boolean symbols + + let make_positive : t -> t = fun ((l, u) as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x @@ -433,7 +438,7 @@ module ItvPure = struct (b, b) - let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned) + let of_normal_path ~unsigned ?boolean = of_path (Bound.of_normal_path ~unsigned ?boolean) let of_offset_path ~is_void = of_path (Bound.of_offset_path ~is_void) @@ -666,7 +671,9 @@ let max_of_ikind integer_type_widths ikind = NonBottom (ItvPure.max_of_ikind integer_type_widths ikind) -let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned path) +let of_normal_path ~unsigned ?boolean path = + NonBottom (ItvPure.of_normal_path ~unsigned ?boolean path) + let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void path) @@ -677,3 +684,5 @@ let of_modeled_path path = NonBottom (ItvPure.of_modeled_path path) let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of path) let is_length_path_of path = bind1_gen ~bot:false (ItvPure.is_length_path_of path) + +let has_only_boolean_symbols = bind1bool ItvPure.has_only_boolean_symbols diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 2f91f0c7d..971766cd5 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -231,7 +231,7 @@ val subst : t -> Bound.eval_sym -> t val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t -val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t +val of_normal_path : unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t @@ -242,3 +242,5 @@ val of_modeled_path : Symb.SymbolPath.partial -> t val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool val is_length_path_of : Symb.SymbolPath.partial -> t -> bool + +val has_only_boolean_symbols : t -> bool diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 6ba32300e..976ce55f6 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -247,14 +247,18 @@ module Symbol = struct let compare_extra_bool _ _ = 0 type t = - | OneValue of {unsigned: extra_bool; path: SymbolPath.t} - | BoundEnd of {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t} + | OneValue of {unsigned: extra_bool; boolean: extra_bool; path: SymbolPath.t} + | BoundEnd of + { unsigned: extra_bool + ; boolean: extra_bool + ; path: SymbolPath.t + ; bound_end: BoundEnd.t } [@@deriving compare] let pp : F.formatter -> t -> unit = fun fmt s -> match s with - | OneValue {unsigned; path} | BoundEnd {unsigned; path} -> + | OneValue {unsigned; boolean; path} | BoundEnd {unsigned; boolean; path} -> SymbolPath.pp fmt path ; ( if Config.developer_mode then match s with @@ -262,7 +266,8 @@ module Symbol = struct Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end) | OneValue _ -> () ) ; - if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if unsigned then 'u' else 's') + if Config.bo_debug > 1 then + F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if boolean then "b" else "") let compare s1 s2 = @@ -293,18 +298,22 @@ module Symbol = struct SymbolPath.equal path1 path2 - type make_t = unsigned:bool -> SymbolPath.t -> t + type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t + + let make_onevalue : make_t = + fun ~unsigned ?(boolean = false) path -> OneValue {unsigned; boolean; path} - let make_onevalue : make_t = fun ~unsigned path -> OneValue {unsigned; path} let make_boundend : BoundEnd.t -> make_t = - fun bound_end ~unsigned path -> BoundEnd {unsigned; path; bound_end} + fun bound_end ~unsigned ?(boolean = false) path -> BoundEnd {unsigned; boolean; path; bound_end} let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp let is_unsigned : t -> bool = function OneValue {unsigned} | BoundEnd {unsigned} -> unsigned + let is_boolean : t -> bool = function OneValue {boolean} | BoundEnd {boolean} -> boolean + let path = function OneValue {path} | BoundEnd {path} -> path let assert_bound_end s be = diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 7dc954723..f72705a58 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -100,6 +100,8 @@ module Symbol : sig val is_unsigned : t -> bool + val is_boolean : t -> bool + val pp_mark : markup:bool -> F.formatter -> t -> unit val equal : t -> t -> bool @@ -110,7 +112,7 @@ module Symbol : sig val assert_bound_end : t -> BoundEnd.t -> unit - type make_t = unsigned:bool -> SymbolPath.t -> t + type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t val make_onevalue : make_t diff --git a/infer/tests/codetoanalyze/java/performance/Cost_test.java b/infer/tests/codetoanalyze/java/performance/Cost_test.java index 0f787ea1e..ec3923f9e 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -119,4 +119,37 @@ public class Cost_test { // Cost: 1 private static void unitCostFunction() {} + + boolean rand() { + if (Math.random() > 0.5) { + return true; + } else { + return false; + } + } + + // Cost: Linear to n, not b + void ignore_boolean_symbols_linear(boolean b, int n) { + for (int i = 0; b && i < n; i++) { + b = true; + } + } + + // Cost should not include the symbol of b. + void ignore_boolean_symbols_constant1(boolean b) { + for (; b; ) { + if (rand()) { + b = true; + } + } + } + + // Cost should not include the symbol of b. + void ignore_boolean_symbols_constant2(boolean b) { + for (; b; ) { + if (rand()) { + b = false; + } + } + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 25d665835..4d738d002 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -87,6 +87,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7963049, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, O(k), degree = 1,{k},Loop at line 90] +codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.ignore_boolean_symbols_linear(boolean,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), O(n), degree = 1,{1+max(0, n)},Loop at line 133,{n},Loop at line 133] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop3(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 237, O(1), degree = 0]