Improve --jobs UI (#3790)

Improve the documentation for the `--jobs` option, change it to use
`hide_short_help` like other unstable options, and print the current
thread number so that users can match the harness to its output.

Example:
```rust

#[kani::modifies(x)]
#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
fn zero(x: &mut [u8]) {
    x.fill(0)
}

#[kani::proof_for_contract(zero)]
fn harness() {
    let mut x = [kani::any(), kani::any(), kani::any()];
    zero(&mut x);
}

#[kani::proof]
fn harness_2() {
    assert!(true);
}

#[kani::proof]
fn harness_3() {
    assert!(false);
}
```

```
cargo kani -j --enable-unstable --output-format=terse -Z function-contracts
Kani Rust Verifier 0.57.0 (cargo plugin)
warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s
Thread 4: Checking harness harness_2...
Thread 2: Checking harness harness_3...
Thread 4: 
VERIFICATION RESULT:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.0137195s

Thread 2: 
VERIFICATION RESULT:
 ** 1 of 1 failed
Failed Checks: assertion failed: false
 File: "src/lib.rs", line 26, in harness_3

VERIFICATION:- FAILED
Verification Time: 0.012914542s

Thread 0: Checking harness harness...
Thread 0: 
VERIFICATION RESULT:
 ** 0 of 217 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 18.47224s

Summary:
Verification failed for - harness_3
Complete - 2 successfully verified harnesses, 1 failures, 3 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>

Author: carolynzech

kani-driver/src/args/mod.rs

@@ -257,8 +257,11 @@ pub struct VerificationArgs {
     // consumes everything
     pub cbmc_args: Vec<OsString>,
 
-    /// Number of parallel jobs, defaults to 1
-    #[arg(short, long, hide = true, requires("enable_unstable"))]
+    /// Number of threads to spawn to verify harnesses in parallel.
+    /// Omit the flag entirely to run sequentially (i.e. one thread).
+    /// Pass -j to run with the thread pool's default number of threads.
+    /// Pass -j <N> to specify N threads.
+    #[arg(short, long, hide_short_help = true, requires("enable_unstable"))]
     pub jobs: Option<Option<usize>>,
 
     /// Enable extra pointer checks such as invalid pointers in relation operations and pointer

kani-driver/src/harness_runner.rs

@@ -103,30 +103,48 @@ impl<'pr> HarnessRunner<'_, 'pr> {
 }
 
 impl KaniSession {
-    fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+    fn process_output(
+        &self,
+        result: &VerificationResult,
+        harness: &HarnessMetadata,
+        thread_index: usize,
+    ) {
         if self.should_print_output() {
             if self.args.output_into_files {
-                self.write_output_to_file(result, harness);
+                self.write_output_to_file(result, harness, thread_index);
             }
 
             let output = result.render(&self.args.output_format, harness.attributes.should_panic);
-            println!("{}", output);
+            if rayon::current_num_threads() > 1 {
+                println!("Thread {thread_index}: {output}");
+            } else {
+                println!("{output}");
+            }
         }
     }
 
     fn should_print_output(&self) -> bool {
         !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
     }
 
-    fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+    fn write_output_to_file(
+        &self,
+        result: &VerificationResult,
+        harness: &HarnessMetadata,
+        thread_index: usize,
+    ) {
         let target_dir = self.result_output_dir().unwrap();
         let file_name = target_dir.join(harness.pretty_name.clone());
         let path = Path::new(&file_name);
         let prefix = path.parent().unwrap();
 
         std::fs::create_dir_all(prefix).unwrap();
         let mut file = File::create(&file_name).unwrap();
-        let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+        let mut file_output =
+            result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+        if rayon::current_num_threads() > 1 {
+            file_output = format!("Thread {thread_index}:\n{file_output}");
+        }
 
         if let Err(e) = writeln!(file, "{}", file_output) {
             eprintln!(
@@ -148,13 +166,18 @@ impl KaniSession {
         binary: &Path,
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
+        let thread_index = rayon::current_thread_index().unwrap_or_default();
         if !self.args.common_args.quiet {
-            println!("Checking harness {}...", harness.pretty_name);
+            if rayon::current_num_threads() > 1 {
+                println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name);
+            } else {
+                println!("Checking harness {}...", harness.pretty_name);
+            }
         }
 
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-        self.process_output(&result, harness);
+        self.process_output(&result, harness, thread_index);
         self.gen_and_add_concrete_playback(harness, &mut result)?;
         Ok(result)
     }