From 4343f9c8b22f2f1ff298f8cfa83d2265d25e8102 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 19 Dec 2018 06:19:35 -0800 Subject: [PATCH] [cost] Adds Log elements to polynomials Reviewed By: ezgicicek Differential Revision: D13175872 fbshipit-source-id: 2f1337317 --- infer/src/backend/Differential.ml | 2 +- infer/src/bufferoverrun/ints.ml | 2 + infer/src/bufferoverrun/ints.mli | 2 + infer/src/bufferoverrun/polynomials.ml | 107 ++++++++++++++++-- infer/src/bufferoverrun/polynomials.mli | 3 +- infer/src/checkers/cost.ml | 2 +- .../costs_summary.json.exp | 2 +- 7 files changed, 105 insertions(+), 15 deletions(-) diff --git a/infer/src/backend/Differential.ml b/infer/src/backend/Differential.ml index 4bc8c58cc..650a7035c 100644 --- a/infer/src/backend/Differential.ml +++ b/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 diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index b629c5c10..e4bcbdefb 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/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.( * ) diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli index b68709edf..9a0c7a6b3 100644 --- a/infer/src/bufferoverrun/ints.mli +++ b/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 diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index b3ec2b643..fe546b6ff 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/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 diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index 2a5b9ef12..71de67557 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/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 diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 5ee1ea1cc..bb4ed0dca 100644 --- a/infer/src/checkers/cost.ml +++ b/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. diff --git a/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp b/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp index 952a00bba..9d2905b4d 100644 --- a/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp +++ b/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}]} \ No newline at end of file +{"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}]} \ No newline at end of file