[cost] Adds Log elements to polynomials

Reviewed By: ezgicicek

Differential Revision: D13175872

fbshipit-source-id: 2f1337317

infer/src/backend/Differential.ml

@@ -111,7 +111,7 @@ module CostsSummary = struct
       DegreeMap.bindings paired_counts.degrees
       |> List.map ~f:(fun (key, {current; previous}) ->
              `Assoc
-               [ ("degree", `Int (Polynomials.Degree.to_int key))
+               [ ("degree", `Int (Polynomials.Degree.encode_to_int key))
                ; ("current", `Int current)
                ; ("previous", `Int previous) ] )
     in

infer/src/bufferoverrun/ints.ml

@@ -77,6 +77,8 @@ module NonNegativeInt = struct
 
   let succ = Z.succ
 
+  let log2_ceil_exn i = Z.log2up i |> Z.of_int
+
   let ( + ) = Z.( + )
 
   let ( * ) = Z.( * )

infer/src/bufferoverrun/ints.mli

@@ -67,6 +67,8 @@ module NonNegativeInt : sig
 
   val succ : t -> t
 
+  val log2_ceil_exn : t -> t
+
   val ( + ) : t -> t -> t
 
   val ( * ) : t -> t -> t

infer/src/bufferoverrun/polynomials.ml

@@ -10,33 +10,115 @@ open! AbstractDomain.Types
 module Bound = Bounds.Bound
 open Ints
 
+module DegreeKind = struct
+  type t = Linear | Log [@@deriving compare]
+
+  let[@warning "-32"] _i_know_log_isn't_used_for_now = Log
+
+  let compute d i =
+    match d with
+    | Linear ->
+        i
+    | Log -> (
+      try NonNegativeInt.log2_ceil_exn i with Invalid_argument _ -> NonNegativeInt.zero )
+
+
+  let pp_hole pp f d x = match d with Linear -> pp f x | Log -> Format.fprintf f "log(%a)" pp x
+end
+
 module Degree = struct
-  type t = NonNegativeInt.t [@@deriving compare]
+  type t = {linear: NonNegativeInt.t; log: NonNegativeInt.t} [@@deriving compare]
+
+  let zero = {linear= NonNegativeInt.zero; log= NonNegativeInt.zero}
+
+  let succ (k : DegreeKind.t) d =
+    match k with
+    | Linear ->
+        {d with linear= NonNegativeInt.succ d.linear}
+    | Log ->
+        {d with log= NonNegativeInt.succ d.log}
 
-  let zero = NonNegativeInt.zero
 
-  let succ = NonNegativeInt.succ
+  let encode_to_int d =
+    (*
+      Constructs an integer compatible with compare.
+      We assume that degrees won't go exceed 100 ;-)
+    *)
+    (NonNegativeInt.to_int_exn d.linear * 100) + NonNegativeInt.to_int_exn d.log
 
-  let to_int = NonNegativeInt.to_int_exn
 
-  let is_zero = NonNegativeInt.is_zero
+  let is_zero d = NonNegativeInt.is_zero d.linear && NonNegativeInt.is_zero d.log
 
-  let pp = NonNegativeInt.pp
+  let pp f d =
+    NonNegativeInt.pp f d.linear ;
+    if not (NonNegativeInt.is_zero d.log) then
+      F.fprintf f " + %a%slog" NonNegativeInt.pp d.log SpecialChars.dot_operator
 end
 
 module type NonNegativeSymbol = sig
   type t [@@deriving compare]
 
+  val classify : t -> (Ints.NonNegativeInt.t, t) Bounds.valclass
+
   val int_lb : t -> NonNegativeInt.t
 
   val int_ub : t -> NonNegativeInt.t option
 
-  val subst : t -> t Symb.Symbol.eval -> (NonNegativeInt.t, t) Bounds.valclass
+  val subst : t -> Bound.eval_sym -> (NonNegativeInt.t, t) Bounds.valclass
 
   val pp : F.formatter -> t -> unit
 end
 
-module MakePolynomial (S : NonNegativeSymbol) = struct
+module type NonNegativeSymbolWithDegreeKind = sig
+  type t0
+
+  include NonNegativeSymbol
+
+  val make : DegreeKind.t -> t0 -> t
+
+  val degree_kind : t -> DegreeKind.t
+end
+
+module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
+  NonNegativeSymbolWithDegreeKind with type t0 = S.t = struct
+  type t0 = S.t [@@deriving compare]
+
+  type t = {degree_kind: DegreeKind.t; symbol: t0} [@@deriving compare]
+
+  let classify ({degree_kind; symbol} as self) =
+    match S.classify symbol with
+    | Constant c ->
+        Bounds.Constant (DegreeKind.compute degree_kind c)
+    | Symbolic _ ->
+        Bounds.Symbolic self
+    | ValTop ->
+        Bounds.ValTop
+
+
+  let make degree_kind symbol = {degree_kind; symbol}
+
+  let int_lb {degree_kind; symbol} = S.int_lb symbol |> DegreeKind.compute degree_kind
+
+  let int_ub {degree_kind; symbol} =
+    S.int_ub symbol |> Option.map ~f:(DegreeKind.compute degree_kind)
+
+
+  let subst {degree_kind; symbol} eval =
+    match S.subst symbol eval with
+    | Constant c ->
+        Bounds.Constant (DegreeKind.compute degree_kind c)
+    | Symbolic symbol ->
+        Bounds.Symbolic {degree_kind; symbol}
+    | ValTop ->
+        Bounds.ValTop
+
+
+  let pp f {degree_kind; symbol} = DegreeKind.pp_hole S.pp f degree_kind symbol
+
+  let degree_kind {degree_kind} = degree_kind
+end
+
+module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
   module M = struct
     include Caml.Map.Make (S)
 
@@ -269,7 +351,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
     M.fold
       (fun t p acc ->
         let d, p' = degree_with_term p in
-        max acc (Degree.succ d, mult_symb p' t) )
+        max acc (Degree.succ (S.degree_kind t) d, mult_symb p' t) )
       terms (Degree.zero, one)
 
 
@@ -329,7 +411,8 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
 end
 
 module NonNegativePolynomial = struct
-  module NonNegativeNonTopPolynomial = MakePolynomial (Bounds.NonNegativeBound)
+  module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
+  module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
   include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial)
 
   let zero = NonTop NonNegativeNonTopPolynomial.zero
@@ -339,7 +422,9 @@ module NonNegativePolynomial = struct
   let of_int_exn i = NonTop (NonNegativeNonTopPolynomial.of_int_exn i)
 
   let of_non_negative_bound b =
-    b |> Bounds.NonNegativeBound.classify |> NonNegativeNonTopPolynomial.of_valclass
+    b
+    |> NonNegativeBoundWithDegreeKind.make DegreeKind.Linear
+    |> NonNegativeBoundWithDegreeKind.classify |> NonNegativeNonTopPolynomial.of_valclass
 
 
   let is_symbolic = function Top -> false | NonTop p -> NonNegativeNonTopPolynomial.is_symbolic p

infer/src/bufferoverrun/polynomials.mli

@@ -11,7 +11,8 @@ module Bound = Bounds.Bound
 module Degree : sig
   type t [@@deriving compare]
 
-  val to_int : t -> int
+  val encode_to_int : t -> int
+  (** Encodes the complex type [t] to an integer that can be used for comparison. *)
 
   val is_zero : t -> bool
 

infer/src/checkers/cost.ml

@@ -603,7 +603,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 |> Option.map ~f:Polynomials.Degree.to_int }
+  ; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.encode_to_int }
 
 
 (* Calculate the final Worst Case Execution Time predicted for each node.

infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp

@@ -1 +1 @@
-{"top":{"current":1,"previous":0},"zero":{"current":0,"previous":0},"degrees":[{"degree":0,"current":3,"previous":2},{"degree":1,"current":1,"previous":1},{"degree":2,"current":0,"previous":1}]}
+{"top":{"current":1,"previous":0},"zero":{"current":0,"previous":0},"degrees":[{"degree":0,"current":3,"previous":2},{"degree":100,"current":1,"previous":1},{"degree":200,"current":0,"previous":1}]}