Run all proof harnesses by default #962

tedinski · 2022-03-18T22:31:58Z

Description of changes:

Hide (but technically keep) --function in favor of --harness which must be #[kani::proof]. Updated all documentation accordingly.
cargo-kani now parses and merges kani-metadata.json files, to support looking up proof harnesses.
- Quick note: I changed dry-run output to report *.symtab.json instead of dry-run.symtab.json
(Minor: I uh, altered --gen-c to print where the file was generated.)
crate-type=lib is now unconditional and we (by documentation) require #[kani::proof]. Technically, --function can still specify anything but you need some method of ensuring the function gets code-gen'd.
THE MEAT: cargo-kani and kani now default to running all proof harnesses found.
- Switch to just one with --harness
- Behavior is to run each one one after another until either one fails (and we stop) or all suceed and we print "All harnesses successfully verified."
Added a new mode for cargo-kani mode tests. We can now add a plain expected file instead of function.expected and this will run cargo-kani without any --function flags.

phew

Resolved issues:

Resolves #464
Resolves #691

Contributes to #477 and #701

Call-outs:

Testing:

How is this change tested? 2 new tests cases, fairly basic. Plus existing whole test suite.
Is this a refactor change? no

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 · 2022-03-18T22:48:34Z

oh, doh. I need to adapt bookrunner to work with needing #[kani::proof] annotations now. Welp, monday.

celinval

Sweet! Mostly minor comments. I do think we should change the behaviour to run all harnesses before failing though.

src/cargo-kani/src/args.rs

src/cargo-kani/src/call_goto_instrument.rs

src/cargo-kani/src/main.rs

celinval · 2022-03-19T01:40:34Z

src/cargo-kani/src/main.rs

-            drop(ctx);
-            std::process::exit(1);
+
+    let metadata = ctx.collect_kani_metadata(&[outputs.metadata])?;


Can we move the duplicated code to a separate function?

I've tried to avoid having any functions that are specific to kani or cargo-kani (except these two of course) because I think these are generally design errors. You'll notice that there are several small variations between these two functions, and trying to abstract those differences out will generally make the code worse, not better.

A small amount of not-really-duplication is better than trying to create a function with a half dozen parameters that only gets called 2 ways. The old python was full of that, and it's just code that only gets worse as people add to it.

That said, I think there IS a little bit I can factor out here, I just need to fix how we do report generation first since I actually broke that...

That makes sense. Thanks

src/cargo-kani/src/metadata.rs

tests/expected/multiple-harnesses/expected

tools/compiletest/src/runtest.rs

tedinski · 2022-03-21T22:24:50Z

tools/compiletest/src/runtest.rs

+        match self.props.kani_panic_step {
+            Some(KaniFailStep::Check) => {
+                self.check();
+            }
+            Some(KaniFailStep::Codegen) => {
+                self.codegen();
+            }
+            Some(KaniFailStep::Verify) | None => {
+                self.verify();
+            }


This change is necessary since we now may run kani-compiler from kani with different flags that compiletest wasn't picking up. This change means we avoid doing redundant work, and these differences only matter for things that expected to fail to check or codegen (which wasn't any existing tests, thankfully)

Just thought I'd note this in the review here, since it got mixed up with a bunch of other changes to get tests working again after switching to using --harness

…parate directories

tedinski · 2022-03-23T19:28:11Z

This should be ready to review again.

It now runs all proof harnesses even if one fails, and prints a summary at the end:

Complete - 2 successfully verified harnesses, 0 failures, 2 total.

Hmm. Possibly I should print which harnesses failed, so you don't have to scroll up to search for them... Let me know your thoughts.

We now also produce all reports with --visualize which required creating multiple directories, one for each harness:

$ cargo kani --visualize
$ ls -l target/
total 24
-rw-rw-r-- 1 ubuntu ubuntu  177 Mar 23 19:13 CACHEDIR.TAG
drwxrwxr-x 7 ubuntu ubuntu 4096 Mar 23 19:13 debug
drwxrwxr-x 4 ubuntu ubuntu 4096 Mar 23 19:22 report-proofs::check_trivial
drwxrwxr-x 4 ubuntu ubuntu 4096 Mar 23 19:22 report-proofs::failed_check
drwxrwxr-x 4 ubuntu ubuntu 4096 Mar 23 19:22 report-proofs::third_harness
drwxrwxr-x 3 ubuntu ubuntu 4096 Mar 23 19:13 x86_64-unknown-linux-gnu

