From 5e1c65d22dfbe18d71524726e84ba1d1f2ecac36 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 4 Sep 2024 10:48:11 -0400 Subject: [PATCH 1/5] change human to pretty and fix kani version --- rfc/src/rfcs/0012-list.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/rfc/src/rfcs/0012-list.md b/rfc/src/rfcs/0012-list.md index fea4a65be7f3..835d14d7c060 100644 --- a/rfc/src/rfcs/0012-list.md +++ b/rfc/src/rfcs/0012-list.md @@ -20,18 +20,18 @@ This feature will not cause any regressions for exisiting users. ## User Experience -Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[human|json]`, which changes the output format. The default is `human`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[pretty|json]`, which changes the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact. -### Human Format +### Pretty Format -The default format, `human`, will print the harnesses and contracts in a project, along with the total counts of each. +The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each. For example: ``` -Kani Version: 0.5.4 +Kani Version: 0.54 Standard Harnesses: - example::verify::check_new @@ -68,15 +68,15 @@ A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `# ### JSON Format -As the name implies, the goal of the `human` output is to be friendly for human readers. If the user wants an output format that's more easily parsed by a script, they can use the `json` option. +If the user wants an output format that's more easily parsed by a script, they can use the `json` option. -The JSON format will contain the same information as the human format, with the addition of file paths and file version. The file version will start at zero and increment whenever we make an update to the format. This way, any users relying on this format for their scripts can realize that changes have occurred and update their logic accordingly. +The JSON format will contain the same information as the pretty format, with the addition of file paths and file version. The file version will start at zero and increment whenever we make an update to the format. This way, any users relying on this format for their scripts can realize that changes have occurred and update their logic accordingly. For example: ```json { - kani-version: 0.5.4, + kani-version: 0.54, file-version: 0, standard-harnesses: [ { From 5c5ca01ed307956920aff806051b41a2b0598291 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 4 Sep 2024 11:19:26 -0400 Subject: [PATCH 2/5] add output schemas --- rfc/src/rfcs/0012-list.md | 44 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/rfc/src/rfcs/0012-list.md b/rfc/src/rfcs/0012-list.md index 835d14d7c060..e908a75bc4ce 100644 --- a/rfc/src/rfcs/0012-list.md +++ b/rfc/src/rfcs/0012-list.md @@ -66,6 +66,26 @@ Totals: A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness. +#### Output Schema +The formal output schema is: +``` +Kani Version: float +Standard Harnesses: List[function] | NONE + - function: string +Contract Harnesses: List[function] | NONE + - function: string +Contracts: Map[function -> contract_harnesses] + - function: string + - contract_harnesses: List[string] | NONE +Totals: Map[string -> int] + - Standard Harnesses: int + - Contract Harnesses: int + - Functions with Contracts: int + - Contracts: int +``` + +All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string. + ### JSON Format If the user wants an output format that's more easily parsed by a script, they can use the `json` option. @@ -132,6 +152,30 @@ For example: } ``` +#### Output Schema +The formal output schema is: +``` +Kani Version: float +File Version: int +Standard Harnesses: List[Object] + - file: string + - harnesses: List[string] +Contract Harnesses: List[Object] + - file: string + - harnesses: List[string] +Contracts: List[Object] + - function: string + - file: string + - harnesses: List[string] +Totals: Object + - standard-harnesses: int + - contract-harnesses: int + - functions-with-contracts: int + - contracts: int +``` + +All sections will be present in the output, regardless of the result. + ## Software Design We will add a new subcommand to `kani-driver`. From 3f48629fe12bcd30ebb862985f68bfa89820717a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 4 Sep 2024 15:02:30 -0400 Subject: [PATCH 3/5] remove output schemas; semantic versioning --- rfc/src/rfcs/0012-list.md | 49 +++++---------------------------------- 1 file changed, 6 insertions(+), 43 deletions(-) diff --git a/rfc/src/rfcs/0012-list.md b/rfc/src/rfcs/0012-list.md index e908a75bc4ce..03e2ef383435 100644 --- a/rfc/src/rfcs/0012-list.md +++ b/rfc/src/rfcs/0012-list.md @@ -31,7 +31,7 @@ The default format, `pretty`, will print the harnesses and contracts in a projec For example: ``` -Kani Version: 0.54 +Kani Rust Verifier 0.54.0 (standalone) Standard Harnesses: - example::verify::check_new @@ -66,38 +66,22 @@ Totals: A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness. -#### Output Schema -The formal output schema is: -``` -Kani Version: float -Standard Harnesses: List[function] | NONE - - function: string -Contract Harnesses: List[function] | NONE - - function: string -Contracts: Map[function -> contract_harnesses] - - function: string - - contract_harnesses: List[string] | NONE -Totals: Map[string -> int] - - Standard Harnesses: int - - Contract Harnesses: int - - Functions with Contracts: int - - Contracts: int -``` - All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string. ### JSON Format If the user wants an output format that's more easily parsed by a script, they can use the `json` option. -The JSON format will contain the same information as the pretty format, with the addition of file paths and file version. The file version will start at zero and increment whenever we make an update to the format. This way, any users relying on this format for their scripts can realize that changes have occurred and update their logic accordingly. +The JSON format will contain the same information as the pretty format, with the addition of file paths and file version. +The file version will use semantic versioning. +This way, any users relying on this format for their scripts can detect when we've released a new major version and update their logic accordingly. For example: ```json { kani-version: 0.54, - file-version: 0, + file-version: 0.1, standard-harnesses: [ { file: /Users/johnsmith/example/kani_standard_proofs.rs @@ -152,29 +136,8 @@ For example: } ``` -#### Output Schema -The formal output schema is: -``` -Kani Version: float -File Version: int -Standard Harnesses: List[Object] - - file: string - - harnesses: List[string] -Contract Harnesses: List[Object] - - file: string - - harnesses: List[string] -Contracts: List[Object] - - function: string - - file: string - - harnesses: List[string] -Totals: Object - - standard-harnesses: int - - contract-harnesses: int - - functions-with-contracts: int - - contracts: int -``` - All sections will be present in the output, regardless of the result. +If there is no result for a given field (e.g., there are no contracts), Kani will output an empty list (or zero for totals). ## Software Design From 5afc8e4a27f3f89cd148a8502e1f008199e29bf2 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 6 Sep 2024 13:40:25 -0400 Subject: [PATCH 4/5] fix version conflict with loop contracts rfc --- rfc/src/SUMMARY.md | 3 ++- rfc/src/rfcs/{0012-list.md => 0013-list.md} | 0 2 files changed, 2 insertions(+), 1 deletion(-) rename rfc/src/rfcs/{0012-list.md => 0013-list.md} (100%) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index c5a7161d0d45..2fb7d0b133cd 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -17,4 +17,5 @@ - [0009-function-contracts](rfcs/0009-function-contracts.md) - [0010-quantifiers](rfcs/0010-quantifiers.md) - [0011-source-coverage](rfcs/0011-source-coverage.md) -- [0012-list](rfcs/0012-list.md) +- [0012-loop-contracts](rfcs/0012-loop-contracts.md) +- [0013-list](rfcs/0013-list.md) diff --git a/rfc/src/rfcs/0012-list.md b/rfc/src/rfcs/0013-list.md similarity index 100% rename from rfc/src/rfcs/0012-list.md rename to rfc/src/rfcs/0013-list.md From 5bf4ceed93b00b556170593612da6b1fe751217d Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 6 Sep 2024 13:47:32 -0400 Subject: [PATCH 5/5] increment rfc version --- rfc/src/rfcs/0013-list.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0013-list.md b/rfc/src/rfcs/0013-list.md index 03e2ef383435..bdbf4681f430 100644 --- a/rfc/src/rfcs/0013-list.md +++ b/rfc/src/rfcs/0013-list.md @@ -2,7 +2,7 @@ - **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612) - **RFC PR:** #3463 - **Status:** Under Review -- **Version:** 0 +- **Version:** 1 -------------------