From b57ccc3364239f94f818f3f6b4bc9baf64f3b909 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 5 Feb 2021 01:14:58 -0800 Subject: [PATCH] [cost] Remove expensive modeling for Provider.get Summary: We are getting lots of FPs due to modeling `Provider.get` as expensive. This is coming from Dependency Injection and Infer cannot statically determine the type of the provider and determine whether that provider is expensive (requires a global analysis and instrumentation). Instead, we are downgrading this method to the default constant cost. Reviewed By: skcho Differential Revision: D26223978 fbshipit-source-id: 79f81c997 --- infer/src/bufferoverrun/bounds.ml | 4 +--- infer/src/bufferoverrun/bounds.mli | 2 +- .../src/bufferoverrun/bufferOverrunModels.ml | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 10 ++++----- infer/src/bufferoverrun/itv.ml | 4 ++-- infer/src/bufferoverrun/itv.mli | 2 +- infer/src/bufferoverrun/symb.ml | 13 +++++------ infer/src/bufferoverrun/symb.mli | 4 ++-- infer/src/cost/costModels.ml | 9 -------- .../java/hoistingExpensive/HoistModeled.java | 19 ++++++---------- .../java/hoistingExpensive/issues.exp | 22 +++++++++---------- 11 files changed, 36 insertions(+), 55 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 78e1be83c..a205d68a2 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -348,9 +348,7 @@ module Bound = struct of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~non_int:false - let of_modeled_path ~is_expensive = - of_path (Symb.SymbolPath.modeled ~is_expensive) ~unsigned:true ~non_int: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 9efcf9eb3..e8145f1e9 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -48,7 +48,7 @@ module Bound : sig val of_length_path : is_void:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t - val of_modeled_path : is_expensive:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t + val of_modeled_path : Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t val of_minmax_bound_min : t -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index bba81c86c..3e6fd38a4 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1595,7 +1595,7 @@ module FileChannel = struct let buf_v = Dom.Mem.find_set buf_locs mem in let range = Symb.SymbolPath.of_callsite ~ret_typ (CallSite.make pname location) - |> Bounds.Bound.of_modeled_path ~is_expensive:false Symb.Symbol.make_onevalue + |> Bounds.Bound.of_modeled_path Symb.Symbol.make_onevalue |> Dom.ModeledRange.of_modeled_function pname location in let mem = Dom.Mem.add_heap_set buf_locs (Dom.Val.set_modeled_range range buf_v) mem in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 739e4643d..b12c05fd9 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -378,12 +378,12 @@ type eval_mode = EvalNormal | EvalPOCond | EvalPOReachability | EvalCost let is_cost_mode = function EvalCost -> true | _ -> false -let eval_sympath_modeled_partial ~mode ~is_expensive p = +let eval_sympath_modeled_partial ~mode p = match (mode, p) with | (EvalNormal | EvalCost), BoField.Prim (Symb.SymbolPath.Callsite _) -> - Itv.of_modeled_path ~is_expensive p |> Val.of_itv + Itv.of_modeled_path p |> Val.of_itv | _, _ -> - (* We only have modeled modeled function calls created in costModels. *) + (* We only have modeled function calls created in costModels. *) assert false @@ -441,8 +441,8 @@ and eval_locpath ~mode params p mem = let eval_sympath ~mode params sympath mem = match sympath with - | Symb.SymbolPath.Modeled {p; is_expensive} -> - let v = eval_sympath_modeled_partial ~mode ~is_expensive p in + | Symb.SymbolPath.Modeled p -> + let v = eval_sympath_modeled_partial ~mode p in (Val.get_itv v, Val.get_traces v) | Symb.SymbolPath.Normal p -> let v = eval_sympath_partial ~mode params p mem in diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index bf65830b6..db3ca5a1c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -583,7 +583,7 @@ module ItvPure = struct let of_length_path ~is_void = of_path (Bound.of_length_path ~is_void) - let of_modeled_path ~is_expensive = of_path (Bound.of_modeled_path ~is_expensive) + let of_modeled_path = of_path Bound.of_modeled_path let is_offset_path_of path x = Bound.is_offset_path_of path (lb x) && Bound.is_offset_path_of path (ub x) @@ -830,7 +830,7 @@ let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void pa let of_length_path ~is_void path = NonBottom (ItvPure.of_length_path ~is_void path) -let of_modeled_path ~is_expensive path = NonBottom (ItvPure.of_modeled_path ~is_expensive path) +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) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 7805890fb..6e1603873 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -269,7 +269,7 @@ val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t val of_length_path : is_void:bool -> Symb.SymbolPath.partial -> t -val of_modeled_path : is_expensive:bool -> Symb.SymbolPath.partial -> t +val of_modeled_path : Symb.SymbolPath.partial -> t val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 0c316895d..770df4ba4 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -64,7 +64,7 @@ module SymbolPath = struct | Normal of partial | Offset of {p: partial; is_void: bool} | Length of {p: partial; is_void: bool} - | Modeled of {p: partial; is_expensive: bool} + | Modeled of partial [@@deriving compare] let equal = [%compare.equal: t] @@ -77,7 +77,7 @@ module SymbolPath = struct let length p ~is_void = Length {p; is_void} - let modeled p ~is_expensive = Modeled {p; is_expensive} + let modeled p = Modeled p let is_this = function | BoField.Prim (Pvar pvar) -> @@ -136,9 +136,8 @@ module SymbolPath = struct let pp_is_void fmt is_void = if is_void then F.fprintf fmt "(v)" let pp fmt = function - | Modeled {p; is_expensive} -> - if is_expensive then F.fprintf fmt "%a(expensive call)" pp_partial p - else F.fprintf fmt "%a.modeled" pp_partial p + | Modeled p -> + F.fprintf fmt "%a.modeled" pp_partial p | Normal p -> pp_partial fmt p | Offset {p; is_void} -> @@ -210,7 +209,7 @@ module SymbolPath = struct let exists_str ~f = function - | Modeled {p} | Normal p | Offset {p} | Length {p} -> + | Modeled p | Normal p | Offset {p} | Length {p} -> exists_str_partial ~f p @@ -239,7 +238,7 @@ module SymbolPath = struct let is_length = function Length _ -> true | _ -> false - let is_global = function Normal p | Offset {p} | Length {p} | Modeled {p} -> is_global_partial p + let is_global = function Normal p | Offset {p} | Length {p} | Modeled p -> is_global_partial p end module Symbol = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 44823aa6c..e40c45d75 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -32,7 +32,7 @@ module SymbolPath : sig | Normal of partial | Offset of {p: partial; is_void: bool} | Length of {p: partial; is_void: bool} - | Modeled of {p: partial; is_expensive: bool} + | Modeled of partial [@@deriving equal] val equal_partial : partial -> partial -> bool @@ -59,7 +59,7 @@ module SymbolPath : sig val length : partial -> is_void:bool -> t - val modeled : partial -> is_expensive:bool -> t + val modeled : partial -> t val is_this : partial -> bool diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml index cf4921f24..4855a0362 100644 --- a/infer/src/cost/costModels.ml +++ b/infer/src/cost/costModels.ml @@ -26,14 +26,6 @@ let linear = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Linear let log = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Log -let provider_get {model_env= {pname; location}} ~ret:(_, ret_typ) _ : BasicCost.t = - let callsite = CallSite.make pname location in - let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in - let itv = Itv.of_modeled_path ~is_expensive:true path in - CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"Provider.get" - location - - module BoundsOf (Container : CostUtils.S) = struct let of_length exp {model_env= {location}} ~ret:_ mem ~of_function ~degree_kind = let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in @@ -351,7 +343,6 @@ module Call = struct &:: "substring" $ any_arg_of_typ (+PatternMatch.Java.implements_lang "String") $+ capt_exp $+ capt_exp $--> JavaString.substring - ; +PatternMatch.Java.implements_inject "Provider" &:: "get" <>--> provider_get ; +PatternMatch.Java.implements_xmob_utils "IntHashMap" &:: "" <>--> unit_cost_model ; +PatternMatch.Java.implements_xmob_utils "IntHashMap" &:: "getElement" <>--> unit_cost_model diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java index 5705ac76c..976337a16 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java @@ -11,9 +11,12 @@ class HoistModeled { @Inject private Provider mProvider; - void expensive_get_hoist(int size) { + void expensive_get_dont_hoist(int size) { for (int i = 0; i < size; i++) { - mProvider.get(); + mProvider.get(); // this could be expensive depending on the + // type of the provider which we cannot + // detect. Hence, we consider this as cheap for + // now. } } @@ -55,17 +58,9 @@ class HoistModeled { } } - void call_expensive_hoist(String s, ArrayList list, Integer el) { + void call_expensive_dont_hoist(String s, ArrayList list) { for (int i = 0; i < 10; i++) { - expensive_get_hoist(10); - } - } - - void expensive_get_hoist_hoist_me(String s, ArrayList list, Integer el) { - String sub; - int length = s.length(); - for (int i = 0; i < 10; i++) { - call_expensive_hoist("ez", list, el); + expensive_get_dont_hoist(10); } } diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp index d0b5c2099..7dadbc818 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp @@ -10,20 +10,18 @@ codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symboli codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 27 is loop-invariant,with estimated cost 5 + 10 ⋅ size, degree = 1,{size},Call to void HoistExpensive.cheap_dont_hoist(int),Loop] codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.symbolic_expensive_iterator_hoist(int,ArrayList)] codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 49 is loop-invariant,with estimated cost 6 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop,{list.length},Call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.call_expensive_hoist(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_hoist(int) at line 60 is loop-invariant,with estimated cost 84 + 10 ⋅ (Provider.get()(expensive call).ub), degree = 1,{Provider.get()(expensive call).ub},Call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_dont_hoist(java.lang.String,java.util.ArrayList):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.call_expensive_dont_hoist(String,ArrayList)] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_dont_hoist(java.lang.String,java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_dont_hoist(int) at line 63 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_contains_dont_hoist(Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 34 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 37 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 41 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 44 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String,int)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 77 is loop-invariant] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist(int)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant,with estimated cost (Provider.get()(expensive call).ub), degree = 1,{Provider.get()(expensive call).ub},Modeled call to Provider.get] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist_hoist_me(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 68 is loop-invariant,with estimated cost 893 + 100 ⋅ (Provider.get()(expensive call).ub), degree = 1,{Provider.get()(expensive call).ub},Call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer),Call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 72 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_dont_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_dont_hoist(int)] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_dont_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_contains_hoist(ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 3, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 23 is loop-invariant,with estimated cost list.length, degree = 1,{list.length},Modeled call to List.contains] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 3, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 26 is loop-invariant,with estimated cost list.length, degree = 1,{list.length},Modeled call to List.contains] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_substring_hoist_FN(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 50 is loop-invariant] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 9, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 54 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 53 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 9, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 57 is loop-invariant]