I notice that the "pretty name" of function is fully qualified. I'm thinking about fixing that (advice?) but if we don't use the fully qualified names, there might be name collisions. (At the very least, colon isn't legal in filenames on windows, so we have to do something...)

celinval · 2022-03-23T21:54:44Z

The way proof is implemented today by using no_mangle guarantees that you can't have name collision between harnesses. I believe if that happens, the compilation fails.

That said, can you replace the :: by .?

zhassan-aws

This is a huge step forward! Awesome work, @tedinski!

Just had a few minor comments.

docs/src/kani-single-file.md

zhassan-aws · 2022-03-25T00:49:43Z

src/cargo-kani/src/main.rs

+                println!("Verification failed for - {}", harness.pretty_name);
+            }
+
+            println!(


Should we still print this summary line when self.args.quiet is true? cargo test prints the summary even with --quiet.

Maybe. In my experience, there is a contingent of "if I say quiet, actually print nothing, just give me a return value" software out there. But... maybe this isn't one that should be that way.

cargo test is a compelling point of comparison. Possibly we should do some output comparisons and decide differently later?

src/cargo-kani/src/metadata.rs

zhassan-aws · 2022-03-25T01:14:15Z

tests/smack/basic/arith.rs

@@ -1,8 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// @expect verified


Is removing the SMACK annotations necessary? They're probably meant for the SMACK testing tool, but they may be useful for us to compare results.

No: I needed to quickly audit those files to fix a few things and I removed what I thought was unnecessary. I don't see how these would ever get used...

tools/bookrunner/src/util.rs

Zyad took over

* Introduce --harness and parse kani-metadata. * run all proof harnesses * enable function-less 'expected' tests for cargo-kani in compiletest * Only mention --harness not --function in docs * use --harness instead of --function in tests, mostly. * Run all harnesses, even if one fails. Also generate all reports in separate directories * Output reports (and harness) with - not :: in file names * Print all failed harnesses in a final summary * Make harness search robust against possible future name collisions

tedinski added 7 commits March 18, 2022 22:11

Introduce --harness and parse kani-metadata.

ea78c8a

run all proof harnesses

ce389be

enable function-less 'expected' tests for cargo-kani in compiletest

38da8d5

add basic tests for proof harnesses for kani and cargo-kani

fe0ea16

Only mention --harness not --function in docs

2e12924

single file? always crate-type=lib

459f7d8

add missing proof attribute to two tests

d7d3f54

tedinski requested a review from a team as a code owner March 18, 2022 22:31

celinval previously requested changes Mar 19, 2022

View reviewed changes

tedinski added 7 commits March 21, 2022 14:35

minor fixes from PR comments

6d9aabb

Merge remote-tracking branch 'origin/main' into proof-harnesses

6200173

Ok, crate-type=bin if --function main

31aab5c

bug fix: provide arguments in correct order to account for --cbmc-args

fba6da4

Merge remote-tracking branch 'origin/main' into proof-harnesses

2b3e473

a ton of test updates, sorry

628e4f0

use --harness instead of --function in tests, mostly.

3403c13

tedinski commented Mar 21, 2022

View reviewed changes

tedinski added 2 commits March 22, 2022 21:53

Run all harnesses, even if one fails. Also generate all reports in se…

c57fae9

…parate directories

merge origin/main

e783a7e

Merge remote-tracking branch 'origin/main' into proof-harnesses

b00b7bf

tedinski added 5 commits March 24, 2022 19:23

merge origin/main, resolve conflicts

e3791ca

Merge remote-tracking branch 'origin/main' into proof-harnesses

afc8f92

Output reports (and harness) with - not :: in file names

45ea3ec

Print all failed harnesses in a final summary

ce1ee44

minor docs tweak to try to trigger github actions

d97ea46

zhassan-aws approved these changes Mar 25, 2022

View reviewed changes

adpaco-aws mentioned this pull request Mar 25, 2022

Documentation: Remaining tasks #970

Closed

6 tasks

tedinski added 2 commits March 25, 2022 15:47

fix typos, comments

7fc1b4d

Make harness search robust against possible future name collisions

f47cdd6

tedinski merged commit 70e5a39 into model-checking:main Mar 25, 2022

tedinski deleted the proof-harnesses branch March 25, 2022 19:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Run all proof harnesses by default #962

Run all proof harnesses by default #962

tedinski commented Mar 18, 2022 •

edited

Loading

tedinski commented Mar 18, 2022

celinval left a comment

celinval Mar 19, 2022

tedinski Mar 21, 2022

celinval Mar 22, 2022

tedinski Mar 21, 2022

tedinski commented Mar 23, 2022

celinval commented Mar 23, 2022

zhassan-aws left a comment

zhassan-aws Mar 25, 2022

tedinski Mar 25, 2022

zhassan-aws Mar 25, 2022

zhassan-aws Mar 25, 2022

tedinski Mar 25, 2022

Run all proof harnesses by default #962

Run all proof harnesses by default #962

Conversation

tedinski commented Mar 18, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

tedinski commented Mar 18, 2022

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tedinski commented Mar 23, 2022

celinval commented Mar 23, 2022

zhassan-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tedinski commented Mar 18, 2022 •

edited

Loading