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 12import argparse 13import errno 14import fnmatch 15import glob 16import os 17import re 18import shutil 19import subprocess 20import tempfile 21import time 22 23# Create a temporary directory 24class TempDir(): 25 def __init__(self, cleanup=True): 26 self.cleanup = cleanup 27 28 def __enter__(self): 29 self.filename = tempfile.mkdtemp() 30 return self.filename 31 32 def __exit__(self, type, value, traceback): 33 if self.cleanup: 34 shutil.rmtree(self.filename) 35 return False 36 37def mkdir_p(path): 38 try: 39 os.makedirs(path) 40 except OSError as exc: 41 if exc.errno == errno.EEXIST: 42 pass 43 else: 44 raise 45 46def rglob(base_path, pattern): 47 """Recursively find files matching glob pattern 'pattern', from base 48 directory 'base_path'.""" 49 results = [] 50 for root, dirnames, filenames in os.walk(base_path): 51 for filename in fnmatch.filter(filenames, pattern): 52 results.append(os.path.join(root, filename)) 53 return results 54 55def read_manifest(filename, base): 56 """Read the files described in a MANIFEST file, which has the form: 57 58 foo/filepattern: 59 description 60 61 bar/filepattern: 62 description 63 64 and return a list of basedir/file pairs. All filenames are w.r.t. 65 the "base" directory. 66 """ 67 results = [] 68 with open(filename) as f: 69 for line in f.xreadlines(): 70 line = line.strip("\r\n") 71 if not line.startswith(" ") and line.endswith(":"): 72 pattern = line.strip().strip(":") 73 base_dir = os.path.split(pattern)[0] 74 g = glob.glob(os.path.join(base, pattern)) 75 if len(g) == 0: 76 print("Warning: Pattern '%s' matches 0 files." % pattern) 77 results += [(base_dir, x) for x in g] 78 return results 79 80def copy_manifest(output_dir, manifest_file, manifest_base, target): 81 """ 82 Given a manifest file "manifest_file" and a base directory "manifest_base" 83 used as the source of the filenames listed in the manifest, copy the 84 files into a subdirectory "target" of "output_dir". 85 86 Returns the manifest when done. 87 """ 88 manifest_dest = os.path.join(output_dir, target) 89 os.mkdir(manifest_dest) 90 dir_src = os.path.join(args.repository, manifest_base) 91 all_files = read_manifest(manifest_file, dir_src) 92 for (b, i) in sorted(all_files): 93 mkdir_p(os.path.join(manifest_dest, b)) 94 src = os.path.join(dir_src, i) 95 dst = os.path.join(manifest_dest, b, os.path.split(i)[1]) 96 if os.path.isdir(src): 97 shutil.copytree(src, dst, symlinks=True) 98 else: 99 shutil.copyfile(src, dst) 100 return all_files 101 102# Check usage. 103parser = argparse.ArgumentParser( 104 description='Generate autocorres release tarball.') 105parser.add_argument('version', metavar='VERSION', 106 type=str, help='Version number of the release, such as "0.95-beta1".') 107parser.add_argument('cparser_tar', metavar='CPARSER_RELEASE', 108 type=str, help='Tarball to the C parser release.') 109parser.add_argument('isabelle_tar', metavar='ISABELLE_TARBALL', 110 type=str, help='Tarball to the official Isabelle release') 111parser.add_argument('-b', '--browse', action='store_true', 112 help='Open shell to browse output prior to tar\'ing.') 113parser.add_argument('-o', '--output', metavar='FILENAME', 114 default=None, help='Output filename. Defaults to "autocorres-<VERSION>.tar.gz".') 115parser.add_argument('--dry-run', action='store_true', 116 help='Do not output any files.', default=False) 117parser.add_argument('-t', '--test', action='store_true', default=False, 118 help='Test the archive.') 119parser.add_argument('--no-cleanup', action='store_true', 120 help='Don''t delete temporary directories.', default=False) 121parser.add_argument('-r', '--repository', metavar='REPO', 122 type=str, help='Path to the L4.verified repository base.', default=None) 123parser.add_argument('--archs', metavar='ARCH,...', 124 type=str, default='ARM,ARM_HYP,X64', 125 help='L4V_ARCHs to include (comma-separated)') 126args = parser.parse_args() 127 128args.archs = args.archs.split(',') 129 130# Setup output filename if the user used the default. 131if args.output is None: 132 args.output = "autocorres-%s.tar.gz" % args.version 133 134# If no repository was specified, assume it is in the cwd. 135if args.repository is None: 136 try: 137 args.repository = subprocess.check_output([ 138 "git", "rev-parse", "--show-toplevel"]).strip() 139 except subprocess.CalledProcessError: 140 parser.error("Could not determine repository location.") 141 142# Get absolute paths to files. 143args.repository = os.path.abspath(args.repository) 144if not args.dry_run: 145 args.output = os.path.abspath(args.output) 146else: 147 args.output = None 148release_files_dir = os.path.join(args.repository, "tools", "autocorres", "tools", "release_files") 149 150# Ensure C-parser exists, and looks like a tarball. 151if not os.path.exists(args.cparser_tar) or not args.cparser_tar.endswith(".tar.gz"): 152 parser.error("Expected a path to the C parser release tarball.") 153args.cparser_tar = os.path.abspath(args.cparser_tar) 154 155# Ensure Isabelle exists, and looks like a tarball. 156if not os.path.exists(args.isabelle_tar) or not args.isabelle_tar.endswith(".tar.gz"): 157 parser.error("Expected a path to the official Isabelle release.") 158args.isabelle_tar = os.path.abspath(args.isabelle_tar) 159 160# Tools for theory dependencies. 161thydeps_tool = os.path.join(args.repository, 'misc', 'scripts', 'thydeps') 162repo_isabelle_dir = os.path.join(args.repository, 'isabelle') 163 164# User's preferred shell, if any. 165user_shell = os.environ.get('SHELL', '/bin/sh') 166 167# Create temp dir. 168with TempDir(cleanup=(not args.no_cleanup)) as base_dir: 169 # Generate base directory. 170 target_dir_name = "autocorres-%s" % args.version 171 target_dir = os.path.join(base_dir, target_dir_name) 172 os.mkdir(target_dir) 173 174 # Copy autocorres files. 175 print("Copying files...") 176 ac_files = copy_manifest(target_dir, 177 os.path.join(release_files_dir, "AUTOCORRES_FILES"), 178 os.path.join(args.repository, "tools", "autocorres"), "autocorres") 179 180 # Copy theories from dependent sessions in the lib directory. 181 lib_deps = '' 182 for arch in args.archs: 183 lib_deps += subprocess.check_output( 184 [thydeps_tool, '-I', repo_isabelle_dir, '-d', '.', '-d', 'tools/autocorres/tests', 185 '-b', 'lib', '-r', 186 'AutoCorresTest'], 187 cwd=args.repository, env=dict(os.environ, L4V_ARCH=arch)) 188 lib_deps = sorted(set(lib_deps.splitlines())) 189 190 for f in lib_deps: 191 f_src = os.path.join(args.repository, 'lib', f) 192 f_dest = os.path.join(target_dir, 'lib', os.path.relpath(f, args.repository)) 193 mkdir_p(os.path.dirname(f_dest)) 194 shutil.copyfile(f_src, f_dest) 195 196 # Copy various other files. 197 shutil.copyfile( 198 os.path.join(args.repository, 'lib', 'Word_Lib', 'ROOT'), 199 os.path.join(target_dir, 'lib', 'Word_Lib', 'ROOT')) 200 shutil.copyfile( 201 os.path.join(release_files_dir, "ROOT.release"), 202 os.path.join(target_dir, "autocorres", "ROOT")) 203 shutil.copyfile( 204 os.path.join(release_files_dir, "ROOTS.base_dir"), 205 os.path.join(target_dir, "ROOTS")) 206 for i in ["README", "ChangeLog"]: 207 shutil.copyfile( 208 os.path.join(release_files_dir, i), 209 os.path.join(target_dir, i)) 210 shutil.copyfile( 211 os.path.join(release_files_dir, "CONTRIBUTORS"), 212 os.path.join(target_dir, "autocorres", "CONTRIBUTORS")) 213 214 # License files. 215 shutil.copyfile( 216 os.path.join(args.repository, "LICENSE_BSD2.txt"), 217 os.path.join(target_dir, "LICENSE_BSD2.txt")) 218 shutil.copyfile( 219 os.path.join(args.repository, "LICENSE_GPLv2.txt"), 220 os.path.join(target_dir, "LICENSE_GPLv2.txt")) 221 222 # Extract dependent sessions in lib. FIXME: rather kludgy 223 print('Extracting sessions from lib/ROOT...') 224 225 # Set up ROOT for the tests dir, for the thydeps tool 226 subprocess.check_call( 227 ['make', 'tests/ROOT'], 228 cwd=os.path.join(args.repository, 'tools', 'autocorres')) 229 230 lib_sessions = ['Lib', 'CLib'] 231 lib_ROOT = os.path.join(args.repository, 'lib', 'ROOT') 232 with open(lib_ROOT, 'r') as lib_root: 233 data = lib_root.read() 234 # Split out session specs. Assume ROOT file has standard indentation. 235 chunks = data.split('\nsession ') 236 # This will have the license header, etc. 237 header = chunks[0] 238 # Remaining sections. Try to remove comments 239 sessions = ['session ' + re.sub(r'\(\*.*?\*\)', '', x, flags=re.DOTALL) 240 for x in chunks[1:]] 241 242 new_root = header 243 wanted_specs = {} 244 for wanted in lib_sessions: 245 spec = [spec for spec in sessions if spec.startswith('session %s ' % wanted)] 246 if len(spec) != 1: 247 print('error: %s session not found in %r' % (wanted, lib_ROOT)) 248 new_root += '\n' + spec[0] 249 250 with open(os.path.join(target_dir, 'lib', 'ROOT'), 'w') as root_f: 251 root_f.write(new_root) 252 253 # For the examples, generate ".thy" files where appropriate, and also 254 # generate an "All.thy" which contains all the examples. 255 def gen_thy_file(c_file): 256 thy_file = os.path.splitext(c_file)[0] + ".thy" 257 base_name = os.path.splitext(os.path.basename(c_file))[0] 258 with open(thy_file, "w") as f: 259 f.write(''' 260theory %s 261imports 262 "AutoCorres.AutoCorres" 263begin 264 265install_C_file "%s" 266 267autocorres "%s" 268 269end 270 '''.strip() % (base_name, 271 os.path.basename(c_file), 272 os.path.basename(c_file) 273 )) 274 275 for f in glob.glob(os.path.join(target_dir, "autocorres", "tests", "parse-tests", "*.c")): 276 gen_thy_file(f) 277 subprocess.check_call([ 278 "python", 279 os.path.join(args.repository, "misc", "scripts", "gen_isabelle_root.py"), 280 "-T", "-o", os.path.join(target_dir, "autocorres", "tests", "AutoCorresTest.thy"), 281 "-i", os.path.join(target_dir, "autocorres", "tests", "parse-tests"), 282 "-i", os.path.join(target_dir, "autocorres", "tests", "proof-tests"), 283 "-i", os.path.join(target_dir, "autocorres", "tests", "examples"), 284 ]) 285 286 # Update include paths: change "../../lib" to "../lib". 287 def inplace_replace_string(filename, old_string, new_string): 288 with open(filename) as f: 289 data = f.read() 290 new_data = data.replace(old_string, new_string) 291 if new_data != data: 292 print(' replaced ../../lib with ../lib in %r' % filename) 293 with open(filename, "w") as f: 294 f.write(new_data) 295 for f in rglob(os.path.join(target_dir, "autocorres"), "*.thy"): 296 inplace_replace_string(f, "../../lib/", "../lib/") 297 298 # Extract the C parser 299 print("Extracting C parser...") 300 # We want to mix the C parser directory structure around a little. 301 with TempDir() as c_parser_working_dir: 302 subprocess.check_call(["tar", "-xz", "-C", c_parser_working_dir, "--strip-components=1", "-f", args.cparser_tar]) 303 # The C parser uses mllex and mlyacc to generate its grammar. We build 304 # the grammar files so that our release won't have a dependency on mlton. 305 print("Generating C parser grammar files...") 306 subprocess.check_call(['make', 'c-parser-deps'], cwd=os.path.join(c_parser_working_dir, "src", "c-parser")) 307 shutil.move(os.path.join(c_parser_working_dir, "src", "c-parser"), os.path.join(target_dir, "c-parser")) 308 shutil.move(os.path.join(c_parser_working_dir, "README"), os.path.join(target_dir, "c-parser", "README")) 309 shutil.move(os.path.join(c_parser_working_dir, "doc", "ctranslation.pdf"), os.path.join(target_dir, "c-parser", "doc", "ctranslation.pdf")) 310 311 # Double-check our theory dependencies. 312 if os.path.exists(thydeps_tool): 313 print("Checking theory dependencies...") 314 thy_deps = '' 315 for arch in args.archs: 316 thy_deps += subprocess.check_output( 317 [thydeps_tool, '-I', repo_isabelle_dir, '-b', '.', '-r', 318 'AutoCorres', 'AutoCorresTest'], 319 cwd=target_dir, env=dict(os.environ, L4V_ARCH=arch)) 320 thy_deps = sorted(set(thy_deps.splitlines())) 321 needed_files = [os.path.join(args.repository, f) 322 for f in thy_deps 323 if f.startswith('tools/autocorres')] 324 325 manifest_files = [os.path.join(dir, file) for dir, file in ac_files] 326 missing_files = [f for f in needed_files if f not in manifest_files] 327 if missing_files: 328 print("Warning: missing dependencies from release manifest:") 329 for f in missing_files: 330 print(" - %s" % f) 331 else: 332 print("Warning: cannot check theory dependencies: missing tool %r" % thydeps_tool) 333 334 # Check for bad strings. 335 print("Searching for bad strings...") 336 for s in ["davidg", "dgreenaway", "jlim", "jalim", "autorefine"]: 337 ret = subprocess.call(["grep", "-i", "-r", s, base_dir]) 338 if not ret: 339 raise Exception("Found a bad string") 340 341 # Set modified date of everything. 342 print("Setting file modification/access dates...") 343 target_time = int(time.mktime(time.localtime())) 344 for (root, dirs, files) in os.walk(base_dir, followlinks=False): 345 for i in dirs + files: 346 os.utime(os.path.join(root, i), (target_time, target_time)) 347 348 # Extract the Isabelle release 349 print("Extracting Isabelle...") 350 base_isabelle_dir = os.path.join(base_dir, "isabelle") 351 mkdir_p(base_isabelle_dir) 352 subprocess.check_call(["tar", "-xz", "-C", base_isabelle_dir, "--strip-components=1", "-f", args.isabelle_tar]) 353 base_isabelle_bin = os.path.join(base_isabelle_dir, "bin", "isabelle") 354 assert os.path.exists(base_isabelle_bin) 355 356 # Build the documentation. 357 def build_docs(tree, isabelle_bin): 358 with TempDir() as doc_build_dir: 359 # Make a copy of the directory, so we don't pollute it. 360 shutil.copytree(tree, os.path.join(doc_build_dir, "doc"), symlinks=True) 361 362 # Build the docs. 363 try: 364 subprocess.check_call( 365 [isabelle_bin, "build", "-c", "-d", ".", "-d", "./autocorres/doc/quickstart", "-v", "AutoCorresQuickstart"], 366 cwd=os.path.join(doc_build_dir, "doc"), env=dict(os.environ, L4V_ARCH="ARM")) 367 except subprocess.CalledProcessError: 368 print("Building documentation failed.") 369 if args.browse: 370 subprocess.call(user_shell, cwd=target_dir) 371 372 # Copy the generated PDF into our output. 373 shutil.copyfile( 374 os.path.join(doc_build_dir, "doc", "autocorres", "doc", "quickstart", "output", "document.pdf"), 375 os.path.join(tree, "quickstart.pdf")) 376 print("Building documentation...") 377 build_docs(target_dir, base_isabelle_bin) 378 379 # Compress everything up. 380 if args.output != None: 381 print("Creating tarball...") 382 subprocess.check_call(["tar", "-cz", "--numeric-owner", 383 "--owner", "nobody", "--group", "nogroup", 384 "-C", base_dir, "-f", args.output, target_dir_name]) 385 386 # Run a test if requested. 387 if args.test: 388 print("Testing release...") 389 try: 390 subprocess.check_call([base_isabelle_bin, "version"], cwd=target_dir) 391 for arch in args.archs: 392 subprocess.check_call([base_isabelle_bin, "build", "-d", ".", "-v", 393 "AutoCorres", "AutoCorresTest"], 394 cwd=target_dir, env=dict(os.environ, L4V_ARCH=arch)) 395 except subprocess.CalledProcessError: 396 print("Test failed") 397 if args.browse: 398 subprocess.call(user_shell, cwd=target_dir) 399 400 # Open a shell in the directory if requested. 401 if args.browse: 402 print("Opening shell...") 403 subprocess.call(user_shell, cwd=target_dir) 404 405