Add SARIF output support via --sarif-result option

doc/cprover-manual/index.md

@@ -36,4 +36,5 @@
 10. Background Information on selected Command-line Options
 
    * [Incremental SMT solver](smt2-incr/)
+   * [SARIF output](sarif-output/)
    * [Unsound options](unsound_options/)

doc/cprover-manual/sarif-output.md

@@ -0,0 +1,45 @@
+[CPROVER Manual TOC](../)
+
+# SARIF Output
+
+CBMC and JBMC support [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`),
+producing both the normal output and a SARIF file.
+
+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 }
+        }
+      }]
+    }]
+  }]
+}
+```

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

@@ -41,6 +41,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;
+}

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

@@ -0,0 +1,15 @@
+CORE
+bounds.c
+--sarif-result - --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-result - 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;
+}

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

@@ -0,0 +1,16 @@
+CORE
+failure.c
+--sarif-result -
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+"\$schema": "https://json\.schemastore\.org/sarif-2\.1\.0\.json"
+"version": "2\.1\.0"
+"ruleId": "main\.assertion\.1"
+"level": "error"
+"text": "assertion x == \(unsigned int\)0 \(FAILURE\)"
+"startLine": 4
+--
+"level": "note"
+--
+Checks that --sarif-result - produces error-level SARIF results for failed assertions.

regression/cbmc-sarif-ui/json-ui-combo/test.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int x = 1;
+  __CPROVER_assert(x == 0, "expected fail");
+}

regression/cbmc-sarif-ui/json-ui-combo/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--json-ui --sarif-result sarif.out
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+"cProverStatus": "failure"
+"property": "main\.assertion\.1"
+"status": "FAILURE"
+--
+--
+Checks that --sarif-result combined with --json-ui produces JSON UI on stdout.

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

@@ -0,0 +1,8 @@
+int main()
+{
+  int x;
+  assert(x >= 0);
+  int y = 1;
+  assert(y == 1);
+  return 0;
+}

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

@@ -0,0 +1,15 @@
+CORE
+mixed.c
+--sarif-result -
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+"ruleId": "main\.assertion\.1"
+"ruleId": "main\.assertion\.2"
+"level": "error"
+"level": "note"
+"text": "assertion x >= 0 \(FAILURE\)"
+"text": "assertion y == 1 \(SUCCESS\)"
+--
+--
+Checks that --sarif-result - correctly reports mixed pass/fail with error and note levels.

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

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 1;
+  assert(x == 1);
+  return 0;
+}

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

@@ -0,0 +1,18 @@
+CORE
+success.c
+--sarif-result -
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+"\$schema": "https://json\.schemastore\.org/sarif-2\.1\.0\.json"
+"version": "2\.1\.0"
+"name": "cbmc"
+"informationUri": "https://www\.cprover\.org/cbmc/"
+"ruleId": "main\.assertion\.1"
+"level": "note"
+"text": "assertion x == 1 \(SUCCESS\)"
+"startLine": 6
+--
+"level": "error"
+--
+Checks that --sarif-result - produces valid SARIF output for successful verification.

regression/cbmc-sarif-ui/test_sarif_valid.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+# Runs cbmc --sarif-result on test inputs and validates the SARIF output.
+# Usage: test_sarif_valid.sh <cbmc-binary>
+# Exit 0 if all validations pass, 1 otherwise.
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+CBMC="$1"
+FAILED=0
+TMPFILE=$(mktemp)
+trap 'rm -f "$TMPFILE"' EXIT
+
+for test_case in success failure bounds mixed; do
+  case "$test_case" in
+    bounds) OPTS="--bounds-check" ;;
+    *)      OPTS="" ;;
+  esac
+
+  "$CBMC" --sarif-result "$TMPFILE" $OPTS "$SCRIPT_DIR/${test_case}/${test_case}.c" >/dev/null 2>&1 || true
+  if ! python3 "$SCRIPT_DIR/validate_sarif.py" "$TMPFILE"; then
+    echo "FAILED: ${test_case}.c"
+    cat "$TMPFILE"
+    FAILED=1
+  fi
+done
+
+# Test combinations with other UI modes
+for ui_mode in "--json-ui" "--xml-ui"; do
+  "$CBMC" $ui_mode --sarif-result "$TMPFILE" "$SCRIPT_DIR/failure/failure.c" >/dev/null 2>&1 || true
+  if ! python3 "$SCRIPT_DIR/validate_sarif.py" "$TMPFILE"; then
+    echo "FAILED: failure.c with $ui_mode"
+    cat "$TMPFILE"
+    FAILED=1
+  fi
+done
+
+if [ $FAILED -eq 0 ]; then
+  echo "All SARIF validation tests passed"
+fi
+exit $FAILED