1#!/usr/bin/env python3
2#
3# Creating the CBMC proofs from Configurations.json.
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
25import collections
26import json
27import logging
28import os
29import pathlib
30import shutil
31import textwrap
32
33from make_proof_makefiles import load_json_config_file
34
35LOGGER = logging.getLogger("ComputeConfigurations")
36
37def prolog():
38    return textwrap.dedent("""\
39        This script Generates Makefile.json from Configrations.json.
40
41        Starting in the current directory, it walks down every subdirectory
42        looking for Configurations.json files. Every found Configurations.json
43        file is assumed to look similar to the following format:
44
45        {
46          "ENTRY": "ARPProcessPacket",
47          "CBMCFLAGS":
48          [
49              "--unwind 1",
50              "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
51              "--nondet-static"
52          ],
53          "OBJS":
54          [
55            "$(ENTRY)_harness.goto",
56            "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
57          ],
58          "DEF":
59          [
60            {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]},
61            {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]}
62          ]
63        }
64
65        The format is mainly taken from the Makefile.json files.
66        The only difference is that it expects a list of json object in the DEF
67        section. This script will generate a Makefile.json in a subdirectory and
68        copy the harness to each subdirectory.
69        The key is later taken as the name for the configuration subdirectory
70        prexied by 'config_'.
71
72        So for the above script, we get two subdirectories:
73        -config_disableClashDetection
74        -config_enableClashDetection
75
76        As an example, the resulting Makefile.json for the
77        config_disableClashDetection directory will be:
78
79        {
80          "ENTRY": "ARPProcessPacket",
81          "CBMCFLAGS": [
82            "--unwind 1",
83            "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
84            "--nondet-static"
85          ],
86          "OBJS": [
87            "$(ENTRY)_harness.goto",
88            "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
89          ],
90          "DEF": [
91            "ipconfigARP_USE_CLASH_DETECTION=0"
92          ]
93        }
94
95        These Makefile.json files then can be turned into Makefiles for running
96        the proof by executing the make-proof-makefiles.py script.
97        """)
98
99
100def process(folder, files):
101    json_content = load_json_config_file(os.path.join(folder,
102                                                      "Configurations.json"))
103    try:
104        def_list = json_content["DEF"]
105    except KeyError:
106        LOGGER.error("Expected DEF as key in a Configurations.json files.")
107        return
108    for config in def_list:
109        logging.debug(config)
110        try:
111            configname = [name for name in config.keys()
112                          if name != "EXPECTED"][0]
113            configbody = config[configname]
114        except (AttributeError, IndexError) as e:
115            LOGGER.error(e)
116            LOGGER.error(textwrap.dedent("""\
117            The expected layout for an entry in the Configurations.json
118            file is a dictonary. Here is an example of the expected format:
119
120            "DEF":
121            [
122              {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]},
123              {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]}
124            ]
125                """))
126            LOGGER.error("The offending entry is %s", config)
127            return
128        new_config_folder = os.path.join(folder, "config_" + configname)
129        pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True)
130        harness_copied = False
131        for file in files:
132            if file.endswith("harness.c"):
133                shutil.copy(os.path.join(folder, file),
134                            os.path.join(new_config_folder, file))
135                harness_copied = True
136
137        if not harness_copied:
138            LOGGER.error("Could not find a harness in folder %s.", folder)
139            LOGGER.error("This folder is not processed do the end!")
140            return
141        # The order of keys must be maintained as otherwise the
142        # make_proof_makefiles script might fail.
143        current_config = collections.OrderedDict(json_content)
144        current_config["DEF"] = configbody
145        if "EXPECTED" in config.keys():
146            current_config["EXPECTED"] = config["EXPECTED"]
147        else:
148            current_config["EXPECTED"] = True
149        with open(os.path.join(new_config_folder, "Makefile.json"),
150                  "w") as output_file:
151            json.dump(current_config, output_file, indent=2)
152
153
154def main():
155    for fldr, _, fyles in os.walk("."):
156        if "Configurations.json" in fyles:
157            process(fldr, fyles)
158
159
160if __name__ == '__main__':
161    logging.basicConfig(format="{script}: %(levelname)s %(message)s".format(
162        script=os.path.basename(__file__)))
163    main()
164