xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/make_common_makefile.py (revision 1ab6eb88857cf1011bf1f8349b43a1c34c7ced0f) 
1#!/usr/bin/env python3
2#
3# Generation of common Makefile for CBMC proofs.
4#
5# Copyright (C) 2022 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
6#
7# Permission is hereby granted, free of charge, to any person obtaining a copy
8# of this software and associated documentation files (the "Software"), to deal
9# in the Software without restriction, including without limitation the rights
10# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
11# copies of the Software, and to permit persons to whom the Software is
12# furnished to do so, subject to the following conditions:
13#
14# The above copyright notice and this permission notice shall be included in all
15# copies or substantial portions of the Software.
16#
17# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
18# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
19# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
20# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
21# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
22# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
23# SOFTWARE.
24
25from pprint import pprint
26import json
27import sys
28import re
29import os
30import argparse
31
32def cleanup_whitespace(string):
33    return re.sub('\s+', ' ', string.strip())
34
35################################################################
36# Operating system specific values
37
38platform_definitions = {
39    "linux": {
40        "platform": "linux",
41        "separator": "/",
42        "define": "-D",
43        "include": "-I",
44    },
45    "macos": {
46        "platform": "darwin",
47        "separator": "/",
48        "define": "-D",
49        "include": "-I",
50    },
51    "windows": {
52        "platform": "win32",
53        "separator": "\\",
54        "define": "/D",
55        "include": "/I",
56    },
57}
58
59
60def default_platform():
61    for platform, definition in platform_definitions.items():
62        if sys.platform == definition["platform"]:
63            return platform
64    return "linux"
65
66
67def patch_path_separator(opsys, string):
68    from_separator = '/'
69    to_separator = platform_definitions[opsys]["separator"]
70
71    def escape_separator(string):
72        return string.split(from_separator + from_separator)
73
74    def change_separator(string):
75        return string.replace(from_separator, to_separator)
76
77    return from_separator.join([change_separator(escaped)
78                                for escaped in escape_separator(string)])
79
80def patch_compile_output(opsys, line, key, value):
81    if opsys != "windows":
82        return line
83
84    if key in ["COMPILE_ONLY", "COMPILE_LINK"] and value is not None:
85        if value[-1] == '/Fo':
86            return re.sub('/Fo\s+', '/Fo', line)
87        if value[-1] == '/Fe':
88            return re.sub('/Fe\s+', '/Fe', line)
89    return line
90
91################################################################
92# Argument parsing
93#
94
95def get_arguments():
96    parser = argparse.ArgumentParser()
97    parser.add_argument(
98        "--system",
99        metavar="OS",
100        choices=platform_definitions,
101        default=str(default_platform()),
102        help="Generate makefiles for operating system OS"
103    )
104    return parser.parse_args()
105
106################################################################
107# Variable definitions
108#
109# JSON files give variable definitions for common, operating system,
110# and harness specfic values
111#
112
113def read_variable_definitions(filename):
114    variable = {}
115    with open(filename) as _file:
116        for key, values in json.load(_file).items():
117            variable[cleanup_whitespace(key)] = [cleanup_whitespace(value)
118                                                 for value in values]
119    return variable
120
121def find_definition_once(key, defines, prefix=None):
122
123    # Try looking up key with and without prefix
124    prefix = "{}_".format(prefix.rstrip('_')) if prefix else ""
125    key2 = key[len(prefix):] if key.startswith(prefix) else prefix + key
126
127    for _key in [key, key2]:
128        _value = defines.get(_key)
129        if _value is not None:
130            return _value
131
132    return None
133
134def find_definition(key, defines):
135    common_defines, opsys_defines, harness_defines = defines
136    return (find_definition_once(key, harness_defines, "H") or
137            find_definition_once(key, opsys_defines, "O") or
138            find_definition_once(key, common_defines, "C"))
139
140################################################################
141# Makefile generation
142
143def construct_definition(opsys, key_prefix, value_prefix, key, definitions):
144    values = definitions.get(key)
145    if not values:
146        return ""
147    if key in ["INC", "DEF"]:
148        values = [patch_path_separator(opsys, value)
149                  for value in values]
150    lines = ["\t{}{} \\".format(value_prefix, value) for value in values]
151    return "{}_{} = \\\n{}\n\t# empty\n".format(key_prefix,
152                                                key,
153                                                '\n'.join(lines))
154
155def write_define(opsys, define, defines, makefile):
156    value = find_definition(define, defines)
157    if value:
158        if define in ["FREERTOS_PLUS_TCP", "PROOFS"]:
159            value = os.path.abspath(value[0])
160        makefile.write("{} = {}\n".format(define, value))
161
162def write_common_defines(opsys, defines, makefile):
163    common_defines, opsys_defines, harness_defines = defines
164
165    for key_prefix, defines in zip(["C", "O", "H"],
166                                   [common_defines,
167                                    opsys_defines,
168                                    harness_defines]):
169        for value_prefix, key in zip([platform_definitions[opsys]["include"],
170                                      platform_definitions[opsys]["define"],
171                                      "", ""],
172                                     ["INC", "DEF", "OPT", "CBMCFLAGS"]):
173            define = construct_definition(opsys,
174                                          key_prefix, value_prefix,
175                                          key, defines)
176            if define:
177                makefile.write(define + "\n")
178
179
180def write_makefile(opsys, template, defines, makefile):
181    with open(template) as _template:
182        for line in _template:
183            line = patch_path_separator(opsys, line)
184            keys = re.findall('@(\w+)@', line)
185            values = [find_definition(key, defines) for key in keys]
186            for key, value in zip(keys, values):
187                if value is not None:
188                    line = line.replace('@{}@'.format(key), " ".join(value))
189                    line = patch_compile_output(opsys, line, key, value)
190            makefile.write(line)
191
192def write_cbmcbatchyaml_target(opsys, _makefile):
193    target = """
194################################################################
195# Build configuration file to run cbmc under cbmc-batch in CI
196
197define encode_options
198'=$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')='
199endef
200
201cbmc-batch.yaml:
202	@echo "Building $@"
203	@$(RM) $@
204	@echo "jobos: ubuntu16" >> $@
205	@echo "cbmcflags: $(call encode_options,$(CBMCFLAGS) --unwinding-assertions)" >> $@
206	@echo "goto: $(ENTRY).goto" >> $@
207	@echo "expected: $(H_EXPECTED)" >> $@
208
209################################################################
210"""
211    if opsys != "windows":
212        _makefile.write(target)
213
214def write_solver(opsys, _makefile):
215    conditional = """
216ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),)
217   SOLVER = --external-sat-solver $(EXTERNAL_SAT_SOLVER)
218endif
219"""
220    if opsys != "windows":
221        _makefile.write(conditional)
222
223def makefile_from_template(opsys, template, defines, makefile="Makefile"):
224    with open(makefile, "w") as _makefile:
225        write_define(opsys, "FREERTOS_PLUS_TCP", defines, _makefile)
226        write_define(opsys, "PROOFS", defines, _makefile)
227        write_common_defines(opsys, defines, _makefile)
228        write_makefile(opsys, template, defines, _makefile)
229        write_cbmcbatchyaml_target(opsys, _makefile)
230        write_solver(opsys, _makefile)
231
232################################################################
233# Main
234
235def main():
236    args = get_arguments()
237
238    common_defines = read_variable_definitions("MakefileCommon.json")
239    opsys_defines = read_variable_definitions("MakefileWindows.json"
240                                              if args.system == "windows"
241                                              else "MakefileLinux.json")
242    harness_defines = {}
243
244    makefile_from_template(args.system,
245                           "Makefile.template",
246                           (common_defines, opsys_defines, harness_defines),
247                           "Makefile.common")
248
249if __name__ == "__main__":
250    main()
251