Add CBMC-running GitHub Action;

karkhaz · karkhaz · commit 48ccceb4bc04 · 2023-03-10T18:35:32.000Z
This commit adds a GitHub Action that runs the CBMC proofs in this
repository upon pushes and pull requests
diff --git 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
@@ -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
@@ -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
@@ -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_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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 = [
+        "<table>",
+        '<tr><td colspan="2" style="font-weight: bold">Tool Versions</td></tr>',
+    ]
+    for tool, version in table.items():
+        if version:
+            v_str = f'<code><pre style="margin: 0">{version}</pre></code>'
+        else:
+            v_str = '<em>not found</em>'
+        lines.append(
+            f'<tr><td style="font-weight: bold; padding-right: 1em; '
+            f'text-align: right;">{tool}:</td>'
+            f'<td>{v_str}</td></tr>')
+    lines.append("</table>")
+    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
@@ -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
@@ -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)
 
