Add SARIF output support via --sarif-ui option #8835

tautschnig · 2026-02-11T15:56:24Z

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

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

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

Copilot

Pull request overview

Adds a new --sarif-ui user-interface mode intended to emit SARIF 2.1.0 JSON, extending existing JSON UI plumbing to output verification results as SARIF “results” entries.

Changes:

Extend ui_message_handlert with a new SARIF_UI mode and streaming helper sarif_output(...).
Convert goto-checker property reporting to emit SARIF result objects.
Add a new regression suite (regression/cbmc-sarif-ui) to validate SARIF JSON structure.

Reviewed changes

Copilot reviewed 34 out of 34 changed files in this pull request and generated 11 comments.

Show a summary per file

File	Description
src/util/ui_message.h	Adds `SARIF_UI` enum value, `sarif_output(...)`, and tracking state.
src/util/ui_message.cpp	Emits SARIF log wrapper on stdout; routes general messages to stderr in SARIF mode.
src/pointer-analysis/show_value_sets.cpp	Treats SARIF like JSON for value-set output.
src/json/json_interface.h	Registers `--sarif-ui` in option/help macros.
src/goto-symex/show_vcc.cpp	Treats SARIF like JSON for `--show-vcc` output.
src/goto-symex/show_program.cpp	Treats SARIF like JSON for `--show-byte-ops` output.
src/goto-programs/show_symbol_table.cpp	Treats SARIF like JSON UI for symbol table output.
src/goto-programs/show_properties.cpp	Adds SARIF case (currently `UNREACHABLE`) in property printing.
src/goto-programs/show_goto_functions.cpp	Adds SARIF case for showing goto functions (JSON-like output).
src/goto-programs/loop_ids.cpp	Adds SARIF case for loop IDs (falls back to PLAIN).
src/goto-programs/class_hierarchy.cpp	Marks SARIF as unimplemented for class hierarchy output.
src/goto-instrument/show_locations.cpp	Marks SARIF as unreachable in locations output.
src/goto-diff/goto_diff_base.cpp	Adds SARIF “not supported” error path.
src/goto-checker/report_util.cpp	Emits SARIF results for properties via `sarif_result(...)` + `sarif_output(...)`.
src/goto-checker/properties.h	Declares `sarif_result(...)`.
src/goto-checker/properties.cpp	Implements SARIF result object construction (ruleId/level/message/locations).
src/goto-checker/cover_goals_report_util.cpp	Routes SARIF case through existing JSON goal output.
src/goto-checker/bmc_util.cpp	Emits SARIF result for error trace (last step).
src/cbmc/cbmc_parse_options.cpp	Allows `--sarif-ui` for some JSON-only modes; updates help text for array constraints.
src/cbmc/c_test_input_generator.cpp	Adds SARIF case (prints test suite text).
jbmc/src/jbmc/jbmc_parse_options.cpp	Adds SARIF case for dumping options as JSON object.
regression/CMakeLists.txt	Adds `cbmc-sarif-ui` regression subdirectory.
regression/cbmc-sarif-ui/Makefile	Adds regression make target and SARIF validation invocation.
regression/cbmc-sarif-ui/CMakeLists.txt	Adds CTest entries for SARIF regression + validation script.
regression/cbmc-sarif-ui/validate_sarif.py	Validates SARIF top-level schema/runs/results structure.
regression/cbmc-sarif-ui/test_sarif_valid.sh	Runs CBMC with `--sarif-ui` on test cases and validates output.
regression/cbmc-sarif-ui/success/success.desc	Adds expected-output checks for SARIF success case.
regression/cbmc-sarif-ui/success/success.c	Test input for success case.
regression/cbmc-sarif-ui/failure/failure.desc	Adds expected-output checks for SARIF failure case.
regression/cbmc-sarif-ui/failure/failure.c	Test input for failure case.
regression/cbmc-sarif-ui/bounds/bounds.desc	Adds expected-output checks for SARIF bounds failures.
regression/cbmc-sarif-ui/bounds/bounds.c	Test input for bounds failures.
regression/cbmc-sarif-ui/mixed/mixed.desc	Adds expected-output checks for mixed pass/fail SARIF output.
regression/cbmc-sarif-ui/mixed/mixed.c	Test input for mixed case.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-11T16:04:22Z

src/goto-programs/show_symbol_table.cpp

+  case ui_message_handlert::uit::SARIF_UI:
+    show_symbol_table_brief_json_ui(symbol_table, ui);
+    break;


Same issue as above: show_symbol_table_brief_json_ui depends on ui.get_json_stream(), but in SARIF_UI json_stream is never initialized, so this will trip the PRECONDITION and terminate. SARIF_UI should not reuse JSON_UI streaming helpers unless the JSON stream is set up for SARIF as well.

Copilot · 2026-02-11T16:04:22Z

src/goto-diff/goto_diff_base.cpp

    case ui_message_handlert::uit::XML_UI:
    {
      msg.error() << "XML output not supported yet" << messaget::eom;
    }
