[cost] Revise message of Provider.get.modeled

Reviewed By: ezgicicek

Differential Revision: D20093595

fbshipit-source-id: 04144b9db

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

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
 

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

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 ->
+  | Symb.SymbolPath.Modeled {p; is_expensive} ->
-      let v = eval_sympath_modeled_partial ~mode p in
+      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

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)
 

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
 

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 ->
+    | Modeled {p; is_expensive} ->
-        F.fprintf fmt "%a.modeled" pp_partial p
+        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

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
 

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

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