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