+    case ui_message_handlert::uit::SARIF_UI:
+    {
+      msg.error() << "SARIF output not supported yet" << messaget::eom;
+    }


Missing break; after the XML_UI case causes fallthrough into SARIF_UI, so --xml-ui will emit both the XML and SARIF 'not supported' errors. Add an explicit break (or [[fallthrough]] if intentional) after the XML_UI block.

Copilot · 2026-02-11T16:04:22Z

src/util/ui_message.cpp

+      out << "{\n";
+      out << "  \"$schema\": "
+             "\"https://json.schemastore.org/sarif-2.1.0.json\",\n";
+      out << "  \"version\": \"2.1.0\",\n";
+      out << "  \"runs\": [\n";
+      out << "    {\n";
+      out << "      \"tool\": {\n";
+      out << "        \"driver\": {\n";
+      out << "          \"name\": \"" << program << "\",\n";
+      out << "          \"version\": \"" << CBMC_VERSION << "\",\n";
+      out
+        << "          \"informationUri\": \"https://www.cprover.org/cbmc/\"\n";
+      out << "        }\n";
+      out << "      },\n";
+      out << "      \"results\": [\n";


The SARIF header is constructed by manually concatenating strings and writing program directly into JSON. If program contains characters that require JSON escaping (quotes, backslashes, control chars), this will produce invalid SARIF/JSON output. Prefer building a json_objectt (or at least using json_stringt for string values) and serializing it, to guarantee proper escaping.

Copilot · 2026-02-11T16:04:23Z

src/util/ui_message.cpp

+    case uit::SARIF_UI:
+      out << data;
+      flush(level);
+      break;


When SARIF_UI is active, print(const jsont &) writes raw JSON to out (stdout). Any code path that logs structured JSON (including print(const structured_datat&) which calls to_json) will therefore interleave arbitrary JSON with the SARIF log wrapper, making stdout invalid SARIF. Consider rejecting print(jsont) / print(structured_datat) under SARIF_UI (INVARIANT), or redirecting them to stderr, or translating them into SARIF results via sarif_output.

Copilot · 2026-02-11T16:04:23Z

src/goto-symex/show_vcc.cpp

+    show_vcc_json(out, equation);
+    break;


The SARIF_UI branch reuses show_vcc_json(out, ...), but show_vcc_json emits output prefixed with ",\n" to append to the JSON_UI stream array format. Under --sarif-ui the UI handler has already written a SARIF log wrapper to stdout, so this will produce invalid mixed output. Consider rejecting SARIF_UI for --show-vcc (similar to XML_UI), or implement a SARIF-compatible representation instead of reusing the JSON_UI append format.

Suggested change

show_vcc_json(out, equation);

break;

msg.error() << "SARIF UI not supported" << messaget::eom;

return;

Copilot · 2026-02-11T16:04:24Z

src/goto-programs/loop_ids.cpp

+    case ui_message_handlert::uit::SARIF_UI:
+      for(const auto &f : goto_functions.function_map)
+        show_loop_ids(ui_message_handlert::uit::PLAIN, f.first, f.second.body);
+      break;


In SARIF_UI mode this falls back to PLAIN output written to stdout. However, ui_message_handlert emits a SARIF log wrapper to stdout in SARIF_UI mode, so mixing plain-text loop output into stdout will invalidate the SARIF JSON. Consider rejecting --sarif-ui for --show-loops, or routing this output to stderr / a separate file, or providing a SARIF representation for loop IDs.

Suggested change

case ui_message_handlert::uit::SARIF_UI:

for(const auto &f : goto_functions.function_map)

show_loop_ids(ui_message_handlert::uit::PLAIN, f.first, f.second.body);

break;

case ui_message_handlert::uit::SARIF_UI:

{

// In SARIF_UI mode, ui_message_handlert emits SARIF JSON to stdout.

// Redirect the PLAIN loop output to stderr to avoid corrupting SARIF.

auto *const old_buf = std::cout.rdbuf();

std::cout.rdbuf(std::cerr.rdbuf());

for(const auto &f : goto_functions.function_map)

show_loop_ids(ui_message_handlert::uit::PLAIN, f.first, f.second.body);

std::cout.rdbuf(old_buf);

break;

}

Copilot · 2026-02-11T16:04:24Z

src/util/ui_message.cpp

+      cmdline.isset("xml-ui") || cmdline.isset("xml-interface") ? uit::XML_UI
+      : cmdline.isset("sarif-ui")                               ? uit::SARIF_UI
+      : cmdline.isset("json-ui") || cmdline.isset("json-interface")
+        ? uit::JSON_UI
+        : uit::PLAIN,


UI selection now prioritizes --sarif-ui over --json-interface. If a user passes both, the handler enters SARIF_UI mode but json_interface(...) will still attempt to read JSON from stdin and set json-ui, which is inconsistent and likely breaks the bidirectional JSON interface. Consider making --sarif-ui mutually exclusive with --json-interface (usage error), or giving --json-interface precedence over SARIF_UI.

