Skip to content

Remove dummy top and is_top implementations from int domains #1727

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 12 commits into from
Apr 17, 2025
Merged

Remove dummy top and is_top implementations from int domains #1727

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
8f99cbd
Remove unused IntDomain.Reverse
sim642 Apr 15, 2025
c9a256f
Remove top and is_top from IntDomain signature
sim642 Apr 15, 2025
eda4fe8
Remove dummy top and is_top implementations from int domains
sim642 Apr 15, 2025
4715c07
Make IntDomain.IntDomWithDefaultIkind.is_top match top
sim642 Apr 15, 2025
f5cd945
Merge branch 'master' into intdomain-no-top
sim642 Apr 15, 2025
d4bf659
Fix IntDomainTest compilation without top
sim642 Apr 15, 2025
6c9eff3
Restore top_overflow in def_exc for operations like add
sim642 Apr 15, 2025
1ce9de0
Make IntDomLifter.is_top fail with exception
sim642 Apr 15, 2025
1452a93
Add test to reveal def_exc unsoundness for __int128
sim642 Apr 15, 2025
e2a74e7
Fix 01-cpa/60-def_exc-int128
sim642 Apr 15, 2025
6bc71bb
Use IInt ikind for DefExc eq and ne tops
sim642 Apr 16, 2025
a968622
Rename def_exc top_range -> overflow_range to match
sim642 Apr 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 14 additions & 16 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand All @@ -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 *)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down
1 change: 0 additions & 1 deletion src/cdomain/value/cdomains/int/enumsDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,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 =
Expand Down
2 changes: 0 additions & 2 deletions src/cdomain/value/cdomains/int/intDomTuple.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down Expand Up @@ -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 }

Expand Down
1 change: 0 additions & 1 deletion src/cdomain/value/cdomains/int/intervalDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
2 changes: 0 additions & 2 deletions src/cdomain/value/cdomains/int/intervalSetDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 () = []
Expand Down
8 changes: 4 additions & 4 deletions src/cdomain/value/cdomains/intDomain.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} *)

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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! *)

Expand Down
16 changes: 6 additions & 10 deletions src/cdomain/value/cdomains/intDomain0.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -519,7 +522,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)
Expand Down Expand Up @@ -906,12 +908,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
Expand Down
18 changes: 15 additions & 3 deletions src/domain/lattice.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Comment on lines -30 to 42
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we go for BoundedMeetSemiLattice and BoundedJoinSemiLattice here as meaningful mathematical objects? And use this opportunity to actually make our PO a PartialOrder and not some sort of lattice in disguise, i.e., remove join, meet, narrow and widen from it?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could try that in #1728 to also weaken arguments of LiftBot and LiftTop.

Splitting the signatures into precise algebraic structures is nice, but it comes with a cost that we already have with Printable and Lattice: to make meaningful use of them, one needs functors for each one, e.g. Printable.Prod, Lattice.POProd, Lattice.BoundedMeetSemiLatticeProd, Lattice.BoundedJoinSemiLatticeProd, Lattice.Prod, etc.
Of course all code duplication can be avoided by include, but they still need to be separate functors with separate names.

I've thought about splitting Printable.S in the past, because it is even more bloated, but it just leads to a bigger mess.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The question is whether all these lifters are used then. If we don't have a BoundedMeetSemiLatticeProd anywhere, no need to provide the functor for it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Of course we don't and by just introducing the signatures, nothing new would be needed: using the most powerful Lattice.Prod will suffice because in all such cases the arguments currently already provide dummy implementations which wouldn't then be needed.
But it means we have to accept such exponential explosion of functors. For example, you might want BoundedMeetSemiLattice which is also JoinSemiLattice (so just without top), etc.

Anyway, it's a completely orthogonal matter to this PR.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not completely orthogonal: I think introducing ill-defined module signatures such as Top (there is a special element intended to be greater than all others and a way to check whether some element is identical to it, but no way to compare elements) only makes it harder to understand what's going on.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could go back to what I did at first and what matches all the signature duplication happening in IntDomain currently: just declare val top: unit -> t directly, as opposed to putting the signature into Lattice to reuse.
Then we just end up with 5 copies of the top type in Goblint, which isn't nice. But IntDomain is currently full of such copy-paste signatures, so it wouldn't be worse, but it wouldn't move towards cleaning it up either.

I just don't think we have a clean and usable naming scheme: a Lattice.S without top would be the combination of BoundedMeetSemiLattice and (unbounded) JoinSemiLattice. What's supposed to be the name for that? BoundedMeetUnboundedJoinSemiLattice isn't particularly nice.
For these one-off combinations it's much cleaner to just include the necessary components, e.g. PO and Top on demand, rather than having to predefine all necessary combinations.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I get what you mean, I just find the notion of having a Top signature that one can implement without even having a PO which would seem essential to being able to give such a thing non-helpful. But this is not a hill I am willing to die on!


(* 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. *)
Expand Down
12 changes: 12 additions & 0 deletions tests/regression/01-cpa/60-def_exc-int128.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
4 changes: 2 additions & 2 deletions tests/unit/cdomains/intDomainTest.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading