pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[cost] Remove expensive modeling for Provider.get

Browse Source 
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
master
Ezgi Çiçek 4 years ago committed by Facebook GitHub Bot
parent 285ddb4a98
commit b57ccc3364
11 changed files with 36 additions and 55 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -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) ->

2
infer/src/bufferoverrun/bounds.mli
Unescape View File

@ -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

2
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -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

10
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -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

4
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -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)

2
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -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

13
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -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

4
infer/src/bufferoverrun/symb.mli
Unescape View File

@ -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

9
infer/src/cost/costModels.ml
Unescape View File

@ -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" &:: "<init>" <>--> unit_cost_model
; +PatternMatch.Java.implements_xmob_utils "IntHashMap"
&:: "getElement" <>--> unit_cost_model

19
infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java
Unescape View File

@ -11,9 +11,12 @@ class HoistModeled {
@Inject private Provider<Integer> 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<Integer> list, Integer el) {
void call_expensive_dont_hoist(String s, ArrayList<Integer> list) {
for (int i = 0; i < 10; i++) {
expensive_get_hoist(10);
}
}
void expensive_get_hoist_hoist_me(String s, ArrayList<Integer> 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);
}
}

22
infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp
Unescape View File

@ -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]

Write Preview
Loading…
Cancel
Save