1#!/usr/bin/env python3
2
3"""
4Write a ninja build file to generate reports for cbmc proofs.
5
6Given a list of folders containing cbmc proofs, write a ninja build
7file the generate reports for these proofs.  The list of folders may
8be given on the command line, in a json file, or found in the file
9system.
10"""
11
12# Add task pool
13
14import sys
15import os
16import platform
17import argparse
18import json
19
20################################################################
21# The command line parser
22
23def argument_parser():
24    """Return the command line parser."""
25
26    parser = argparse.ArgumentParser(
27        description='Generate ninja build file for cbmc proofs.',
28        epilog="""
29            Given a list of folders containing cbmc proofs, write a ninja build
30            file the generate reports for these proofs.  The list of folders may
31            be given on the command line, in a json file, or found in the file
32            system.
33            In the json file, there should be a dict mapping the key "proofs"
34            to a list of folders containing proofs.
35            The file system, all folders folders under the current directory
36            containing a file named 'cbmc-batch.yaml' is considered a
37            proof folder.
38            This script assumes that the proof is driven by a Makefile
39            with targets goto, cbmc, coverage, property, and report.
40            This script does not work with Windows and Visual Studio.
41        """
42    )
43    parser.add_argument('folders', metavar='PROOF', nargs='*',
44                        help='Folder containing a cbmc proof')
45    parser.add_argument('--proofs', metavar='JSON',
46                        help='Json file listing folders containing cbmc proofs')
47    return parser
48
49################################################################
50# The list of folders containing proofs
51#
52# The list of folders will be taken from
53# 1. the list PROOFS defined here or
54# 2. the command line
55# 3. the json file specified on the command line containing a
56#    dict mapping the key JSON_KEY to a list of folders
57# 4. the folders below the current directory containing
58#    a file named FS_KEY
59#
60
61PROOFS = [
62]
63
64JSON_KEY = 'proofs'
65FS_KEY = 'cbmc-batch.yaml'
66
67def find_proofs_in_json_file(filename):
68    """Read the list of folders containing proofs from a json file."""
69
70    if not filename:
71        return []
72    try:
73        with open(filename) as proofs:
74            return json.load(proofs)[JSON_KEY]
75    except (FileNotFoundError, KeyError):
76        raise UserWarning("Can't find key {} in json file {}".format(JSON_KEY, filename))
77    except json.decoder.JSONDecodeError:
78        raise UserWarning("Can't parse json file {}".format(filename))
79
80def find_proofs_in_filesystem():
81    """Locate the folders containing proofs in the filesystem."""
82
83    proofs = []
84    for root, _, files in os.walk('.'):
85        if FS_KEY in files:
86            proofs.append(os.path.normpath(root))
87    return proofs
88
89################################################################
90# The strings used to write sections of the ninja file
91
92NINJA_RULES = """
93################################################################
94# task pool to force sequential builds of goto binaries
95
96pool goto_pool
97  depth = 1
98
99################################################################
100# proof target rules
101
102rule build_goto
103  command = make -C ${folder} goto
104  pool = goto_pool
105
106rule build_cbmc
107  command = make -C ${folder} cbmc
108
109rule build_coverage
110  command = make -C ${folder} coverage
111
112rule build_property
113  command = make -C ${folder} property
114
115rule build_report
116  command = make -C ${folder} report
117
118rule clean_folder
119  command = make -C ${folder} clean
120
121rule veryclean_folder
122  command = make -C ${folder} veryclean
123
124rule open_proof
125  command = open ${folder}/html/index.html
126
127"""
128
129NINJA_BUILDS = """
130################################################################
131# {folder} proof targets
132
133build {folder}/{entry}.goto: build_goto
134  folder={folder}
135
136build {folder}/cbmc.txt: build_cbmc {folder}/{entry}.goto
137  folder={folder}
138
139build {folder}/coverage.xml: build_coverage {folder}/{entry}.goto
140  folder={folder}
141
142build {folder}/property.xml: build_property {folder}/{entry}.goto
143  folder={folder}
144
145build {folder}/html/index.html: build_report {folder}/{entry}.goto {folder}/cbmc.txt {folder}/coverage.xml {folder}/property.xml
146  folder={folder}
147
148build clean_{folder}: clean_folder
149  folder={folder}
150
151build veryclean_{folder}: veryclean_folder
152  folder={folder}
153
154build open_{folder}: open_proof
155  folder={folder}
156
157build {folder}: phony {folder}/html/index.html
158
159default {folder}
160
161"""
162
163NINJA_GLOBALS = """
164################################################################
165# global targets
166
167build clean: phony {clean_targets}
168
169build veryclean: phony {veryclean_targets}
170
171build open: phony {open_targets}
172"""
173
174################################################################
175# The main function
176
177def get_entry(folder):
178    """Find the name of the proof in the proof Makefile."""
179
180    with open('{}/Makefile'.format(folder)) as makefile:
181        for line in makefile:
182            if line.strip().lower().startswith('entry'):
183                return line[line.find('=')+1:].strip()
184            if line.strip().lower().startswith('h_entry'):
185                return line[line.find('=')+1:].strip()
186    raise UserWarning("Can't find ENTRY in {}/Makefile".format(folder))
187
188def write_ninja_build_file():
189    """Write a ninja build file to generate proof results."""
190
191    if platform.system().lower() == 'windows':
192        print("This script does not run on Windows.")
193        sys.exit()
194
195    args = argument_parser().parse_args()
196
197    proofs = (PROOFS or
198              args.folders or
199              find_proofs_in_json_file(args.proofs) or
200              find_proofs_in_filesystem())
201
202    with open('build.ninja', 'w') as ninja:
203        ninja.write(NINJA_RULES)
204        for proof in proofs:
205            entry = get_entry(proof)
206            ninja.write(NINJA_BUILDS.format(folder=proof, entry=entry))
207        targets = lambda kind, folders: ' '.join(
208            ['{}_{}'.format(kind, folder) for folder in folders]
209        )
210        ninja.write(NINJA_GLOBALS.format(
211            clean_targets=targets('clean', proofs),
212            veryclean_targets=targets('veryclean', proofs),
213            open_targets=targets('open', proofs)
214        ))
215
216################################################################
217
218if __name__ == "__main__":
219    write_ninja_build_file()
220