begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/make_proof_makefiles.py

   1 #!/usr/bin/env python3
   2 #
   3 # Generation of Makefiles for CBMC proofs.
   4 #
   5 # Copyright (C) 2019 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
  25
  26 import argparse
  27 import ast
  28 import collections
  29 import json
  30 import logging
  31 import operator
  32 import os
  33 import os.path
  34 import platform
  35 import re
  36 import sys
  37 import textwrap
  38 import traceback
  39
  40
  41 # ______________________________________________________________________________
  42 # Compatibility between different python versions
  43 # ``````````````````````````````````````````````````````````````````````````````
  44
  45 # Python 3 doesn't have basestring
  46 try:
  47     basestring
  48 except NameError:
  49     basestring = str
  50
  51 # ast.Num was deprecated in python 3.8
  52 _plat = platform.python_version().split(".")
  53 if _plat[0] == "3" and int(_plat[1]) > 7:
  54     ast_num = ast.Constant
  55 else:
  56     ast_num = ast.Num
  57 # ______________________________________________________________________________
  58
  59
  60 def prolog():
  61     return textwrap.dedent("""\
  62         This script generates Makefiles that can be used either on Windows (with
  63         NMake) or Linux (with GNU Make). The Makefiles consist only of variable
  64         definitions; they are intended to be used with a common Makefile that
  65         defines the actual rules.
  66
  67         The Makefiles are generated from JSON specifications. These are simple
  68         key-value dicts, but can contain variables and computation, as
  69         well as comments (lines whose first character is "#"). If the
  70         JSON file contains the following information:
  71
  72                 {
  73                     # 'T was brillig, and the slithy toves
  74                     "FOO": "BAR",
  75                     "BAZ": "{FOO}",
  76
  77                     # Did gyre and gimble in the wabe;
  78                     "QUUX": 30
  79                     "XYZZY": "__eval 5 if {QUUZ} < 5 else min({QUUX}, 60)"
  80                 }
  81
  82         then the resulting Makefile will look like
  83
  84                 H_FOO = BAR
  85                 H_BAZ = BAR
  86                 H_QUUX = 30
  87                 H_XYZZY = 30
  88
  89         The language used for evaluation is highly restricted; arbitrary
  90         python is not allowed.  JSON values that are lists will be
  91         joined with whitespace:
  92
  93                 { "FOO": ["BAR", "BAZ", "QUX"] }
  94
  95                 ->
  96
  97                 H_FOO = BAR BAZ QUX
  98
  99         As a special case, if a key is equal to "DEF", "INC" (and maybe more,
 100         read the code) the list of values is treated as a list of defines or
 101         include paths. Thus, they have -D or /D, or -I or /I, prepended to them
 102         as appropriate for the platform.
 103
 104
 105                 { "DEF": ["DEBUG", "FOO=BAR"] }
 106
 107                 on Linux ->
 108
 109                 H_DEF = -DDEBUG -DFOO=BAR
 110
 111         Pathnames are written with a forward slash in the JSON file. In
 112         each value, all slashes are replaced with backslashes if
 113         generating Makefiles for Windows. If you wish to generate a
 114         slash even on Windows, use two slashes---that will be changed
 115         into a single forward slash on both Windows and Linux.
 116
 117                 {
 118                     "INC": [ "my/cool/directory" ],
 119                     "DEF": [ "HALF=//2" ]
 120                 }
 121
 122                 On Windows ->
 123
 124                 H_INC = /Imy\cool\directory
 125                 H_DEF = /DHALF=/2
 126
 127         When invoked, this script walks the directory tree looking for files
 128         called "Makefile.json". It reads that file and dumps a Makefile in that
 129         same directory. We assume that this script lives in the same directory
 130         as a Makefile called "Makefile.common", which contains the actual Make
 131         rules. The final line of each of the generated Makefiles will be an
 132         include statement, including Makefile.common.
 133     """)
 134
 135 def load_json_config_file(file):
 136     with open(file) as handle:
 137         lines = handle.read().splitlines()
 138     no_comments = "\n".join([line for line in lines
 139                              if line and not line.lstrip().startswith("#")])
 140     try:
 141         data = json.loads(no_comments,
 142                           object_pairs_hook=collections.OrderedDict)
 143     except json.decoder.JSONDecodeError:
 144         traceback.print_exc()
 145         logging.error("parsing file %s", file)
 146         sys.exit(1)
 147     return data
 148
 149
 150 def dump_makefile(dyr, system):
 151     data = load_json_config_file(os.path.join(dyr, "Makefile.json"))
 152
 153     makefile = collections.OrderedDict()
 154
 155     # Makefile.common expects a variable called OBJS_EXCEPT_HARNESS to be
 156     # set to a list of all the object files except the harness.
 157     if "OBJS" not in data:
 158         logging.error(
 159             "Expected a list of object files in %s/Makefile.json" % dyr)
 160         exit(1)
 161     makefile["OBJS_EXCEPT_HARNESS"] = " ".join(
 162         o for o in data["OBJS"] if not o.endswith("_harness.goto"))
 163
 164     so_far = collections.OrderedDict()
 165     for name, value in data.items():
 166         if isinstance(value, list):
 167             new_value = []
 168             for item in value:
 169                 new_value.append(compute(item, so_far, system, name, dyr, True))
 170             makefile[name] = " ".join(new_value)
 171         else:
 172             makefile[name] = compute(value, so_far, system, name, dyr)
 173
 174     if (("EXPECTED" not in makefile.keys()) or
 175             str(makefile["EXPECTED"]).lower() == "true"):
 176         makefile["EXPECTED"] = "SUCCESSFUL"
 177     elif str(makefile["EXPECTED"]).lower() == "false":
 178         makefile["EXPECTED"] = "FAILURE"
 179     makefile = ["H_%s = %s" % (k, v) for k, v in makefile.items()]
 180
 181     # Deal with the case of a harness being nested several levels under
 182     # the top-level proof directory, where the common Makefile lives
 183     common_dir_path = "..%s" % _platform_choices[system]["path-sep"]
 184     common_dir_path = common_dir_path * len(dyr.split(os.path.sep)[1:])
 185
 186     with open(os.path.join(dyr, "Makefile"), "w") as handle:
 187         handle.write(("""{contents}
 188
 189 {include} {common_dir_path}Makefile.common""").format(
 190             contents="\n".join(makefile),
 191             include=_platform_choices[system]["makefile-inc"],
 192             common_dir_path=common_dir_path))
 193
 194
 195 def compute(value, so_far, system, key, harness, appending=False):
 196     if not isinstance(value, (basestring, float, int)):
 197         logging.error(wrap("""\
 198                         in file %s, the key '%s' has value '%s',
 199                         which is of the wrong type (%s)"""),
 200                       os.path.join(harness, "Makefile.json"), key,
 201                       str(value), str(type(value)))
 202         exit(1)
 203
 204     value = str(value)
 205     try:
 206         var_subbed = value.format(**so_far)
 207     except KeyError as e:
 208         logging.error(wrap("""\
 209                         in file %s, the key '%s' has value '%s', which
 210                         contains the variable %s, but that variable has
 211                         not previously been set in the file"""),
 212                       os.path.join(harness, "Makefile.json"), key,
 213                       value, str(e))
 214         exit(1)
 215
 216     if var_subbed[:len("__eval")] != "__eval":
 217         tmp = re.sub("//", "__DOUBLE_SLASH__", var_subbed)
 218         tmp = re.sub("/", _platform_choices[system]["path-sep-re"], tmp)
 219         evaluated = re.sub("__DOUBLE_SLASH__", "/", tmp)
 220     else:
 221         to_eval = var_subbed[len("__eval"):].strip()
 222         logging.debug("About to evaluate '%s'", to_eval)
 223         evaluated = eval_expr(to_eval,
 224                               os.path.join(harness, "Makefile.json"),
 225                               key, value)
 226
 227     if key == "DEF":
 228         final_value = "%s%s" % (_platform_choices[system]["define"],
 229                                 evaluated)
 230     elif key == "INC":
 231         final_value = "%s%s" % (_platform_choices[system]["include"],
 232                                 evaluated)
 233     else:
 234         final_value = evaluated
 235
 236     # Allow this value to be used for future variable substitution
 237     if appending:
 238         try:
 239             so_far[key] = "%s %s" % (so_far[key], final_value)
 240         except KeyError:
 241             so_far[key] = final_value
 242         logging.debug("Appending final value '%s' to key '%s'",
 243                       final_value, key)
 244     else:
 245         so_far[key] = final_value
 246         logging.info("Key '%s' set to final value '%s'", key, final_value)
 247
 248     return final_value
 249
 250
 251 def eval_expr(expr_string, harness, key, value):
 252     """
 253     Safe evaluation of purely arithmetic expressions
 254     """
 255     try:
 256         tree = ast.parse(expr_string, mode="eval").body
 257     except SyntaxError:
 258         traceback.print_exc()
 259         logging.error(wrap("""\
 260             in file %s at key '%s', value '%s' contained the expression
 261             '%s' which is an invalid expression"""), harness, key,
 262                       value, expr_string)
 263         exit(1)
 264
 265     def eval_single_node(node):
 266         logging.debug(node)
 267         if isinstance(node, ast_num):
 268             return node.n
 269         # We're only doing IfExp, which is Python's ternary operator
 270         # (i.e. it's an expression). NOT If, which is a statement.
 271         if isinstance(node, ast.IfExp):
 272             # Let's be strict and only allow actual booleans in the guard
 273             guard = eval_single_node(node.test)
 274             if guard is not True and guard is not False:
 275                 logging.error(wrap("""\
 276                     in file %s at key '%s', there was an invalid guard
 277                     for an if statement."""), harness, key)
 278                 exit(1)
 279             if guard:
 280                 return eval_single_node(node.body)
 281             return eval_single_node(node.orelse)
 282         if isinstance(node, ast.Compare):
 283             left = eval_single_node(node.left)
 284             # Don't allow expressions like (a < b) < c
 285             right = eval_single_node(node.comparators[0])
 286             op = eval_single_node(node.ops[0])
 287             return op(left, right)
 288         if isinstance(node, ast.BinOp):
 289             left = eval_single_node(node.left)
 290             right = eval_single_node(node.right)
 291             op = eval_single_node(node.op)
 292             return op(left, right)
 293         if isinstance(node, ast.Call):
 294             valid_calls = {
 295                 "max": max,
 296                 "min": min,
 297             }
 298             if node.func.id not in valid_calls:
 299                 logging.error(wrap("""\
 300                     in file %s at key '%s', there was an invalid
 301                     call to %s()"""), harness, key, node.func.id)
 302                 exit(1)
 303             left = eval_single_node(node.args[0])
 304             right = eval_single_node(node.args[1])
 305             return valid_calls[node.func.id](left, right)
 306         try:
 307             return {
 308                 ast.Eq: operator.eq,
 309                 ast.NotEq: operator.ne,
 310                 ast.Lt: operator.lt,
 311                 ast.LtE: operator.le,
 312                 ast.Gt: operator.gt,
 313                 ast.GtE: operator.ge,
 314
 315                 ast.Add: operator.add,
 316                 ast.Sub: operator.sub,
 317                 ast.Mult: operator.mul,
 318                 # Use floordiv (i.e. //) so that we never need to
 319                 # cast to an int
 320                 ast.Div: operator.floordiv,
 321             }[type(node)]
 322         except KeyError:
 323             logging.error(wrap("""\
 324                 in file %s at key '%s', there was expression that
 325                 was impossible to evaluate"""), harness, key)
 326             exit(1)
 327
 328     return eval_single_node(tree)
 329
 330
 331 _platform_choices = {
 332     "linux": {
 333         "platform": "linux",
 334         "path-sep": "/",
 335         "path-sep-re": "/",
 336         "define": "-D",
 337         "include": "-I",
 338         "makefile-inc": "include",
 339     },
 340     "windows": {
 341         "platform": "win32",
 342         "path-sep": "\\",
 343         "path-sep-re": re.escape("\\"),
 344         "define": "/D",
 345         "include": "/I",
 346         "makefile-inc": "!INCLUDE",
 347     },
 348 }
 349 # Assuming macos is the same as linux
 350 _mac_os = dict(_platform_choices["linux"])
 351 _mac_os["platform"] = "darwin"
 352 _platform_choices["macos"] = _mac_os
 353
 354
 355 def default_platform():
 356     for arg_string, os_data in _platform_choices.items():
 357         if sys.platform == os_data["platform"]:
 358             return arg_string
 359     return "linux"
 360
 361
 362 _args = [{
 363     "flags": ["-s", "--system"],
 364     "metavar": "OS",
 365     "choices": _platform_choices,
 366     "default": str(default_platform()),
 367     "help": textwrap.dedent("""\
 368                 which operating system to generate makefiles for.
 369                 Defaults to the current platform (%(default)s);
 370                 choices are {choices}""").format(
 371                     choices="[%s]" % ", ".join(_platform_choices)),
 372 }, {
 373     "flags": ["-v", "--verbose"],
 374     "help": "verbose output",
 375     "action": "store_true",
 376 }, {
 377     "flags": ["-w", "--very-verbose"],
 378     "help": "very verbose output",
 379     "action": "store_true",
 380     }]
 381
 382
 383 def get_args():
 384     pars = argparse.ArgumentParser(
 385         description=prolog(),
 386         formatter_class=argparse.RawDescriptionHelpFormatter)
 387     for arg in _args:
 388         flags = arg.pop("flags")
 389         pars.add_argument(*flags, **arg)
 390     return pars.parse_args()
 391
 392
 393 def set_up_logging(args):
 394     fmt = "{script}: %(levelname)s %(message)s".format(
 395         script=os.path.basename(__file__))
 396     if args.very_verbose:
 397         logging.basicConfig(format=fmt, level=logging.DEBUG)
 398     elif args.verbose:
 399         logging.basicConfig(format=fmt, level=logging.INFO)
 400     else:
 401         logging.basicConfig(format=fmt, level=logging.WARNING)
 402
 403 def wrap(string):
 404     return re.sub(r"\s+", " ", re.sub("\n", " ", string))
 405
 406 def main():
 407     args = get_args()
 408     set_up_logging(args)
 409
 410     for root, _, fyles in os.walk("."):
 411         if "Makefile.json" in fyles:
 412             dump_makefile(root, args.system)
 413
 414
 415 if __name__ == "__main__":
 416     main()