Merge pull request #1727 from goblint/intdomain-no-top

Remove dummy `top` and `is_top` implementations from int domains

Author: sim642

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -81,8 +81,8 @@ struct
   let name () = "def_exc"
 
 
-  let top_range = R.of_interval range_ikind (-99L, 99L) (* Since there is no top ikind we use a range that includes both ILongLong [-63,63] and IULongLong [0,64]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
-  let top () = `Excluded (S.empty (), top_range)
+  let overflow_range = R.of_interval range_ikind (-999L, 999L) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
+  let top_overflow () = `Excluded (S.empty (), overflow_range)
   let bot () = `Bot
   let top_of ik = `Excluded (S.empty (), size ik)
   let bot_of ik = bot ()
@@ -117,8 +117,6 @@ struct
       let upperb = Exclusion.max_of_range r in
       Z.compare i upperb <= 0
 
-  let is_top x = x = top ()
-
   let equal_to i = function
     | `Bot -> failwith "unsupported: equal_to with bottom"
     | `Definite x -> if i = x then `Eq else `Neq
@@ -351,10 +349,10 @@ struct
       (* We don't bother with exclusion sets: *)
       | `Excluded _, `Definite _
       | `Definite _, `Excluded _
-      | `Excluded _, `Excluded _ -> top ()
+      | `Excluded _, `Excluded _ -> top_overflow ()
       (* The good case: *)
       | `Definite x, `Definite y ->
-        (try `Definite (f x y) with | Division_by_zero -> top ())
+        (try `Definite (f x y) with | Division_by_zero -> top_overflow ())
       | `Bot, `Bot -> `Bot
       | _ ->
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
@@ -367,7 +365,7 @@ struct
     norm ik @@
     match x,y with
     (* If both are exclusion sets, there isn't anything we can do: *)
-    | `Excluded _, `Excluded _ -> top ()
+    | `Excluded _, `Excluded _ -> top_overflow ()
     (* A definite value should be applied to all members of the exclusion set *)
     | `Definite x, `Excluded (s,r) -> def_exc f x s r
     (* Same thing here, but we should flip the operator to map it properly *)
@@ -382,11 +380,11 @@ struct
   (* The equality check: *)
   let eq ik x y = match x,y with
     (* Not much to do with two exclusion sets: *)
-    | `Excluded _, `Excluded _ -> top ()
+    | `Excluded _, `Excluded _ -> top_of IInt
     (* Is x equal to an exclusion set, if it is a member then NO otherwise we
      * don't know: *)
-    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt false else top ()
-    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt false else top ()
+    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt false else top_of IInt
+    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt false else top_of IInt
     (* The good case: *)
     | `Definite x, `Definite y -> of_bool IInt (x = y)
     | `Bot, `Bot -> `Bot
@@ -397,11 +395,11 @@ struct
   (* The inequality check: *)
   let ne ik x y = match x,y with
     (* Not much to do with two exclusion sets: *)
-    | `Excluded _, `Excluded _ -> top ()
+    | `Excluded _, `Excluded _ -> top_of IInt
     (* Is x unequal to an exclusion set, if it is a member then Yes otherwise we
      * don't know: *)
-    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt true else top ()
-    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt true else top ()
+    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt true else top_of IInt
+    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt true else top_of IInt
     (* The good case: *)
     | `Definite x, `Definite y -> of_bool IInt (x <> y)
     | `Bot, `Bot -> `Bot
@@ -460,12 +458,12 @@ struct
         else if Z.equal i Z.one then
           of_interval IBool (Z.zero, Z.one)
         else
-          top ()
+          top_of ik
       | `Definite _, `Excluded _
-      | `Excluded _, `Excluded _ -> top ()
+      | `Excluded _, `Excluded _ -> top_of ik
       (* The good case: *)
       | `Definite x, `Definite y ->
-        (try `Definite (Z.logand x y) with | Division_by_zero -> top ())
+        (try `Definite (Z.logand x y) with | Division_by_zero -> top_of ik)
       | `Bot, `Bot -> `Bot
       | _ ->
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)

src/cdomain/value/cdomains/int/enumsDomain.ml

@@ -19,7 +19,6 @@ module Enums : S with type int_t = Z.t = struct
   type int_t = Z.t
   let name () = "enums"
   let bot () = failwith "bot () not implemented for Enums"
-  let top () = failwith "top () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
   let top_of ik =

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -114,7 +114,6 @@ module IntDomTupleImpl = struct
     | _ -> true
 
   (* f0: constructors *)
-  let top () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top } ()
   let bot () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot } ()
   let top_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of }
   let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
@@ -206,7 +205,6 @@ module IntDomTupleImpl = struct
 
   (* exists/for_all *)
   let is_bot = exists % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_bot }
-  let is_top = for_all % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_top }
   let is_top_of ik = for_all % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_top_of ik }
   let is_excl_list = exists % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_excl_list }
 

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -9,7 +9,6 @@ struct
 
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
-  let top () = failwith @@ "top () not implemented for " ^ (name ())
   let top_of ik = Some (range ik)
   let bot () = None
   let bot_of ik = bot () (* TODO: improve *)

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -31,8 +31,6 @@ struct
 
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
-  let top () = failwith @@ "top () not implemented for " ^ (name ())
-
   let top_of ik = [range ik]
 
   let bot () = []

src/cdomain/value/cdomains/intDomain.mli

@@ -170,7 +170,8 @@ end
 (* Shared signature of IntDomain implementations and the lifted IntDomains *)
 module type B =
 sig
-  include Lattice.S
+  include Lattice.PO
+  include Lattice.Bot with type t := t
   type int_t
   (** {b Accessing values of the ADT} *)
 
@@ -215,6 +216,7 @@ end
 module type IkindUnawareS =
 sig
   include B
+  include Lattice.Top with type t := t
   include Arith with type t:= t
   val starting   : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending     : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
@@ -316,6 +318,7 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type
 module type Y =
 sig
   include B
+  include Lattice.Top with type t := t
   include Arith with type t:=t
 
   val of_int: Cil.ikind -> int_t -> t
@@ -439,9 +442,6 @@ module Flat (Base: IkindUnawareS): IkindUnawareS with type t = [ `Bot | `Lifted
 module Lift (Base: IkindUnawareS): IkindUnawareS with type t = [ `Bot | `Lifted of Base.t | `Top ] and type int_t = Base.int_t
 (** Just like {!Value.Flat} except the order is preserved. *)
 
-module Reverse (Base: IkindUnawareS): IkindUnawareS with type t = Base.t and type int_t = Base.int_t
-(** Reverses bot, top, leq, join, meet *)
-
 (* module Interval : S *)
 (** Interval domain with int64-s --- use with caution! *)
 

src/cdomain/value/cdomains/intDomain0.ml

@@ -161,7 +161,8 @@ end
 (* Shared functions between S and Z *)
 module type B =
 sig
-  include Lattice.S
+  include Lattice.PO
+  include Lattice.Bot with type t := t
   type int_t
   val bot_of: Cil.ikind -> t
   val top_of: Cil.ikind -> t
@@ -185,6 +186,7 @@ end
 module type IkindUnawareS =
 sig
   include B
+  include Lattice.Top with type t := t
   include Arith with type t := t
   val starting   : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending     : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
@@ -277,8 +279,8 @@ end
 
 module type Y =
 sig
-  (* include B *)
   include B
+  include Lattice.Top with type t := t
   include Arith with type t:= t
   val of_int: Cil.ikind -> int_t -> t
   val of_bool: Cil.ikind -> bool -> t
@@ -319,7 +321,7 @@ struct
   let is_bot x = I.is_bot x.v
   let top_of ikind = { v = I.top_of ikind; ikind}
   let top () = failwith "top () is not implemented for IntDomLifter."
-  let is_top x = I.is_top x.v
+  let is_top _ = failwith "is_top is not implemented for IntDomLifter."
 
   (* Leq does not check for ikind, because it is used in invariant with arguments of different type.
      TODO: check ikinds here and fix invariant to work with right ikinds *)
@@ -417,6 +419,7 @@ module IntDomWithDefaultIkind (I: Y) (Ik: Ikind) : Y with type t = I.t and type
 struct
   include I
   let top () = I.top_of (Ik.ikind ())
+  let is_top x = I.is_top_of (Ik.ikind ()) x
   let bot () = I.bot_of (Ik.ikind ())
 end
 
@@ -520,7 +523,6 @@ module Std (B: sig
   include Printable.StdLeaf
   let name = B.name (* overwrite the one from Printable.Std *)
   open B
-  let is_top x = failwith "is_top not implemented for IntDomain.Std"
   let is_bot x = B.equal x (bot_of Cil.IInt) (* Here we assume that the representation of bottom is independent of the ikind
                                                 This may be true for intdomain implementations, but not e.g. for IntDomLifter. *)
   let is_top_of ik x = B.equal x (top_of ik)
@@ -907,12 +909,6 @@ end
 module Flattened = Flat (Integers (IntOps.Int64Ops))
 module Lifted = Lift (Integers (IntOps.Int64Ops))
 
-module Reverse (Base: IkindUnawareS) =
-struct
-  include Base
-  include (Lattice.Reverse (Base) : Lattice.S with type t := Base.t)
-end
-
 module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t = D.t = struct
 
   include D

src/domain/lattice.ml

@@ -27,16 +27,28 @@ sig
   val pretty_diff: unit -> (t * t) -> Pretty.doc
 end
 
-(* complete lattice *)
-module type S =
+module type Bot =
 sig
-  include PO
+  type t
   val bot: unit -> t
   val is_bot: t -> bool
+end
+
+module type Top =
+sig
+  type t
   val top: unit -> t
   val is_top: t -> bool
 end
 
+(* complete lattice *)
+module type S =
+sig
+  include PO
+  include Bot with type t := t
+  include Top with type t := t
+end
+
 exception TopValue
 (** Exception raised by a topless lattice in place of a top value.
     Surrounding lattice functors may handle this on their own. *)

tests/regression/01-cpa/60-def_exc-int128.c

@@ -0,0 +1,12 @@
+#include <goblint.h>
+#include <limits.h>
+
+// There are no 128bit integer literals...
+__int128 int128max = ((__int128) LLONG_MAX) << 64 | ULLONG_MAX;
+
+int main() {
+  __int128 x, y, z;
+  z = x + y;
+  __goblint_check(z < int128max); // UNKNOWN!
+  return 0;
+}

tests/unit/cdomains/intDomainTest.ml

@@ -555,8 +555,8 @@ struct
                                             (Printf.sprintf "test_shift_right_ik_%s" (CilType.Ikind.show ik)) Int.shift_right I.shift_right :: acc
                                         ) [] ik_lst |> QCheck_ounit.to_ounit2_test_list
 
-  let bot = `B (I.bot ())
-  let top = `B (I.top ())
+  let bot = `B (I.bot_of ik)
+  let top = `B (I.top_of ik)
 
   let isSigned = GoblintCil.Cil.isSigned