Copilot · 2026-02-11T16:04:24Z

src/pointer-analysis/show_value_sets.cpp

+  case ui_message_handlert::uit::SARIF_UI:
+    std::cout << value_set_analysis.output_json(goto_model);
+    break;


SARIF_UI is handled here by emitting the same JSON output as JSON_UI to stdout. However, in SARIF_UI mode ui_message_handlert writes a SARIF log wrapper to stdout in its constructor/destructor, so this will produce invalid mixed output (SARIF header + value-set JSON). Either reject SARIF_UI for show_value_sets, or ensure this output is routed somewhere that doesn't corrupt the SARIF log (e.g., stderr), or provide a SARIF-compatible representation.

Copilot · 2026-02-11T16:04:24Z

src/goto-programs/show_properties.cpp

      UNREACHABLE;
      break;

+    case ui_message_handlert::uit::SARIF_UI:
+      UNREACHABLE;


show_properties(...) dispatches to show_properties_json(...) only when ui == JSON_UI. With --sarif-ui, it takes the non-JSON path and then hits case SARIF_UI: UNREACHABLE;, which will abort if a user runs --show-properties --sarif-ui (e.g., in cbmc or goto-instrument). Consider handling SARIF_UI explicitly in the top-level dispatch (similar to JSON_UI), or emitting a supported/unsupported error instead of UNREACHABLE.

Suggested change

UNREACHABLE;

break;

case ui_message_handlert::uit::SARIF_UI:

UNREACHABLE;

msg.error() << "JSON UI is not supported for show_properties; "

<< "use --xml-ui or plain output instead"

<< messaget::eom;

break;

case ui_message_handlert::uit::SARIF_UI:

msg.error() << "SARIF UI is not supported for show_properties; "

<< "use --xml-ui or plain output instead"

<< messaget::eom;

Copilot · 2026-02-11T16:04:25Z

src/goto-programs/show_symbol_table.cpp

+  case ui_message_handlert::uit::SARIF_UI:
+    show_symbol_table_json_ui(symbol_table, ui);
+    break;


In the SARIF_UI branch this calls show_symbol_table_json_ui(..., ui), but show_symbol_table_json_ui requires ui.get_json_stream() which is only initialized for JSON_UI. With --sarif-ui, json_stream is null and the PRECONDITION in get_json_stream() will fail at runtime. Consider either (1) treating SARIF_UI as unsupported for this command and emitting a clear error, or (2) initializing/using a SARIF-specific output path that does not depend on the JSON stream array UI wrapper.

codecov · 2026-02-11T16:46:07Z

Codecov Report

❌ Patch coverage is 50.58140% with 85 lines in your changes missing coverage. Please review.
✅ Project coverage is 79.97%. Comparing base (15eb10a) to head (c78613f).

Files with missing lines	Patch %	Lines
src/goto-checker/report_util.cpp	19.04%	17 Missing ⚠️
src/util/ui_message.cpp	82.45%	10 Missing ⚠️
src/goto-checker/properties.cpp	77.50%	9 Missing ⚠️
src/pointer-analysis/show_value_sets.cpp	0.00%	7 Missing ⚠️
src/cbmc/c_test_input_generator.cpp	0.00%	6 Missing ⚠️
src/goto-programs/show_symbol_table.cpp	0.00%	6 Missing ⚠️
src/goto-checker/bmc_util.cpp	0.00%	5 Missing ⚠️
jbmc/src/jbmc/jbmc_parse_options.cpp	0.00%	4 Missing ⚠️
src/goto-programs/loop_ids.cpp	0.00%	4 Missing ⚠️
src/goto-programs/show_goto_functions.cpp	0.00%	4 Missing ⚠️
... and 8 more

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8835      +/-   ##
===========================================
- Coverage    80.00%   79.97%   -0.03%     
===========================================
  Files         1700     1700              
  Lines       188252   188416     +164     
  Branches        73       73              
===========================================
+ Hits        150613   150693      +80     
- Misses       37639    37723      +84

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Add SARIF output support via --sarif-ui option

c78613f

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

Copilot AI review requested due to automatic review settings February 11, 2026 15:56

tautschnig requested review from TGWDB, kroening, martin-cs and peterschrammel as code owners February 11, 2026 15:56

Copilot started reviewing on behalf of tautschnig February 11, 2026 15:57 View session

Copilot AI reviewed Feb 11, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add SARIF output support via --sarif-ui option #8835

Add SARIF output support via --sarif-ui option #8835

tautschnig commented Feb 11, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

Copilot AI Feb 11, 2026

Uh oh!

codecov bot commented Feb 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Add SARIF output support via --sarif-ui option #8835

Are you sure you want to change the base?

Add SARIF output support via --sarif-ui option #8835

Conversation

tautschnig commented Feb 11, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Feb 11, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant