mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-29 00:36:16 -04:00
416 lines
14 KiB
Python
Executable file
416 lines
14 KiB
Python
Executable file
#!/usr/bin/env python3
|
|
#
|
|
# Generation of Makefiles for CBMC proofs.
|
|
#
|
|
# Copyright (C) 2019 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 the Software without restriction, including without limitation the rights
|
|
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
|
# copies of the Software, and to permit persons to whom the Software is
|
|
# furnished to do so, subject to the following conditions:
|
|
#
|
|
# The above copyright notice and this permission notice shall be included in all
|
|
# copies or substantial portions of the Software.
|
|
#
|
|
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
|
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
|
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
|
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
|
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
|
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
|
# SOFTWARE.
|
|
|
|
|
|
import argparse
|
|
import ast
|
|
import collections
|
|
import json
|
|
import logging
|
|
import operator
|
|
import os
|
|
import os.path
|
|
import platform
|
|
import re
|
|
import sys
|
|
import textwrap
|
|
import traceback
|
|
|
|
|
|
# ______________________________________________________________________________
|
|
# Compatibility between different python versions
|
|
# ``````````````````````````````````````````````````````````````````````````````
|
|
|
|
# Python 3 doesn't have basestring
|
|
try:
|
|
basestring
|
|
except NameError:
|
|
basestring = str
|
|
|
|
# ast.Num was deprecated in python 3.8
|
|
_plat = platform.python_version().split(".")
|
|
if _plat[0] == "3" and int(_plat[1]) > 7:
|
|
ast_num = ast.Constant
|
|
else:
|
|
ast_num = ast.Num
|
|
# ______________________________________________________________________________
|
|
|
|
|
|
def prolog():
|
|
return textwrap.dedent("""\
|
|
This script generates Makefiles that can be used either on Windows (with
|
|
NMake) or Linux (with GNU Make). The Makefiles consist only of variable
|
|
definitions; they are intended to be used with a common Makefile that
|
|
defines the actual rules.
|
|
|
|
The Makefiles are generated from JSON specifications. These are simple
|
|
key-value dicts, but can contain variables and computation, as
|
|
well as comments (lines whose first character is "#"). If the
|
|
JSON file contains the following information:
|
|
|
|
{
|
|
# 'T was brillig, and the slithy toves
|
|
"FOO": "BAR",
|
|
"BAZ": "{FOO}",
|
|
|
|
# Did gyre and gimble in the wabe;
|
|
"QUUX": 30
|
|
"XYZZY": "__eval 5 if {QUUZ} < 5 else min({QUUX}, 60)"
|
|
}
|
|
|
|
then the resulting Makefile will look like
|
|
|
|
H_FOO = BAR
|
|
H_BAZ = BAR
|
|
H_QUUX = 30
|
|
H_XYZZY = 30
|
|
|
|
The language used for evaluation is highly restricted; arbitrary
|
|
python is not allowed. JSON values that are lists will be
|
|
joined with whitespace:
|
|
|
|
{ "FOO": ["BAR", "BAZ", "QUX"] }
|
|
|
|
->
|
|
|
|
H_FOO = BAR BAZ QUX
|
|
|
|
As a special case, if a key is equal to "DEF", "INC" (and maybe more,
|
|
read the code) the list of values is treated as a list of defines or
|
|
include paths. Thus, they have -D or /D, or -I or /I, prepended to them
|
|
as appropriate for the platform.
|
|
|
|
|
|
{ "DEF": ["DEBUG", "FOO=BAR"] }
|
|
|
|
on Linux ->
|
|
|
|
H_DEF = -DDEBUG -DFOO=BAR
|
|
|
|
Pathnames are written with a forward slash in the JSON file. In
|
|
each value, all slashes are replaced with backslashes if
|
|
generating Makefiles for Windows. If you wish to generate a
|
|
slash even on Windows, use two slashes---that will be changed
|
|
into a single forward slash on both Windows and Linux.
|
|
|
|
{
|
|
"INC": [ "my/cool/directory" ],
|
|
"DEF": [ "HALF=//2" ]
|
|
}
|
|
|
|
On Windows ->
|
|
|
|
H_INC = /Imy\cool\directory
|
|
H_DEF = /DHALF=/2
|
|
|
|
When invoked, this script walks the directory tree looking for files
|
|
called "Makefile.json". It reads that file and dumps a Makefile in that
|
|
same directory. We assume that this script lives in the same directory
|
|
as a Makefile called "Makefile.common", which contains the actual Make
|
|
rules. The final line of each of the generated Makefiles will be an
|
|
include statement, including Makefile.common.
|
|
""")
|
|
|
|
def load_json_config_file(file):
|
|
with open(file) as handle:
|
|
lines = handle.read().splitlines()
|
|
no_comments = "\n".join([line for line in lines
|
|
if line and not line.lstrip().startswith("#")])
|
|
try:
|
|
data = json.loads(no_comments,
|
|
object_pairs_hook=collections.OrderedDict)
|
|
except json.decoder.JSONDecodeError:
|
|
traceback.print_exc()
|
|
logging.error("parsing file %s", file)
|
|
sys.exit(1)
|
|
return data
|
|
|
|
|
|
def dump_makefile(dyr, system):
|
|
data = load_json_config_file(os.path.join(dyr, "Makefile.json"))
|
|
|
|
makefile = collections.OrderedDict()
|
|
|
|
# Makefile.common expects a variable called OBJS_EXCEPT_HARNESS to be
|
|
# set to a list of all the object files except the harness.
|
|
if "OBJS" not in data:
|
|
logging.error(
|
|
"Expected a list of object files in %s/Makefile.json" % dyr)
|
|
exit(1)
|
|
makefile["OBJS_EXCEPT_HARNESS"] = " ".join(
|
|
o for o in data["OBJS"] if not o.endswith("_harness.goto"))
|
|
|
|
so_far = collections.OrderedDict()
|
|
for name, value in data.items():
|
|
if isinstance(value, list):
|
|
new_value = []
|
|
for item in value:
|
|
new_value.append(compute(item, so_far, system, name, dyr, True))
|
|
makefile[name] = " ".join(new_value)
|
|
else:
|
|
makefile[name] = compute(value, so_far, system, name, dyr)
|
|
|
|
if (("EXPECTED" not in makefile.keys()) or
|
|
str(makefile["EXPECTED"]).lower() == "true"):
|
|
makefile["EXPECTED"] = "SUCCESSFUL"
|
|
elif str(makefile["EXPECTED"]).lower() == "false":
|
|
makefile["EXPECTED"] = "FAILURE"
|
|
makefile = ["H_%s = %s" % (k, v) for k, v in makefile.items()]
|
|
|
|
# Deal with the case of a harness being nested several levels under
|
|
# the top-level proof directory, where the common Makefile lives
|
|
common_dir_path = "..%s" % _platform_choices[system]["path-sep"]
|
|
common_dir_path = common_dir_path * len(dyr.split(os.path.sep)[1:])
|
|
|
|
with open(os.path.join(dyr, "Makefile"), "w") as handle:
|
|
handle.write(("""{contents}
|
|
|
|
{include} {common_dir_path}Makefile.common""").format(
|
|
contents="\n".join(makefile),
|
|
include=_platform_choices[system]["makefile-inc"],
|
|
common_dir_path=common_dir_path))
|
|
|
|
|
|
def compute(value, so_far, system, key, harness, appending=False):
|
|
if not isinstance(value, (basestring, float, int)):
|
|
logging.error(wrap("""\
|
|
in file %s, the key '%s' has value '%s',
|
|
which is of the wrong type (%s)"""),
|
|
os.path.join(harness, "Makefile.json"), key,
|
|
str(value), str(type(value)))
|
|
exit(1)
|
|
|
|
value = str(value)
|
|
try:
|
|
var_subbed = value.format(**so_far)
|
|
except KeyError as e:
|
|
logging.error(wrap("""\
|
|
in file %s, the key '%s' has value '%s', which
|
|
contains the variable %s, but that variable has
|
|
not previously been set in the file"""),
|
|
os.path.join(harness, "Makefile.json"), key,
|
|
value, str(e))
|
|
exit(1)
|
|
|
|
if var_subbed[:len("__eval")] != "__eval":
|
|
tmp = re.sub("//", "__DOUBLE_SLASH__", var_subbed)
|
|
tmp = re.sub("/", _platform_choices[system]["path-sep-re"], tmp)
|
|
evaluated = re.sub("__DOUBLE_SLASH__", "/", tmp)
|
|
else:
|
|
to_eval = var_subbed[len("__eval"):].strip()
|
|
logging.debug("About to evaluate '%s'", to_eval)
|
|
evaluated = eval_expr(to_eval,
|
|
os.path.join(harness, "Makefile.json"),
|
|
key, value)
|
|
|
|
if key == "DEF":
|
|
final_value = "%s%s" % (_platform_choices[system]["define"],
|
|
evaluated)
|
|
elif key == "INC":
|
|
final_value = "%s%s" % (_platform_choices[system]["include"],
|
|
evaluated)
|
|
else:
|
|
final_value = evaluated
|
|
|
|
# Allow this value to be used for future variable substitution
|
|
if appending:
|
|
try:
|
|
so_far[key] = "%s %s" % (so_far[key], final_value)
|
|
except KeyError:
|
|
so_far[key] = final_value
|
|
logging.debug("Appending final value '%s' to key '%s'",
|
|
final_value, key)
|
|
else:
|
|
so_far[key] = final_value
|
|
logging.info("Key '%s' set to final value '%s'", key, final_value)
|
|
|
|
return final_value
|
|
|
|
|
|
def eval_expr(expr_string, harness, key, value):
|
|
"""
|
|
Safe evaluation of purely arithmetic expressions
|
|
"""
|
|
try:
|
|
tree = ast.parse(expr_string, mode="eval").body
|
|
except SyntaxError:
|
|
traceback.print_exc()
|
|
logging.error(wrap("""\
|
|
in file %s at key '%s', value '%s' contained the expression
|
|
'%s' which is an invalid expression"""), harness, key,
|
|
value, expr_string)
|
|
exit(1)
|
|
|
|
def eval_single_node(node):
|
|
logging.debug(node)
|
|
if isinstance(node, ast_num):
|
|
return node.n
|
|
# We're only doing IfExp, which is Python's ternary operator
|
|
# (i.e. it's an expression). NOT If, which is a statement.
|
|
if isinstance(node, ast.IfExp):
|
|
# Let's be strict and only allow actual booleans in the guard
|
|
guard = eval_single_node(node.test)
|
|
if guard is not True and guard is not False:
|
|
logging.error(wrap("""\
|
|
in file %s at key '%s', there was an invalid guard
|
|
for an if statement."""), harness, key)
|
|
exit(1)
|
|
if guard:
|
|
return eval_single_node(node.body)
|
|
return eval_single_node(node.orelse)
|
|
if isinstance(node, ast.Compare):
|
|
left = eval_single_node(node.left)
|
|
# Don't allow expressions like (a < b) < c
|
|
right = eval_single_node(node.comparators[0])
|
|
op = eval_single_node(node.ops[0])
|
|
return op(left, right)
|
|
if isinstance(node, ast.BinOp):
|
|
left = eval_single_node(node.left)
|
|
right = eval_single_node(node.right)
|
|
op = eval_single_node(node.op)
|
|
return op(left, right)
|
|
if isinstance(node, ast.Call):
|
|
valid_calls = {
|
|
"max": max,
|
|
"min": min,
|
|
}
|
|
if node.func.id not in valid_calls:
|
|
logging.error(wrap("""\
|
|
in file %s at key '%s', there was an invalid
|
|
call to %s()"""), harness, key, node.func.id)
|
|
exit(1)
|
|
left = eval_single_node(node.args[0])
|
|
right = eval_single_node(node.args[1])
|
|
return valid_calls[node.func.id](left, right)
|
|
try:
|
|
return {
|
|
ast.Eq: operator.eq,
|
|
ast.NotEq: operator.ne,
|
|
ast.Lt: operator.lt,
|
|
ast.LtE: operator.le,
|
|
ast.Gt: operator.gt,
|
|
ast.GtE: operator.ge,
|
|
|
|
ast.Add: operator.add,
|
|
ast.Sub: operator.sub,
|
|
ast.Mult: operator.mul,
|
|
# Use floordiv (i.e. //) so that we never need to
|
|
# cast to an int
|
|
ast.Div: operator.floordiv,
|
|
}[type(node)]
|
|
except KeyError:
|
|
logging.error(wrap("""\
|
|
in file %s at key '%s', there was expression that
|
|
was impossible to evaluate"""), harness, key)
|
|
exit(1)
|
|
|
|
return eval_single_node(tree)
|
|
|
|
|
|
_platform_choices = {
|
|
"linux": {
|
|
"platform": "linux",
|
|
"path-sep": "/",
|
|
"path-sep-re": "/",
|
|
"define": "-D",
|
|
"include": "-I",
|
|
"makefile-inc": "include",
|
|
},
|
|
"windows": {
|
|
"platform": "win32",
|
|
"path-sep": "\\",
|
|
"path-sep-re": re.escape("\\"),
|
|
"define": "/D",
|
|
"include": "/I",
|
|
"makefile-inc": "!INCLUDE",
|
|
},
|
|
}
|
|
# Assuming macos is the same as linux
|
|
_mac_os = dict(_platform_choices["linux"])
|
|
_mac_os["platform"] = "darwin"
|
|
_platform_choices["macos"] = _mac_os
|
|
|
|
|
|
def default_platform():
|
|
for arg_string, os_data in _platform_choices.items():
|
|
if sys.platform == os_data["platform"]:
|
|
return arg_string
|
|
return "linux"
|
|
|
|
|
|
_args = [{
|
|
"flags": ["-s", "--system"],
|
|
"metavar": "OS",
|
|
"choices": _platform_choices,
|
|
"default": str(default_platform()),
|
|
"help": textwrap.dedent("""\
|
|
which operating system to generate makefiles for.
|
|
Defaults to the current platform (%(default)s);
|
|
choices are {choices}""").format(
|
|
choices="[%s]" % ", ".join(_platform_choices)),
|
|
}, {
|
|
"flags": ["-v", "--verbose"],
|
|
"help": "verbose output",
|
|
"action": "store_true",
|
|
}, {
|
|
"flags": ["-w", "--very-verbose"],
|
|
"help": "very verbose output",
|
|
"action": "store_true",
|
|
}]
|
|
|
|
|
|
def get_args():
|
|
pars = argparse.ArgumentParser(
|
|
description=prolog(),
|
|
formatter_class=argparse.RawDescriptionHelpFormatter)
|
|
for arg in _args:
|
|
flags = arg.pop("flags")
|
|
pars.add_argument(*flags, **arg)
|
|
return pars.parse_args()
|
|
|
|
|
|
def set_up_logging(args):
|
|
fmt = "{script}: %(levelname)s %(message)s".format(
|
|
script=os.path.basename(__file__))
|
|
if args.very_verbose:
|
|
logging.basicConfig(format=fmt, level=logging.DEBUG)
|
|
elif args.verbose:
|
|
logging.basicConfig(format=fmt, level=logging.INFO)
|
|
else:
|
|
logging.basicConfig(format=fmt, level=logging.WARNING)
|
|
|
|
def wrap(string):
|
|
return re.sub(r"\s+", " ", re.sub("\n", " ", string))
|
|
|
|
def main():
|
|
args = get_args()
|
|
set_up_logging(args)
|
|
|
|
for root, _, fyles in os.walk("."):
|
|
if "Makefile.json" in fyles:
|
|
dump_makefile(root, args.system)
|
|
|
|
|
|
if __name__ == "__main__":
|
|
main()
|