Remove dummy top and is_top implementations from int domains
#1727
Conversation
Most domains have dummy implementations which aren't used.
| | `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 ik | ||
| | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt false else top_of ik |
There was a problem hiding this comment.
Should this not be top_of Iint then? Just for symmetry with the other case?
There was a problem hiding this comment.
That sounds right, so I've changed it in eq and ne.
Although these things look like a mess: other comparisons (e.g. lt) go as far as returning top_bool, regardless of ik.
| (* 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 |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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!
While doing #1726 I noticed this beauty:
analyzer/src/cdomain/value/cdomains/int/defExcDomain.ml
Line 84 in 18489f3
Although it's supposed to be harmless.
Nevertheless, int domains have dummy
topandis_topimplementations: in many cases even justfailwiths because they aren't actually needed. Instead, we only ever usetop_ofandis_top_of, as evidenced by the fact that we never crash with these dummy implementations.Therefore, this is a slight cleanup of the (rather messy) int domain signature to not require
topandis_topat all.EDIT: Now also fixes unsoundness of def_exc for
__int128.