update rfc

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -643,9 +643,9 @@ impl GotoCodegenResults {
             proof_harnesses: proofs,
             unsupported_features,
             test_harnesses: tests,
-            // We don't collect the functions under contract because the logic assumes that, if contract attributes are present,
-            // they are well-formed, which Kani only checks if we run verification or the list subcommand (i.e., for ReachabilityType::Harnesses).
-            // In those cases, we use the CodegenUnits object to generate the metadata instead of this function.
+            // We don't collect the contracts metadata because the FunctionWithContractPass
+            // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns,
+            // which are the two ReachabilityTypes under which the compiler calls this function.
             contracted_functions: vec![],
         }
     }

rfc/src/rfcs/0013-list.md

@@ -31,6 +31,7 @@ This subcommand does not fail. In the case that it does not find any harnesses o
 The default format, `pretty`, prints a "Contracts" table and a "Standard Harnesses" list.
 Each row of the "Contracts" table consists of a function, the number of contracts it has, and its contract harnesses.
 A function is listed if it has contracts or it is the target of contract harness(es).
+The results are printed in lexographic order.
 
 For example:
 
@@ -59,8 +60,8 @@ or is the target of a contract harness (#[kani::proof_for_contract]).
 |-------|-------------------------|----------------|-------------------------------------|
 
 Standard Harnesses (#[kani::proof]):
-1. example::verify::check_new
-2. example::verify::check_modify
+1. example::verify::check_modify
+2. example::verify::check_new
 ```
 
 All sections will be present in the output, regardless of the result.
@@ -166,25 +167,28 @@ pub struct ContractedFunction {
     pub harnesses: Vec<String>,
 }
 ```
-We extend `KaniMetadata` and `CodegenUnits` with new `contracted_functions: Vec<ContractedFunction>` fields.
+We extend `KaniMetadata` with a new `contracted_functions: Vec<ContractedFunction>` field.
+
+### Driver Changes
+We add a new subcommand to `kani-driver`.
+This subcommand exists for both `cargo kani` and `kani` invocations.
+The driver constructs a `Project` representing the input.
+(For `kani` invocations, the driver either constructs a `standalone_project` or a `std_project` depending on whether the use passed the `--std` flag).
+The `Project` is populated with `metadata: Vec<KaniMetadata>` from `kani-compiler`.
+We iterate through this metadata to print a table with the results or output a `kani-list.json` file, depending on the user-specified `format` argument.
 
 ### Compiler Changes
 
-This subcommand is concerned with two fields of `KaniMetadata`: `proof_harnesses` and `contracted_functions`.
-In `codegen_crate()`, `kani-compiler` will check if we are running the list subcommand, and, if so, it constructs a new `CodegenUnits` object.
-The `CodegenUnits` constructor handles initializing the `proof_harnesses` field for us.
-We add new functionality to populate the `contracted_functions` field, which we explain in two parts:
+In `codegen_crate`, we update the generation of `KaniMetadata` to include the new `contracted_functions` field.
+We populate this field in two parts:
 
 #### Part 1: Map Functions to Harnesses
 
-First, we iterate through each local item in the crate and construct a map of functions to contract harnesses.
-The keys in this map are functions that either 1) have contracts or 2) are targets of contract harnesses.
-These are not necessarily identical sets; functions under contract may not have harnesses, and targets of contract harnesses may not have contracts.
-
-Observe that we iterate through each local item in the crate (`stable_mir::CrateItem`), not each local *instance* (`stable_mir::Instance`).
+First, we iterate through each local item in the crate and construct a map of functions under contract to their contract harnesses.
+We iterate through each local item in the crate (`stable_mir::CrateItem`), not each local *instance* (`stable_mir::Instance`).
 This is so that we can include generic functions with contracts in the output.
 `Instances` are monomorphized.
-When we're verifying a contract harness, this monomorphization assumption is fine;  if the harness calls the function under contract, a monomorphized version of the function must exist.
+When we're verifying a contract harness, this monomorphization assumption is fine; if the harness calls the function under contract, a monomorphized version of the function must exist.
 However, if we are just trying to list metadata, we cannot rely on this assumption that the function under contract gets called, and therefore cannot assume that a monomorphized version of the generic function exists.
 For example, imagine running `kani list` on a file with only these contents:
 ```rust
@@ -195,8 +199,6 @@ Kani should be able to find `foo` and report it has a contract,
 but we cannot construct a `stable_mir::Instance` from `foo` because it requires monomorphization.
 
 #### Part 2: Count Contracts
-For each function in the map from Part 1, we count its contracts, then construct a `ContractedFunction` object for it.
-
 Since we are counting the contracts at the MIR level, we work with the expanded version of the contract attribute macros.
 We locate the body of the `kanitool::checked_with` closure, then count the number of `kani::assume()` and `kani::assert()` calls.
 For example, given the following code (example taken from `kani_macros` contracts documentation):
@@ -234,16 +236,7 @@ let mut __kani_check_div =
 Observe that there is one `kani::assume()` call for the `requires` contract and one `kani::assert()`
 call for the `ensures` contract, so we can obtain the total number of contracts by counting these calls.
 
-Once these parts are complete, `CodegenUnits` contains all of the required metadata.
-We use an existing method (`CodegenUnits::write_metadata`) to write this metadata to a file.
-
-### Driver Changes
-We add a new subcommand to `kani-driver`.
-This subcommand exists for both `cargo kani` and `kani` invocations.
-The driver constructs a `Project` representing the input.
-(For `kani` invocations, the driver either constructs a `standalone_project` or a `std_project` depending on whether the use passed the `--std` flag).
-The `Project` is populated with `metadata: Vec<KaniMetadata>` from `kani-compiler`.
-We iterate through this metadata to print a table with the results or output a `kani-list.json` file, depending on the user-specified `format` argument.
+Once these parts are complete, we generate a `ContractedFunction` object for each function under contract and populate it with the data gathered above.
 
 ## Rationale and alternatives
 
@@ -300,10 +293,16 @@ However, users could still be confused by this choice because Kani allows users
 (If Kani detects no contract-related attributes at all, it errors.)
 A user may be confused as to why the list subcommand reports zero contracts when they are running a `proof_for_contract` harness without errors.
 
+### Compiler - Build Cache
+The compiler is unaware of the list subcommand; i.e., there are no special arguments to indicate to the compiler that the list subcommand is running.
+If the user only wants to invoke the list subcommand, this design wastes work, since Kani generates unnecessary GOTO files.
+However, it also allows the compiler to take advantage of the build cache.
+If a user verifies their code and then invokes `list` (or vice versa),
+the compiler will be invoked with the same arguments both times, which means that it can just use the cached targets from the first compiler invocation.
 
 ## Open questions
 
-1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts, the number of `requires`, `ensures`, or `modifies` contracts, or the locations of the contracts.
+1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts or the number of `requires` and `ensures` contracts.
 2. More generally, we could introduce additional options that collect information about other Kani attributes (e.g., stubs). The default would be to leave them out, but this way a user could get more verbose output if they so choose.
 3. Do we want to add a filtering option? For instance, `--harnesses <pattern>` and `--contracts <pattern>`, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. (If we do this work, we could use it to improve our `--harness` [pattern handling for verification](https://github.com/model-checking/kani/blob/main/kani-driver/src/metadata.rs#L187-L189)).