Add SARIF output support via --sarif-result option

[tautschnig]

Add --sarif-result 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

• 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.

[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.

[codecov]

Codecov Report

❌ Patch coverage is 83.11688% with 13 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.01%. Comparing base (bacf91c) to head (64e301b).

Files with missing lines	Patch %	Lines
src/goto-checker/properties.cpp	77.50%	9 Missing ⚠️
src/cbmc/cbmc_parse_options.cpp	70.00%	3 Missing ⚠️
src/util/ui_message.cpp	80.00%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8835   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1700     1701    +1     
  Lines       188344   188417   +73     
  Branches        73       73           
========================================
+ Hits        150701   150768   +67     
- Misses       37643    37649    +6     

☔ 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.

[kroening]

ebmc uses a different approach to outputting various artefacts; I am wondering if this feature is making a good case to do the same in cbmc.

The class ui_message_handlert acts as a gigantic switchboard, and needs to know all output formats, for all kinds of artefacts (results, traces).

It may make sense to use an artefact-specific case-split instead.

[tautschnig]

ebmc uses a different approach to outputting various artefacts; I am wondering if this feature is making a good case to do the same in cbmc.

The class ui_message_handlert acts as a gigantic switchboard, and needs to know all output formats, for all kinds of artefacts (results, traces).

It may make sense to use an artefact-specific case-split instead.

Good point, the previous approach was indeed cumbersome and also prone to future bugs being introduced. Reworked to align with ebmc's approach.

[Copilot]

Pull request overview

Copilot reviewed 32 out of 32 changed files in this pull request and generated 8 comments.

---

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

[Copilot]

Pull request overview

Copilot reviewed 32 out of 32 changed files in this pull request and generated 3 comments.

---

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