diff --git a/.gitmodules b/.gitmodules index 4f71488570..6e19c98a7a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -40,9 +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 [submodule "FreeRTOS-Plus/Source/Application-Protocols/coreMQTT-Agent"] path = FreeRTOS-Plus/Source/Application-Protocols/coreMQTT-Agent url = https://github.com/FreeRTOS/coreMQTT-Agent.git diff --git a/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py index c0f8a48c88..f95de775ba 100755 --- a/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py +++ b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py @@ -148,19 +148,14 @@ def run_cmd(cmd, **args): return proc -def run_build(litani, jobs): - cmd = [str(litani), "run-build"] +def run_build(jobs): + cmd = ["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): +def add_proof_jobs(proof_directory, proof_root): proof_directory = pathlib.Path(proof_directory) harnesses = [ f for f in os.listdir(proof_directory) if f.endswith("_harness.c")] @@ -180,7 +175,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): # Build goto-binary run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make -B veryclean goto", "--outputs", goto_binary, "--pipeline-name", proof_name, @@ -193,7 +188,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): cbmc_out = str(proof_directory / "cbmc.txt") run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make cbmc", "--inputs", goto_binary, "--outputs", cbmc_out, @@ -208,7 +203,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): property_out = str(proof_directory / "property.xml") run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make property", "--inputs", goto_binary, "--outputs", property_out, @@ -220,7 +215,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): coverage_out = str(proof_directory / "coverage.xml") run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make coverage", "--inputs", goto_binary, "--outputs", coverage_out, @@ -234,7 +229,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): # Check whether the CBMC proof actually passed. More details in the # Makefile rule for check-cbmc-result. run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make check-cbmc-result", "--inputs", cbmc_out, "--pipeline-name", proof_name, @@ -245,7 +240,7 @@ def add_proof_jobs(proof_directory, proof_root, litani): # Generate report run_cmd([ - str(litani), "add-job", + "litani", "add-job", "--command", "make report", "--inputs", cbmc_out, property_out, coverage_out, "--outputs", str(proof_directory / "html"), @@ -259,11 +254,11 @@ def add_proof_jobs(proof_directory, proof_root, litani): return True -def configure_proof_dirs(proof_dirs, proof_root, counter, litani): +def configure_proof_dirs(proof_dirs, proof_root, counter): for proof_dir in proof_dirs: print_counter(counter) - success = add_proof_jobs(proof_dir, proof_root, litani) + success = add_proof_jobs(proof_dir, proof_root) counter["pass" if success else "fail"].append(proof_dir) counter["complete"] += 1 @@ -274,12 +269,11 @@ def main(): set_up_logging(args.verbose) proof_root = pathlib.Path(__file__).resolve().parent - litani = get_litani_path(proof_root) run_cmd(["./prepare.py"], check=True, cwd=str(proof_root)) if not args.no_standalone: run_cmd( - [str(litani), "init", "--project", args.project_name], check=True) + ["litani", "init", "--project", args.project_name], check=True) proof_dirs = list(get_proof_dirs(proof_root, args.proofs)) if not proof_dirs: @@ -294,7 +288,7 @@ def main(): "width": int(math.log10(len(proof_dirs))) + 1 } - configure_proof_dirs(proof_dirs, proof_root, counter, litani) + configure_proof_dirs(proof_dirs, proof_root, counter) print_counter(counter) print("", file=sys.stderr) @@ -305,8 +299,9 @@ def main(): [str(f) for f in counter["fail"]])) if not args.no_standalone: - run_build(litani, args.parallel_jobs) + run_build(args.parallel_jobs) if __name__ == "__main__": main() + diff --git a/FreeRTOS/Test/litani b/FreeRTOS/Test/litani deleted file mode 160000 index 8b4a4ffb33..0000000000 --- a/FreeRTOS/Test/litani +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 8b4a4ffb330119c7f4d9abd5996313eccd2c4ab1 diff --git a/README.md b/README.md index 40fa5ab469..9bb4156ae9 100644 --- a/README.md +++ b/README.md @@ -62,3 +62,10 @@ The [FreeRTOS/coreMQTT-Agent-Demos](https://github.com/FreeRTOS/coreMQTT-Agent-D The demos show a single MQTT connection usage between multiple application tasks for interacting with AWS services (including [Over-the-air-Updates](https://docs.aws.amazon.com/freertos/latest/userguide/freertos-ota-dev.html), [Device Shadow](https://docs.aws.amazon.com/iot/latest/developerguide/iot-device-shadows.html), [Device Defender](https://docs.aws.amazon.com/iot/latest/developerguide/device-defender.html)) alongside performing simple Publish-Subscribe operations. +## CBMC + +The `FreeRTOS/Test/CBMC/proofs` directory contains CBMC proofs. + +To learn more about CBMC and proofs specifically, review the training material [here](https://model-checking.github.io/cbmc-training). + +In order to run these proofs you will need to install CBMC and other tools by following the instructions [here](https://model-checking.github.io/cbmc-training/installation.html).