Add SARIF output support via --sarif-result option

Add --sarif-result <file> option that writes a SARIF (Static Analysis
Results Interchange Format) 2.1.0 log for verification results. Use
--sarif-result - to write to stdout.

Following ebmc's artefact-specific approach, SARIF output is handled by
a standalone sarif_report() function rather than adding a new UI mode to
ui_message_handlert. This avoids extending the switchboard pattern in
the message handler.

The option can be combined with any UI mode (--json-ui, --xml-ui, or
plain text), producing both the normal output and a SARIF file.

Fixes: #6851

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

doc/cprover-manual/cbmc-tutorial.md

@@ -137,6 +137,47 @@ possible output format.
     cbmc file1.c --bounds-check --pointer-check --trace --xml-ui
 ```
 
+CBMC also supports [SARIF](https://sarifweb.azurewebsites.net/) (Static
+Analysis Results Interchange Format) output, which is widely supported by IDEs
+and CI systems. Use `--sarif-result` to write SARIF output to a file:
+
+```
+    cbmc file1.c --bounds-check --pointer-check --sarif-result results.sarif
+```
+
+Use `-` as the filename to write to standard output. The `--sarif-result`
+option can be combined with other UI modes (e.g., `--json-ui`, `--xml-ui`).
+
+This produces a JSON document conforming to the SARIF 2.1.0 schema, with each
+property reported as a SARIF result entry including rule identifier, severity
+level, message, and source location. For example:
+
+```json
+{
+  "$schema": "https://json.schemastore.org/sarif-2.1.0.json",
+  "version": "2.1.0",
+  "runs": [{
+    "tool": {
+      "driver": {
+        "name": "CBMC ...",
+        "informationUri": "https://www.cprover.org/cbmc/"
+      }
+    },
+    "results": [{
+      "ruleId": "main.assertion.1",
+      "level": "error",
+      "message": { "text": "assertion x > 0 (FAILURE)" },
+      "locations": [{
+        "physicalLocation": {
+          "artifactLocation": { "uri": "example.c" },
+          "region": { "startLine": 5 }
+        }
+      }]
+    }]
+  }]
+}
+```
+
 ## Verifying Modules
 
 In the example above, we used a program that starts with a `main`

doc/man/cbmc.1

@@ -590,6 +590,9 @@ use JSON\-formatted output
 \fB\-\-json\-interface\fR
 bi\-directional JSON interface
 .TP
+\fB\-\-sarif\-result\fR \fIfile\fR
+write SARIF\-formatted results to \fIfile\fR (use \- for stdout)
+.TP
 \fB\-\-trace\-json\-extended\fR
 add rawLhs property to trace
 .TP

doc/man/jbmc.1

@@ -505,6 +505,9 @@ use JSON\-formatted output
 \fB\-\-json\-interface\fR
 bi\-directional JSON interface
 .TP
+\fB\-\-sarif\-result\fR \fIfile\fR
+write SARIF\-formatted results to \fIfile\fR (use \- for stdout)
+.TP
 \fB\-\-validate\-goto\-model\fR
 enable additional well\-formedness checks on the
 goto program

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1048,6 +1048,7 @@ void jbmc_parse_optionst::help()
     " {y--version} \t show version and exit\n"
     HELP_XML_INTERFACE
     HELP_JSON_INTERFACE
+    HELP_SARIF_RESULT
     HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH

jbmc/src/jbmc/jbmc_parse_options.h

@@ -54,6 +54,7 @@ class optionst;
   "(no-assertions)(no-assumptions)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
+  OPT_SARIF_RESULT \
   "(smt1)" /* rejected, will eventually disappear */ \
   OPT_SOLVER \
   OPT_STRING_REFINEMENT \

regression/CMakeLists.txt

@@ -40,6 +40,7 @@ add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-shadow-memory)
 add_subdirectory(cbmc-output-file)
+add_subdirectory(cbmc-sarif-ui)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)
 add_subdirectory(goto-instrument-chc)

regression/Makefile

@@ -12,6 +12,7 @@ DIRS = cbmc-shadow-memory \
        cpp \
        cbmc-concurrency \
        cbmc-cover \
+       cbmc-sarif-ui \
        cbmc-incr-oneloop \
        cbmc-incr-smt2 \
        cbmc-incr \

regression/cbmc-sarif-ui/CMakeLists.txt

@@ -0,0 +1,9 @@
+add_test_pl_tests("$<TARGET_FILE:cbmc>")
+
+add_test(
+  NAME cbmc-sarif-validation
+  COMMAND bash "${CMAKE_CURRENT_SOURCE_DIR}/test_sarif_valid.sh"
+    "$<TARGET_FILE:cbmc>"
+  WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+)
+set_tests_properties(cbmc-sarif-validation PROPERTIES LABELS "CORE;CBMC")

regression/cbmc-sarif-ui/Makefile

@@ -0,0 +1,14 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@bash test_sarif_valid.sh ../../src/cbmc/cbmc
+
+tests.log: ../test.pl test
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests*.log

regression/cbmc-sarif-ui/bounds/bounds.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int a[5];
+  int i;
+  a[i] = 1;
+  return 0;
+}