Emit SARIF output for Code Scanning (#4547)

Adds a new --sarif PATH option to write a SARIF v2.1.0 report for
verification results.

- Failed properties are reported as error; undetermined/unknown
properties as warning
- CBMC timeout/OOM is reported as error
- Artifact paths are made repo-relative when possible
- Docs and tests included

Example:
  cargo kani --sarif kani.sarif

GitHub Actions upload:
  - uses: github/codeql-action/upload-sarif@v3
    with:
      sarif_file: kani.sarif

Co-authored-by: KAMIYO <kamiyo-ai@users.noreply.github.com>

Author: mizuki0x

docs/src/install-github-ci.md

@@ -41,9 +41,28 @@ The action takes the following optional parameters:
   See `cargo kani --help` for a full list of options.
   Useful options include:
   - `--output-format=terse` to generate terse output.
+  - `--sarif <path>` to write a SARIF report that can be uploaded to GitHub Code Scanning.
   - `--tests` to run on proofs inside the `test` module (needed for running Bolero).
   - `--workspace` to run on all crates within your repository.
 
+### Uploading SARIF to GitHub Code Scanning
+
+If you run Kani with `--sarif`, you can upload the report so results show up as Code Scanning alerts.
+
+```yaml
+      - name: 'Run Kani on your code.'
+        uses: model-checking/kani-github-action@v<MAJOR>.<MINOR>
+        with:
+          args: --sarif kani.sarif
+
+      - name: 'Upload SARIF'
+        uses: github/codeql-action/upload-sarif@v3
+        with:
+          sarif_file: kani.sarif
+```
+
+Your workflow must grant `security-events: write` permissions to upload SARIF results.
+
 ## FAQ
 - **Kani takes too long for my CI**: Try running Kani on a
   [schedule](https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule)

docs/src/verification-results.md

@@ -159,3 +159,19 @@ SUMMARY:
 
 VERIFICATION:- SUCCESSFUL
 ```
+
+## SARIF output
+
+Kani can emit SARIF (Static Analysis Results Interchange Format) for integration with tools such as GitHub Code Scanning.
+
+Generate a SARIF report:
+```bash
+cargo kani --sarif kani.sarif
+```
+
+In GitHub Actions, upload the SARIF file:
+```yaml
+- uses: github/codeql-action/upload-sarif@v3
+  with:
+    sarif_file: kani.sarif
+```

kani-driver/src/args/mod.rs

@@ -351,6 +351,10 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub run_sanity_checks: bool,
 
+    /// Write SARIF output (Static Analysis Results Interchange Format) to the given path.
+    #[arg(long, value_name = "PATH")]
+    pub sarif: Option<PathBuf>,
+
     /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
     /// If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL.
     #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
@@ -767,13 +771,25 @@ impl ValidateArgs for VerificationArgs {
                 --output-format=old.",
                 ));
             }
+            if self.sarif.is_some() && self.output_format == OutputFormat::Old {
+                return Err(Error::raw(
+                    ErrorKind::ArgumentConflict,
+                    "Conflicting options: --sarif isn't compatible with --output-format=old.",
+                ));
+            }
             if self.concrete_playback.is_some() && self.jobs().will_multithread() {
                 // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called.
                 return Err(Error::raw(
                     ErrorKind::ArgumentConflict,
                     "Conflicting options: --concrete-playback isn't compatible with --jobs specifying multiple threads.",
                 ));
             }
+            if self.sarif.is_some() && self.only_codegen {
+                return Err(Error::raw(
+                    ErrorKind::ArgumentConflict,
+                    "Conflicting options: --sarif isn't compatible with --only-codegen.",
+                ));
+            }
             if self.jobs().will_multithread() && self.output_format != OutputFormat::Terse {
                 // More verbose output formats make it hard to interpret output right now when run in parallel.
                 // This can be removed when we change up how results are printed.
@@ -853,6 +869,18 @@ impl ValidateArgs for VerificationArgs {
                 ),
             ));
         }
+        if let Some(out_file) = &self.sarif
+            && out_file.exists()
+            && out_file.is_dir()
+        {
+            return Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: `--sarif` argument `{}` is a directory",
+                    out_file.display()
+                ),
+            ));
+        }
 
         Ok(())
     }
@@ -1138,6 +1166,24 @@ mod tests {
         );
     }
 
+    #[test]
+    fn check_sarif_parsing() {
+        let args = parse_unstable_disabled("--sarif out.sarif").unwrap();
+        assert_eq!(args.verify_opts.sarif, Some(PathBuf::from("out.sarif")));
+    }
+
+    #[test]
+    fn check_sarif_conflicts() {
+        expect_validation_error(
+            "kani file.rs --sarif out.sarif --output-format=old",
+            ErrorKind::ArgumentConflict,
+        );
+        expect_validation_error(
+            "kani file.rs --sarif out.sarif --only-codegen",
+            ErrorKind::ArgumentConflict,
+        );
+    }
+
     #[test]
     fn check_enable_stubbing() {
         let res = parse_unstable_disabled("--harness foo").unwrap();

kani-driver/src/main.rs

@@ -36,6 +36,7 @@ mod harness_runner;
 mod list;
 mod metadata;
 mod project;
+mod sarif;
 mod session;
 mod util;
 mod version;
@@ -159,6 +160,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
         session.save_coverage_results(&project, &results, &timestamp)?;
     }
 
+    session.write_sarif(&results)?;
     session.print_final_summary(&results)
 }