1#!/usr/bin/env python3
2#
3# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4#
5# Licensed under the Apache License, Version 2.0 (the "License"). You may not
6# use this file except in compliance with the License. A copy of the License is
7# located at
8#
9#     http://aws.amazon.com/apache2.0/
10#
11# or in the "license" file accompanying this file. This file is distributed on
12# an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express
13# or implied. See the License for the specific language governing permissions
14# and limitations under the License.
15
16
17import argparse
18import logging
19import math
20import os
21import pathlib
22import subprocess
23import sys
24
25
26DESCRIPTION = "Configure and run all CBMC proofs in parallel"
27# Keep this hard-wrapped at 70 characters, as it gets printed verbatim
28# in the terminal. 70 characters stops here -----------------------> |
29EPILOG = """
30This tool automates the process of running `make report` in each of
31the CBMC proof directories. The tool calculates the dependency graph
32of all tasks needed to build, run, and report on all the proofs, and
33executes these tasks in parallel.
34
35The tool is roughly equivalent to doing this:
36
37        litani init --project "Amazon FreeRTOS Plus TCP";
38
39        for proof in $(find . -name cbmc-batch.yaml); do
40            pushd $(dirname ${proof});
41            make report;
42            popd;
43        done
44
45        litani run-build;
46
47except that it is much faster and provides some convenience options.
48The CBMC CI runs this script with no arguments to build and run all
49proofs in parallel.
50
51The --no-standalone argument omits the `litani init` and `litani
52run-build`; use it when you want to add additional proof jobs, not
53just the CBMC ones. In that case, you would run `litani init`
54yourself; then run `run-cbmc-proofs --no-standalone`; add any
55additional jobs that you want to execute with `litani add-job`; and
56finally run `litani run-build`.
57"""
58
59
60def get_args():
61    pars = argparse.ArgumentParser(
62        description=DESCRIPTION, epilog=EPILOG,
63        formatter_class=argparse.RawDescriptionHelpFormatter)
64    for arg in [{
65            "flags": ["-j", "--parallel-jobs"],
66            "type": int,
67            "metavar": "N",
68            "help": "run at most N proof jobs in parallel",
69    }, {
70            "flags": ["--no-standalone"],
71            "action": "store_true",
72            "help": "only configure proofs: do not initialize nor run",
73    }, {
74            "flags": ["-p", "--proofs"],
75            "nargs": "+",
76            "metavar": "DIR",
77            "help": "only run proof in directory DIR (can pass more than one)",
78    }, {
79            "flags": ["--project-name"],
80            "metavar": "NAME",
81            "default": "Amazon FreeRTOS Plus TCP",
82            "help": "Project name for report. Default: %(default)s",
83    }, {
84            "flags": ["--verbose"],
85            "action": "store_true",
86            "help": "verbose output",
87    }]:
88        flags = arg.pop("flags")
89        pars.add_argument(*flags, **arg)
90    return pars.parse_args()
91
92
93def set_up_logging(verbose):
94    if verbose:
95        level = logging.DEBUG
96    else:
97        level = logging.WARNING
98    logging.basicConfig(
99        format="run-cbmc-proofs: %(message)s", level=level)
100
101
102def print_counter(counter):
103    print(
104        "\rConfiguring CBMC proofs: "
105        "{complete:{width}} / {total:{width}}".format(
106            **counter), end="", file=sys.stderr)
107
108
109def get_proof_dirs(proof_root, proof_list):
110    if proof_list is not None:
111        proofs_remaining = list(proof_list)
112    else:
113        proofs_remaining = []
114
115    for root, _, fyles in os.walk(proof_root):
116        proof_name = str(pathlib.Path(root).name)
117        if proof_list and proof_name not in proof_list:
118            continue
119        if proof_list and proof_name in proofs_remaining:
120            proofs_remaining.remove(proof_name)
121        if "cbmc-batch.yaml" in fyles:
122            yield pathlib.Path(root)
123
124    if proofs_remaining:
125        logging.error(
126            "The following proofs were not found: %s",
127            ", ".join(proofs_remaining))
128        sys.exit(1)
129
130
131def run_cmd(cmd, **args):
132    if "shell" in args and args["shell"]:
133        if not isinstance(cmd, str):
134            raise UserWarning("Command must be a string if shell=True")
135        str_cmd = cmd
136    else:
137        if not isinstance(cmd, list):
138            raise UserWarning("Command passed to run_cmd must be a list")
139        str_cmd = " ".join(cmd)
140
141    logging.info("Command: %s", str_cmd)
142
143    proc = subprocess.run(cmd, **args)
144
145    if proc.returncode:
146        logging.error("Command failed: %s", str_cmd)
147
148    return proc
149
150
151def run_build(jobs):
152    cmd = ["litani", "run-build"]
153    if jobs:
154        cmd.extend(["-j", str(jobs)])
155    run_cmd(cmd, check=True)
156
157
158def add_proof_jobs(proof_directory, proof_root):
159    proof_directory = pathlib.Path(proof_directory)
160    harnesses = [
161        f for f in os.listdir(proof_directory) if f.endswith("_harness.c")]
162    if not len(harnesses) == 1:
163        logging.error(
164            "Found %d harnesses in directory '%s'", len(harnesses),
165            proof_directory)
166        return False
167
168    # Neither the harness name nor the proof directory is unique enough,
169    # due to proof configurations. Use the relative path instead.
170    proof_name = str(proof_directory.relative_to(proof_root))
171
172    goto_binary = str(
173        (proof_directory / ("%s.goto" % harnesses[0][:-2])).resolve())
174
175    # Build goto-binary
176
177    run_cmd([
178        "litani", "add-job",
179        "--command", "make -B veryclean goto",
180        "--outputs", goto_binary,
181        "--pipeline-name", proof_name,
182        "--ci-stage", "build",
183        "--cwd", str(proof_directory),
184        "--description", ("%s: building goto-binary" % proof_name),
185    ], check=True)
186
187    # Run 3 CBMC tasks
188
189    cbmc_out = str(proof_directory / "cbmc.txt")
190    run_cmd([
191        "litani", "add-job",
192        "--command", "make cbmc",
193        "--inputs", goto_binary,
194        "--outputs", cbmc_out,
195        "--pipeline-name", proof_name,
196        "--ci-stage", "test",
197        "--tags", "stats-group:safety check",
198        # Make returns 2 if the underlying command exited abnormally
199        "--ignore-returns", "2",
200        "--cwd", str(proof_directory),
201        "--description", ("%s: running safety checks" % proof_name),
202    ], check=True)
203
204    property_out = str(proof_directory / "property.xml")
205    run_cmd([
206        "litani", "add-job",
207        "--command", "make property",
208        "--inputs", goto_binary,
209        "--outputs", property_out,
210        "--pipeline-name", proof_name,
211        "--ci-stage", "test",
212        "--cwd", str(proof_directory),
213        "--description", ("%s: printing properties" % proof_name),
214    ], check=True)
215
216    coverage_out = str(proof_directory / "coverage.xml")
217    run_cmd([
218        "litani", "add-job",
219        "--command", "make coverage",
220        "--inputs", goto_binary,
221        "--outputs", coverage_out,
222        "--pipeline-name", proof_name,
223        "--ci-stage", "test",
224        "--cwd", str(proof_directory),
225        "--tags", "stats-group:coverage computation",
226        "--description", ("%s: computing coverage" % proof_name),
227    ], check=True)
228
229    # Check whether the CBMC proof actually passed. More details in the
230    # Makefile rule for check-cbmc-result.
231    run_cmd([
232        "litani", "add-job",
233        "--command", "make check-cbmc-result",
234        "--inputs", cbmc_out,
235        "--pipeline-name", proof_name,
236        "--ci-stage", "report",
237        "--cwd", str(proof_directory),
238        "--description", ("%s: checking CBMC result" % proof_name),
239    ], check=True)
240
241    # Generate report
242    run_cmd([
243        "litani", "add-job",
244        "--command", "make report",
245        "--inputs", cbmc_out, property_out, coverage_out,
246        "--outputs", str(proof_directory / "html"),
247        "--pipeline-name", proof_name,
248        "--ci-stage", "report",
249        "--cwd", str(proof_directory),
250        "--tags", "stats-group:report generation",
251        "--description", ("%s: generating report" % proof_name),
252    ], check=True)
253
254    return True
255
256
257def configure_proof_dirs(proof_dirs, proof_root, counter):
258    for proof_dir in proof_dirs:
259        print_counter(counter)
260
261        success = add_proof_jobs(proof_dir, proof_root)
262
263        counter["pass" if success else "fail"].append(proof_dir)
264        counter["complete"] += 1
265
266
267def main():
268    args = get_args()
269    set_up_logging(args.verbose)
270
271    proof_root = pathlib.Path(__file__).resolve().parent
272
273    run_cmd(["./prepare.py"], check=True, cwd=str(proof_root))
274    if not args.no_standalone:
275        run_cmd(
276            ["litani", "init", "--project", args.project_name], check=True)
277
278    proof_dirs = list(get_proof_dirs(proof_root, args.proofs))
279    if not proof_dirs:
280        logging.error("No proof directories found")
281        sys.exit(1)
282
283    counter = {
284        "pass": [],
285        "fail": [],
286        "complete": 0,
287        "total": len(proof_dirs),
288        "width": int(math.log10(len(proof_dirs))) + 1
289    }
290
291    configure_proof_dirs(proof_dirs, proof_root, counter)
292
293    print_counter(counter)
294    print("", file=sys.stderr)
295
296    if counter["fail"]:
297        logging.error(
298            "Failed to configure the following proofs:\n%s", "\n".join(
299                [str(f) for f in counter["fail"]]))
300
301    if not args.no_standalone:
302        run_build(args.parallel_jobs)
303
304    out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest"
305    out_dir = out_sym.resolve()
306
307    local_copy = pathlib.Path("output")/"latest"
308    local_copy.parent.mkdir(exist_ok=True)
309    local_copy.symlink_to(out_dir)
310
311
312if __name__ == "__main__":
313    main()
314