Simplify witness invariants for bitfield domain

[sim642]

I just happened to look into a witness we now produce with the portfolio at a level which enables the bitfield domain and saw lots of trivial invariants like (i & 0) == 0.
The non-relational witness invariant simplification (#1517) happened before the bitfield domain was introduced. The latter wasn't added to witness invariant tests, so this went unnoticed.

This is a bit unfortunate because we now have a bunch of logic for simplifying non-relational and relational witness invariants, but then we also added these, so the SV-COMP 2026 witnesses might again be unnecessarily large...

[sim642]

This is wrong for a top _Bool, but I'm having hard time understanding why.

The representation of top int is 0b?...?, (zs:-1, os:-1), but the representation of top _Bool is 0b0...0?, (zs:-1, os:1). These are not consistent: for int it has an infinite sequence of unknown bits (including higher bits that fit into int), but for _Bool it's one unknown bit with infinitely many definite zero bits in front.
I suspect this causes something to go wrong because the invariant generation is made to believe that there are all these definite 0 bits, but they're outside of the type range.

What are the bits outside of type size supposed to be?
I'm not sure who supervised #1623, @michael-schwarz, @jerhard? Does anyone know

[michael-schwarz]

I think it was @jerhard and @DrMichaelPetter who supervised it, I only sat in on some meetings, so this may be wrong:

Iirc, the idea is that it's mathematical integers and the two's complement just proceeds infinitely long (which is consistent with what happens on upcast iirc)? Not sure if this helps clarify?

[sim642]

For mathematical integers I don't see an issue: they have infinitely many bits and it makes sense to speak about all of them, whether they can be zero or one. And it's very convenient that Zarith has this neat representation with infinite leading ones.

The problem is that this doesn't define what the behavior is supposed to be on machine integers.
Can the 1000th bit of int be a zero or a one? (My comment implies says it may be either.)
What about the 1000th bit of _Bool? (My comment implies it must be zero.)

What does this mean? I don't know. Neither type actually has such bit, so it's not like the concrete semantics forces such behavior. One could even argue that all bits above the type size should be bot because they can't be either because they don't exist.
(In which case both the zeros and ones mask have leading 0s. So none of the Zarith two's complement trickery would even be needed.)

Here's what we currently do for top values:

analyzer/src/cdomain/value/cdomains/int/bitfieldDomain.ml

Lines 196 to 198 in 3988737

	let top_of ?bitfield ik = (* TODO: use bitfield *)
	if GoblintCil.isSigned ik then top ()
	else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))

Signed types give an abstraction which allows infinitely many zeros and ones. For unsigned types, it may be infinitely may zeros, but only ones up to the type size (which means higher bits will definitely be zero).

If I change that function to return always top (), no test fails. So there's no clear reason for the distinction.
I tried looking at the cited Miné paper, but I didn't immediately see an answer: it defines abstract domains on mathematical integers and then just slaps a wrap operation around every operation or something.
However, we carry the ikind together with the abstract value, instead of building abstract domains on mathematical integers, so it's not exactly the same anyway.

[michael-schwarz]

If I change that function to return always top (), no test fails.

I think this may just be because our tests are poor. I think the case where it would make a difference is if you do an upcast from one unsigned type to a bigger one. There, because of our definition hopefully the upper bound would survive?

---

But overall, I'm also not sure what the best / most helpful thing would be.

[sim642]

For now, I just wrapped things into a Cil.fitsInInt. Apparently, it wasn't just problematic for _Bool, but unsigned types in general, where the mask for definite leading zeroes (represented by some negative integer) doesn't really fit the type itself and truncates/wraps wrongly.
It's a bit similar to the issues around goblint/cil#111.

[sim642]

I did verify-validate sv-benchmarks runs on level02 (which always uses bitfield) between 3988737be and 44d2b76c8: https://goblint.cs.ut.ee/results/305-all-validate-level02-pr-1897-after/table-generator-cmp.table.html#/.
A few things to note from that.

There's a huge reduction in the number of generated invariants (~65% on average):

So these trivial bitfield invariants really inflate our witnesses.

There are now 54 more self-validated witnesses: https://goblint.cs.ut.ee/results/305-all-validate-level02-pr-1897-after/table-generator-cmp.table.html#/table?filter=1(0*status*(status(notIn(TIMEOUT,TIMEOUT%20%28ERROR%20%28witness%20error%29%29,TIMEOUT%20%28SEGMENTATION%20FAULT%29,TIMEOUT%20%28true%29,true)),category(notIn()))),3(0*status*(status(in(true)),category(notIn()))).
That includes many of the loop-lit programs from the unassume paper.
It's hard to tell whether any of those were previously unconfirmed because they contained the wrong _Bool/unsigned invariants.

However, there are also cases where the simplified definite-zero invariants actually help. For example before, our own invariant could not be confirmed:

[Warning][Witness] invariant unconfirmed: (~ n & -1024) == -1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/mcmillan2006.i:31:5)

But now it can be in the simpler form:

[Success][Witness] invariant confirmed: (n & -1024) == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/mcmillan2006.i:31:5)

So it looks like bitfield evaluation isn't always as precise as it could be.

[michael-schwarz]

Maybe we split out the issue about unsigned types and then merge this?