From b50e1cba51be24b7ab93ad439566392c54bc4504 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 11 Nov 2019 02:24:35 -0800 Subject: [PATCH] [inferbo] Extend bound to express Min/Max(bound, bound) Summary: This diff extends bound domain to express Min/Max of another bounds, so it can keep some more precision in `Math.min/max`. limitation: `MinMaxB`, the constructor of the bound, can contain only linear expressions or previous min/max expressions. Reviewed By: ezgicicek Differential Revision: D18395365 fbshipit-source-id: fc90d27fd --- infer/src/bufferoverrun/bounds.ml | 98 +++++++++++++++---- infer/src/bufferoverrun/bounds.mli | 6 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 6 +- infer/src/bufferoverrun/itv.ml | 27 +++-- infer/src/bufferoverrun/itv.mli | 4 +- .../java/performance/MathTest.java | 8 ++ .../codetoanalyze/java/performance/issues.exp | 5 +- 7 files changed, 124 insertions(+), 30 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 23d600c3f..cf362ce1b 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -232,6 +232,7 @@ module Bound = struct | MInf | Linear of Z.t * SymLinear.t | MinMax of Z.t * Sign.t * MinMax.t * Z.t * Symb.Symbol.t + | MinMaxB of MinMax.t * t * t | PInf [@@deriving compare] @@ -251,7 +252,7 @@ module Bound = struct b - let pp_mark : markup:bool -> F.formatter -> t -> unit = + let rec pp_mark : markup:bool -> F.formatter -> t -> unit = fun ~markup f -> function | MInf -> F.pp_print_string f "-oo" @@ -268,6 +269,8 @@ module Bound = struct if Z.(equal c zero) then (Sign.pp ~need_plus:false) f sign else F.fprintf f "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ; F.fprintf f "%a(%a, %a)" MinMax.pp m Z.pp_print d (Symb.Symbol.pp_mark ~markup) x + | MinMaxB (m, x, y) -> + F.fprintf f "%a(%a, %a)" MinMax.pp m (pp_mark ~markup) x (pp_mark ~markup) y let pp = pp_mark ~markup:false @@ -296,6 +299,8 @@ module Bound = struct let is_zero : t -> bool = is_some_const Z.zero + let is_infty : t -> bool = function MInf | PInf -> true | _ -> false + let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true let is_minf = function MInf -> true | _ -> false @@ -345,13 +350,15 @@ module Bound = struct false ) - let is_symbolic : t -> bool = function + let rec is_symbolic : t -> bool = function | MInf | PInf -> false | Linear (_, se) -> not (SymLinear.is_empty se) | MinMax _ -> true + | MinMaxB (_, x, y) -> + is_symbolic x || is_symbolic y let mk_MinMax (c, sign, m, d, s) = @@ -377,7 +384,7 @@ module Bound = struct Some c | MinMax _ -> None - | MInf | PInf | Linear _ -> + | MinMaxB _ | MInf | PInf | Linear _ -> assert false @@ -390,7 +397,7 @@ module Bound = struct Some c | MinMax _ -> None - | MInf | PInf | Linear _ -> + | MinMaxB _ | MInf | PInf | Linear _ -> assert false @@ -401,7 +408,7 @@ module Bound = struct big_int_ub_of_minmax - let big_int_lb = function + let rec big_int_lb = function | MInf -> None | PInf -> @@ -410,9 +417,11 @@ module Bound = struct big_int_lb_of_minmax b | Linear (c, se) -> SymLinear.big_int_lb se |> Option.map ~f:(Z.( + ) c) + | MinMaxB (m, x, y) -> + Option.map2 (big_int_lb x) (big_int_lb y) ~f:(MinMax.eval_big_int m) - let big_int_ub = function + let rec big_int_ub = function | MInf -> assert false | PInf -> @@ -421,6 +430,8 @@ module Bound = struct big_int_ub_of_minmax b | Linear (c, se) -> SymLinear.big_int_ub se |> Option.map ~f:(Z.( + ) c) + | MinMaxB (m, x, y) -> + Option.map2 (big_int_ub x) (big_int_ub y) ~f:(MinMax.eval_big_int m) let linear_ub_of_minmax = function @@ -430,7 +441,7 @@ module Bound = struct Some (Linear (c, SymLinear.singleton_minus_one x)) | MinMax _ -> None - | MInf | PInf | Linear _ -> + | MinMaxB _ | MInf | PInf | Linear _ -> assert false @@ -441,7 +452,7 @@ module Bound = struct Some (Linear (c, SymLinear.singleton_minus_one x)) | MinMax _ -> None - | MInf | PInf | Linear _ -> + | MinMaxB _ | MInf | PInf | Linear _ -> assert false @@ -490,9 +501,17 @@ module Bound = struct | Linear (c, se), MinMax _ -> (SymLinear.is_le_zero se && le_opt2 Z.leq c (big_int_lb_of_minmax y)) || le_opt2 le x (linear_lb_of_minmax y) + | MinMaxB (Max, x1, x2), y -> + le x1 y && le x2 y + | MinMaxB (Min, x1, x2), y -> + le x1 y || le x2 y + | x, MinMaxB (Max, y1, y2) -> + le x y1 || le x y2 + | x, MinMaxB (Min, y1, y2) -> + le x y1 && le x y2 - let lt : t -> t -> bool = + let rec lt : t -> t -> bool = fun x y -> match (x, y) with | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf -> @@ -501,6 +520,14 @@ module Bound = struct le (Linear (Z.succ c, x)) y | MinMax (c, sign, min_max, d, x), _ -> le (mk_MinMax (Z.succ c, sign, min_max, d, x)) y + | MinMaxB (Max, x1, x2), y -> + lt x1 y && lt x2 y + | MinMaxB (Min, x1, x2), y -> + lt x1 y || lt x2 y + | x, MinMaxB (Max, y1, y2) -> + lt x y1 || lt x y2 + | x, MinMaxB (Min, y1, y2) -> + lt x y1 && lt x y2 | _, _ -> false @@ -509,11 +536,26 @@ module Bound = struct let eq : t -> t -> bool = fun x y -> le x y && le y x + let mk_MinMaxB (m, x, y) = + if le x y then match m with Min -> x | Max -> y + else if le y x then match m with Min -> y | Max -> x + else + match (x, y) with + | (Linear _ | MinMax _), (Linear _ | MinMax _) -> + MinMaxB (m, x, y) + | _, _ -> ( + match m with Min -> MInf | Max -> PInf ) + + + let of_minmax_bound_min x y = mk_MinMaxB (Min, x, y) + + let of_minmax_bound_max x y = mk_MinMaxB (Max, x, y) + let xcompare = PartialOrder.of_le ~le let is_const : t -> bool = function Linear (_, se) -> SymLinear.is_zero se | _ -> false - let neg : t -> t = function + let rec neg : t -> t = function | MInf -> PInf | PInf -> @@ -522,6 +564,8 @@ module Bound = struct if Z.(equal c zero) && SymLinear.is_zero x then b else Linear (Z.neg c, SymLinear.neg x) | MinMax (c, sign, min_max, d, x) -> mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x) + | MinMaxB (m, x, y) -> + mk_MinMaxB (MinMax.neg m, neg x, neg y) let exact_min : otherwise:(t -> t -> t) -> t -> t -> t = @@ -819,7 +863,7 @@ module Bound = struct fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None - let plus_exact : weak:bool -> otherwise:(t -> t -> t) -> t -> t -> t = + let rec plus_exact : weak:bool -> otherwise:(t -> t -> t) -> t -> t -> t = fun ~weak ~otherwise x y -> if is_zero x then y else if is_zero y then x @@ -836,6 +880,8 @@ module Bound = struct when SymLinear.is_signed_one_symbol_of ~weak (Sign.neg sign) x1 x2 -> let c = Sign.eval_big_int sign Z.(c1 + c2) d in mk_MinMax (c, Sign.neg sign, MinMax.neg min_max, d, x1) + | MinMaxB (m, x, y), z -> + mk_MinMaxB (m, plus_exact ~weak ~otherwise x z, plus_exact ~weak ~otherwise y z) | _ -> otherwise x y @@ -873,7 +919,7 @@ module Bound = struct plus_u ~weak:false - let mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t = + let rec mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t = fun bound_end n x -> if NonZeroInt.is_one n then x else @@ -896,6 +942,8 @@ module Bound = struct of_big_int Z.(i * (n :> Z.t)) | None -> of_bound_end bound_end ) + | MinMaxB (m, x, y) -> + mk_MinMaxB (m, mult_const bound_end n x, mult_const bound_end n y) let mult_const_l = mult_const Symb.BoundEnd.LowerBound @@ -946,13 +994,15 @@ module Bound = struct let div_const_u = div_const Symb.BoundEnd.UpperBound - let get_symbols : t -> Symb.SymbolSet.t = function + let rec get_symbols : t -> Symb.SymbolSet.t = function | MInf | PInf -> Symb.SymbolSet.empty | Linear (_, se) -> SymLinear.get_symbols se | MinMax (_, _, _, _, s) -> Symb.SymbolSet.singleton s + | MinMaxB (_, x, y) -> + Symb.SymbolSet.union (get_symbols x) (get_symbols y) let has_void_ptr_symb x = @@ -964,7 +1014,7 @@ module Bound = struct let are_similar b1 b2 = Symb.SymbolSet.equal (get_symbols b1) (get_symbols b2) (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *) - let subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted = + let rec subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted = let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted = fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x) in @@ -1027,9 +1077,9 @@ module Bound = struct | NonBottom x' -> let res = match (sign, min_max, x') with - | Plus, Min, MInf | Minus, Max, PInf -> + | Plus, Min, (MInf | MinMaxB _) | Minus, Max, (PInf | MinMaxB _) -> MInf - | Plus, Max, PInf | Minus, Min, MInf -> + | Plus, Max, (PInf | MinMaxB _) | Minus, Min, (MInf | MinMaxB _) -> PInf | sign, Min, PInf | sign, Max, MInf -> of_big_int (Sign.eval_big_int sign c d) @@ -1076,6 +1126,12 @@ module Bound = struct (big_int_of_minmax bound_end x' |> Option.value ~default:d))) ) in NonBottom res ) + | MinMaxB (m, x, y) -> ( + match (subst ~subst_pos x eval_sym, subst ~subst_pos y eval_sym) with + | Bottom, _ | _, Bottom -> + Bottom + | NonBottom x, NonBottom y -> + NonBottom (mk_MinMaxB (m, x, y)) ) let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym @@ -1091,13 +1147,17 @@ module Bound = struct b - let simplify_bound_ends_from_paths x = + let rec simplify_bound_ends_from_paths x = match x with | MInf | PInf | MinMax _ -> x | Linear (c, se) -> let se' = SymLinear.simplify_bound_ends_from_paths se in if phys_equal se se' then x else Linear (c, se') + | MinMaxB (m, a, b) -> + let a' = simplify_bound_ends_from_paths a in + let b' = simplify_bound_ends_from_paths b in + if phys_equal a a' && phys_equal b b' then x else mk_MinMaxB (m, a', b') let is_same_symbol b1 b2 = @@ -1108,13 +1168,15 @@ module Bound = struct None - let exists_str ~f = function + let rec exists_str ~f = function | MInf | PInf -> false | Linear (_, s) -> SymLinear.exists_str ~f s | MinMax (_, _, _, _, s) -> Symb.Symbol.exists_str ~f s + | MinMaxB (_, x, y) -> + exists_str ~f x || exists_str ~f y end type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 6c586b8e9..c7f7669b0 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -44,12 +44,18 @@ module Bound : sig val of_modeled_path : Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t + val of_minmax_bound_min : t -> t -> t + + val of_minmax_bound_max : t -> t -> t + val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool val is_length_path_of : Symb.SymbolPath.partial -> t -> bool val is_zero : t -> bool + val is_infty : t -> bool + val is_not_infty : t -> bool val is_minf : t -> bool diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index e8a071949..cfbe8da3e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1417,7 +1417,9 @@ module Call = struct &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int ; -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone ; +PatternMatch.implements_lang "Math" - &:: "max" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.max_sem + &:: "max" <>$ capt_exp $+ capt_exp + $--> eval_binop ~f:(Itv.max_sem ~use_minmax_bound:true) ; +PatternMatch.implements_lang "Math" - &:: "min" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.min_sem ] + &:: "min" <>$ capt_exp $+ capt_exp + $--> eval_binop ~f:(Itv.min_sem ~use_minmax_bound:true) ] end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index d631707a1..02b71e0e0 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -358,12 +358,23 @@ module ItvPure = struct let lor_sem : t -> t -> Boolean.t = fun x y -> Boolean.or_ (to_bool x) (to_bool y) - let min_sem : t -> t -> t = - fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2) + let lift_minmax_bound ~use_minmax_bound ~mk ~f x y = + let r = f x y in + if use_minmax_bound && Bound.is_infty r && Bound.is_not_infty x && Bound.is_not_infty y then + mk x y + else r - let max_sem : t -> t -> t = - fun (l1, u1) (l2, u2) -> (Bound.underapprox_max l1 l2, Bound.overapprox_max u1 u2) + let min_sem : ?use_minmax_bound:bool -> t -> t -> t = + fun ?(use_minmax_bound = false) (l1, u1) (l2, u2) -> + let lift = lift_minmax_bound ~use_minmax_bound ~mk:Bound.of_minmax_bound_min in + (lift ~f:Bound.underapprox_min l1 l2, lift ~f:Bound.overapprox_min u1 u2) + + + let max_sem : ?use_minmax_bound:bool -> t -> t -> t = + fun ?(use_minmax_bound = false) (l1, u1) (l2, u2) -> + let lift = lift_minmax_bound ~use_minmax_bound ~mk:Bound.of_minmax_bound_max in + (lift ~f:Bound.underapprox_max l1 l2, lift ~f:Bound.overapprox_max u1 u2) let is_invalid : t -> bool = fun (l, u) -> Bound.is_pinf l || Bound.is_minf u || Bound.lt u l @@ -672,9 +683,13 @@ let land_sem : t -> t -> Boolean.t = bind2b ItvPure.land_sem let lor_sem : t -> t -> Boolean.t = bind2b ItvPure.lor_sem -let min_sem : t -> t -> t = lift2 ItvPure.min_sem +let min_sem : ?use_minmax_bound:bool -> t -> t -> t = + fun ?use_minmax_bound -> lift2 (ItvPure.min_sem ?use_minmax_bound) + + +let max_sem : ?use_minmax_bound:bool -> t -> t -> t = + fun ?use_minmax_bound -> lift2 (ItvPure.max_sem ?use_minmax_bound) -let max_sem : t -> t -> t = lift2 ItvPure.max_sem let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 0015007a4..8ce91543a 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -213,9 +213,9 @@ val lor_sem : t -> t -> Boolean.t val lt_sem : t -> t -> Boolean.t -val min_sem : t -> t -> t +val min_sem : ?use_minmax_bound:bool -> t -> t -> t -val max_sem : t -> t -> t +val max_sem : ?use_minmax_bound:bool -> t -> t -> t val mod_sem : t -> t -> t diff --git a/infer/tests/codetoanalyze/java/performance/MathTest.java b/infer/tests/codetoanalyze/java/performance/MathTest.java index f9ca612a4..0bec21f1b 100644 --- a/infer/tests/codetoanalyze/java/performance/MathTest.java +++ b/infer/tests/codetoanalyze/java/performance/MathTest.java @@ -16,6 +16,14 @@ class MathTest { for (int i = 0; i < Math.max(0, arr.length); i++) {} } + void max2_symbolic(int x, int y) { + for (int i = 0; i < Math.max(x, y); i++) {} + } + + void call_max2_constant() { + max2_symbolic(10, 20); + } + void linear(int p) { for (int count = 0; count < p; count++) {} } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 8c4fbf4fc..86ca25ab1 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -180,8 +180,9 @@ codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.M codetoanalyze/java/performance/MapTest.java, MapTest.keySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 13,{map.length},Loop at line 13] codetoanalyze/java/performance/MapTest.java, MapTest.putAll_linear(java.util.Map):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 28,{map.length},Loop at line 28] codetoanalyze/java/performance/MapTest.java, MapTest.values_linear(java.util.Map):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ (map.length + 1) + 3 ⋅ (map.length + 2), O(map.length), degree = 1,{map.length + 2},Loop at line 22,{map.length + 1},Loop at line 22] -codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.call_with_max_linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (max(1, x)), O(x), degree = 1,{max(1, x)},call to void MathTest.linear(int),Loop at line 20] -codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ p, O(p), degree = 1,{p},Loop at line 20] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.call_with_max_linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (max(1, x)), O(x), degree = 1,{max(1, x)},call to void MathTest.linear(int),Loop at line 28] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ p, O(p), degree = 1,{p},Loop at line 28] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (max(x, y)), O((max(x, y))), degree = 1,{max(x, y)},Loop at line 20] codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 16,{arr.length},Loop at line 16] codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, O(this.mId.length), degree = 1,{this.mId.length},call to int StringTest.indexof_linear(String),Modeled call to String.indexOf] codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(java.lang.String,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-j + m.length), O((-j + m.length)), degree = 1,{-j + m.length},Modeled call to String.indexOf]