diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3e58fe14..e2d51615 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -124,3 +124,19 @@ jobs: with: config: .github/memory_statistics_config.json check_against: docs/doxygen/include/size_table.md + proof_ci: + runs-on: cbmc_ubuntu-latest_64-core + steps: + - name: Set up CBMC runner + uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main + with: + kissat_tag: latest + cbmc_version: "5.73.0" + - run: | + git submodule update --init --recursive --checkout + sudo apt-get update + sudo apt-get install --yes --no-install-recommends gcc-multilib build-essential + - name: Run CBMC + uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main + with: + proofs_dir: test/cbmc/proofs diff --git a/test/cbmc/proofs/HTTPClient_AddHeader/Makefile b/test/cbmc/proofs/HTTPClient_AddHeader/Makefile index 7394ec1f..a9bd0f8b 100644 --- a/test/cbmc/proofs/HTTPClient_AddHeader/Makefile +++ b/test/cbmc/proofs/HTTPClient_AddHeader/Makefile @@ -58,4 +58,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/httpHeaderStrncpy.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile b/test/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile index 71fcf7c5..20bfa6a9 100644 --- a/test/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile +++ b/test/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile @@ -48,4 +48,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/httpHeaderStrncpy.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile b/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile index e8c8208d..509eeb59 100644 --- a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile +++ b/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/Makefile @@ -57,4 +57,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/httpHeaderStrncpy.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/cbmc-proof.txt b/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/cbmc-proof.txt deleted file mode 100644 index 6ed46f12..00000000 --- a/test/cbmc/proofs/HTTPClient_InitializeRequestHeaders/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile b/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile index f96dbc4e..f5155dc7 100644 --- a/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile +++ b/test/cbmc/proofs/HTTPClient_ReadHeader/Makefile @@ -44,4 +44,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/HTTPClient_ReadHeader_llhttp_execute. PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/HTTPClient_Send/Makefile b/test/cbmc/proofs/HTTPClient_Send/Makefile index 49273bde..931729ad 100644 --- a/test/cbmc/proofs/HTTPClient_Send/Makefile +++ b/test/cbmc/proofs/HTTPClient_Send/Makefile @@ -74,4 +74,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/httpHeaderStrncpy.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/HTTPClient_strerror/Makefile b/test/cbmc/proofs/HTTPClient_strerror/Makefile index 05dfe5b5..ea3c41e3 100644 --- a/test/cbmc/proofs/HTTPClient_strerror/Makefile +++ b/test/cbmc/proofs/HTTPClient_strerror/Makefile @@ -33,4 +33,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile b/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile index d6a98ee0..57d26c84 100644 --- a/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile +++ b/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile @@ -20,4 +20,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile b/test/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile index 8df45dad..f39923a9 100644 --- a/test/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile +++ b/test/cbmc/proofs/findHeaderOnHeaderCompleteCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/findHeaderValueParserCallback/Makefile b/test/cbmc/proofs/findHeaderValueParserCallback/Makefile index 53ca9f71..226b1f8e 100644 --- a/test/cbmc/proofs/findHeaderValueParserCallback/Makefile +++ b/test/cbmc/proofs/findHeaderValueParserCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnBodyCallback/Makefile b/test/cbmc/proofs/httpParserOnBodyCallback/Makefile index 77d96812..9e3f8697 100644 --- a/test/cbmc/proofs/httpParserOnBodyCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnBodyCallback/Makefile @@ -18,4 +18,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memmove.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnBodyCallback/cbmc-proof.txt b/test/cbmc/proofs/httpParserOnBodyCallback/cbmc-proof.txt deleted file mode 100644 index 6ed46f12..00000000 --- a/test/cbmc/proofs/httpParserOnBodyCallback/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile b/test/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile index e7c3635b..9ea2d735 100644 --- a/test/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnHeaderFieldCallback/Makefile @@ -17,4 +17,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/callback_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile b/test/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile index 8cae4cf9..5af9f46c 100644 --- a/test/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnHeaderValueCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile b/test/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile index 8c42da25..cc5f3836 100644 --- a/test/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnHeadersCompleteCallback/Makefile @@ -17,4 +17,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/callback_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile b/test/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile index 4b9e17dc..4441f791 100644 --- a/test/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnMessageBeginCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile b/test/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile index cd3074e3..dc76ba48 100644 --- a/test/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnMessageCompleteCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/httpParserOnStatusCallback/Makefile b/test/cbmc/proofs/httpParserOnStatusCallback/Makefile index da847919..f0454bf6 100644 --- a/test/cbmc/proofs/httpParserOnStatusCallback/Makefile +++ b/test/cbmc/proofs/httpParserOnStatusCallback/Makefile @@ -16,4 +16,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/source/core_http_client.c +EXTERNAL_SAT_SOLVER := kissat + include ../Makefile.common diff --git a/test/cbmc/proofs/lib/print_tool_versions.py b/test/cbmc/proofs/lib/print_tool_versions.py new file mode 100755 index 00000000..bdeb429e --- /dev/null +++ b/test/cbmc/proofs/lib/print_tool_versions.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + + +import logging +import pathlib +import shutil +import subprocess + + +_TOOLS = [ + "cadical", + "cbmc", + "cbmc-viewer", + "cbmc-starter-kit-update", + "kissat", + "litani", +] + + +def _format_versions(table): + lines = [ + "", + '', + ] + for tool, version in table.items(): + if version: + v_str = f'
{version}
' + else: + v_str = 'not found' + lines.append( + f'' + f'') + lines.append("
Tool Versions
{tool}:{v_str}
") + return "\n".join(lines) + + +def _get_tool_versions(): + ret = {} + for tool in _TOOLS: + err = f"Could not determine version of {tool}: " + ret[tool] = None + if not shutil.which(tool): + logging.error("%s'%s' not found on $PATH", err, tool) + continue + cmd = [tool, "--version"] + proc = subprocess.Popen(cmd, text=True, stdout=subprocess.PIPE) + try: + out, _ = proc.communicate(timeout=10) + except subprocess.TimeoutExpired: + logging.error("%s'%s --version' timed out", err, tool) + continue + if proc.returncode: + logging.error( + "%s'%s --version' returned %s", err, tool, str(proc.returncode)) + continue + ret[tool] = out.strip() + return ret + + +def main(): + exe_name = pathlib.Path(__file__).name + logging.basicConfig(format=f"{exe_name}: %(message)s") + + table = _get_tool_versions() + out = _format_versions(table) + print(out) + + +if __name__ == "__main__": + main() diff --git a/test/cbmc/proofs/lib/summarize.py b/test/cbmc/proofs/lib/summarize.py index a5fec96f..50dbcc33 100644 --- a/test/cbmc/proofs/lib/summarize.py +++ b/test/cbmc/proofs/lib/summarize.py @@ -4,6 +4,8 @@ import argparse import json import logging +import os +import sys DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize @@ -89,8 +91,9 @@ def _get_status_and_proof_summaries(run_dict): count_statuses[status_pretty_name] += 1 except KeyError: count_statuses[status_pretty_name] = 1 - proof = proof_pipeline["name"] - proofs.append([proof, status_pretty_name]) + if proof_pipeline["name"] == "print_tool_versions": + continue + proofs.append([proof_pipeline["name"], status_pretty_name]) statuses = [["Status", "Count"]] for status, count in count_statuses.items(): statuses.append([status, str(count)]) @@ -102,18 +105,39 @@ def print_proof_results(out_file): Print 2 strings that summarize the proof results. When printing, each string will render as a GitHub flavored Markdown table. """ - print("## Summary of CBMC proof results") - try: - with open(out_file, encoding='utf-8') as run_json: - run_dict = json.load(run_json) - summaries = _get_status_and_proof_summaries( - run_dict) - for summary in summaries: - print(_get_rendered_table(summary)) - except Exception as ex: # pylint: disable=broad-except - logging.critical("Could not print results. Exception: %s", str(ex)) + output = "## Summary of CBMC proof results\n\n" + with open(out_file, encoding='utf-8') as run_json: + run_dict = json.load(run_json) + status_table, proof_table = _get_status_and_proof_summaries(run_dict) + for summary in (status_table, proof_table): + output += _get_rendered_table(summary) + + print(output) + sys.stdout.flush() + + github_summary_file = os.getenv("GITHUB_STEP_SUMMARY") + if github_summary_file: + with open(github_summary_file, "a") as handle: + print(output, file=handle) + handle.flush() + else: + logging.warning( + "$GITHUB_STEP_SUMMARY not set, not writing summary file") + + msg = ( + "Click the 'Summary' button to view a Markdown table " + "summarizing all proof results") + if run_dict["status"] != "success": + logging.error("Not all proofs passed.") + logging.error(msg) + sys.exit(1) + logging.info(msg) if __name__ == '__main__': args = get_args() - print_proof_results(args.run_file) + logging.basicConfig(format="%(levelname)s: %(message)s") + try: + print_proof_results(args.run_file) + except Exception as ex: # pylint: disable=broad-except + logging.critical("Could not print results. Exception: %s", str(ex)) diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index c172de31..3882b67b 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -223,7 +223,7 @@ def run_build(litani, jobs, fail_on_proof_failure, summarize): cmd.extend(["--out-file", str(out_file)]) logging.debug(" ".join(cmd)) - proc = subprocess.run(cmd, check=False) + proc = subprocess.run(cmd, check=False, timeout=360) if proc.returncode and not fail_on_proof_failure: logging.critical("Failed to run litani run-build") @@ -313,11 +313,15 @@ async def configure_proof_dirs( # pylint: disable=too-many-arguments profiling = [ "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else [] + env = dict(os.environ) + env["EXTERNAL_SAT_SOLVER"] = "kissat" + # Allow interactive tasks to preempt proof configuration proc = await asyncio.create_subprocess_exec( - "nice", "-n", "15", "make", *pools, + "nice", "-n", "15", "make", "EXTERNAL_SAT_SOLVER=kissat", *pools, *profiling, "-B", report_target, "" if debug else "--quiet", cwd=path, - stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE) + stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE, + env=env) stdout, stderr = await proc.communicate() logging.debug("returncode: %s", str(proc.returncode)) logging.debug("stdout:") @@ -334,22 +338,6 @@ async def configure_proof_dirs( # pylint: disable=too-many-arguments queue.task_done() -def add_tool_version_job(): - cmd = [ - "litani", "add-job", - "--command", "cbmc-starter-kit-print-tool-versions .", - "--description", "printing out tool versions", - "--phony-outputs", str(uuid.uuid4()), - "--pipeline-name", "print_tool_versions", - "--ci-stage", "report", - "--tags", "front-page-text", - ] - proc = subprocess.run(cmd) - if proc.returncode: - logging.critical("Could not add tool version printing job") - sys.exit(1) - - async def main(): # pylint: disable=too-many-locals args = get_args() set_up_logging(args.verbose) @@ -419,8 +407,6 @@ async def main(): # pylint: disable=too-many-locals await proof_queue.join() - add_tool_version_job() - print_counter(counter) print("", file=sys.stderr)