Skip to content

RFC: Unreachable properties should be marked "UNREACHABLE" not "SUCCESS" #6276

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

Open
danielsn opened this issue Aug 5, 2021 · 5 comments
Open
Labels
aws Bugs or features of importance to AWS CBMC users RFC Request for comment

Comments

@danielsn
Copy link
Contributor

danielsn commented Aug 5, 2021

It is confusing to users when an unreachable property succeeds

@danielsn danielsn added the aws Bugs or features of importance to AWS CBMC users label Aug 5, 2021
@SaswatPadhi SaswatPadhi added the RFC Request for comment label Aug 6, 2021
@SaswatPadhi
Copy link
Contributor

Sounds somewhat related to #6057. A false assumption makes subsequent assertions essentially unreachable.

@jimgrundy
Copy link
Collaborator

Agree that this is related to #6057.

Re-phrasing my comments from that issue:

I'm used to a model checker that offers the following primitive concepts:

assume(p) : add p to the path condition
assert(p) : attempt to satisfy (path & ~p). If satisfied report error. If unsat, report success. (checks a universal property)
cover(p) : attempt to satisfy (path & p). If unsatisfiable report error. If sat, report success. (checks an existential property)

@kroening mentioned the other day that CBMC (used to) support a cover primitive like this, but it didn't seem to get used much, or maybe people didn't find it intuitive. My experience was that this construct was extremely valuable for debugging.

Imagine a world in which you have this construct. Then you can achieve the goal we are shooting for here by transforming:

assume(p);

into

cover(p); assume(p);

My former tool (Jasper) would also perform the following transformation automatically (controllable with a switch):

assert(p -> q);

into

cover(p);
assert(p -> q);

For the situation @danielsn describes one would transform an assert as follows:

assert(p);

into

cover(true);
assert(p);

One of our team just spend I think a full day debugging a vacuous assumption.

@peterschrammel
Copy link
Member

If you are happy to run a separate command then you can achieve that by running CBMC with the --cover assertion option, which checks __CPROVER_assert(false) (non-aborting) instead of assert(p).

@jimgrundy
Copy link
Collaborator

"If you are happy to run a separate command then you can achieve that by running CBMC with the --cover assertion option, which checks __CPROVER_assert(false) (non-aborting) instead of assert(p)."

A separate command could be fine. It doesn't do all I might want (wouldn't have helped our team mate notice which assumption caused the contradiction), but it might do all that this issue is asking for. What do you think @SaswatPadhi and @danielsn, does that address this issue? Can we close this?

@jimgrundy jimgrundy added aws-medium aws Bugs or features of importance to AWS CBMC users and removed aws Bugs or features of importance to AWS CBMC users labels Aug 24, 2021
@jimgrundy
Copy link
Collaborator

Just bringing this to the attention of @remi-delmas-3000

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users RFC Request for comment
Projects
None yet
Development

No branches or pull requests

4 participants