Store failure reason into assess metadata #2166
Conversation
|
I still need to implement when and how to disable the text decoration while invoking cargo. Redirecting the output causes a bunch of escape characters to leak. |
This will allow us to retrieve crash information from Kani driver once we merge #2166.
For cases where we redirect the output, we shouldn't print color messages.
We have to manually trip the ansi escape formatting.
celinval
force-pushed
the
issue-2165-assess-error
branch
from
97155e4 to
e572b1f
Compare
kani-driver/src/assess/metadata.rs
Outdated
| @@ -27,6 +27,12 @@ use super::AssessArgs; | |||
| /// This is not a stable interface. | |||
| #[derive(Serialize, Deserialize)] | |||
| pub struct AssessMetadata { | |||
| // TODO: The assess cache should check this field to know whether the version should change. | |||
There was a problem hiding this comment.
I'm not clear on this comment. What is "assess cache"? What does "whether the version should change" mean?
There was a problem hiding this comment.
Assess scan has an --existing-only option that won't rerun assess but only parse existing metadata files. What I'm trying to state here, is that this option shouldn't reuse metadata files that were generated by older versions of Kani, since the results might no longer hold.
I can rewrite this comment to make it clearer.
| @@ -1,3 +1 @@ | |||
| error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**). | |||
| error: could not compile `crate_with_global_asm` due to previous error | |||
There was a problem hiding this comment.
This is a useful line that points out the name of the crate that had an error. Is the crate name available elsewhere?
There was a problem hiding this comment.
There seems to be a bug on Cargo that it counts an extra error if you use --message-format=json. Basically, the compiler prints an error message saying how many errors were found. In regular mode, cargo excludes this message, but when emitting json, cargo skips that, and counts it as an extra error.
I.e., for this test to pass, I have three options:
- Remove the check from here.
- Update the error count:
error: could not compile `crate_with_global_asm` due to 2 previous errors
- Update the expected message to not include the number of errors:
error: could not compile `crate_with_global_asm`
I picked the first since it was the simplest, but I can change. Any preference?
There was a problem hiding this comment.
I see. In that case, the option you went with is fine. I just wanted to make sure the message still gets printed.
There was a problem hiding this comment.
FYI, I updated this one expected test to have the message that includes the name of the crate and the counter as a sanity check, but I didn't bother adding to all the other tests, because one would hope that Cargo will update that counter eventually. In that case, we would only need to update one test.
The console crate already has the strip function we need
Conflicts:
tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected
Description of changes:
We now store Kani's version and the failure reason (if there's one) into the assess metadata. For now, we still need to manually parse this information, but this moves us closer to #2058 and #2165.
In order to collect more details about the compilation errors, we now inspect the cargo diagnostic messages.
Resolved issues:
N/A
Related RFC:
Optional #ISSUE-NUMBER.
Call-outs:
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.