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