Add SARIF output support via --sarif-ui option

Implements Static Analysis Results Interchange Format (SARIF) support
as an extension of the existing json-ui option.

Fixes: #6851

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

Author: tautschnig

doc/cprover-manual/cbmc-tutorial.md

@@ -137,6 +137,44 @@ 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:
+
+```
+    cbmc file1.c --bounds-check --pointer-check --sarif-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\-ui\fR
+use SARIF\-formatted output (Static Analysis Results Interchange Format)
+.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\-ui\fR
+use SARIF\-formatted output (Static Analysis Results Interchange Format)
+.TP
 \fB\-\-validate\-goto\-model\fR
 enable additional well\-formedness checks on the
 goto program

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -414,6 +414,12 @@ int jbmc_parse_optionst::doit()
     case ui_message_handlert::uit::XML_UI:
       log.debug() << options.to_xml();
       break;
+    case ui_message_handlert::uit::SARIF_UI:
+    {
+      json_objectt json_options{{"options", options.to_json()}};
+      log.debug() << json_options;
+      break;
+    }
   }
 
   register_language(new_ansi_c_language);

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/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;
+}

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

@@ -0,0 +1,15 @@
+CORE
+bounds.c
+--sarif-ui --bounds-check
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+"\$schema": "https://json\.schemastore\.org/sarif-2\.1\.0\.json"
+"version": "2\.1\.0"
+"ruleId": "main\.array_bounds\.1"
+"ruleId": "main\.array_bounds\.2"
+"level": "error"
+"startLine": 5
+--
+--
+Checks that --sarif-ui produces multiple SARIF results for bounds-check failures.

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

@@ -0,0 +1,6 @@
+int main()
+{
+  unsigned x;
+  assert(x == 0);
+  return 0;
+}