Cost domain is not an abstract domain

Reviewed By: skcho

Differential Revision: D14247682

fbshipit-source-id: a16a34945

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 *)

infer/src/bufferoverrun/ints.ml

@@ -83,8 +83,6 @@ module NonNegativeInt = struct
 
   let ( * ) = Z.( * )
 
-  let max = Z.max
-
   let pp = Z.pp_print
 end
 

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
 

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 ->

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
 

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"
 

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