1#!/usr/bin/env python3
2#
3# Generation of patches 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
25
26import json
27import os
28import re
29import subprocess
30import textwrap
31import unittest
32
33from patches_constants import PATCHES_DIR
34from patches_constants import HEADERS
35
36
37DEFINE_REGEX_MAKEFILE = re.compile(r"(?:['\"])?([\w]+)")
38DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)")
39
40class DirtyGitError(Exception):
41    pass
42
43class PatchCreationError(Exception):
44    pass
45
46def prolog():
47    return textwrap.dedent("""\
48        This script generates patch files for the header files used
49        in the cbmc proof. These patches permit setting values of preprocessor
50        macros as part of the proof configuration.
51    """)
52
53
54def find_all_defines():
55    """Collects all define values in Makefile.json.
56
57       Some of the Makefiles use # in the json to make comments.
58       As this is non standard json, we need to remove the comment
59       lines before parsing. Then we extract all defines from the file.
60    """
61    defines = set()
62
63    proof_dir = os.path.abspath(os.path.join(PATCHES_DIR, "..", "proofs"))
64
65    for fldr, _, fyles in os.walk(proof_dir):
66        if "Makefile.json" in fyles:
67            file = os.path.join(fldr, "Makefile.json")
68            key = "DEF"
69        elif "MakefileCommon.json" in fyles:
70            file = os.path.join(fldr, "MakefileCommon.json")
71            key = "DEF "
72        else:
73            continue
74        with open(file, "r") as source:
75            content = "".join([line for line in source
76                               if line and not line.strip().startswith("#")])
77            makefile = json.loads(content)
78            if key in makefile.keys():
79                """This regex parses the define declaration in Makefile.json
80                   'macro(x)=false' is an example for a declaration.
81                   'macro' is expected to be matched.
82                """
83                for define in makefile[key]:
84                    matched = DEFINE_REGEX_MAKEFILE.match(define)
85                    if matched:
86                        defines.add(matched.group(1))
87    return defines
88
89def manipulate_headerfile(defines, header_file):
90    """Wraps all defines used in an ifndef."""
91
92    # This regex matches the actual define in the header file.
93    modified_content = ""
94    with open(header_file, "r") as source:
95        last = ""
96        for line in source:
97            match = DEFINE_REGEX_HEADER.match(line)
98            if (match and
99                    match.group(1) in defines and
100                    not last.lstrip().startswith("#ifndef")):
101                full_def = line
102                # this loop deals with multiline definitions
103                while line.rstrip().endswith("\\"):
104                    line = next(source)
105                    full_def += line
106                # indentation for multiline definitions can be improved
107                modified_content += textwrap.dedent("""\
108                    #ifndef {target}
109                        {original}\
110                    #endif
111                    """.format(target=match.group(1), original=full_def))
112            else:
113                modified_content += line
114            last = line
115    with open(header_file, "w") as output:
116        output.write(modified_content)
117
118
119def header_dirty(header_files):
120    """Check that the header_file is not previously modified."""
121
122    # Git does not update the modified file list returned by diff-files on
123    # apply -R (at least not on MacOS).
124    # Running git status updates git's internal state.
125    status = subprocess.run(["git", "status"], stdout=subprocess.DEVNULL,
126                            stderr=subprocess.PIPE, universal_newlines=True)
127
128    diff_state = subprocess.run(["git", "diff-files"], stdout=subprocess.PIPE,
129                                stderr=subprocess.PIPE, universal_newlines=True)
130
131    if status.returncode:
132        raise DirtyGitError(textwrap.dedent("""\
133                Could not run git status. Exited: {}
134                stderr: {}
135                """.format(status.returncode, status.stderr)))
136
137    if diff_state.returncode:
138        raise DirtyGitError(textwrap.dedent("""\
139                Could not run git diff-files. Exited: {}
140                stderr: {}
141                """.format(diff_state.returncode, diff_state.stderr)))
142
143    for header_file in header_files:
144        if os.path.basename(header_file) + "\n" in diff_state.stdout:
145            return True
146    return False
147
148
149def create_patch(defines, header_file):
150    """Computes a patch enclosing defines used in CBMC proofs with #ifndef."""
151    manipulate_headerfile(defines, header_file)
152    patch = subprocess.run(["git", "diff", header_file],
153                           stdout=subprocess.PIPE,
154                           stderr=subprocess.PIPE, universal_newlines=True)
155    cleaned = subprocess.run(["git", "checkout", "--", header_file],
156                             stdout=subprocess.DEVNULL,
157                             stderr=subprocess.PIPE, universal_newlines=True)
158
159    if patch.returncode:
160        raise PatchCreationError(textwrap.dedent("""\
161                git diff exited with error code: {}
162                stderr: {}
163                """.format(patch.returncode, patch.stderr)))
164
165    if cleaned.returncode:
166        raise DirtyGitError(textwrap.dedent("""\
167                git checkout for cleaning files failed with error code: {}
168                on file {}
169                stderr: {}
170                """.format(cleaned.returncode, header_file, cleaned.stderr)))
171
172    header_path_part = header_file.replace(os.sep, "_")
173    path_name = "auto_patch_" + header_path_part + ".patch"
174    path_name = os.path.join(PATCHES_DIR, path_name)
175    if patch.stdout:
176        with open(path_name, "w") as patch_file:
177            patch_file.write(patch.stdout)
178
179
180def create_patches(headers):
181    defines = find_all_defines()
182
183    if not header_dirty(headers):
184        for header in headers:
185            create_patch(defines, header)
186    else:
187        raise DirtyGitError(textwrap.dedent("""\
188                It seems like one of the header files is in dirty state.
189                This script cannot patch files in dirty state.
190                """))
191
192# Invoke 'python3 -m unittest compute_patch.py" for running tests.
193class TestDefineRegexes(unittest.TestCase):
194    def test_makefile_regex(self):
195        input1 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}"
196        input2 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES=50"
197        input3 = "'configASSERT(X)=__CPROVER_assert(x, \"must hold\")'"
198        input4 = '"configASSERT (X)=__CPROVER_assert(x, "must hold")"'
199        input5 = "configASSERT(X)=__CPROVER_assert(x,\"must hold\")"
200
201        match1 = DEFINE_REGEX_MAKEFILE.match(input1)
202        match2 = DEFINE_REGEX_MAKEFILE.match(input2)
203        match3 = DEFINE_REGEX_MAKEFILE.match(input3)
204        match4 = DEFINE_REGEX_MAKEFILE.match(input4)
205        match5 = DEFINE_REGEX_MAKEFILE.match(input5)
206
207        self.assertIsNotNone(match1)
208        self.assertIsNotNone(match2)
209        self.assertIsNotNone(match3)
210        self.assertIsNotNone(match4)
211        self.assertIsNotNone(match5)
212
213        self.assertEqual(match1.group(1),
214                         "ipconfigETHERNET_MINIMUM_PACKET_BYTES")
215        self.assertEqual(match2.group(1),
216                         "ipconfigETHERNET_MINIMUM_PACKET_BYTES")
217        self.assertEqual(match3.group(1), "configASSERT")
218        self.assertEqual(match4.group(1), "configASSERT")
219        self.assertEqual(match5.group(1), "configASSERT")
220
221
222    def test_header_regex(self):
223        input1 = ("#define configASSERT( x )    if( ( x ) == 0 )" +
224                  "vAssertCalled( __FILE__, __LINE__ )")
225        input2 = "#define ipconfigMAX_ARP_RETRANSMISSIONS           ( 5 )"
226        input3 = "#define ipconfigINCLUDE_FULL_INET_ADDR            1"
227
228        match1 = DEFINE_REGEX_HEADER.match(input1)
229        match2 = DEFINE_REGEX_HEADER.match(input2)
230        match3 = DEFINE_REGEX_HEADER.match(input3)
231
232        self.assertIsNotNone(match1)
233        self.assertIsNotNone(match2)
234        self.assertIsNotNone(match3)
235
236        self.assertEqual(match1.group(1), "configASSERT")
237        self.assertEqual(match2.group(1), "ipconfigMAX_ARP_RETRANSMISSIONS")
238        self.assertEqual(match3.group(1), "ipconfigINCLUDE_FULL_INET_ADDR")
239
240if __name__ == '__main__':
241    create_patches(HEADERS)
242