Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add YAML witness validation by invariant checking #745

Merged
merged 26 commits into from
May 31, 2022
Merged

Conversation

sim642
Copy link
Member

@sim642 sim642 commented May 25, 2022

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

@sim642 sim642 added feature sv-comp SV-COMP (analyses, results), witnesses benchmarking pr-dependency Depends or builds on another PR, which should be merged before labels May 25, 2022
@sim642
Copy link
Member Author

sim642 commented May 25, 2022

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.

This avoids unknown value escape warnings.
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

Base automatically changed from yaml-witness to master May 27, 2022 07:59
Comment on lines +281 to +283
List.iter (fun (v: Cil.varinfo) ->
Hashtbl.replace env v.vname (Cabs2cil.EnvVar v, v.vdecl)
) (fd.sformals @ fd.slocals);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label May 30, 2022
@sim642 sim642 merged commit d21a2f3 into master May 31, 2022
@sim642 sim642 deleted the yaml-witness-validate branch May 31, 2022 09:36
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
benchmarking feature sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants