diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 16323775e..8c0c7fb3e 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -304,22 +304,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 ?boolean partial = - let s = make_symbol ~unsigned ?boolean (path_of_partial partial) in + let of_path path_of_partial make_symbol ~unsigned ?non_int partial = + let s = make_symbol ~unsigned ?non_int (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 ~boolean:false + of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false ~non_int:false let of_length_path ~is_void = - of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~boolean:false + of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~non_int:false - let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~boolean:false + let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~non_int: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 962f55981..73cca2a45 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -36,7 +36,7 @@ module Bound : sig val pinf : t val of_normal_path : - Symb.Symbol.make_t -> unsigned:bool -> ?boolean:bool -> Symb.SymbolPath.partial -> t + Symb.Symbol.make_t -> unsigned:bool -> ?non_int: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 dca99b2c9..13e3fbc09 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -433,11 +433,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 ~boolean = + let itv_val ~non_int = 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 ~boolean path) + of_itv ~traces (Itv.of_normal_path ~unsigned ~non_int path) in let ptr_to_c_array_alloc deref_path size = let allocsite = Allocsite.make_symbol deref_path in @@ -450,10 +450,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 ~boolean:false + | Tint IBool | Tfloat _ | Tfun _ | TVar _ -> + itv_val ~non_int:true + | Tint _ | Tvoid -> + itv_val ~non_int:false | Tptr (elt, _) -> if is_java || SPath.is_this path then let deref_kind = @@ -503,7 +503,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 ~boolean:false + itv_val ~non_int:false | None -> let l = Loc.of_path path in let traces = traces_of_loc l in @@ -623,7 +623,7 @@ module MemPure = struct match filter_loc loc with | Some loop_head_loc -> let itv = Val.get_itv v in - if Itv.has_only_boolean_symbols itv then acc + if Itv.has_only_non_int_symbols itv then acc else Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial |> Polynomials.NonNegativePolynomial.mult acc diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index aac12e9e9..1e5af6883 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -416,9 +416,9 @@ module ItvPure = struct fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u) - let has_only_boolean_symbols x = + let has_only_non_int_symbols x = let symbols = get_symbols x in - (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_boolean symbols + (not (SymbolSet.is_empty symbols)) && SymbolSet.for_all Symb.Symbol.is_non_int symbols let make_positive : t -> t = @@ -440,7 +440,7 @@ module ItvPure = struct (b, b) - let of_normal_path ~unsigned ?boolean = of_path (Bound.of_normal_path ~unsigned ?boolean) + let of_normal_path ~unsigned ?non_int = of_path (Bound.of_normal_path ~unsigned ?non_int) let of_offset_path ~is_void = of_path (Bound.of_offset_path ~is_void) @@ -673,8 +673,8 @@ let max_of_ikind integer_type_widths ikind = NonBottom (ItvPure.max_of_ikind integer_type_widths ikind) -let of_normal_path ~unsigned ?boolean path = - NonBottom (ItvPure.of_normal_path ~unsigned ?boolean path) +let of_normal_path ~unsigned ?non_int path = + NonBottom (ItvPure.of_normal_path ~unsigned ?non_int path) let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void path) @@ -687,4 +687,4 @@ let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of pat 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 +let has_only_non_int_symbols = bind1bool ItvPure.has_only_non_int_symbols diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 971766cd5..09cb61d98 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 -> ?boolean:bool -> Symb.SymbolPath.partial -> t +val of_normal_path : unsigned:bool -> ?non_int:bool -> Symb.SymbolPath.partial -> t val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t @@ -243,4 +243,4 @@ 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 +val has_only_non_int_symbols : t -> bool diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 5fcaf80b3..8c81dab2a 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -252,11 +252,13 @@ module Symbol = struct let compare_extra_bool _ _ = 0 + (* NOTE: non_int represents the symbols that are not integer type, + so that their ranges are not used in the cost checker. *) type t = - | OneValue of {unsigned: extra_bool; boolean: extra_bool; path: SymbolPath.t} + | OneValue of {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t} | BoundEnd of { unsigned: extra_bool - ; boolean: extra_bool + ; non_int: extra_bool ; path: SymbolPath.t ; bound_end: BoundEnd.t } [@@deriving compare] @@ -264,7 +266,7 @@ module Symbol = struct let pp : F.formatter -> t -> unit = fun fmt s -> match s with - | OneValue {unsigned; boolean; path} | BoundEnd {unsigned; boolean; path} -> + | OneValue {unsigned; non_int; path} | BoundEnd {unsigned; non_int; path} -> SymbolPath.pp fmt path ; ( if Config.developer_mode then match s with @@ -273,7 +275,7 @@ module Symbol = struct | OneValue _ -> () ) ; if Config.bo_debug > 1 then - F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if boolean then "b" else "") + F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if non_int then "n" else "") let compare s1 s2 = @@ -304,21 +306,21 @@ module Symbol = struct SymbolPath.equal path1 path2 - type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t + type make_t = unsigned:bool -> ?non_int:bool -> SymbolPath.t -> t let make_onevalue : make_t = - fun ~unsigned ?(boolean = false) path -> OneValue {unsigned; boolean; path} + fun ~unsigned ?(non_int = false) path -> OneValue {unsigned; non_int; path} let make_boundend : BoundEnd.t -> make_t = - fun bound_end ~unsigned ?(boolean = false) path -> BoundEnd {unsigned; boolean; path; bound_end} + fun bound_end ~unsigned ?(non_int = false) path -> BoundEnd {unsigned; non_int; 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 is_non_int : t -> bool = function OneValue {non_int} | BoundEnd {non_int} -> non_int let path = function OneValue {path} | BoundEnd {path} -> path diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index a8f87f27a..634a5bac5 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -100,7 +100,7 @@ module Symbol : sig val is_unsigned : t -> bool - val is_boolean : t -> bool + val is_non_int : t -> bool val pp_mark : markup:bool -> F.formatter -> t -> unit @@ -112,7 +112,7 @@ module Symbol : sig val check_bound_end : t -> BoundEnd.t -> unit - type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t + type make_t = unsigned:bool -> ?non_int: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 ec3923f9e..d9f2b42d1 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -152,4 +152,22 @@ public class Cost_test { } } } + + // Cost should not include the symbol of f. + void ignore_float_symbols_constant(float f) { + for (; f < (float) 1.0; ) { + if (rand()) { + f = (float) 1.0; + } + } + } + + // Cost should not include the symbol of d. + void ignore_double_symbols_constant(double d) { + for (; d < (double) 1.0; ) { + if (rand()) { + d = 1.0; + } + } + } }