diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 12e1a9c046b..3925cc85472 100644 --- a/doc/cprover-manual/index.md +++ b/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/) diff --git a/doc/cprover-manual/sarif-output.md b/doc/cprover-manual/sarif-output.md new file mode 100644 index 00000000000..88411bb32ba --- /dev/null +++ b/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 } + } + }] + }] + }] +} +``` diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 0e454caf4c1..a891ca69279 100644 --- a/doc/man/cbmc.1 +++ b/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 diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 05f70b7805b..ea61365f839 100644 --- a/doc/man/jbmc.1 +++ b/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 diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 7ed4105af63..d52271513f1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/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 diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 80a11dc1b52..578a3457810 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/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 \ diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 6d8a6fe0702..ab473b3d33a 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index 010916f58d9..a44e82d552f 100644 --- a/regression/Makefile +++ b/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 \ diff --git a/regression/cbmc-sarif-ui/CMakeLists.txt b/regression/cbmc-sarif-ui/CMakeLists.txt new file mode 100644 index 00000000000..5781cfabfb2 --- /dev/null +++ b/regression/cbmc-sarif-ui/CMakeLists.txt @@ -0,0 +1,9 @@ +add_test_pl_tests("$") + +add_test( + NAME cbmc-sarif-validation + COMMAND bash "${CMAKE_CURRENT_SOURCE_DIR}/test_sarif_valid.sh" + "$" + WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" +) +set_tests_properties(cbmc-sarif-validation PROPERTIES LABELS "CORE;CBMC") diff --git a/regression/cbmc-sarif-ui/Makefile b/regression/cbmc-sarif-ui/Makefile new file mode 100644 index 00000000000..191b9558366 --- /dev/null +++ b/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 diff --git a/regression/cbmc-sarif-ui/bounds/bounds.c b/regression/cbmc-sarif-ui/bounds/bounds.c new file mode 100644 index 00000000000..c69e40db048 --- /dev/null +++ b/regression/cbmc-sarif-ui/bounds/bounds.c @@ -0,0 +1,7 @@ +int main() +{ + int a[5]; + int i; + a[i] = 1; + return 0; +} diff --git a/regression/cbmc-sarif-ui/bounds/bounds.desc b/regression/cbmc-sarif-ui/bounds/bounds.desc new file mode 100644 index 00000000000..543d77f0a4b --- /dev/null +++ b/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. diff --git a/regression/cbmc-sarif-ui/failure/failure.c b/regression/cbmc-sarif-ui/failure/failure.c new file mode 100644 index 00000000000..d25b7d8dbe1 --- /dev/null +++ b/regression/cbmc-sarif-ui/failure/failure.c @@ -0,0 +1,6 @@ +int main() +{ + unsigned x; + assert(x == 0); + return 0; +} diff --git a/regression/cbmc-sarif-ui/failure/failure.desc b/regression/cbmc-sarif-ui/failure/failure.desc new file mode 100644 index 00000000000..6db8543d3a6 --- /dev/null +++ b/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. diff --git a/regression/cbmc-sarif-ui/json-ui-combo/test.c b/regression/cbmc-sarif-ui/json-ui-combo/test.c new file mode 100644 index 00000000000..af243e451ac --- /dev/null +++ b/regression/cbmc-sarif-ui/json-ui-combo/test.c @@ -0,0 +1,5 @@ +int main() +{ + int x = 1; + __CPROVER_assert(x == 0, "expected fail"); +} diff --git a/regression/cbmc-sarif-ui/json-ui-combo/test.desc b/regression/cbmc-sarif-ui/json-ui-combo/test.desc new file mode 100644 index 00000000000..d946645444a --- /dev/null +++ b/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. diff --git a/regression/cbmc-sarif-ui/mixed/mixed.c b/regression/cbmc-sarif-ui/mixed/mixed.c new file mode 100644 index 00000000000..82d80bbe416 --- /dev/null +++ b/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; +} diff --git a/regression/cbmc-sarif-ui/mixed/mixed.desc b/regression/cbmc-sarif-ui/mixed/mixed.desc new file mode 100644 index 00000000000..6f11302a7fc --- /dev/null +++ b/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. diff --git a/regression/cbmc-sarif-ui/success/success.c b/regression/cbmc-sarif-ui/success/success.c new file mode 100644 index 00000000000..e27cf63b951 --- /dev/null +++ b/regression/cbmc-sarif-ui/success/success.c @@ -0,0 +1,8 @@ +#include + +int main() +{ + int x = 1; + assert(x == 1); + return 0; +} diff --git a/regression/cbmc-sarif-ui/success/success.desc b/regression/cbmc-sarif-ui/success/success.desc new file mode 100644 index 00000000000..2a7d6d12ccd --- /dev/null +++ b/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. diff --git a/regression/cbmc-sarif-ui/test_sarif_valid.sh b/regression/cbmc-sarif-ui/test_sarif_valid.sh new file mode 100755 index 00000000000..2f3c5173e23 --- /dev/null +++ b/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 +# 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 diff --git a/regression/cbmc-sarif-ui/validate_sarif.py b/regression/cbmc-sarif-ui/validate_sarif.py new file mode 100755 index 00000000000..44ea8bdb27c --- /dev/null +++ b/regression/cbmc-sarif-ui/validate_sarif.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 + +"""Validate SARIF 2.1.0 output from CBMC. + +Reads SARIF JSON from stdin and validates: +- Valid JSON +- Required SARIF 2.1.0 top-level structure +- Required run/tool/results structure +- Required fields in each result object +Exits 0 on success, 1 on validation failure. +""" + +import json +import sys + + +def validate_sarif(data): + errors = [] + + if not isinstance(data, dict): + errors.append("Root must be a JSON object") + return errors + + # Top-level fields + if data.get("version") != "2.1.0": + errors.append( + f"Expected version '2.1.0', got '{data.get('version')}'") + + if "$schema" not in data: + errors.append("Missing '$schema' field") + + if not isinstance(data.get("runs"), list) or len(data["runs"]) == 0: + errors.append("'runs' must be a non-empty array") + return errors + + for i, run in enumerate(data["runs"]): + if not isinstance(run, dict): + errors.append(f"runs[{i}] must be an object") + continue + + # Tool + tool = run.get("tool") + if not isinstance(tool, dict): + errors.append(f"runs[{i}].tool must be an object") + else: + driver = tool.get("driver") + if not isinstance(driver, dict): + errors.append(f"runs[{i}].tool.driver must be an object") + else: + if "name" not in driver: + errors.append( + f"runs[{i}].tool.driver.name is required") + + # Results + results = run.get("results") + if not isinstance(results, list): + errors.append(f"runs[{i}].results must be an array") + continue + + for j, result in enumerate(results): + if not isinstance(result, dict): + errors.append(f"runs[{i}].results[{j}] must be an object") + continue + + if "ruleId" not in result: + errors.append( + f"runs[{i}].results[{j}].ruleId is required") + + if "message" not in result: + errors.append( + f"runs[{i}].results[{j}].message is required") + elif "text" not in result.get("message", {}): + errors.append( + f"runs[{i}].results[{j}].message.text is required") + + level = result.get("level") + valid_levels = {"none", "note", "warning", "error"} + if level is not None and level not in valid_levels: + errors.append( + f"runs[{i}].results[{j}].level '{level}' " + f"not in {valid_levels}") + + # Validate locations structure if present + locations = result.get("locations", []) + for k, loc in enumerate(locations): + if not isinstance(loc, dict): + errors.append( + f"runs[{i}].results[{j}].locations[{k}] " + f"must be an object") + continue + pl = loc.get("physicalLocation", {}) + if not isinstance(pl, dict): + errors.append( + f"runs[{i}].results[{j}].locations[{k}]" + f".physicalLocation must be an object") + continue + if "artifactLocation" in pl: + al = pl["artifactLocation"] + if not isinstance(al, dict): + errors.append( + f"runs[{i}].results[{j}].locations[{k}]" + f".physicalLocation.artifactLocation " + f"must be an object") + continue + if "uri" not in al: + errors.append( + f"runs[{i}].results[{j}].locations[{k}]" + f".physicalLocation.artifactLocation.uri " + f"is required") + + return errors + + +def main(): + if len(sys.argv) > 1: + with open(sys.argv[1]) as f: + raw = f.read() + else: + raw = sys.stdin.read() + + try: + data = json.loads(raw) + except json.JSONDecodeError as e: + print(f"SARIF VALIDATION FAILED: Invalid JSON: {e}") + return 1 + + errors = validate_sarif(data) + if errors: + print("SARIF VALIDATION FAILED:") + for error in errors: + print(f" - {error}") + return 1 + + n_results = sum( + len(run.get("results", [])) + for run in data.get("runs", [])) + print(f"SARIF VALIDATION SUCCESSFUL ({n_results} results)") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/regression/cbmc-sarif-ui/xml-ui-combo/test.c b/regression/cbmc-sarif-ui/xml-ui-combo/test.c new file mode 100644 index 00000000000..af243e451ac --- /dev/null +++ b/regression/cbmc-sarif-ui/xml-ui-combo/test.c @@ -0,0 +1,5 @@ +int main() +{ + int x = 1; + __CPROVER_assert(x == 0, "expected fail"); +} diff --git a/regression/cbmc-sarif-ui/xml-ui-combo/test.desc b/regression/cbmc-sarif-ui/xml-ui-combo/test.desc new file mode 100644 index 00000000000..a9c1ac5a8e0 --- /dev/null +++ b/regression/cbmc-sarif-ui/xml-ui-combo/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--xml-ui --sarif-result sarif.out +activate-multi-line-match +^EXIT=10$ +^SIGNAL=0$ + +FAILURE +-- +-- +Checks that --sarif-result combined with --xml-ui produces XML UI on stdout. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6548067d791..e5761f9ff85 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -44,6 +44,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -776,6 +777,26 @@ int cbmc_parse_optionst::doit() const resultt result = (*verifier)(); verifier->report(); + if(cmdline.isset("sarif-result")) + { + const auto &filename = cmdline.get_value("sarif-result"); + if(filename == "-") + { + sarif_report(verifier->get_properties(), "cbmc", std::cout); + } + else + { + std::ofstream out(filename); + if(!out) + { + log.error() << "failed to open SARIF output file: " << filename + << messaget::eom; + return CPROVER_EXIT_INTERNAL_ERROR; + } + sarif_report(verifier->get_properties(), "cbmc", out); + } + } + return result_to_exit_code(result); } @@ -1079,6 +1100,7 @@ void cbmc_parse_optionst::help() "User-interface options:\n" HELP_XML_INTERFACE HELP_JSON_INTERFACE + HELP_SARIF_RESULT HELP_GOTO_TRACE HELP_FLUSH " {y--verbosity} {u#} \t verbosity level (default 6)\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a5890bfb88d..a4692569435 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -49,6 +49,7 @@ class optionst; OPT_GOTO_CHECK \ OPT_XML_INTERFACE \ OPT_JSON_INTERFACE \ + OPT_SARIF_RESULT \ OPT_SOLVER \ OPT_STRING_REFINEMENT_CBMC \ OPT_SHOW_GOTO_FUNCTIONS \ diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 0750b9d2274..f5c33665dd8 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -11,6 +11,7 @@ SRC = bmc_util.cpp \ multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ + sarif_report.cpp \ single_loop_incremental_symex_checker.cpp \ single_path_symex_checker.cpp \ single_path_symex_only_checker.cpp \ diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 676b75efdae..f1efe6cacf0 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -144,6 +144,75 @@ void json( json(result, property_id, property_info); } +/// Convert property to SARIF result format +json_objectt +sarif_result(const irep_idt &property_id, const property_infot &property_info) +{ + json_objectt result; + + // Map property status to SARIF level + std::string level; + switch(property_info.status) + { + case property_statust::FAIL: + level = "error"; + break; + case property_statust::ERROR: + level = "error"; + break; + case property_statust::UNKNOWN: + level = "warning"; + break; + case property_statust::NOT_REACHABLE: + level = "note"; + break; + case property_statust::PASS: + level = "note"; + break; + case property_statust::NOT_CHECKED: + level = "note"; + break; + } + + result["ruleId"] = json_stringt(property_id); + result["level"] = json_stringt(level); + + json_objectt message; + message["text"] = json_stringt( + property_info.description + " (" + as_string(property_info.status) + ")"); + result["message"] = message; + + // Add location information + json_arrayt locations; + json_objectt location; + json_objectt physical_location; + json_objectt artifact_location; + json_objectt region; + + const auto &src_loc = property_info.pc->source_location(); + if(!src_loc.get_file().empty()) + { + artifact_location["uri"] = json_stringt(src_loc.get_file()); + physical_location["artifactLocation"] = artifact_location; + + if(!src_loc.get_line().empty()) + { + region["startLine"] = json_numbert(id2string(src_loc.get_line())); + if(!src_loc.get_column().empty()) + { + region["startColumn"] = json_numbert(id2string(src_loc.get_column())); + } + physical_location["region"] = region; + } + + location["physicalLocation"] = physical_location; + locations.push_back(location); + result["locations"] = locations; + } + + return result; +} + int result_to_exit_code(resultt result) { switch(result) diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index 9a74b700fd3..254b9452944 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -94,6 +94,10 @@ json(const irep_idt &property_id, const property_infot &property_info); /// Write the property info into the given JSON stream object void json(json_stream_objectt &, const irep_idt &, const property_infot &); +/// Convert property to SARIF result format +json_objectt +sarif_result(const irep_idt &property_id, const property_infot &property_info); + int result_to_exit_code(resultt result); /// Return the number of properties with given \p status diff --git a/src/goto-checker/sarif_report.cpp b/src/goto-checker/sarif_report.cpp new file mode 100644 index 00000000000..e62b55e8078 --- /dev/null +++ b/src/goto-checker/sarif_report.cpp @@ -0,0 +1,52 @@ +/*******************************************************************\ + +Module: SARIF Report + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// SARIF Report + +#include "sarif_report.h" + +#include +#include + +void sarif_report( + const propertiest &properties, + const std::string &program, + std::ostream &out) +{ + json_objectt sarif; + sarif["$schema"] = + json_stringt("https://json.schemastore.org/sarif-2.1.0.json"); + sarif["version"] = json_stringt("2.1.0"); + + json_arrayt runs; + json_objectt run; + + // tool + json_objectt driver; + driver["name"] = json_stringt(program); + driver["version"] = json_stringt(CBMC_VERSION); + driver["informationUri"] = + json_stringt("https://www.cprover.org/" + program + "/"); + json_objectt tool; + tool["driver"] = std::move(driver); + run["tool"] = std::move(tool); + + // results + json_arrayt results; + for(const auto &property_pair : properties) + { + results.push_back(sarif_result(property_pair.first, property_pair.second)); + } + run["results"] = std::move(results); + + runs.push_back(std::move(run)); + sarif["runs"] = std::move(runs); + + out << sarif << '\n'; +} diff --git a/src/goto-checker/sarif_report.h b/src/goto-checker/sarif_report.h new file mode 100644 index 00000000000..f2368e45a0c --- /dev/null +++ b/src/goto-checker/sarif_report.h @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: SARIF Report + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// SARIF Report + +#ifndef CPROVER_GOTO_CHECKER_SARIF_REPORT_H +#define CPROVER_GOTO_CHECKER_SARIF_REPORT_H + +#include "properties.h" + +#include +#include + +/// Write a complete SARIF 2.1.0 log to \p out for the given \p properties. +/// \param properties: the verification results +/// \param program: tool name (e.g. "cbmc") +/// \param out: output stream +void sarif_report( + const propertiest &properties, + const std::string &program, + std::ostream &out); + +#endif // CPROVER_GOTO_CHECKER_SARIF_REPORT_H diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 66872711d00..a102d016e79 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -57,6 +57,7 @@ void goto_difft::output_functions() const case ui_message_handlert::uit::XML_UI: { msg.error() << "XML output not supported yet" << messaget::eom; + break; } } } diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index e3658577b91..41d1181bdc7 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -105,6 +105,7 @@ void show_loop_ids( break; case ui_message_handlert::uit::JSON_UI: + { json_objectt json_result; json_arrayt &loops=json_result["loops"].make_array(); @@ -113,5 +114,6 @@ void show_loop_ids( std::cout << ",\n" << json_result; break; + } } } diff --git a/src/json/json_interface.h b/src/json/json_interface.h index dea5a47a074..c972035cd8e 100644 --- a/src/json/json_interface.h +++ b/src/json/json_interface.h @@ -37,12 +37,18 @@ class message_handlert; /// \endcode void json_interface(cmdlinet &, message_handlert &); -#define OPT_JSON_INTERFACE \ - "(json-ui)" \ +#define OPT_JSON_INTERFACE \ + "(json-ui)" \ "(json-interface)" #define HELP_JSON_INTERFACE \ " {y--json-ui} \t use JSON-formatted output\n" \ " {y--json-interface} \t bi-directional JSON interface\n" +#define OPT_SARIF_RESULT "(sarif-result):" + +#define HELP_SARIF_RESULT \ + " {y--sarif-result} {ufile} \t write SARIF-formatted results to file" \ + " (use - for stdout)\n" + #endif // CPROVER_JSON_JSON_INTERFACE_H diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 69302626dc7..6539f8cd132 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -68,18 +68,17 @@ ui_message_handlert::ui_message_handlert( const std::string &program) : ui_message_handlert( nullptr, - cmdline.isset("xml-ui") || cmdline.isset("xml-interface") - ? uit::XML_UI - : cmdline.isset("json-ui") || cmdline.isset("json-interface") - ? uit::JSON_UI - : uit::PLAIN, + cmdline.isset("xml-ui") || cmdline.isset("xml-interface") ? uit::XML_UI + : cmdline.isset("json-ui") || cmdline.isset("json-interface") + ? uit::JSON_UI + : uit::PLAIN, program, cmdline.isset("flush"), cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic" ? timestampert::clockt::MONOTONIC - : cmdline.get_value("timestamp") == "wall" - ? timestampert::clockt::WALL_CLOCK - : timestampert::clockt::NONE + : cmdline.get_value("timestamp") == "wall" + ? timestampert::clockt::WALL_CLOCK + : timestampert::clockt::NONE : timestampert::clockt::NONE) { if(get_ui() == uit::PLAIN) diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 8d92e33b816..21dfdc3fafd 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -17,11 +17,17 @@ Author: Daniel Kroening, kroening@kroening.com class console_message_handlert; class json_stream_arrayt; +class jsont; class ui_message_handlert : public message_handlert { public: - enum class uit { PLAIN, XML_UI, JSON_UI }; + enum class uit + { + PLAIN, + XML_UI, + JSON_UI + }; ui_message_handlert(const class cmdlinet &, const std::string &program); @@ -42,6 +48,7 @@ class ui_message_handlert : public message_handlert PRECONDITION(json_stream!=nullptr); return *json_stream; } + void print(unsigned level, const structured_datat &data) override; protected: