1#!/usr/bin/env python3
2#
3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4#
5# SPDX-License-Identifier: BSD-2-Clause
6#
7
8#
9# Generate the file "umm_types.txt", required for generating theory files used
10# in Isabelle sessions "CSpec" and beyond.
11#
12
13import subprocess
14import argparse
15import os
16import sys
17import tempfile
18import shutil
19
20# Create a temporary directory
21
22
23class TempDir(object):
24    def __enter__(self, cleanup=True):
25        self.filename = tempfile.mkdtemp()
26        self.cleanup = cleanup
27        return self.filename
28
29    def __exit__(self, type, value, traceback):
30        if self.cleanup:
31            shutil.rmtree(self.filename)
32        return False
33
34
35parser = argparse.ArgumentParser(
36    description="Generate a 'umm_types.txt' file from the C parser, required by the bitfield generator.")
37parser.add_argument('input', metavar='INPUT', type=str,
38                    help="C file to parse")
39parser.add_argument('output', metavar='OUTPUT', type=str,
40                    help="output filename")
41parser.add_argument('--root', metavar='ROOT', type=str,
42                    help="add Isabelle ROOT or ROOTS file path", action='append')
43args = parser.parse_args()
44
45if "ISABELLE_PROCESS" not in os.environ or "ISABELLE_TOOL" not in os.environ:
46    print("Run this from within 'isabelle env'.")
47    sys.exit(1)
48
49THY_DATA = """
50theory UmmTypesFile
51  imports CParser.CTranslation
52begin
53declare [[allow_underscore_idents = true]]
54external_file "%(input)s"
55setup {* IsarInstall.gen_umm_types_file "%(input)s" "%(output)s" *}
56end
57"""
58
59ROOT_DATA = """
60session UmmTypes = CParser +
61  theories UmmTypesFile
62"""
63
64# Create a new theory file and ROOT file in a temporary directory.
65with TempDir() as tmp_dir:
66    filenames = {
67        "input": os.path.abspath(args.input),
68        "output": os.path.abspath(args.output),
69    }
70    with open(os.path.join(tmp_dir, "UmmTypesFile.thy"), "w") as f:
71        f.write(THY_DATA % filenames)
72    with open(os.path.join(tmp_dir, "ROOT"), "w") as f:
73        f.write(ROOT_DATA % filenames)
74
75    # Run Isabelle over it.
76    def interleave(a, l):
77        result = []
78        for x in l:
79            result.append(a)
80            result.append(x)
81        return result
82    print("\nGenerating umm_types data file...\n")
83    subprocess.check_call([
84        os.environ["ISABELLE_TOOL"], "build", "-c"]
85        + interleave("-d", [os.path.abspath(x) for x in args.root])
86        + ["-d", ".", "-v", "-b", "UmmTypes"],
87        cwd=tmp_dir)
88