Skip to content

Commit f12e31b

Browse files
carolynzechcarolynzech
committed
print crate in output tables
1 parent 954b7e6 commit f12e31b

File tree

11 files changed

+376
-371
lines changed

11 files changed

+376
-371
lines changed

‎kani-driver/src/autoharness/mod.rs

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,17 +83,20 @@ fn postprocess_project(
8383
/// Print automatic harness metadata to the terminal.
8484
fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
8585
let mut chosen_table = PrettyTable::new();
86-
chosen_table.set_header(vec!["Selected Function"]);
86+
chosen_table.set_header(vec!["Crate", "Selected Function"]);
8787

8888
let mut skipped_table = PrettyTable::new();
89-
skipped_table.set_header(vec!["Skipped Function", "Reason for Skipping"]);
89+
skipped_table.set_header(vec!["Crate", "Skipped Function", "Reason for Skipping"]);
9090

9191
for md in metadata {
9292
let autoharness_md = md.autoharness_md.unwrap();
93-
chosen_table.add_rows(autoharness_md.chosen.into_iter().map(|func| vec![func]));
93+
chosen_table.add_rows(
94+
autoharness_md.chosen.into_iter().map(|func| vec![md.crate_name.clone(), func]),
95+
);
9496
skipped_table.add_rows(autoharness_md.skipped.into_iter().filter_map(|(func, reason)| {
9597
match reason {
9698
AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => Some(vec![
99+
md.crate_name.clone(),
97100
func,
98101
format!(
99102
"{reason} {}",
@@ -105,7 +108,9 @@ fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
105108
]),
106109
AutoHarnessSkipReason::GenericFn
107110
| AutoHarnessSkipReason::NoBody
108-
| AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]),
111+
| AutoHarnessSkipReason::UserFilter => {
112+
Some(vec![md.crate_name.clone(), func, reason.to_string()])
113+
}
109114
// We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation.
110115
// For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations),
111116
// it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful.
@@ -193,13 +198,15 @@ impl KaniSession {
193198

194199
let mut verified_fns = PrettyTable::new();
195200
verified_fns.set_header(vec![
201+
"Crate",
196202
"Selected Function",
197203
"Kind of Automatic Harness",
198204
"Verification Result",
199205
]);
200206

201207
for success in successes {
202208
verified_fns.add_row(vec![
209+
success.harness.crate_name.clone(),
203210
success.harness.pretty_name.clone(),
204211
success.harness.attributes.kind.to_string(),
205212
success.result.status.to_string(),
@@ -208,6 +215,7 @@ impl KaniSession {
208215

209216
for failure in failures {
210217
verified_fns.add_row(vec![
218+
failure.harness.crate_name.clone(),
211219
failure.harness.pretty_name.clone(),
212220
failure.harness.attributes.kind.to_string(),
213221
failure.result.status.to_string(),

‎tests/script-based-pre/cargo_autoharness_contracts/contracts.expected

Lines changed: 34 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,23 @@
11
Kani generated automatic harnesses for 7 function(s):
2-
+---------------------------------------------+
3-
| Selected Function |
4-
+=============================================+
5-
| should_fail::max |
6-
|---------------------------------------------|
7-
| should_pass::alignment::Alignment |
8-
|---------------------------------------------|
9-
| should_pass::alignment::Alignment::as_usize |
10-
|---------------------------------------------|
11-
| should_pass::div |
12-
|---------------------------------------------|
13-
| should_pass::has_loop_contract |
14-
|---------------------------------------------|
15-
| should_pass::has_recursion_gcd |
16-
|---------------------------------------------|
17-
| should_pass::unchecked_mul |
18-
+---------------------------------------------+
2+
+-----------------------------+---------------------------------------------+
3+
| Crate | Selected Function |
4+
+===========================================================================+
5+
| cargo_autoharness_contracts | should_fail::max |
6+
|-----------------------------+---------------------------------------------|
7+
| cargo_autoharness_contracts | should_pass::alignment::Alignment |
8+
|-----------------------------+---------------------------------------------|
9+
| cargo_autoharness_contracts | should_pass::alignment::Alignment::as_usize |
10+
|-----------------------------+---------------------------------------------|
11+
| cargo_autoharness_contracts | should_pass::div |
12+
|-----------------------------+---------------------------------------------|
13+
| cargo_autoharness_contracts | should_pass::has_loop_contract |
14+
|-----------------------------+---------------------------------------------|
15+
| cargo_autoharness_contracts | should_pass::has_recursion_gcd |
16+
|-----------------------------+---------------------------------------------|
17+
| cargo_autoharness_contracts | should_pass::unchecked_mul |
18+
+-----------------------------+---------------------------------------------+
1919

2020
Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
21-
2221
Autoharness: Checking function should_fail::max's contract against all possible inputs...
2322
assertion\
2423
- Status: FAILURE\
@@ -55,23 +54,23 @@ Manual Harness Summary:
5554
No proof harnesses (functions with #[kani::proof]) were found to verify.
5655

5756
Autoharness Summary:
58-
+---------------------------------------------+-----------------------------+---------------------+
59-
| Selected Function | Kind of Automatic Harness | Verification Result |
60-
+=================================================================================================+
61-
| should_pass::alignment::Alignment | #[kani::proof] | Success |
62-
|---------------------------------------------+-----------------------------+---------------------|
63-
| should_pass::alignment::Alignment::as_usize | #[kani::proof_for_contract] | Success |
64-
|---------------------------------------------+-----------------------------+---------------------|
65-
| should_pass::div | #[kani::proof_for_contract] | Success |
66-
|---------------------------------------------+-----------------------------+---------------------|
67-
| should_pass::has_loop_contract | #[kani::proof] | Success |
68-
|---------------------------------------------+-----------------------------+---------------------|
69-
| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success |
70-
|---------------------------------------------+-----------------------------+---------------------|
71-
| should_pass::unchecked_mul | #[kani::proof_for_contract] | Success |
72-
|---------------------------------------------+-----------------------------+---------------------|
73-
| should_fail::max | #[kani::proof_for_contract] | Failure |
74-
+---------------------------------------------+-----------------------------+---------------------+
57+
+-----------------------------+---------------------------------------------+-----------------------------+---------------------+
58+
| Crate | Selected Function | Kind of Automatic Harness | Verification Result |
59+
+===============================================================================================================================+
60+
| cargo_autoharness_contracts | should_pass::alignment::Alignment | #[kani::proof] | Success |
61+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
62+
| cargo_autoharness_contracts | should_pass::alignment::Alignment::as_usize | #[kani::proof_for_contract] | Success |
63+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
64+
| cargo_autoharness_contracts | should_pass::div | #[kani::proof_for_contract] | Success |
65+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
66+
| cargo_autoharness_contracts | should_pass::has_loop_contract | #[kani::proof] | Success |
67+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
68+
| cargo_autoharness_contracts | should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success |
69+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
70+
| cargo_autoharness_contracts | should_pass::unchecked_mul | #[kani::proof_for_contract] | Success |
71+
|-----------------------------+---------------------------------------------+-----------------------------+---------------------|
72+
| cargo_autoharness_contracts | should_fail::max | #[kani::proof_for_contract] | Failure |
73+
+-----------------------------+---------------------------------------------+-----------------------------+---------------------+
7574
Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20.
7675
If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract).
7776
Complete - 6 successfully verified functions, 1 failures, 7 total.

‎tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
Kani generated automatic harnesses for 1 function(s):
2-
+-------------------+
3-
| Selected Function |
4-
+===================+
5-
| yes_harness |
6-
+-------------------+
2+
+--------------------------------+-------------------+
3+
| Crate | Selected Function |
4+
+====================================================+
5+
| cargo_autoharness_dependencies | yes_harness |
6+
+--------------------------------+-------------------+
77

88
Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
99

@@ -14,9 +14,9 @@ Manual Harness Summary:
1414
No proof harnesses (functions with #[kani::proof]) were found to verify.
1515

1616
Autoharness Summary:
17-
+-------------------+---------------------------+---------------------+
18-
| Selected Function | Kind of Automatic Harness | Verification Result |
19-
+=====================================================================+
20-
| yes_harness | #[kani::proof] | Success |
21-
+-------------------+---------------------------+---------------------+
17+
+--------------------------------+-------------------+---------------------------+---------------------+
18+
| Crate | Selected Function | Kind of Automatic Harness | Verification Result |
19+
+======================================================================================================+
20+
| cargo_autoharness_dependencies | yes_harness | #[kani::proof] | Success |
21+
+--------------------------------+-------------------+---------------------------+---------------------+
2222
Complete - 1 successfully verified functions, 0 failures, 1 total.

‎tests/script-based-pre/cargo_autoharness_exclude/exclude.expected

Lines changed: 17 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,29 @@
11
Kani generated automatic harnesses for 1 function(s):
2-
+-------------------+
3-
| Selected Function |
4-
+===================+
5-
| include::simple |
6-
+-------------------+
2+
+---------------------------+-------------------+
3+
| Crate | Selected Function |
4+
+===============================================+
5+
| cargo_autoharness_include | include::simple |
6+
+---------------------------+-------------------+
77

88
Kani did not generate automatic harnesses for 2 function(s).
99
If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
10-
+------------------+--------------------------------+
11-
| Skipped Function | Reason for Skipping |
12-
+===================================================+
13-
| excluded::simple | Did not match provided filters |
14-
|------------------+--------------------------------|
15-
| include::generic | Generic Function |
16-
+------------------+--------------------------------+
17-
10+
+---------------------------+------------------+--------------------------------+
11+
| Crate | Skipped Function | Reason for Skipping |
12+
+===============================================================================+
13+
| cargo_autoharness_include | excluded::simple | Did not match provided filters |
14+
|---------------------------+------------------+--------------------------------|
15+
| cargo_autoharness_include | include::generic | Generic Function |
16+
+---------------------------+------------------+--------------------------------+
1817
Autoharness: Checking function include::simple against all possible inputs...
1918
VERIFICATION:- SUCCESSFUL
2019

2120
Manual Harness Summary:
2221
No proof harnesses (functions with #[kani::proof]) were found to verify.
2322

2423
Autoharness Summary:
25-
+-------------------+---------------------------+---------------------+
26-
| Selected Function | Kind of Automatic Harness | Verification Result |
27-
+=====================================================================+
28-
| include::simple | #[kani::proof] | Success |
29-
+-------------------+---------------------------+---------------------+
24+
+---------------------------+-------------------+---------------------------+---------------------+
25+
| Crate | Selected Function | Kind of Automatic Harness | Verification Result |
26+
+=================================================================================================+
27+
| cargo_autoharness_include | include::simple | #[kani::proof] | Success |
28+
+---------------------------+-------------------+---------------------------+---------------------+
3029
Complete - 1 successfully verified functions, 0 failures, 1 total.

0 commit comments

Comments
 (0)