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