[cost] Abstract type for polynomial degree

Reviewed By: ezgicicek

Differential Revision: D13175851

fbshipit-source-id: db9078037

infer/src/backend/Differential.ml

@@ -54,9 +54,11 @@ let dedup (issues : Jsonbug_t.jsonbug list) =
 
 
 module CostsSummary = struct
-  type 'a count = {top: 'a; zero: 'a; degrees: 'a Int.Map.t}
+  module DegreeMap = Caml.Map.Make (Polynomials.Degree)
 
-  let init = {top= 0; zero= 0; degrees= Int.Map.empty}
+  type 'a count = {top: 'a; zero: 'a; degrees: 'a DegreeMap.t}
+
+  let init = {top= 0; zero= 0; degrees= DegreeMap.empty}
 
   type previous_current = {previous: int; current: int}
 
@@ -67,10 +69,12 @@ module CostsSummary = struct
           assert (CostDomain.BasicCost.is_top e) ;
           {t with top= t.top + 1}
       | Some d when CostDomain.BasicCost.is_zero e ->
-          assert (Int.equal d 0) ;
+          assert (Polynomials.Degree.is_zero d) ;
           {t with zero= t.zero + 1}
       | Some d ->
-          let degrees = Int.Map.update t.degrees d ~f:(function None -> 1 | Some x -> x + 1) in
+          let degrees =
+            DegreeMap.update d (function None -> Some 1 | Some x -> Some (x + 1)) t.degrees
+          in
           {t with degrees}
     in
     List.fold ~init
@@ -81,16 +85,18 @@ module CostsSummary = struct
 
   let pair_counts ~current_counts ~previous_counts =
     let compute_degrees current previous =
-      let merge_aux ~key:_ v =
+      let merge_aux _ cur_opt prev_opt =
-        match v with
+        match (cur_opt, prev_opt) with
-        | `Both (current, previous) ->
+        | Some current, Some previous ->
             Some {current; previous}
-        | `Left current ->
+        | Some current, None ->
             Some {current; previous= 0}
-        | `Right previous ->
+        | None, Some previous ->
             Some {current= 0; previous}
+        | None, None ->
+            None
       in
-      Int.Map.merge ~f:merge_aux current previous
+      DegreeMap.merge merge_aux current previous
     in
     { top= {current= current_counts.top; previous= previous_counts.top}
     ; zero= {current= current_counts.zero; previous= previous_counts.zero}
@@ -102,10 +108,12 @@ module CostsSummary = struct
     let previous_counts = count previous_costs in
     let paired_counts = pair_counts ~current_counts ~previous_counts in
     let json_degrees =
-      Int.Map.to_alist ~key_order:`Increasing paired_counts.degrees
+      DegreeMap.bindings paired_counts.degrees
       |> List.map ~f:(fun (key, {current; previous}) ->
-             `Assoc [("degree", `Int key); ("current", `Int current); ("previous", `Int previous)]
+             `Assoc
-         )
+               [ ("degree", `Int (Polynomials.Degree.to_int key))
+               ; ("current", `Int current)
+               ; ("previous", `Int previous) ] )
     in
     let create_assoc current previous =
       `Assoc [("current", `Int current); ("previous", `Int previous)]

infer/src/bufferoverrun/ints.ml

@@ -71,8 +71,12 @@ module NonNegativeInt = struct
     i
 
 
+  let to_int_exn = Z.to_int
+
   let ( <= ) ~lhs ~rhs = lhs <= rhs
 
+  let succ = Z.succ
+
   let ( + ) = Z.( + )
 
   let ( * ) = Z.( * )

infer/src/bufferoverrun/ints.mli

@@ -57,12 +57,16 @@ module NonNegativeInt : sig
 
   val of_big_int_exn : Z.t -> t
 
+  val to_int_exn : t -> int
+
   val is_zero : t -> bool
 
   val is_one : t -> bool
 
   val ( <= ) : lhs:t -> rhs:t -> bool
 
+  val succ : t -> t
+
   val ( + ) : t -> t -> t
 
   val ( * ) : t -> t -> t

infer/src/bufferoverrun/polynomials.ml

@@ -10,6 +10,20 @@ open! AbstractDomain.Types
 module Bound = Bounds.Bound
 open Ints
 
+module Degree = struct
+  type t = NonNegativeInt.t [@@deriving compare]
+
+  let zero = NonNegativeInt.zero
+
+  let succ = NonNegativeInt.succ
+
+  let to_int = NonNegativeInt.to_int_exn
+
+  let is_zero = NonNegativeInt.is_zero
+
+  let pp = NonNegativeInt.pp
+end
+
 module type NonNegativeSymbol = sig
   type t [@@deriving compare]
 
@@ -257,8 +271,8 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
     M.fold
       (fun t p acc ->
         let d, p' = degree_with_term p in
-        max acc (d + 1, mult_symb p' t) )
+        max acc (Degree.succ d, mult_symb p' t) )
-      terms (0, one)
+      terms (Degree.zero, one)
 
 
   let degree p = fst (degree_with_term p)
@@ -371,7 +385,9 @@ module NonNegativePolynomial = struct
     | NonTop _, Top ->
         -1
     | NonTop p1, NonTop p2 ->
-        NonNegativeNonTopPolynomial.degree p1 - NonNegativeNonTopPolynomial.degree p2
+        Degree.compare
+          (NonNegativeNonTopPolynomial.degree p1)
+          (NonNegativeNonTopPolynomial.degree p2)
 
 
   let pp_degree fmt p =
@@ -379,7 +395,7 @@ module NonNegativePolynomial = struct
     | Top ->
         Format.pp_print_string fmt "Top"
     | NonTop p ->
-        Format.pp_print_int fmt (NonNegativeNonTopPolynomial.degree p)
+        Degree.pp fmt (NonNegativeNonTopPolynomial.degree p)
 
 
   let pp_degree_hum fmt p =

infer/src/bufferoverrun/polynomials.mli

@@ -8,6 +8,16 @@
 open! IStd
 module Bound = Bounds.Bound
 
+module Degree : sig
+  type t [@@deriving compare]
+
+  val to_int : t -> int
+
+  val is_zero : t -> bool
+
+  val pp : Format.formatter -> t -> unit
+end
+
 module NonNegativePolynomial : sig
   include AbstractDomain.WithTop
 
@@ -33,7 +43,7 @@ module NonNegativePolynomial : sig
 
   val subst : astate -> Bound.eval_sym -> astate
 
-  val degree : astate -> int option
+  val degree : astate -> Degree.t option
 
   val compare_by_degree : astate -> astate -> int
 

infer/src/checkers/cost.ml

@@ -609,7 +609,7 @@ type extras_TransferFunctionsWCET =
 
 let compute_errlog_extras cost =
   { Jsonbug_t.cost_polynomial= Some (Format.asprintf "%a" BasicCost.pp cost)
-  ; cost_degree= BasicCost.degree cost }
+  ; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.to_int }
 
 
 (* Calculate the final Worst Case Execution Time predicted for each node.
@@ -641,7 +641,7 @@ module TransferFunctionsWCET = struct
     let degree_str =
       match BasicCost.degree cost with
       | Some degree ->
-          Format.sprintf ", degree = %d" degree
+          Format.asprintf ", degree = %a" Polynomials.Degree.pp degree
       | None ->
           ""
     in