[cost] Add highest degree trace of the current cost to differential

Reviewed By: mbouaziz

Differential Revision: D14164176

fbshipit-source-id: a1c7dd251

infer/src/backend/Differential.ml

@@ -144,6 +144,12 @@ let issue_of_cost cost_info ~delta ~prev_cost ~curr_cost =
     else if CostDomain.BasicCost.is_zero curr_cost then IssueType.zero_execution_time_call
     else IssueType.performance_variation
   in
+  let curr_degree_with_term = CostDomain.BasicCost.get_degree_with_term curr_cost in
+  let curr_cost_msg fmt () =
+    Format.fprintf fmt "Cost is %a (degree is %a)" CostDomain.BasicCost.pp curr_cost
+      (CostDomain.BasicCost.pp_degree ~only_bigO:false)
+      curr_degree_with_term
+  in
   if (not Config.filtering) || issue_type.IssueType.enabled then
     let qualifier =
       let pp_delta fmt delta =
@@ -153,24 +159,34 @@ let issue_of_cost cost_info ~delta ~prev_cost ~curr_cost =
         | `Increased ->
             Format.fprintf fmt "increased"
       in
-      let pp_extra_msg fmt cost_polynomial =
-        if Config.developer_mode then
-          Format.fprintf fmt "Cost is %a (degree is %a)" CostDomain.BasicCost.pp cost_polynomial
-            CostDomain.BasicCost.pp_degree cost_polynomial
+      let pp_extra_msg fmt () =
+        if Config.developer_mode then curr_cost_msg fmt ()
         else Format.fprintf fmt "Please make sure this is an expected change."
       in
+      let prev_degree_with_term = CostDomain.BasicCost.get_degree_with_term prev_cost in
       Format.asprintf "Complexity of this function has %a from %a to %a. %a"
         (MarkupFormatter.wrap_bold pp_delta)
         delta
-        (MarkupFormatter.wrap_monospaced CostDomain.BasicCost.pp_degree_hum)
-        prev_cost
-        (MarkupFormatter.wrap_monospaced CostDomain.BasicCost.pp_degree_hum)
-        curr_cost pp_extra_msg curr_cost
+        (MarkupFormatter.wrap_monospaced (CostDomain.BasicCost.pp_degree ~only_bigO:true))
+        prev_degree_with_term
+        (MarkupFormatter.wrap_monospaced (CostDomain.BasicCost.pp_degree ~only_bigO:true))
+        curr_degree_with_term pp_extra_msg ()
     in
     let line = cost_info.Jsonbug_t.loc.lnum in
     let column = cost_info.Jsonbug_t.loc.cnum in
     let trace =
-      [Errlog.make_trace_element 0 {Location.line; col= column; file= source_file} "" []]
+      let curr_cost_trace =
+        [ Errlog.make_trace_element 0
+            {Location.line; col= column; file= source_file}
+            (Format.asprintf "Updated %a" curr_cost_msg ())
+            [] ]
+      in
+      Option.value_map ~default:curr_cost_trace
+        ~f:(fun (_, degree_term) ->
+          let symbol_list = Polynomials.NonNegativeNonTopPolynomial.get_symbols degree_term in
+          ("", curr_cost_trace) :: List.map symbol_list ~f:Bounds.NonNegativeBound.make_err_trace
+          |> Errlog.concat_traces )
+        curr_degree_with_term
     in
     let severity = Exceptions.Advice in
     Some

infer/src/backend/InferPrint.ml

@@ -344,11 +344,18 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
     match cost_opt with
     | Some {post} ->
         let basic_operation_cost = CostDomain.get_operation_cost post in
+        let degree_with_term = CostDomain.BasicCost.get_degree_with_term basic_operation_cost in
         let hum =
           { Jsonbug_t.hum_polynomial=
               Format.asprintf "%a" CostDomain.BasicCost.pp basic_operation_cost
-          ; hum_degree= Format.asprintf "%a" CostDomain.BasicCost.pp_degree basic_operation_cost
-          ; big_o= Format.asprintf "%a" CostDomain.BasicCost.pp_degree_hum basic_operation_cost }
+          ; hum_degree=
+              Format.asprintf "%a"
+                (CostDomain.BasicCost.pp_degree ~only_bigO:false)
+                degree_with_term
+          ; big_o=
+              Format.asprintf "%a"
+                (CostDomain.BasicCost.pp_degree ~only_bigO:true)
+                degree_with_term }
         in
         let cost_item =
           let file = SourceFile.to_rel_path loc.Location.file in

infer/src/bufferoverrun/polynomials.ml

@@ -360,8 +360,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
 
   let degree p = fst (degree_with_term p)
 
-  let degree_term p = snd (degree_with_term p)
-
   let multiplication_sep = F.sprintf " %s " SpecialChars.multiplication_sign
 
   let pp : F.formatter -> t -> unit =
@@ -420,9 +418,10 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
     get_symbols_sub p []
 end
 
+module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
+module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
+
 module NonNegativePolynomial = struct
-  module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
-  module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
   include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial)
 
   let zero = NonTop NonNegativeNonTopPolynomial.zero
@@ -489,27 +488,25 @@ module NonNegativePolynomial = struct
           (NonNegativeNonTopPolynomial.degree p2)
 
 
-  let pp_degree fmt p =
-    match p with
+  let get_degree_with_term = function
     | Top ->
-        Format.pp_print_string fmt "Top"
+        None
     | NonTop p ->
-        Degree.pp fmt (NonNegativeNonTopPolynomial.degree p)
-
-
-  let pp_degree_hum fmt p =
-    match p with
-    | Top ->
-        Format.pp_print_string fmt "Top"
-    | NonTop p ->
-        Format.fprintf fmt "O(%a)" NonNegativeNonTopPolynomial.pp
-          (NonNegativeNonTopPolynomial.degree_term p)
+        Some (NonNegativeNonTopPolynomial.degree_with_term p)
 
 
   let get_symbols p : Bounds.NonNegativeBound.t list =
     match p with Top -> assert false | NonTop p -> NonNegativeNonTopPolynomial.get_symbols p
 
 
+  let pp_degree ~only_bigO fmt = function
+    | None ->
+        Format.pp_print_string fmt "Top"
+    | Some (degree, degree_term) ->
+        if only_bigO then Format.fprintf fmt "O(%a)" NonNegativeNonTopPolynomial.pp degree_term
+        else Degree.pp fmt degree
+
+
   let encode astate = Marshal.to_string astate [] |> Base64.encode_exn
 
   let decode enc_str = Marshal.from_string (Base64.decode_exn enc_str) 0

infer/src/bufferoverrun/polynomials.mli

@@ -23,6 +23,12 @@ module Degree : sig
   val pp : Format.formatter -> t -> unit
 end
 
+module NonNegativeNonTopPolynomial : sig
+  type t
+
+  val get_symbols : t -> Bounds.NonNegativeBound.t list
+end
+
 module NonNegativePolynomial : sig
   include AbstractDomain.WithTop
 
@@ -54,13 +60,14 @@ module NonNegativePolynomial : sig
 
   val compare_by_degree : t -> t -> int
 
-  val pp_degree : Format.formatter -> t -> unit
-
-  val pp_degree_hum : Format.formatter -> t -> unit
+  val pp_degree :
+    only_bigO:bool -> Format.formatter -> (Degree.t * NonNegativeNonTopPolynomial.t) option -> unit
 
   val encode : t -> string
 
   val decode : string -> t
 
   val get_symbols : t -> Bounds.NonNegativeBound.t list
+
+  val get_degree_with_term : t -> (Degree.t * NonNegativeNonTopPolynomial.t) option
 end

infer/tests/build_systems/differential_of_costs_report/Makefile

@@ -3,22 +3,23 @@
 # This source code is licensed under the MIT license found in the
 # LICENSE file in the root directory of this source tree.
 
-# E2E test for anonymous class renaming
+# E2E test for differential of costs
 
 TESTS_DIR = ../..
 SOURCES = src/DiffExample.java.current src/DiffExample.java.previous
 CLEAN_EXTRA = src/Diff*.java *.class
-
 include $(TESTS_DIR)/differential.make
+INFERPRINT_ISSUES_FIELDS = \
+	"bug_type,bucket,file,procedure,line_offset,bug_trace"
 
 $(CURRENT_REPORT) $(PREVIOUS_REPORT): $(JAVA_DEPS)
 
 $(CURRENT_REPORT):
 	$(QUIET)$(COPY) src/DiffExample.java.current src/DiffExample.java
-	$(QUIET)$(call silent_on_success,Testing Differential skips anon class renamings: current,\
+	$(QUIET)$(call silent_on_success,Testing Cost Differential: current,\
 	$(INFER_BIN) --enable-issue-type INFINITE_EXECUTION_TIME_CALL --cost-only -o $(CURRENT_DIR) -- $(JAVAC) src/*.java)
 
 $(PREVIOUS_REPORT):
 	$(QUIET)$(COPY) src/DiffExample.java.previous src/DiffExample.java
-	$(QUIET)$(call silent_on_success,Testing Differential skips anon class renamings: previous,\
+	$(QUIET)$(call silent_on_success,Testing Cost Differential: previous,\
 	$(INFER_BIN) --enable-issue-type INFINITE_EXECUTION_TIME_CALL --cost-only -o $(PREVIOUS_DIR) -- $(JAVAC) src/*.java)

infer/tests/build_systems/differential_of_costs_report/fixed.exp

@@ -1 +1 @@
-PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f6(java.util.ArrayList):void, 0
+PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f6(java.util.ArrayList):void, 0, [Updated Cost is 5 + list.length × log(list.length) (degree is 1 + 1⋅log),{list.length},call to void DiffExample.f5(ArrayList),Modeled call to List.length,{list.length},call to void DiffExample.f5(ArrayList),Modeled call to List.length]

infer/tests/build_systems/differential_of_costs_report/introduced.exp

@@ -1,3 +1,3 @@
-INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0
-PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f4(int):int, 0
-PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f5(java.util.ArrayList):void, 0
+INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0, []
+PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f4(int):int, 0, [Updated Cost is 6 + 5 ⋅ k (degree is 1),{k},Loop at line 44]
+PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f5(java.util.ArrayList):void, 0, [Updated Cost is 2 + list.length × log(list.length) (degree is 1 + 1⋅log),{list.length},Modeled call to List.length,{list.length},Modeled call to List.length]