From 0185b76c3d57e72a3863dcff6bdf5ce763c14724 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 28 Feb 2019 03:55:28 -0800 Subject: [PATCH] Cost domain is not an abstract domain Reviewed By: skcho Differential Revision: D14247682 fbshipit-source-id: a16a34945 --- infer/src/absint/AbstractDomain.mli | 18 +++++++++++++++--- infer/src/bufferoverrun/ints.ml | 2 -- infer/src/bufferoverrun/ints.mli | 2 -- infer/src/bufferoverrun/polynomials.ml | 23 +++++++---------------- infer/src/bufferoverrun/polynomials.mli | 6 +++++- infer/src/checkers/costDomain.ml | 2 +- infer/src/istd/PrettyPrintable.mli | 3 +++ 7 files changed, 31 insertions(+), 25 deletions(-) diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index bf2188c2e..145e5b6d9 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -76,7 +76,11 @@ end module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted module TopLiftedUtils : sig + val ( <= ) : le:(lhs:'a -> rhs:'a -> bool) -> lhs:'a top_lifted -> rhs:'a top_lifted -> bool + val pp_top : Format.formatter -> unit + + val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a top_lifted -> unit end (** Cartesian product of two domains. *) @@ -129,11 +133,19 @@ module type MapS = sig include WithBottom with type t := t end -(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. +include + sig + [@@@warning "-60"] + + (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map *) -module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : - MapS with type key = PPMap.key and type value = ValueDomain.t and type t = ValueDomain.t PPMap.t + module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : + MapS + with type key = PPMap.key + and type value = ValueDomain.t + and type t = ValueDomain.t PPMap.t +end (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else *) diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index e4bcbdefb..765e5156f 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/infer/src/bufferoverrun/ints.ml @@ -83,8 +83,6 @@ module NonNegativeInt = struct let ( * ) = Z.( * ) - let max = Z.max - let pp = Z.pp_print end diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli index 9a0c7a6b3..63daa80ed 100644 --- a/infer/src/bufferoverrun/ints.mli +++ b/infer/src/bufferoverrun/ints.mli @@ -73,8 +73,6 @@ module NonNegativeInt : sig val ( * ) : t -> t -> t - val max : t -> t -> t - val pp : F.formatter -> t -> unit end diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index ff27900bf..d94242297 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -298,15 +298,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct PartialOrder.join cmp_const cmp_terms - (* Possible optimization for later: x join x^2 = x^2 instead of x + x^2 *) - let rec join : t -> t -> t = - fun p1 p2 -> - if phys_equal p1 p2 then p1 - else - { const= NonNegativeInt.max p1.const p2.const - ; terms= M.increasing_union ~f:join p1.terms p2.terms } - - (* assumes symbols are not comparable *) (* TODO: improve this for comparable symbols *) let min_default_left : t -> t -> t = @@ -320,10 +311,6 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct if is_constant p1 then p1 else if is_constant p2 then p2 else p1 - let widen : prev:t -> next:t -> num_iters:int -> t = - fun ~prev:_ ~next:_ ~num_iters:_ -> assert false - - let subst callee_pname loc = let exception ReturnTop in (* avoids top-lifting everything *) @@ -422,7 +409,13 @@ module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNega module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind) module NonNegativePolynomial = struct - include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial) + type t = NonNegativeNonTopPolynomial.t top_lifted + + let top = Top + + let ( <= ) = AbstractDomain.TopLiftedUtils.( <= ) ~le:NonNegativeNonTopPolynomial.( <= ) + + let pp = AbstractDomain.TopLiftedUtils.pp ~pp:NonNegativeNonTopPolynomial.pp let zero = NonTop NonNegativeNonTopPolynomial.zero @@ -460,8 +453,6 @@ module NonNegativePolynomial = struct NonTop (NonNegativeNonTopPolynomial.min_default_left p1 p2) - let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top - let subst callee_pname loc p eval_sym = match p with | Top -> diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index a576064e5..05484500d 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/infer/src/bufferoverrun/polynomials.mli @@ -30,7 +30,11 @@ module NonNegativeNonTopPolynomial : sig end module NonNegativePolynomial : sig - include AbstractDomain.WithTop + include PrettyPrintable.PrintableType + + val ( <= ) : lhs:t -> rhs:t -> bool + + val top : t val zero : t diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 24a0f03dd..dcc181849 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -49,7 +49,7 @@ end {OperationCost, AllocationCost, IOCost} -> BasicCost.t *) module VariantCostMap = struct - include AbstractDomain.MapOfPPMap (CostKindMap) (BasicCost) + include PrettyPrintable.PPMonoMapOfPPMap (CostKindMap) (BasicCost) let[@warning "-32"] add _ = Logging.die InternalError "Don't call me" diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index 941cf1396..83e283783 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -140,5 +140,8 @@ module MakePPSet (Ord : PrintableOrderedType) : PPSet with type elt = Ord.t module MakePPMap (Ord : PrintableOrderedType) : PPMap with type key = Ord.t +module PPMonoMapOfPPMap (M : PPMap) (Val : PrintableType) : + PPMonoMap with type key = M.key and type value = Val.t and type t = Val.t M.t + module MakePPMonoMap (Ord : PrintableOrderedType) (Val : PrintableType) : PPMonoMap with type key = Ord.t and type value = Val.t