Skip to content

Commit

Permalink
Copy CBMC output directory to CI location
Browse files Browse the repository at this point in the history
This commit ensures that the output directory for CBMC proofs is in the
correct location expected by the FreeRTOS CI-CD repository.
  • Loading branch information
karkhaz committed Mar 10, 2023
1 parent bc30def commit 6d8af85
Show file tree
Hide file tree
Showing 3 changed files with 82 additions and 2 deletions.
74 changes: 74 additions & 0 deletions test/cbmc/proofs/lib/print_tool_versions.py
Original file line number Diff line number Diff line change
@@ -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()
File renamed without changes.
10 changes: 8 additions & 2 deletions test/cbmc/proofs/run-cbmc-proofs.py
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ def run_build(jobs):
cmd = ["litani", "run-build"]
if jobs:
cmd.extend(["-j", str(jobs)])
run_cmd(cmd, check=True, timeout=3600)
run_cmd(cmd, check=True)


def add_proof_jobs(proof_directory, proof_root):
Expand Down Expand Up @@ -301,7 +301,13 @@ def main():
if not args.no_standalone:
run_build(args.parallel_jobs)

out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest"
out_dir = out_sym.resolve()

local_copy = pathlib.Path("output")/"latest"
local_copy.parent.mkdir(exist_ok=True)
local_copy.symlink_to(out_dir)


if __name__ == "__main__":
main()

0 comments on commit 6d8af85

Please sign in to comment.