Run VeriFast proofs in CI

FreeRTOS/Test/CBMC/proofs/.gitignore

@@ -7,4 +7,7 @@ cbmc-batch.yaml
 **/*.txt
 **/*.goto
 
+.litani_cache_dir
+Makefile.json
+
 !CMakeLists.txt

FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py

@@ -61,6 +61,7 @@ def get_args():
     pars = argparse.ArgumentParser(
         description=DESCRIPTION, epilog=EPILOG,
         formatter_class=argparse.RawDescriptionHelpFormatter)
+    tools = ["cbmc", "verifast"]
     for arg in [{
             "flags": ["-j", "--parallel-jobs"],
             "type": int,
@@ -80,6 +81,14 @@ def get_args():
             "metavar": "NAME",
             "default": "FreeRTOS",
             "help": "Project name for report. Default: %(default)s",
+    }, {
+            "flags": ["--verification-tool"],
+            "metavar": "T",
+            "help": "which verification tools to run. default: all of them, "
+                    "choices: %(choices)s",
+            "choices": tools,
+            "default": tools,
+            "nargs": "+",
     }, {
             "flags": ["--verbose"],
             "action": "store_true",
@@ -264,18 +273,8 @@ def configure_proof_dirs(proof_dirs, proof_root, counter):
         counter["complete"] += 1
 
 
-def main():
-    args = get_args()
-    set_up_logging(args.verbose)
-
-    proof_root = pathlib.Path(__file__).resolve().parent
-
-    run_cmd(["./prepare.py"], check=True, cwd=str(proof_root))
-    if not args.no_standalone:
-        run_cmd(
-            ["litani", "init", "--project", args.project_name], check=True)
-
-    proof_dirs = list(get_proof_dirs(proof_root, args.proofs))
+def add_cbmc_proofs(proof_root, proofs):
+    proof_dirs = list(get_proof_dirs(proof_root, proofs))
     if not proof_dirs:
         logging.error("No proof directories found")
         sys.exit(1)
@@ -298,10 +297,66 @@ def main():
             "Failed to configure the following proofs:\n%s", "\n".join(
                 [str(f) for f in counter["fail"]]))
 
+
+def add_verifast_proofs(verifast_root):
+    with open(verifast_root / "proof-configuration") as handle:
+        for line in handle:
+            line = line.strip()
+            if line.startswith("*") or line.startswith("/*") or not line:
+                continue
+            parts = line.split()
+            coverage, proof_name, flags = parts[0], parts[1], ""
+            if len(parts) > 2:
+                flags = " ".join(parts[2:])
+            fyle = verifast_root / proof_name
+
+            out_file = verifast_root / "out" / f"{proof_name}.stdout"
+            cmd = f"verifast -I include -c {flags} {fyle.resolve()}"
+
+            run_cmd([
+                "litani", "add-job",
+                "--command", cmd,
+                "--outputs", str(out_file),
+                "--stdout-file", str(out_file),
+                "--pipeline-name", f"VeriFast/{proof_name}",
+                "--ci-stage", "test",
+                "--cwd", str(verifast_root),
+                "--tags", "tool:verifast",
+                "--description", f"{proof_name}: running VeriFast",
+            ], check=True)
+
+            run_cmd([
+                "litani", "add-job",
+                "--command", f"grep '{coverage} statements verified' < {out_file}",
+                "--inputs", str(out_file),
+                "--phony-outputs", f"{proof_name}_coverage_result",
+                "--pipeline-name", f"VeriFast/{proof_name}",
+                "--ci-stage", "report",
+                "--cwd", str(verifast_root),
+                "--tags", "tool:verifast",
+                "--description", f"{proof_name}: checking VeriFast coverage",
+            ], check=True)
+
+
+def main():
+    args = get_args()
+    set_up_logging(args.verbose)
+
+    proof_root = pathlib.Path(__file__).resolve().parent
+    run_cmd(["./prepare.py"], check=True, cwd=str(proof_root))
+
+    if not args.no_standalone:
+        run_cmd(
+            ["litani", "init", "--project", args.project_name], check=True)
+
+    if "cbmc" in args.verification_tool:
+        add_cbmc_proofs(proof_root, args.proofs)
+    if "verifast" in args.verification_tool:
+        add_verifast_proofs(proof_root.parent.parent / "VeriFast")
+
     if not args.no_standalone:
         run_build(args.parallel_jobs)
 
 
 if __name__ == "__main__":
     main()
-

FreeRTOS/Test/VeriFast/.gitignore

@@ -0,0 +1 @@
+out

FreeRTOS/Test/VeriFast/README.md

@@ -56,6 +56,7 @@ Then click `Verify` and `Verify Program` (or press F5). Note that the following
 proofs require arithmetic overflow checking to be turned off (click `Verify`
 and uncheck `Check arithmetic overflow`).
 
+  - `queue/create.c`
   - `queue/prvCopyDataToQueue.c`
   - `queue/xQueueGenericSendFromISR.c`
   - `queue/xQueueReceiveFromISR.c`
@@ -80,22 +81,29 @@ queue/xQueueGenericSend.c
 0 errors found (335 statements verified)
 ```
 
+To make the proof run as part of the regression suite (see below) in continuous
+integration, add the name of the proof to the `proof-configuration` file
+together with its coverage number.
+
+
 ## Running proof regression
 
-The following will check all proofs in the repo along with a statement coverage
-regression.
+The VeriFast proofs are run together with the CBMC proofs, with the results
+collected on a single dashboard. Change into the Test/CBMC/proof directory and
+run
 
 ```
-$ VERIFAST=/path/to/verifast make
+$ run-cbmc-proofs.py
 ```
 
-If you have made changes to the proofs so the statement coverage no longer
-matches then you can temporarily turn off coverage checking:
+This runs all the proofs in parallel. To run only the VeriFast proofs, you can
+run
 
 ```
-$ VERIFAST=/path/to/verifast NO_COVERAGE=1 make
+$ run-cbmc-proofs.py --verification-tool verifast
 ```
 
+
 ## Annotation burden
 
 VeriFast can emit statistics about the number of source code lines and

FreeRTOS/Test/VeriFast/docs/signoff.md

@@ -71,16 +71,19 @@ A side-by-side diff with respect to the source code can be generated. See
 The main queue changes are:
 
   - merge cTxLock and cRxLock critical regions: under approximate queue
-	unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
+    unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
     single critical region instead of two separate critical regions. In
-	practice, this is not an issue since no ISR function reads-from both
+    practice, this is not an issue since no ISR function reads-from both
     cTxLock and cRxLock.
   - model single malloc of struct and buffer: split the single malloc of the
     queue struct and storage into two separate mallocs.
   - xQueueGenericReset happens-before concurrent behavior: assume that queue
     initialisation is not concurrent.
   - do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
-    the list structs of the queue implementation
+    the list structs of the queue implementation.
+  - we do not use the prvIncrementQueueTxLock or prvIncrementQueueRxLock macros
+    in xQueueGenericSendFromISR and xQueueReceiveFromISR functions.
+  - we prove an older version of xQueueGenericReset that always resets a queue
 
 The main list changes are:
 

FreeRTOS/Test/VeriFast/include/proof/common.gh

@@ -1,6 +1,6 @@
 /*
  * FreeRTOS V202112.00
- * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in