refactor: make concrete values parser use serde trace structs #1601

sanjit-bhat · 2022-08-28T21:40:09Z

Description of changes:

This PR does the following:

It adds more trace properties to the CBMC output parser.
It removes the previous logic in the CBMC output parser to stream the output to a file.
It refactors the concrete values parser. Before, it read the CBMC output file, parsed it, and extracted concrete values. Now, it takes in the parsed CBMC output and extracts concrete values.

Resolved issues:

Resolves #1477.

Testing:

How is this change tested?

No tests were added. The CBMC output parser updates are tested via none of the existing regressions failing. The concrete values extractor is tested via all the concrete playback tests.

Is this a refactor change?

Yes, in some ways; no, in other ways. It is not a refactor change because it adds new fields to the CBMC output parser. It is a refactor change because the higher-level functionality of extracting concrete values still stays the same.

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.

sanjit-bhat · 2022-08-28T21:41:29Z

This should probably be reviewed by at least @celinval and @adpaco-aws.

kani-driver/src/cbmc_output_parser.rs

celinval

This looks much cleaner. Thanks

One thing I noticed is that we are printing a lot of INFO messages on a per harness basis. I don't expect you to change that in this PR, but maybe avoid adding more for now.

kani-driver/src/call_cbmc.rs

kani-driver/src/cbmc_output_parser.rs

celinval · 2022-08-31T20:35:22Z

kani-driver/src/concrete_playback.rs

+        if verification_output.status == VerificationStatus::Success {
+            if !self.args.quiet {
+                println!(
+                    "INFO: The concrete playback feature does not generate unit tests when verification succeeds."


Since we have removed the --harness [h] requirement, I think this info here might be too verbose.

I'm not sure I understand why --harness impacts the verbosity here.

Regardless of whether that's required or not, I see how this could be a bit too verbose. I'm unclear what the correct behavior should be here: 1) print INFO, 2) quietly skip generating a unit test, 3) print ERROR and panic. I think 3) is too much. I assume that if the user inputted this flag, they expect a test case to be generated. So if it's not, 2) is too passive, and we should at least tell them with 1) (the current approach).

What are your thoughts on this?

Well, if I run cargo kani in a project where all proofs succeed (the common case if Kani is integrated in CI), this message would be printed once per proof, so I agree it's a little too verbose. What about printing if --verbose? Another option is to change cargo kani to print a message (only one, at the end) if the user passed the concrete playback flag but all proofs passed.

I would expect only one INFO message at the end if all harnesses succeeded.

Ah, that makes sense. It would be much less verbose when you have a bunch of successful harnesses and only one failing harness.

I updated the code to add a inform_if_no_failed function. This informs the user at the very end if there are no failed harnesses.

kani-driver/src/concrete_playback.rs

sanjit-bhat · 2022-08-31T23:34:08Z

@adpaco-aws do you have any additional feedback? If not, GitHub shows that you're still requesting changes.

sanjit-bhat · 2022-08-31T23:44:05Z

Edit: Looks like this magically fixed itself 🤷🏾‍♂️ . Disregard this.

I'm getting a weird error on just the ubuntu-20.04 regression. No clue what's causing this. I'm unable to re-produce locally when I run cargo doc --workspace --no-deps --exclude std.

2022-08-31T23:36:17.6305038Z  Documenting kani v0.9.0 (/home/runner/work/kani/kani/library/kani)
2022-08-31T23:36:18.1704240Z error: couldn't generate documentation: No such file or directory (os error 2)
2022-08-31T23:36:18.1707362Z   |
2022-08-31T23:36:18.1708384Z   = note: failed to create or modify "/home/runner/work/kani/kani/target/doc/kani/slice/struct.AnySlice.html"
2022-08-31T23:36:18.1709077Z 
2022-08-31T23:36:18.1908332Z error: could not document `kani`
2022-08-31T23:36:18.1908970Z 
2022-08-31T23:36:18.1909470Z Caused by:
2022-08-31T23:36:18.1911731Z   process didn't exit successfully: `rustdoc --edition=2021 --crate-type lib --crate-name kani library/kani/src/lib.rs -o /home/runner/work/kani/kani/target/doc --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat -C metadata=6a4d7a21ecff31cd -L dependency=/home/runner/work/kani/kani/target/debug/deps --extern kani_macros=/home/runner/work/kani/kani/target/debug/deps/libkani_macros-2f09c8ff5b9d853c.so '-Aclippy::expect_fun_call' '-Aclippy::or_fun_call' '-Aclippy::new_without_default' --crate-version 0.9.0` (exit status: 1)
2022-08-31T23:36:18.1913297Z warning: build failed, waiting for other jobs to finish...
2022-08-31T23:36:18.7002243Z ##[error]Process completed with exit code 101.

