PrivPrecCompare: Add bot_in_blob_leq_bot so bot and Blob(bot) are considered equal

[michael-schwarz]

This was needed to not report spurious precision differences for the benchmarks in my thesis.
If we want this on the main branch, we can merge, otherwise we can close it.

[sim642]

I haven't thought about it much or checked if this would completely break something, but I wonder if such thing could/should be non-optional. I think ValueDomain.join has cases for joining blobs with non-blobs by lifting the joining into the blob, etc. Perhaps something similar should be in leq unconditionally to maintain its algebraic consistency with join, etc.

I suspect domain quickchecking doesn't really work on ValueDomain, so such consistency might not be too easy to check that way.

[michael-schwarz]

I am also not sure if one wants to have this in general, but I think having it in the compare scripts and having the option to dis/enable it, seems like it is generally a step in the right direction?

[michael-schwarz]

Do we want to merge this or close it? I'm fine with either!

[sim642]

I was wondering about these join cases:

analyzer/src/cdomain/value/cdomains/valueDomain.ml

Lines 603 to 604 in 99df9da

	| Blob (x,s,o), y
	| y, Blob (x,s,o) -> Blob (join (x:t) y, s, o)

But they're actually after these:

analyzer/src/cdomain/value/cdomains/valueDomain.ml

Lines 589 to 590 in 99df9da

	| (Bot, x) -> x
	| (x, Bot) -> x

So the special cases don't even trigger for such things. Indeed, then this isn't what should normally happen, but I'm ok with having it for comparison.