From 8de2b93cab33d8a1e7ca6c3ab20b5605d9788bc8 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Sat, 24 Nov 2018 14:48:01 -0800 Subject: [PATCH] [cost] Abstract type for polynomial degree Reviewed By: ezgicicek Differential Revision: D13175851 fbshipit-source-id: db9078037 --- infer/src/backend/Differential.ml | 34 +++++++++++++++---------- infer/src/bufferoverrun/ints.ml | 4 +++ infer/src/bufferoverrun/ints.mli | 4 +++ infer/src/bufferoverrun/polynomials.ml | 24 ++++++++++++++--- infer/src/bufferoverrun/polynomials.mli | 12 ++++++++- infer/src/checkers/cost.ml | 4 +-- 6 files changed, 62 insertions(+), 20 deletions(-) diff --git a/infer/src/backend/Differential.ml b/infer/src/backend/Differential.ml index 2b4e83511..24a840d0f 100644 --- a/infer/src/backend/Differential.ml +++ b/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 = - match v with - | `Both (current, previous) -> + let merge_aux _ cur_opt prev_opt = + match (cur_opt, prev_opt) with + | 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)] diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index d2d72a63a..b629c5c10 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/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.( * ) diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli index baea58cf7..b68709edf 100644 --- a/infer/src/bufferoverrun/ints.mli +++ b/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 diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 231960e57..bd7d206a2 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/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) ) - terms (0, one) + max acc (Degree.succ d, mult_symb p' t) ) + 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 = diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index 034313d9f..d988c6752 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/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 diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 57ac7f204..99e0fecad 100644 --- a/infer/src/checkers/cost.ml +++ b/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