Add YAML witness validation by invariant checking

[sim642]

This is on top of #744.

The validation implemented here is quite primitive: the YAML witness is parsed and the invariants are checked on our final solution using the EvalInt query. It is very similar to the expression evaluation transformation used by semantic search. For each invariant, a corresponding message is printed, similarly to the messages printed for in-program assertions.

This primitive form of witness validation is what could be used for relational traces precision benchmarking: one privatization generates the YAML witness and another privatization can then try to prove the same invariants. It doesn't really work for Apron analysis though, because the way Formatcil parses expressions produces invalid ASTs for the kind of expressions currently generated by Apron analysis: goblint/cil#95.

A more reliable solution would be to do something about Formatcil, but a quick workaround would also be to change Apron analysis to output expressions that it can directly parse, e.g. by inserting a few extra casts or whatnot.

By switching from Formatcil to Frontc via goblint/cil#97, it works for Apron analysis and the additional explicit casts might even be unnecessary now.
Moreover, it allows && and || to be used in invariants. During normal parsing we ask CIL to convert them to if statements, but for parsing these invariants, that is temporarily disabled. I went over a bunch of Cil.exp pattern matchings to make them explicit (no wildcard case) such that it would be easier to find where, e.g. Question is being/should be handled.

Examples

Singlethreaded

./regtest.sh 01 04 --enable witness.yaml.enabled
./regtest.sh 01 04 --set witness.yaml.validate witness.yml

Base privatization

./regtest.sh 13 01 --enable witness.yaml.enabled
./regtest.sh 13 01 --set witness.yaml.validate witness.yml

Apron privatization

./regtest.sh 36 89 --enable witness.yaml.enabled
./regtest.sh 36 89 --set witness.yaml.validate witness.yml

Using logical operators

./regtest.sh 01 04 --enable witness.yaml.enabled --enable ana.int.enums --disable witness.invariant.split-conjunction
./regtest.sh 01 04 --set witness.yaml.validate witness.yml

PS. This is an interesting example because we can validate an invariant from enums domain without enabling enums during validation!

TODO

• Merge Add standalone expression AST checking cil#96.
• Merge Expose standalone expression parsing via Frontc cil#97.
• Update opam pin after CIL merges.

[sim642]

A more reliable solution would be to do something about Formatcil, but a quick workaround would also be to change Apron analysis to output expressions that it can directly parse, e.g. by inserting a few extra casts or whatnot.

I did that to IntDomain invariants, but Apron analysis invariants already had it. The mismatching thing there was the ikind of 0 used in the constraint.
That doesn't still work because Formatcil does even more stupid things: when it parses ==, then the result type of the comparison is the type of the arguments (long long for Apron), but it should always be int by the standard.
Works after switching from Formatcil to Frontc.

[michael-schwarz]

Nice!

[michael-schwarz]

Did you test with locals that got renamed because several locals of the same name (and different scopes) existed in the function?

[sim642]

Good point, I didn't think about it here, but I think there's not much to do about it either. On the witness generation side, there's InvariantCil.exp_replace_original_name that maps things to original names. But here for parsing we'd somehow need to know, which of the variables with the same original name was in scope at a particular location inside the function after they've been all pulled up and renamed.

As I mentioned in goblint/cil#97, the normal Cabs2cil uses tons of global variables to keep track of things and these block scopes and alpha renaming tables (and undos in alpha renaming tables) are among those. But all those structures are mutated, so we cannot go back to a particular location and have the exact state of those internal globals that normally keep track of this. One way would be to keep the CABS of all functions around and redo Cabs2cil for the function where the invariant belongs to, so it reconstructs that state, such that we can convert the invariant expression exactly as it would have been at a particular location and abort Cabs2cil, but that seems super ugly.

But here's a maybe radical idea: we make CIL not do those renames at all and just continue with a single fundec containing multiple local varinfos with same vname. Since we identify variables by vid, not vname, this should have no effect on the semantics, only results presentation (which is nicer with less renaming anyway). And somehow also eliminate the pulling up of all locals from all block scopes, such that the scopes are also later observable.

Anyway, tackling that whole issue is probably too much to do right here, but for the time being, a variable name in the expression would just find the first varinfo that has it unrenamed. All the others would have names with suffixes, which won't be used unless you directly also use that name in the invariant, but that would violate the semantics of it being insertable as an assertion.

[sim642]

I extracted this problem to #747 for further discussion and future fixes, so this can be merged.