adpaco-aws

Thanks @sanjit-bhat ! Please wait for @celinval to take another look.

sanjit-bhat · 2022-09-01T16:34:13Z

@celinval can you merge into main once CI runs? I don't have write access anymore.

sanjit-bhat added 6 commits August 26, 2022 16:38

feat: add necessary trace components

32597a9

pushing what I have so far

fee579d

this now works on one example

72d55c8

switch to returning concrete vals

67d4fcd

switch from parse to extract in diagnostics

0b6e397

Merge branch 'main' into serde-parser

6723307

sanjit-bhat requested a review from a team as a code owner August 28, 2022 21:40

sanjit-bhat added 4 commits August 28, 2022 17:53

fix clippy warnings

37ce3a3

refactor some var names

6618e1f

refactor if lets

c151d2c

remove .iter()

2d1a2f5

sanjit-bhat changed the title ~~feat: make concrete values parser use serde trace structs~~ refactor: make concrete values parser use serde trace structs Aug 28, 2022

adpaco-aws suggested changes Aug 29, 2022

View reviewed changes

kani-driver/src/cbmc_output_parser.rs Show resolved Hide resolved

sanjit-bhat added 2 commits August 30, 2022 13:54

print item as we get it from iterator

02d53f6

Merge branch 'main' into serde-parser

535b801

sanjit-bhat requested a review from adpaco-aws August 30, 2022 17:55

Merge branch 'main' into serde-parser

25f972a

celinval reviewed Aug 31, 2022

View reviewed changes

adpaco-aws reviewed Aug 31, 2022

View reviewed changes

kani-driver/src/concrete_playback.rs Show resolved Hide resolved

kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved

kani-driver/src/concrete_playback.rs Show resolved Hide resolved

sanjit-bhat added 6 commits August 31, 2022 18:22

refactor processed_items to use filter_map

eb87b72

move playback_mode extraction to beginning match arm

3d889a5

ensure quiet not on when in concrete playback print mode

96c2954

move result extraction to a separate func

ea2ec6a

use extract_property_class func

74e394c

inform only once if no failed harnesses

f1c16a8

fix kani fmt

a38e035

sanjit-bhat requested a review from celinval August 31, 2022 23:45

sanjit-bhat requested review from adpaco-aws and removed request for celinval August 31, 2022 23:45

adpaco-aws approved these changes Sep 1, 2022

View reviewed changes

celinval approved these changes Sep 1, 2022

View reviewed changes

Merge branch 'main' into serde-parser

35cd6c9

adpaco-aws merged commit 4093b2d into model-checking:main Sep 1, 2022

sanjit-bhat deleted the serde-parser branch September 1, 2022 18:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: make concrete values parser use serde trace structs #1601

refactor: make concrete values parser use serde trace structs #1601

sanjit-bhat commented Aug 28, 2022 •

edited

Loading

sanjit-bhat commented Aug 28, 2022

celinval left a comment

celinval Aug 31, 2022

sanjit-bhat Aug 31, 2022 •

edited

Loading

adpaco-aws Aug 31, 2022

celinval Aug 31, 2022

sanjit-bhat Aug 31, 2022

sanjit-bhat commented Aug 31, 2022

sanjit-bhat commented Aug 31, 2022 •

edited

Loading

adpaco-aws left a comment

sanjit-bhat commented Sep 1, 2022 •

edited

Loading

refactor: make concrete values parser use serde trace structs #1601

refactor: make concrete values parser use serde trace structs #1601

Conversation

sanjit-bhat commented Aug 28, 2022 • edited Loading

Description of changes:

Resolved issues:

Testing:

Checklist

sanjit-bhat commented Aug 28, 2022

celinval left a comment

Choose a reason for hiding this comment

celinval Aug 31, 2022

Choose a reason for hiding this comment

sanjit-bhat Aug 31, 2022 • edited Loading

Choose a reason for hiding this comment

adpaco-aws Aug 31, 2022

Choose a reason for hiding this comment

celinval Aug 31, 2022

Choose a reason for hiding this comment

sanjit-bhat Aug 31, 2022

Choose a reason for hiding this comment

sanjit-bhat commented Aug 31, 2022

sanjit-bhat commented Aug 31, 2022 • edited Loading

adpaco-aws left a comment

Choose a reason for hiding this comment

sanjit-bhat commented Sep 1, 2022 • edited Loading

sanjit-bhat commented Aug 28, 2022 •

edited

Loading

sanjit-bhat Aug 31, 2022 •

edited

Loading

sanjit-bhat commented Aug 31, 2022 •

edited

Loading

sanjit-bhat commented Sep 1, 2022 •

edited

Loading