Gracefully exit from kani-driver process

[celinval]

Description of changes:

When an error that was properly handled ocurrs in kani-driver we now gracefully exit and return ExitStatus::FAILURE.

We still print all error context to keep a similar experiece to what it was before. However, this will no longer include the backtrace if users set RUST_BACKTRACE=1.

The backtrace will still be included if you enable the debug logs and also enable the backtrace. I.e.:

export RUST_BACKTRACE=1
export KANI_LOG=kani_driver=debug
cargo kani

Resolved issues:

Resolves #2064

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

• How is this change tested?

• Is this a refactor change?

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tedinski]

This is at least not the fix I'd do for #2064. I think we should detect when RUST_BACKTRACE is set but RUST_LIB_BACKTRACE is not, and then default it the other way.

You can see documentation on this environment variable in: https://docs.rs/anyhow/latest/anyhow/

[celinval]

It makes sense. What you are suggesting is already the current behavior though. The standard library checks those variables before generating the backtrace.

That said, it doesn't fix the problem at hand. So I think the question here is whether #2064 should be fixed in the first place. @zhassan-aws ?

[tedinski]

I think we should fix it. The behavior I was suggesting is this:

If you want only panics to have backtraces, set RUST_BACKTRACE=1 and RUST_LIB_BACKTRACE=0.

So to fix this in kani-driver, if the former is set, and the latter is not, then we explicitly set the latter to 0.

[celinval]

Ah, I see what you are saying, you think we should change the behavior only when RUST_BACKTRACE=1 and RUST_LIB_BACKTRACE isn't set, right? Why is that? Do you think people just aren't used to the second variable?

This PR mimics cargo and rustc behavior, which I think makes more sense. No matter the value of RUST_BACKTRACE and RUST_LIB_BACKTRACE, these two tools won't print the stack trace of an error that is due to a user error (like compilation error). Note that today passing the wrong argument will not print the error stack, no matter the values of these two variables.

No matter which approach we take, we should consider improving the driver error handling to make a distinction between internal tool error and user error, so this can be handled in a better way.

[zhassan-aws]

So I think the question here is whether #2064 should be fixed in the first place. @zhassan-aws ?

I think it should be fixed, because a backtrace gives an impression that something is broken in the tool.

[zhassan-aws]

A few minor comments. Otherwise, looks good (if @tedinski is OK with the changes).

[zhassan-aws]

"consider create" -> "create" or "consider creating"

[tedinski]

Do you think people just aren't used to the second variable?

Pretty much.

Also, just want to make it clear: I don't object to this change.

[celinval]

Do you think people just aren't used to the second variable?

Yeah, tbh, I am not a big fan of the design they came up with these two variables. It's not very intuitive.

Pretty much.

Also, just want to make it clear: I don't object to this change.

Sounds good. Thanks!