Repository navigation
Conversation
The validator took a bottom answer for an invariant as dead code, which counts as confirmed. But bottom may also come from the invariant itself, e.g. (char)(x + 1) with x == INT_MAX overflows under assume_none, so false invariants were confirmed. Dead code is now recognized by the state being bottom, and a bottom answer in a live state is unconfirmed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The invariant b == & g is true, but the relational analysis evaluates (_Bool)((unsigned long)b == (unsigned long)(& g)) to false, so the meet with base's answer is bottom in a live state. Previously, this bottom was taken as dead code and the invariant was confirmed by chance; now it is unconfirmed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
| if Spec.D.is_bot (LHT.find lh lvar) then | ||
| acc (* dead code *) | ||
| else ( |
There was a problem hiding this comment.
This will skip over parsing the invariants for dead locations, so syntactically invalid invariants there would be accepted. I'm not sure that should be the case.
There was a problem hiding this comment.
This is fixed now, it first does the parsing, as in the previous implementation.
| let result: VR.result = match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with | ||
| | Ok inv_exp -> | ||
| begin match Queries.eval_bool {f = (fun (type a) (q: a Queries.t) -> ask_local lvar q)} inv_exp with | ||
| | `Bot -> Unconfirmed (* the state is not dead, so bottom comes from the invariant itself, e.g. an overflow assumed not to happen *) |
There was a problem hiding this comment.
There's a bigger issue here than just invariants must-overflowing: may-overflowing invariants should also not be allowed. Or any other kind of UB in the invariants.
So this seems to patch over one corner case, but what does that give us?
There was a problem hiding this comment.
So this seems to patch over one corner case, but what does that give us?
Well, the problem was that previously, we assumed that if an invariant evaluates to bottom (which may be due to Goblint assuming that no overflow can happen), the invariant would trivially be considered to hold. So this is an issue this is fixing.
There was a problem hiding this comment.
But yes, one could extend this to the case of may-overflows, by checking whether each expression may contain any overflow.
| [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1) | ||
| [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1) | ||
| [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1) | ||
| [Warning][Witness] invariant unconfirmed: b == & g (95-witness-mm-escape.c:19:1) |
There was a problem hiding this comment.
This is odd: I don't see a problem with this pointer equality invariant.
Checking for dead code before parsing skipped invalid invariants there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The witness was copied from 56-witness/03, including its uuid and producer. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
[Opus 5.5]:
Goblint confirmed some incorrect witness invariants during validation. For example, with
x == INT_MAXundersem.int.signed_overflowassume_none, the invariant(char)(x + 1)(which is0, i.e., false) was confirmed.This was because the validator took a bottom answer of
eval_boolfor an invariant as dead code, which counts as confirmed. But bottom may also come from evaluating the invariant itself in a live state: here,x + 1overflows, whichassume_noneassumes not to happen, so the invariant evaluates to bottom. Similarly, contradicting answers of different analyses for the invariant result in bottom.We fix this by recognizing dead code by the (local) state being bottom, instead of by the answer for the invariant. A bottom answer in a live state now makes the invariant unconfirmed.
Tests
56-witness/81: the false invariant(char)(x + 1)is unconfirmed instead of confirmed.46-apron2/95: the true invariantb == & gis now unconfirmed instead of confirmed. The relational analysis evaluates(_Bool)((unsigned long)b == (unsigned long)(& g))to false, so its meet with base's answer is bottom in a live state. Previously, this was taken as dead code and the invariant was confirmed by chance. The wrong answer of the relational analysis is a separate issue.This is needed for #2206, which makes base answer bottom (instead of crashing) when operating on bottom while answering queries in the final solution.
🤖 Generated with Claude Code