Cleanup: Only have one query for must-equality between expressions

[michael-schwarz]

We currently have two different queries for must equality of expressions:

• ExpEq (answered by var_eq and octagon and used in base)
• MustBeEqual (answered by base, expRelation, and octagon and used in base and for arrays)

(I am to blame here, I introduced the second one in my Master's thesis).

With this PR:

• We use MustBeEqual everywhere where ExpEq was used
• Fix expRelation to always answer top for floats (see Unsoundness in SV-COMP Prerun #141)

This means that we use all analyses to answer the question whether to expressions must be equal, rather than different ones in different scenarios.

[sim642]

As this is also a query with boolean results, it brings me flashbacks from when I implemented #130 and #137, concerning all the Must, May, Not and no-Not scheme of them. Specifically, how results of boolean queries are supposed to combine if answered by multiple analyses. The boolean result lattice for queries has false leq top.

For example, if one analysis answers MustBeEqual with true and the other one with false, then MCP2 meets them (as reminded by #155), giving false in that lattice. Shouldn't the point of such query be that if one analysis is really precise and can prove the equality, we should trust it, instead of dropping down to the level of the most imprecise analysis, which answered that query? In that sense, it seems to me like the query should be named, answered and used the other way around, like "not equal", so that they meet according to the more precise analysis.
(Maybe the less confusing alternative would be to have two different boolean result lattices with opposite orders and the queries give the one which matches their semantics for combining.)

Also, in some places, e.g. MustBeEqual in base, things have been abused to instead return the top of the query result lattice, which is larger than the top of the boolean lattice. This is such that the imprecise false result wouldn't override others. I feel like this should never be done and instead queries like this should always return results of the correct type, while having their ordering for meet thought through instead of hacked around.

This is in no way a criticism of just MustBeEqual but likely affects many of the other queries too. For example, it's the reason I added a NotSingleThreaded query even though a SingleThreaded query exists, but I wanted the results from different analyses combined in the other way.

[michael-schwarz]

For example, if one analysis answers MustBeEqual with true and the other one with false, then MCP2 meets them (as reminded by #155), giving false in that lattice. Shouldn't the point of such query be that if one analysis is really precise and can prove the equality, we should trust it, instead of dropping down to the level of the most imprecise analysis, which answered that query?

I agree.

Maybe the less confusing alternative would be to have two different boolean result lattices with opposite orders and the queries give the one which matches their semantics for combining.

I think this the cleaner solution, as a negation of MustBeEqual would have to be MayBeUnequal which causes all sorts of knots when thinking about it.
Maybe a better way to handle this is to not have this boolean lattice, but instead two different lattices
T: \bot \leq True \leq \top and F: \bot \leq False \leq \top. This would mean having more queries, but would make it impossible to get confused about the ordering:

E.g. MayBeEqual would return sth from F whereas MustBeEqual would return something from T. I think it is only in rare circumstances that we are interested in both possible answers at the same time.

[michael-schwarz]

I experimented with MayHold with false \leq true and MustHold with true \leq false. I think this is nicer as it forces ne to think about the order when defining such a query. I'm not too happy with the names though, any better suggestions?

If this is what we want to do, I can replace all instance of the Bool result type by this one.

[sim642]

I think this the cleaner solution, as a negation of MustBeEqual would have to be MayBeUnequal which causes all sorts of knots when thinking about it.

That's true, especially if you need to figure out what result false means for MayBeUnequal.

When these issues occurred to me, I think I dug a bit in the git history and found that some things were at some point renamed and flipped to avoid the Not in their name. I suspect these changes might have been done without any consideration about differing meet behavior. I think it often hasn't mattered either because many queries are just answered by one (activated) analysis. But anyway, if we want to clarify this in general, we might have to go over all of the boolean queries anyway.

Maybe a better way to handle this is to not have this boolean lattice, but instead two different lattices
T: \bot \leq True \leq \top and F: \bot \leq False \leq \top. This would mean having more queries, but would make it impossible to get confused about the ordering:

How would it mean more queries? I think the same queries would suffice but their return values would be somewhat weird, e.g. MustBeEqual would return True or \top (of the entire query result lattice). It would actually avoid duplicate meaning of the two tops (of the boolean lattice and the query result lattice), because all analyses being imprecise enough not to be able to prove equality is just as good as no analysis answering at all. Right now many places where queries are made have such special logic for Top also.

But then the natural continuation would be to also want to do the same to all the other variants in the query result type as many of them also have their own specific bottom and top. That might be too much work again.

So in that sense I feel like each result variant should be a standalone lattice (and thus there be two separate variants for boolean and reverse-boolean lattice). Each query (if implemented by an analysis) should then always return something within the appropriate variant. Top of the result lattice should be reserved for "not answered" instead of "not answered or unknown". And bottom of the result lattice should be reserved for "conflicting result types" instead of "conflicting result types or conflicting values of the same type".

EDIT: And then the queries themselves should probably always have "Must" or "May" in their name, to be very clear about their behavior and result variant. At least given the lack of #33.

[michael-schwarz]

How would it mean more queries?

At least now MustBeEqual in base.ml seems to have been with understanding that both Bool true and Bool false are definite answers. But i guess this was only confused usage.

So in that sense I feel like each result variant should be a standalone lattice (and thus there be two separate variants for boolean and reverse-boolean lattice). Each query (if implemented by an analysis) should then always return something within the appropriate variant. Top of the result lattice should be reserved for "not answered" instead of "not answered or unknown". And bottom of the result lattice should be reserved for "conflicting result types" instead of "conflicting result types or conflicting values of the same type".

That's pretty much the thing I now have, right? Minus the \top and \bot in the boolean lattices, but I guess there is no need for them?

[sim642]

I experimented with MayHold with false \leq true and MustHold with true \leq false. I think this is nicer as it forces ne to think about the order when defining such a query. I'm not too happy with the names though, any better suggestions?

Maybe MayBool and MustBool instead, so they still refer to the type as previously and as everything else. Because it isn't unthinkable that similar may/must ordering issues could affect queries of other types as well (although maybe not among the ones we currently have, I never checked).

---

That's pretty much the thing I now have, right? Minus the \top and \bot in the boolean lattices, but I guess there is no need for them?

The change you committed in the meanwhile matches what I originally had in mind and as I said above, I think I'd prefer it that way for now anyway.

[michael-schwarz]

Ok, I switched them all over to MustBool or MayBool now and removed the plain Bool one.

During this, I noticed that SingleThreaded and NotSingleThreaded seem to express exactly the same thing, i.e. are MustBeSingleThreaded and MayNotBeSingleThreaded. So I removed the MayNotBeSingleThreaded one. Would be good if someone else can confirm that this is indeed the case.

[sim642]

During this, I noticed that SingleThreaded and NotSingleThreaded seem to express exactly the same thing, i.e. are MustBeSingleThreaded and MayNotBeSingleThreaded. So I removed the MayNotBeSingleThreaded one. Would be good if someone else can confirm that this is indeed the case.

That seems correct. When I added the negated variant to get the meet right, I initially didn't want to remove the non-negated one in case something actually depended on it working the other way for whatever reason.

I made a few additional commits here: one about flipping a MayBeNot query to MustBe for better clarity and the other for adding some missing operations which I think the default case didn't cover like the old boolean lattice.

[michael-schwarz]

I started a run of this on some larger programs, if this doesn't lead to any curious changes, I'll merge it later today.

[michael-schwarz]

The only thing that changed is two more cases of issue #153.