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