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

[loop-hoisting] Incorporate cost trace into EXPENSIVE_LOOP_INVARIANT_CALL issues

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D14934254

fbshipit-source-id: 23af117b6
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent 6d25b0990d
commit 7e16aafdba
5 changed files with 50 additions and 43 deletions
Show Stats Download Patch File Download Diff File

16
infer/src/bufferoverrun/polynomials.ml
Unescape View File

@ -585,6 +585,22 @@ module NonNegativePolynomial = struct
else Degree.pp fmt degree
let degree_str p =
match degree p with
| Some degree ->
Format.asprintf ", degree = %a" Degree.pp degree
| None ->
""
let polynomial_traces p =
match get_symbols p with
| Below symbols ->
List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces
| Above trace ->
TopTraces.make_err_trace trace
let encode astate = Marshal.to_string astate [] |> Base64.encode_exn
let decode enc_str = Marshal.from_string (Base64.decode_exn enc_str) 0

9
infer/src/bufferoverrun/polynomials.mli
Unescape View File

@ -19,8 +19,6 @@ module Degree : sig
(** Encodes the complex type [t] to an integer that can be used for comparison. *)
val is_zero : t -> bool
val pp : Format.formatter -> t -> unit
end
module NonNegativeNonTopPolynomial : sig
@ -73,16 +71,17 @@ module NonNegativePolynomial : sig
val degree : t -> Degree.t option
val degree_str : t -> string
val compare_by_degree : t -> t -> int
val pp_degree : only_bigO:bool -> Format.formatter -> degree_with_term -> unit
val polynomial_traces : t -> Errlog.loc_trace
val encode : t -> string
val decode : string -> t
val get_symbols :
t -> (Bounds.NonNegativeBound.t list, TopTraces.t) AbstractDomain.Types.below_above
val get_degree_with_term : t -> degree_with_term
end

25
infer/src/checkers/cost.ml
Unescape View File

@ -715,22 +715,7 @@ module WorstCaseCost = struct
end
module Check = struct
let polynomial_traces cost =
match BasicCost.get_symbols cost with
| Below symbols ->
List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces
| Above trace ->
Polynomials.TopTraces.make_err_trace trace
let report_threshold proc_desc summary ~name ~location ~cost ~threshold ~kind =
let degree_str =
match BasicCost.degree cost with
| Some degree ->
Format.asprintf ", degree = %a" Polynomials.Degree.pp degree
| None ->
""
in
let report_issue_type =
match kind with
| CostDomain.AllocationCost ->
@ -745,18 +730,19 @@ module Check = struct
| CostDomain.IOCost ->
IssueType.expensive_IO_call
in
let degree_str = BasicCost.degree_str cost in
let message =
F.asprintf
"%s from the beginning of the function up to this program point is likely above the \
acceptable threshold of %d (estimated cost %a%s)"
name threshold BasicCost.pp_hum cost degree_str
in
let cost_trace =
let cost_trace_elem =
let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp_hum cost degree_str in
Errlog.make_trace_element 0 location cost_desc []
in
Reporting.log_error summary ~loc:location
~ltr:(cost_trace :: polynomial_traces cost)
~ltr:(cost_trace_elem :: BasicCost.polynomial_traces cost)
~extras:(compute_errlog_extras cost) report_issue_type message
@ -768,8 +754,9 @@ module Check = struct
suffix
in
let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
Reporting.log_error ~loc ~ltr:(polynomial_traces cost) ~extras:(compute_errlog_extras cost)
summary issue message
Reporting.log_error ~loc
~ltr:(BasicCost.polynomial_traces cost)
~extras:(compute_errlog_extras cost) summary issue message
in
if BasicCost.is_top cost then
report IssueType.infinite_execution_time_call "cannot be computed"

27
infer/src/checkers/hoisting.ml
Unescape View File

@ -7,6 +7,7 @@
open! IStd
module F = Format
module InstrCFG = ProcCfg.NormalOneInstrPerNode
module BasicCost = CostDomain.BasicCost
module Call = struct
type t =
@ -70,20 +71,26 @@ let get_hoist_inv_map tenv ~get_callee_purity reaching_defs_invariant_map loop_h
let do_report extract_cost_if_expensive summary (Call.{pname; loc} as call) loop_head_loc =
let issue, cost_msg =
let exp_desc =
F.asprintf "The call to %a at %a is loop-invariant" Typ.Procname.pp pname Location.pp loc
in
let loop_inv_trace_elem = Errlog.make_trace_element 0 loc exp_desc [] in
let issue, cost_msg, ltr =
match extract_cost_if_expensive call with
| Some cost ->
let degree_str = BasicCost.degree_str cost in
let cost_trace_elem =
let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp_hum cost degree_str in
Errlog.make_trace_element 0 loc cost_desc []
in
( IssueType.expensive_loop_invariant_call
, F.asprintf " and expensive (has complexity %a)"
(CostDomain.BasicCost.pp_degree ~only_bigO:true)
cost )
(BasicCost.pp_degree ~only_bigO:true)
(BasicCost.get_degree_with_term cost)
, loop_inv_trace_elem :: cost_trace_elem :: BasicCost.polynomial_traces cost )
| None ->
(IssueType.invariant_call, "")
in
let exp_desc =
F.asprintf "The call to %a at %a is loop-invariant" Typ.Procname.pp pname Location.pp loc
(IssueType.invariant_call, "", [loop_inv_trace_elem])
in
let ltr = [Errlog.make_trace_element 0 loc exp_desc []] in
let message =
F.asprintf "%s%s. It can be moved out of the loop at %a." exp_desc cost_msg Location.pp
loop_head_loc
@ -117,9 +124,7 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f
~callee_cost:(CostDomain.get_operation_cost cost_record)
~loc
in
Option.some_if
(CostDomain.BasicCost.is_symbolic cost)
(CostDomain.BasicCost.get_degree_with_term cost)
Option.some_if (CostDomain.BasicCost.is_symbolic cost) cost
| _ ->
None

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

@ -6,21 +6,21 @@ codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.incr(in
codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.instantiated_cheap_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.instantiated_cheap_hoist(int)]
codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.instantiated_cheap_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 33 is loop-invariant]
codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.symbolic_expensive_hoist(int)]
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 26 is loop-invariant]
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 26 is loop-invariant,with estimated cost 6 + 11 ⋅ size, degree = 1,{size},call to void HoistExpensive.cheap_dont_hoist(int),Loop at line 18]
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 48 is loop-invariant]
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 48 is loop-invariant,with estimated cost 7 + 14 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 40,{list.length - 1},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 40]
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 58 is loop-invariant]
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 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.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_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.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]
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().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, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 66 is loop-invariant]
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 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.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]
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_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, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 49 is loop-invariant]
codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 7, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 52 is loop-invariant]
codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, 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 - 3), degree = 1,{s.length - 3},Modeled call to String.substring]
codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 7, 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 - 1), degree = 1,{s.length - 1},Modeled call to String.substring]

Write Preview
Loading…
Cancel
Save