1#!/usr/bin/env python3
2#
3# Compute type header files for c modules
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
25
26import argparse
27import logging
28import os
29import re
30import shutil
31import subprocess
32import sys
33from tempfile import TemporaryDirectory
34
35def epilog():
36    return """\
37        This program dumps a header file containing the types and macros
38        contained in the C file passed as input. It uses `goto-instrument`
39        from the CBMC tool suite instead of the preprocessor, to dump types
40        and other constructs as well as preprocessor directives.
41
42        This program should be used in cases where types or macros declared
43        for internal use in a C file use are needed to write a test harness
44        or CBMC proof.  The intention is that the build process will run
45        this program to dump the header file, and the proof will #include
46        the header.
47    """
48
49_DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)")
50
51
52def get_module_name(fyle):
53    base = os.path.basename(fyle)
54    return base.split(".")[0]
55
56
57def collect_defines(fyle):
58    collector_result = ""
59    continue_define = False
60    in_potential_def_scope = ""
61    potential_define = False
62    potential_define_confirmed = False
63    with open(fyle) as in_file:
64        for line in in_file:
65            matched = _DEFINE_REGEX_HEADER.match(line)
66            if line.strip().startswith("#if"):
67                potential_define = True
68                in_potential_def_scope += line
69            elif line.strip().startswith("#endif") and potential_define:
70                if potential_define_confirmed:
71                    in_potential_def_scope += line
72                    collector_result += in_potential_def_scope
73                in_potential_def_scope = ""
74                potential_define = False
75                potential_define_confirmed = False
76            elif matched and potential_define:
77                potential_define_confirmed = True
78                in_potential_def_scope += line
79            elif matched or continue_define:
80                continue_define = line.strip("\n").endswith("\\")
81                collector_result += line
82            elif potential_define:
83                in_potential_def_scope += line
84    return collector_result
85
86
87def make_header_file(goto_binary, fyle, target_folder):
88    fyle = os.path.normpath(fyle)
89    with TemporaryDirectory() as tmpdir:
90        module = get_module_name(fyle)
91        header_file = "{}_datastructure.h".format(module)
92
93        drop_header_cmd = ["goto-instrument",
94                           "--dump-c-type-header",
95                           module,
96                           goto_binary,
97                           header_file]
98        res = subprocess.run(drop_header_cmd,
99                             stdout=subprocess.PIPE,
100                             stderr=subprocess.STDOUT,
101                             universal_newlines=True,
102                             cwd=tmpdir)
103        if res.returncode:
104            logging.error("Dumping type header for file '%s' failed", fyle)
105            logging.error("The command `%s` returned %s",
106                          drop_header_cmd,
107                          res.stdout)
108            logging.error("The return code is %d", int(res.returncode))
109            sys.exit(1)
110
111        header = os.path.normpath(os.path.join(tmpdir, header_file))
112        collected = collect_defines(fyle)
113        logging.debug("Dumping the following header file to '%s':\n%s\n"
114                      "// END GENERATED HEADER FILE", header, collected)
115        with open(header, "a") as out:
116            print(collected, file=out)
117
118        target_file = os.path.normpath(os.path.join(target_folder, header_file))
119        shutil.move(header, target_file)
120
121
122_ARGS = [{
123    "flags": ["--c-file"],
124    "metavar": "F",
125    "help": "source file to extract types and headers from",
126    "required": True
127}, {
128    "flags": ["--binary"],
129    "metavar": "B",
130    "help": "file compiled from the source file with CBMC's goto-cc compiler",
131    "required": True
132}, {
133    "flags": ["--out-dir"],
134    "metavar": "D",
135    "help": ("directory to write the generated header file to "
136             "(default: %(default)s)"),
137    "default": os.path.abspath(os.getcwd()),
138}, {
139    "flags": ["--verbose", "-v"],
140    "help": "verbose output",
141    "action": "store_true"
142}]
143
144
145if __name__ == '__main__':
146    pars = argparse.ArgumentParser(
147        epilog=epilog(),
148        description="Dump a C file's types and macros to a separate file")
149    for arg in _ARGS:
150        flags = arg.pop("flags")
151        pars.add_argument(*flags, **arg)
152
153    args = pars.parse_args()
154
155    fmt = "{script}: %(levelname)s %(message)s".format(
156        script=os.path.basename(__file__))
157    if args.verbose:
158        logging.basicConfig(format=fmt, level=logging.DEBUG)
159    else:
160        logging.basicConfig(format=fmt, level=logging.INFO)
161
162    make_header_file(args.binary, args.c_file, args.out_dir)
163