From ef74f3f18dfcc9fcb7f00f232a9f622362e95804 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 25 Feb 2020 06:38:06 -0800 Subject: [PATCH] [cost] Revise message of Provider.get.modeled Reviewed By: ezgicicek Differential Revision: D20093595 fbshipit-source-id: 04144b9db --- infer/src/bufferoverrun/bounds.ml | 4 +++- infer/src/bufferoverrun/bounds.mli | 2 +- infer/src/bufferoverrun/bufferOverrunModels.ml | 2 +- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 8 ++++---- 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 | 6 +++--- .../codetoanalyze/java/hoistingExpensive/issues.exp | 6 +++--- 10 files changed, 27 insertions(+), 24 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 61fd07abe..62e9369cd 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -337,7 +337,9 @@ module Bound = struct of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true ~non_int:false - let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true ~non_int:false + let of_modeled_path ~is_expensive = + of_path (Symb.SymbolPath.modeled ~is_expensive) ~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 87bcc85e5..8b165998e 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 : 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_minmax_bound_min : t -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 35682fedb..400ca7da0 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1227,7 +1227,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 Symb.Symbol.make_onevalue + |> Bounds.Bound.of_modeled_path ~is_expensive:false 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 dc44029f3..300be8f24 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -376,10 +376,10 @@ type eval_mode = EvalNormal | EvalPOCond | EvalPOReachability | EvalCost let is_cost_mode = function EvalCost -> true | _ -> false -let eval_sympath_modeled_partial ~mode p = +let eval_sympath_modeled_partial ~mode ~is_expensive p = match (mode, p) with | (EvalNormal | EvalCost), Symb.SymbolPath.Callsite _ -> - Itv.of_modeled_path p |> Val.of_itv + Itv.of_modeled_path ~is_expensive p |> Val.of_itv | _, _ -> (* We only have modeled modeled function calls created in costModels. *) assert false @@ -439,8 +439,8 @@ and eval_locpath ~mode params p mem = let eval_sympath ~mode params sympath mem = match sympath with - | Symb.SymbolPath.Modeled p -> - let v = eval_sympath_modeled_partial ~mode p in + | Symb.SymbolPath.Modeled {p; is_expensive} -> + let v = eval_sympath_modeled_partial ~mode ~is_expensive 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 1430cc457..48bfdab8e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -575,7 +575,7 @@ module ItvPure = struct let of_length_path ~is_void = of_path (Bound.of_length_path ~is_void) - let of_modeled_path = of_path Bound.of_modeled_path + let of_modeled_path ~is_expensive = of_path (Bound.of_modeled_path ~is_expensive) let is_offset_path_of path x = Bound.is_offset_path_of path (lb x) && Bound.is_offset_path_of path (ub x) @@ -822,7 +822,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 path = NonBottom (ItvPure.of_modeled_path path) +let of_modeled_path ~is_expensive path = NonBottom (ItvPure.of_modeled_path ~is_expensive 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 7eb70248f..a56742eb4 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -263,7 +263,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 : Symb.SymbolPath.partial -> t +val of_modeled_path : is_expensive:bool -> 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 08f0bbf07..1096d6cd7 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -96,7 +96,7 @@ module SymbolPath = struct | Normal of partial | Offset of {p: partial; is_void: bool} | Length of {p: partial; is_void: bool} - | Modeled of partial + | Modeled of {p: partial; is_expensive: bool} [@@deriving compare] let equal = [%compare.equal: t] @@ -109,7 +109,7 @@ module SymbolPath = struct let length p ~is_void = Length {p; is_void} - let modeled p = Modeled p + let modeled p ~is_expensive = Modeled {p; is_expensive} let is_this = function Pvar pvar -> Pvar.is_this pvar || Pvar.is_self pvar | _ -> false @@ -165,8 +165,9 @@ module SymbolPath = struct let pp_is_void fmt is_void = if is_void then F.fprintf fmt "(v)" let pp fmt = function - | Modeled p -> - F.fprintf fmt "%a.modeled" pp_partial p + | 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 | Normal p -> pp_partial fmt p | Offset {p; is_void} -> @@ -237,7 +238,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 @@ -264,7 +265,7 @@ module SymbolPath = struct 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 956db58bf..8a34a3f68 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -38,7 +38,7 @@ module SymbolPath : sig | Normal of partial | Offset of {p: partial; is_void: bool} | Length of {p: partial; is_void: bool} - | Modeled of partial + | Modeled of {p: partial; is_expensive: bool} [@@deriving equal] val equal_partial : partial -> partial -> bool @@ -65,7 +65,7 @@ module SymbolPath : sig val length : partial -> is_void:bool -> t - val modeled : partial -> t + val modeled : partial -> is_expensive:bool -> t val is_this : partial -> bool diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml index a7e4e872e..56b39c285 100644 --- a/infer/src/cost/costModels.ml +++ b/infer/src/cost/costModels.ml @@ -23,10 +23,10 @@ let linear = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Linear let log = cost_of_exp ~degree_kind:Polynomials.DegreeKind.Log -let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = +let expensive_modeled ~of_function {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 path in + let itv = Itv.of_modeled_path ~is_expensive:true path in CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location @@ -187,7 +187,7 @@ module Call = struct $+ capt_exp $+ capt_exp $--> JavaString.substring ; +PatternMatch.implements_inject "Provider" &:: "get" - <>--> modeled ~of_function:"Provider.get" + <>--> expensive_modeled ~of_function:"Provider.get" ; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "" <>--> unit_cost_model ; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "getElement" <>--> unit_cost_model ; +PatternMatch.implements_xmob_utils "IntHashMap" &:: "put" <>--> unit_cost_model diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp index fe8803ac9..3f8d7f1b1 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp @@ -11,7 +11,7 @@ codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symboli 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, 1, 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 7 + 14 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 41,{list.length},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 41] 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, 1, 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 85 + 10 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 1, 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 85 + 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.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, 4, 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_substring_dont_hoist(java.lang.String):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String)] @@ -19,9 +19,9 @@ codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_su 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, 3, 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, 1, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant,with estimated cost Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},Modeled call to Provider.get] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 1, 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, 2, 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 904 + 100 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.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.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, 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 904 + 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.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, 2, 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_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)]