From f6dff3fea38219a825870fc923f8d13e8540ca51 Mon Sep 17 00:00:00 2001 From: Carl Lundin <53273776+lundinc2@users.noreply.github.com> Date: Fri, 12 Feb 2021 10:21:07 -0800 Subject: Add Litani to run CBMC proofs (#501) Update to out of source makefile build and add run-cbmc-proofs.py CBMC proofs can now be run with Litani with the command "./run-cbmc-proofs.py" Based on commits: * 1646301 - Ignore CBMC proof failures, fail the build later (4 months ago) * 7e8c91a - Fix Makefile prerequisite symbol for CBMC proofs (4 months ago) * bee04be - Enable CBMC proofs to run in CI (4 months ago) Found in https://github.com/FreeRTOS/FreeRTOS-Plus-TCP --- .github/scripts/core_checker.py | 3 +- .gitmodules | 3 + FreeRTOS/Test/CBMC/proofs/Makefile.template | 48 ++-- FreeRTOS/Test/CBMC/proofs/MakefileLinux.json | 2 +- FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py | 313 +++++++++++++++++++++++++++ FreeRTOS/Test/litani | 1 + 6 files changed, 351 insertions(+), 19 deletions(-) create mode 100755 FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py create mode 160000 FreeRTOS/Test/litani diff --git a/.github/scripts/core_checker.py b/.github/scripts/core_checker.py index cb731c1f1..7ac053eeb 100755 --- a/.github/scripts/core_checker.py +++ b/.github/scripts/core_checker.py @@ -261,7 +261,8 @@ FREERTOS_IGNORED_PATTERNS = [ FREERTOS_IGNORED_FILES = [ 'fyi-another-way-to-ignore-file.txt', 'mbedtls_config.h', - 'requirements.txt' + 'requirements.txt', + 'run-cbmc-proofs.py' ] FREERTOS_HEADER = [ diff --git a/.gitmodules b/.gitmodules index 84723b4d1..902969180 100644 --- a/.gitmodules +++ b/.gitmodules @@ -40,3 +40,6 @@ [submodule "FreeRTOS-Plus/ThirdParty/wolfSSL"] path = FreeRTOS-Plus/ThirdParty/wolfSSL url = https://github.com/wolfSSL/wolfssl.git +[submodule "FreeRTOS/Test/aws-build-accumulator"] + path = FreeRTOS/Test/litani + url = https://github.com/awslabs/aws-build-accumulator.git diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index 0e47abe4d..fa5558f7f 100644 --- a/FreeRTOS/Test/CBMC/proofs/Makefile.template +++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template @@ -47,16 +47,6 @@ INSTFLAGS = \ $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \ # empty -# ____________________________________________________________________ -# Rules -# -# Rules for building a:FR object files. These are not harness-specific, -# and several harnesses might depend on a particular a:FR object, so -# define them all once here. - -@RULE_GOTO@ - $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ - # ____________________________________________________________________ # Rules # @@ -73,14 +63,27 @@ unpatch: # # Rules for building the CBMC harness -queue_datastructure.h: $(H_OBJS_EXCEPT_HARNESS) - python3 @TYPE_HEADER_SCRIPT@ --binary $(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c +C_SOURCES = $(patsubst %.goto,%.c,$(H_OBJS_EXCEPT_HARNESS)) -$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER) +# Build each goto-binary out-of-source (i.e. in a 'gotos' directory +# underneath each proof directory, to make it safe to build all proofs +# in parallel +OOS_OBJS = $(patsubst %.c,gotos/%.goto,$(C_SOURCES)) + +CWD=$(abspath .) + +gotos/%.goto: %.c + mkdir -p $(dir $@) $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@ -$(ENTRY)1.goto: $(OBJS) - $(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness $(OBJS) +queue_datastructure.h: gotos/$(FREERTOS)/Source/queue.goto + python3 @TYPE_HEADER_SCRIPT@ --binary $(CWD)/gotos$(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c + +$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER) + $(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) $(ENTRY)_harness.c + +$(ENTRY)1.goto: $(ENTRY)_harness.goto $(OOS_OBJS) + $(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness @RULE_INPUT@ $(ENTRY)2.goto: $(ENTRY)1.goto $(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \ @@ -111,10 +114,13 @@ $(ENTRY).goto: $(ENTRY)5.goto goto: $(MAKE) patch - $(MAKE) $(ENTRY).goto + $(MAKE) -B $(ENTRY).goto +# Ignore the return code for CBMC, so that we can still generate the +# report if the proof failed. If the proof failed, we separately fail +# the entire job using the check-cbmc-result rule. cbmc.txt: $(ENTRY).goto - - cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 + -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 @@ -139,6 +145,13 @@ report: cbmc.txt property.xml coverage.xml --property property.xml \ --block coverage.xml +# This rule depends only on cbmc.txt and has no dependents, so it will +# not block the report from being generated if it fails. This rule is +# intended to fail if and only if the CBMC safety check that emits +# cbmc.txt yielded a proof failure. +check-cbmc-result: cbmc.txt + grep -e "^VERIFICATION SUCCESSFUL" $^ + # ____________________________________________________________________ # Rules # @@ -154,6 +167,7 @@ clean: veryclean: clean @RM_RECURSIVE@ html + @RM_RECURSIVE@ gotos distclean: veryclean cd $(PROOFS)/../patches && ./unpatch.py diff --git a/FreeRTOS/Test/CBMC/proofs/MakefileLinux.json b/FreeRTOS/Test/CBMC/proofs/MakefileLinux.json index 08442a2ab..a4e96aebe 100644 --- a/FreeRTOS/Test/CBMC/proofs/MakefileLinux.json +++ b/FreeRTOS/Test/CBMC/proofs/MakefileLinux.json @@ -10,7 +10,7 @@ "-o" ], "RULE_INPUT": [ - "$<" + "$^" ], "RULE_OUTPUT": [ "$@" diff --git a/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py new file mode 100755 index 000000000..539126283 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You may not +# use this file except in compliance with the License. A copy of the License is +# located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is distributed on +# an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express +# or implied. See the License for the specific language governing permissions +# and limitations under the License. + + +import argparse +import logging +import math +import os +import pathlib +import subprocess +import sys + + +DESCRIPTION = "Configure and run all CBMC proofs in parallel" +# Keep this hard-wrapped at 70 characters, as it gets printed verbatim +# in the terminal. 70 characters stops here -----------------------> | +EPILOG = """ +This tool automates the process of running `make report` in each of +the CBMC proof directories. The tool calculates the dependency graph +of all tasks needed to build, run, and report on all the proofs, and +executes these tasks in parallel. + +The tool is roughly equivalent to doing this: + + litani init --project "FreeRTOS"; + + for proof in $(find . -name cbmc-batch.yaml); do + pushd $(dirname ${proof}); + make report; + popd; + done + + litani run-build; + +except that it is much faster and provides some convenience options. +The CBMC CI runs this script with no arguments to build and run all +proofs in parallel. + +The --no-standalone argument omits the `litani init` and `litani +run-build`; use it when you want to add additional proof jobs, not +just the CBMC ones. In that case, you would run `litani init` +yourself; then run `run-cbmc-proofs --no-standalone`; add any +additional jobs that you want to execute with `litani add-job`; and +finally run `litani run-build`. +""" + + +def get_args(): + pars = argparse.ArgumentParser( + description=DESCRIPTION, epilog=EPILOG, + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in [{ + "flags": ["-j", "--parallel-jobs"], + "type": int, + "metavar": "N", + "help": "run at most N proof jobs in parallel", + }, { + "flags": ["--no-standalone"], + "action": "store_true", + "help": "only configure proofs: do not initialize nor run", + }, { + "flags": ["-p", "--proofs"], + "nargs": "+", + "metavar": "DIR", + "help": "only run proof in directory DIR (can pass more than one)", + }, { + "flags": ["--project-name"], + "metavar": "NAME", + "default": "FreeRTOS", + "help": "Project name for report. Default: %(default)s", + }, { + "flags": ["--verbose"], + "action": "store_true", + "help": "verbose output", + }]: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(verbose): + if verbose: + level = logging.DEBUG + else: + level = logging.WARNING + logging.basicConfig( + format="run-cbmc-proofs: %(message)s", level=level) + + +def print_counter(counter): + print( + "\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format( + **counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list): + if proof_list is not None: + proofs_remaining = list(proof_list) + else: + proofs_remaining = [] + + for root, _, fyles in os.walk(proof_root): + proof_name = str(pathlib.Path(root).name) + if proof_list and proof_name not in proof_list: + continue + if proof_list and proof_name in proofs_remaining: + proofs_remaining.remove(proof_name) + if "cbmc-batch.yaml" in fyles: + yield pathlib.Path(root) + + if proofs_remaining: + logging.error( + "The following proofs were not found: %s", + ", ".join(proofs_remaining)) + sys.exit(1) + + +def run_cmd(cmd, **args): + if "shell" in args and args["shell"]: + if not isinstance(cmd, str): + raise UserWarning("Command must be a string if shell=True") + str_cmd = cmd + else: + if not isinstance(cmd, list): + raise UserWarning("Command passed to run_cmd must be a list") + str_cmd = " ".join(cmd) + + logging.info("Command: %s", str_cmd) + + proc = subprocess.run(cmd, **args) + + if proc.returncode: + logging.error("Command failed: %s", str_cmd) + + return proc + + +def run_build(litani, jobs): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + + run_cmd(cmd, check=True) + + +def get_litani_path(proof_root): + return proof_root.parent.parent / "litani" / "litani" + + +def add_proof_jobs(proof_directory, proof_root, litani): + proof_directory = pathlib.Path(proof_directory) + harnesses = [ + f for f in os.listdir(proof_directory) if f.endswith("_harness.c")] + if not len(harnesses) == 1: + logging.error( + "Found %d harnesses in directory '%s'", len(harnesses), + proof_directory) + return False + + # Neither the harness name nor the proof directory is unique enough, + # due to proof configurations. Use the relative path instead. + proof_name = str(proof_directory.relative_to(proof_root)) + + goto_binary = str( + (proof_directory / ("%s.goto" % harnesses[0][:-2])).resolve()) + + # Build goto-binary + + run_cmd([ + str(litani), "add-job", + "--command", "make -B veryclean goto", + "--outputs", goto_binary, + "--pipeline-name", proof_name, + "--ci-stage", "build", + "--cwd", str(proof_directory), + "--description", ("%s: building goto-binary" % proof_name), + ], check=True) + + # Run 3 CBMC tasks + + cbmc_out = str(proof_directory / "cbmc.txt") + run_cmd([ + str(litani), "add-job", + "--command", "make cbmc", + "--inputs", goto_binary, + "--outputs", cbmc_out, + "--pipeline-name", proof_name, + "--ci-stage", "test", + "--tags", "stats-group:safety check", + # Make returns 2 if the underlying command exited abnormally + "--ignore-returns", "2", + "--cwd", str(proof_directory), + "--description", ("%s: running safety checks" % proof_name), + ], check=True) + + property_out = str(proof_directory / "property.xml") + run_cmd([ + str(litani), "add-job", + "--command", "make property", + "--inputs", goto_binary, + "--outputs", property_out, + "--pipeline-name", proof_name, + "--ci-stage", "test", + "--cwd", str(proof_directory), + "--description", ("%s: printing properties" % proof_name), + ], check=True) + + coverage_out = str(proof_directory / "coverage.xml") + run_cmd([ + str(litani), "add-job", + "--command", "make coverage", + "--inputs", goto_binary, + "--outputs", coverage_out, + "--pipeline-name", proof_name, + "--ci-stage", "test", + "--cwd", str(proof_directory), + "--tags", "stats-group:coverage computation", + "--description", ("%s: computing coverage" % proof_name), + ], check=True) + + # Check whether the CBMC proof actually passed. More details in the + # Makefile rule for check-cbmc-result. + run_cmd([ + str(litani), "add-job", + "--command", "make check-cbmc-result", + "--inputs", cbmc_out, + "--pipeline-name", proof_name, + "--ci-stage", "report", + "--cwd", str(proof_directory), + "--description", ("%s: checking CBMC result" % proof_name), + ], check=True) + + # Generate report + run_cmd([ + str(litani), "add-job", + "--command", "make report", + "--inputs", cbmc_out, property_out, coverage_out, + "--outputs", str(proof_directory / "html"), + "--pipeline-name", proof_name, + "--ci-stage", "report", + "--cwd", str(proof_directory), + "--tags", "stats-group:report generation", + "--description", ("%s: generating report" % proof_name), + ], check=True) + + return True + + +def configure_proof_dirs(proof_dirs, proof_root, counter, litani): + for proof_dir in proof_dirs: + print_counter(counter) + + success = add_proof_jobs(proof_dir, proof_root, litani) + + counter["pass" if success else "fail"].append(proof_dir) + counter["complete"] += 1 + + +def main(): + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(__file__).resolve().parent + litani = get_litani_path(proof_root) + + if not args.no_standalone: + run_cmd( + ["./prepare.py"], check=True, cwd=str(proof_root)) + run_cmd( + [str(litani), "init", "--project", args.project_name], check=True) + + proof_dirs = list(get_proof_dirs(proof_root, args.proofs)) + if not proof_dirs: + logging.error("No proof directories found") + sys.exit(1) + + counter = { + "pass": [], + "fail": [], + "complete": 0, + "total": len(proof_dirs), + "width": int(math.log10(len(proof_dirs))) + 1 + } + + configure_proof_dirs(proof_dirs, proof_root, counter, litani) + + print_counter(counter) + print("", file=sys.stderr) + + if counter["fail"]: + logging.error( + "Failed to configure the following proofs:\n%s", "\n".join( + [str(f) for f in counter["fail"]])) + + if not args.no_standalone: + run_build(litani, args.parallel_jobs) + + +if __name__ == "__main__": + main() diff --git a/FreeRTOS/Test/litani b/FreeRTOS/Test/litani new file mode 160000 index 000000000..3fc5e02bc --- /dev/null +++ b/FreeRTOS/Test/litani @@ -0,0 +1 @@ +Subproject commit 3fc5e02bc17483352546ac4c81078fde64cab674 -- cgit v1.2.1