diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml index 1e13ce0a2..a7e4e872e 100644 --- a/infer/src/cost/costModels.ml +++ b/infer/src/cost/costModels.ml @@ -52,20 +52,28 @@ module JavaString = struct let begin_itv = BufferOverrunDomain.Val.get_itv begin_v in let end_itv = BufferOverrunDomain.Val.get_itv end_v in let itv = - if Boolean.is_true (Itv.le_sem begin_itv end_itv) then Itv.minus end_itv begin_itv - else end_itv + if + Boolean.is_true (Itv.le_sem Itv.zero begin_itv) + && Boolean.is_true (Itv.le_sem begin_itv end_itv) + then Itv.minus end_itv begin_itv + else + (* in practice, either we have two symbolic bounds that are semantically + incomparable at this point or there is an out of bounds exception. In + both cases, we don't want to give negative cost so we + behave as if there is no model and give unit cost. *) + Itv.of_int 1 in CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.substring" location - let substring exp begin_idx model_env ~ret:_ inferbo_mem = + let substring_no_end exp begin_idx model_env ~ret:_ inferbo_mem = substring_aux ~begin_idx ~end_v:(BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem) model_env inferbo_mem - let substring_no_end begin_idx end_idx ({integer_type_widths} as model_env) ~ret:_ inferbo_mem = + let substring begin_idx end_idx ({integer_type_widths} as model_env) ~ret:_ inferbo_mem = substring_aux ~begin_idx ~end_v:(BufferOverrunSemantics.eval integer_type_widths end_idx inferbo_mem) model_env inferbo_mem @@ -163,7 +171,7 @@ module Call = struct &:: "shuffle" <>$ capt_exp $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle" ; +PatternMatch.implements_lang "String" - &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring + &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end ; +PatternMatch.implements_lang "String" &:: "indexOf" <>$ capt_exp $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") @@ -176,7 +184,7 @@ module Call = struct ; +PatternMatch.implements_lang "String" &:: "substring" $ any_arg_of_typ (+PatternMatch.implements_lang "String") - $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end + $+ capt_exp $+ capt_exp $--> JavaString.substring ; +PatternMatch.implements_inject "Provider" &:: "get" <>--> modeled ~of_function:"Provider.get" diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java index ac8ea97c0..5705ac76c 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java @@ -42,14 +42,16 @@ class HoistModeled { } } - void linear_substring_hoist(String s, ArrayList list, Integer el) { + void linear_substring_hoist_FN(String s, ArrayList list, Integer el) { String sub; int length = s.length(); for (int i = 0; i < 10; i++) { - sub = s.substring(2, length - 1); + sub = + s.substring( + 2, length - 1); // can't determine statically that 2 <= length-1. So we give unit cost } for (int i = 0; i < 10; i++) { - sub = s.substring(1); + sub = s.substring(1); // ditto } } @@ -66,4 +68,13 @@ class HoistModeled { call_expensive_hoist("ez", list, el); } } + + void constant_substring_dont_hoist(String s, int x) { + String sub; + int length = s.length(); + int y = -1; + for (int i = 0; i < 10; i++) { + sub = s.substring(x, y); + } + } } diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp index c0caefaf6..fe8803ac9 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp @@ -11,17 +11,19 @@ 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 58 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().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.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)] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 1, 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,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_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 66 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().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.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(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(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 49 is loop-invariant,with estimated cost (s.length - 1), degree = 1,{s.length - 1},Modeled call to String.substring] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 5, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 52 is loop-invariant,with estimated cost s.length, degree = 1,{s.length},Modeled call to String.substring] +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, 3, 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, 7, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 54 is loop-invariant]