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