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 8import argparse 9import errno 10import fnmatch 11import glob 12import os 13import re 14import shutil 15import subprocess 16import tempfile 17import time 18 19# Create a temporary directory 20 21 22class TempDir(): 23 def __init__(self, cleanup=True): 24 self.cleanup = cleanup 25 26 def __enter__(self): 27 self.filename = tempfile.mkdtemp() 28 return self.filename 29 30 def __exit__(self, type, value, traceback): 31 if self.cleanup: 32 shutil.rmtree(self.filename) 33 return False 34 35 36def mkdir_p(path): 37 try: 38 os.makedirs(path) 39 except OSError as exc: 40 if exc.errno == errno.EEXIST: 41 pass 42 else: 43 raise 44 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 55 56def read_manifest(filename, base): 57 """Read the files described in a MANIFEST file, which has the form: 58 59 foo/filepattern: 60 description 61 62 bar/filepattern: 63 description 64 65 and return a list of basedir/file pairs. All filenames are w.r.t. 66 the "base" directory. 67 """ 68 results = [] 69 with open(filename) as f: 70 for line in f.xreadlines(): 71 line = line.strip("\r\n") 72 if not line.startswith(" ") and line.endswith(":"): 73 pattern = line.strip().strip(":") 74 base_dir = os.path.split(pattern)[0] 75 g = glob.glob(os.path.join(base, pattern)) 76 if len(g) == 0: 77 print("Warning: Pattern '%s' matches 0 files." % pattern) 78 results += [(base_dir, x) for x in g] 79 return results 80 81 82def copy_manifest(output_dir, manifest_file, manifest_base, target): 83 """ 84 Given a manifest file "manifest_file" and a base directory "manifest_base" 85 used as the source of the filenames listed in the manifest, copy the 86 files into a subdirectory "target" of "output_dir". 87 88 Returns the manifest when done. 89 """ 90 manifest_dest = os.path.join(output_dir, target) 91 os.mkdir(manifest_dest) 92 dir_src = os.path.join(args.repository, manifest_base) 93 all_files = read_manifest(manifest_file, dir_src) 94 for (b, i) in sorted(all_files): 95 mkdir_p(os.path.join(manifest_dest, b)) 96 src = os.path.join(dir_src, i) 97 dst = os.path.join(manifest_dest, b, os.path.split(i)[1]) 98 if os.path.isdir(src): 99 shutil.copytree(src, dst, symlinks=True) 100 else: 101 shutil.copyfile(src, dst) 102 return all_files 103 104 105# Check usage. 106parser = argparse.ArgumentParser( 107 description='Generate autocorres release tarball.') 108parser.add_argument('version', metavar='VERSION', 109 type=str, help='Version number of the release, such as "0.95-beta1".') 110parser.add_argument('cparser_tar', metavar='CPARSER_RELEASE', 111 type=str, help='Tarball to the C parser release.') 112parser.add_argument('isabelle_tar', metavar='ISABELLE_TARBALL', 113 type=str, help='Tarball to the official Isabelle release') 114parser.add_argument('-b', '--browse', action='store_true', 115 help='Open shell to browse output prior to tar\'ing.') 116parser.add_argument('-o', '--output', metavar='FILENAME', 117 default=None, help='Output filename. Defaults to "autocorres-<VERSION>.tar.gz".') 118parser.add_argument('--dry-run', action='store_true', 119 help='Do not output any files.', default=False) 120parser.add_argument('-t', '--test', action='store_true', default=False, 121 help='Test the archive.') 122parser.add_argument('--no-cleanup', action='store_true', 123 help='Don''t delete temporary directories.', default=False) 124parser.add_argument('-r', '--repository', metavar='REPO', 125 type=str, help='Path to the L4.verified repository base.', default=None) 126parser.add_argument('--archs', metavar='ARCH,...', 127 type=str, default='ARM,ARM_HYP,X64,RISCV64', 128 help='L4V_ARCHs to include (comma-separated)') 129args = parser.parse_args() 130 131args.archs = args.archs.split(',') 132 133# Setup output filename if the user used the default. 134if args.output is None: 135 args.output = "autocorres-%s.tar.gz" % args.version 136 137# If no repository was specified, assume it is in the cwd. 138if args.repository is None: 139 try: 140 args.repository = subprocess.check_output([ 141 "git", "rev-parse", "--show-toplevel"]).strip() 142 except subprocess.CalledProcessError: 143 parser.error("Could not determine repository location.") 144 145# Get absolute paths to files. 146args.repository = os.path.abspath(args.repository) 147if not args.dry_run: 148 args.output = os.path.abspath(args.output) 149else: 150 args.output = None 151release_files_dir = os.path.join(args.repository, "tools", "autocorres", "tools", "release_files") 152 153# Ensure C-parser exists, and looks like a tarball. 154if not os.path.exists(args.cparser_tar) or not args.cparser_tar.endswith(".tar.gz"): 155 parser.error("Expected a path to the C parser release tarball.") 156args.cparser_tar = os.path.abspath(args.cparser_tar) 157 158# Ensure Isabelle exists, and looks like a tarball. 159if not os.path.exists(args.isabelle_tar) or not args.isabelle_tar.endswith(".tar.gz"): 160 parser.error("Expected a path to the official Isabelle release.") 161args.isabelle_tar = os.path.abspath(args.isabelle_tar) 162 163# Tools for theory dependencies. 164thydeps_tool = os.path.join(args.repository, 'misc', 'scripts', 'thydeps') 165repo_isabelle_dir = os.path.join(args.repository, 'isabelle') 166 167# User's preferred shell, if any. 168user_shell = os.environ.get('SHELL', '/bin/sh') 169 170# Create temp dir. 171with TempDir(cleanup=(not args.no_cleanup)) as base_dir: 172 # Generate base directory. 173 target_dir_name = "autocorres-%s" % args.version 174 target_dir = os.path.join(base_dir, target_dir_name) 175 os.mkdir(target_dir) 176 177 # Copy autocorres files. 178 print("Copying files...") 179 ac_files = copy_manifest(target_dir, 180 os.path.join(release_files_dir, "AUTOCORRES_FILES"), 181 os.path.join(args.repository, "tools", "autocorres"), "autocorres") 182 183 # Copy theories from dependent sessions in the lib directory. 184 lib_deps = '' 185 for arch in args.archs: 186 lib_deps += subprocess.check_output( 187 [thydeps_tool, '-I', repo_isabelle_dir, '-d', '.', '-d', 'tools/autocorres/tests', 188 '-b', 'lib', '-r', 189 'AutoCorresTest'], 190 cwd=args.repository, env=dict(os.environ, L4V_ARCH=arch)) 191 lib_deps = sorted(set(lib_deps.splitlines())) 192 193 for f in lib_deps: 194 f_src = os.path.join(args.repository, 'lib', f) 195 f_dest = os.path.join(target_dir, 'lib', os.path.relpath(f, args.repository)) 196 mkdir_p(os.path.dirname(f_dest)) 197 shutil.copyfile(f_src, f_dest) 198 199 # Copy various other files. 200 shutil.copyfile( 201 os.path.join(args.repository, 'lib', 'Word_Lib', 'ROOT'), 202 os.path.join(target_dir, 'lib', 'Word_Lib', 'ROOT')) 203 shutil.copyfile( 204 os.path.join(release_files_dir, "ROOT.release"), 205 os.path.join(target_dir, "autocorres", "ROOT")) 206 shutil.copyfile( 207 os.path.join(release_files_dir, "ROOTS.base_dir"), 208 os.path.join(target_dir, "ROOTS")) 209 for i in ["README", "ChangeLog"]: 210 shutil.copyfile( 211 os.path.join(release_files_dir, i), 212 os.path.join(target_dir, i)) 213 shutil.copyfile( 214 os.path.join(release_files_dir, "CONTRIBUTORS"), 215 os.path.join(target_dir, "autocorres", "CONTRIBUTORS")) 216 217 # License files. 218 shutil.copytree( 219 os.path.join(args.repository, "LICENSES"), 220 os.path.join(target_dir, "LICENSES")) 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, 303 "--strip-components=1", "-f", args.cparser_tar]) 304 # The C parser uses mllex and mlyacc to generate its grammar. We build 305 # the grammar files so that our release won't have a dependency on mlton. 306 print("Generating C parser grammar files...") 307 subprocess.check_call(['make', 'c-parser-deps'], 308 cwd=os.path.join(c_parser_working_dir, "src", "c-parser")) 309 shutil.move(os.path.join(c_parser_working_dir, "src", "c-parser"), 310 os.path.join(target_dir, "c-parser")) 311 shutil.move(os.path.join(c_parser_working_dir, "README.md"), 312 os.path.join(target_dir, "c-parser", "README.md")) 313 shutil.move(os.path.join(c_parser_working_dir, "doc", "ctranslation.pdf"), 314 os.path.join(target_dir, "c-parser", "doc", "ctranslation.pdf")) 315 316 # Double-check our theory dependencies. 317 if os.path.exists(thydeps_tool): 318 print("Checking theory dependencies...") 319 thy_deps = '' 320 for arch in args.archs: 321 thy_deps += subprocess.check_output( 322 [thydeps_tool, '-I', repo_isabelle_dir, '-b', '.', '-r', 323 'AutoCorres', 'AutoCorresTest'], 324 cwd=target_dir, env=dict(os.environ, L4V_ARCH=arch)) 325 thy_deps = sorted(set(thy_deps.splitlines())) 326 needed_files = [os.path.join(args.repository, f) 327 for f in thy_deps 328 if f.startswith('tools/autocorres')] 329 330 manifest_files = [os.path.join(dir, file) for dir, file in ac_files] 331 missing_files = [f for f in needed_files if f not in manifest_files] 332 if missing_files: 333 print("Warning: missing dependencies from release manifest:") 334 for f in missing_files: 335 print(" - %s" % f) 336 else: 337 print("Warning: cannot check theory dependencies: missing tool %r" % thydeps_tool) 338 339 # Check for bad strings. 340 print("Searching for bad strings...") 341 for s in ["davidg", "dgreenaway", "jlim", "jalim", "autorefine"]: 342 ret = subprocess.call(["grep", "-i", "-r", s, base_dir]) 343 if not ret: 344 raise Exception("Found a bad string") 345 346 # Set modified date of everything. 347 print("Setting file modification/access dates...") 348 target_time = int(time.mktime(time.localtime())) 349 for (root, dirs, files) in os.walk(base_dir, followlinks=False): 350 for i in dirs + files: 351 os.utime(os.path.join(root, i), (target_time, target_time)) 352 353 # Extract the Isabelle release 354 print("Extracting Isabelle...") 355 base_isabelle_dir = os.path.join(base_dir, "isabelle") 356 mkdir_p(base_isabelle_dir) 357 subprocess.check_call(["tar", "-xz", "-C", base_isabelle_dir, 358 "--strip-components=1", "-f", args.isabelle_tar]) 359 base_isabelle_bin = os.path.join(base_isabelle_dir, "bin", "isabelle") 360 assert os.path.exists(base_isabelle_bin) 361 362 # Build the documentation. 363 def build_docs(tree, isabelle_bin): 364 with TempDir() as doc_build_dir: 365 # Make a copy of the directory, so we don't pollute it. 366 shutil.copytree(tree, os.path.join(doc_build_dir, "doc"), symlinks=True) 367 368 # Build the docs. 369 try: 370 subprocess.check_call( 371 [isabelle_bin, "build", "-c", "-d", ".", "-d", 372 "./autocorres/doc/quickstart", "-v", "AutoCorresQuickstart"], 373 cwd=os.path.join(doc_build_dir, "doc"), env=dict(os.environ, L4V_ARCH="ARM")) 374 except subprocess.CalledProcessError: 375 print("Building documentation failed.") 376 if args.browse: 377 subprocess.call(user_shell, cwd=target_dir) 378 379 # Copy the generated PDF into our output. 380 shutil.copyfile( 381 os.path.join(doc_build_dir, "doc", "autocorres", "doc", 382 "quickstart", "output", "document.pdf"), 383 os.path.join(tree, "quickstart.pdf")) 384 print("Building documentation...") 385 build_docs(target_dir, base_isabelle_bin) 386 387 # Compress everything up. 388 if args.output != None: 389 print("Creating tarball...") 390 subprocess.check_call(["tar", "-cz", "--numeric-owner", 391 "--owner", "nobody", "--group", "nogroup", 392 "-C", base_dir, "-f", args.output, target_dir_name]) 393 394 # Run a test if requested. 395 if args.test: 396 print("Testing release...") 397 try: 398 subprocess.check_call([base_isabelle_bin, "version"], cwd=target_dir) 399 for arch in args.archs: 400 subprocess.check_call([base_isabelle_bin, "build", "-d", ".", "-v", 401 "AutoCorres", "AutoCorresTest"], 402 cwd=target_dir, env=dict(os.environ, L4V_ARCH=arch)) 403 except subprocess.CalledProcessError: 404 print("Test failed") 405 if args.browse: 406 subprocess.call(user_shell, cwd=target_dir) 407 408 # Open a shell in the directory if requested. 409 if args.browse: 410 print("Opening shell...") 411 subprocess.call(user_shell, cwd=target_dir) 412