1#!/bin/bash
2#
3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4#
5# SPDX-License-Identifier: BSD-2-Clause
6#
7
8#
9# Generate a standalone tarball of the C parser.
10#
11
12set -e
13
14case $(uname) in
15  Darwin* ) TAR=gnutar ; SEDIOPT="-i ''" ;;
16  * ) TAR=tar ; SEDIOPT=-i ;;
17esac
18
19
20warn ()
21{
22  echo "$1" >&2
23}
24
25die ()
26{
27  echo "$1" >&2
28  echo "Fatal error"
29  exit 1
30}
31
32if [ $# -ne 1 ]
33then
34    echo "Usage:" >&2
35    die "  $0 tag" >&2
36fi
37
38# Get the directory that this script is running in.
39CPARSER_DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
40TOPLEVEL_DIR=$( git -C ${CPARSER_DIR} rev-parse --show-toplevel)
41RELEASE_ARCHS='ARM ARM_HYP X64 RISCV64'
42pushd "${TOPLEVEL_DIR}"
43
44# Ensure that our working directory is clean.
45if git status --porcelain | grep -q -v '^??' ; then
46    if [[ -v ALLOW_DIRTY ]]; then
47        warn "WARNING: Dirty working tree."
48    else
49        warn "ERROR: Dirty working tree. Set the environment vairable ALLOW_DIRTY to ignore."
50        exit 1
51    fi
52fi
53
54# Create working directories.
55tmpdir=$(mktemp -d)
56outputdir=$tmpdir/c-parser
57echo "Outputs being placed in \"${outputdir}\"."
58
59# Parse command line arguments.
60tag=$1
61stem=c-parser-$tag
62shift
63
64[ -a "$stem" ] && die "Directory $stem already exists."
65
66safemakedir ()
67{
68    if [ ! -d "$1" ]
69    then
70        warn "Creating $1"
71        mkdir -p "$1"
72    else
73        warn "WARNING: release will be merged with existing $1 directory"
74    fi
75}
76safemakedir "$outputdir/src/lib"
77safemakedir "$outputdir/src/c-parser"
78safemakedir "$outputdir/doc"
79
80
81echo "Tarring standard sources"
82# Some testfiles have non-ASCII filenames, so we need git ls-files -z. Ugh.
83git -C "${TOPLEVEL_DIR}" ls-files -z | tr '\0' '\n' |
84    grep ^tools/c-parser |
85    grep -v tools/c-parser/notes |
86    grep -v tools/c-parser/mkrelease |
87   tar -v -T - -c -f - -l |
88  (cd "$outputdir/src" ; tar xf -)
89
90echo "Getting theory dependencies"
91CPARSER_DEPS=$(tempfile)
92for ARCH in $RELEASE_ARCHS; do
93    L4V_ARCH=$ARCH misc/scripts/thydeps -I ./isabelle -d . -b . -r CParser
94done |
95    sort -u >"$CPARSER_DEPS"
96
97if grep -q -vE '^(lib/|tools/c-parser/)' "$CPARSER_DEPS"; then
98    echo >&2 'unexpected dependencies outside lib/ and tools/c-parser/:'
99    grep >&2 -vE '^(lib/|tools/c-parser/)' "$CPARSER_DEPS"
100    exit 1
101fi
102
103echo "Copying misc files"
104grep '^lib/' "$CPARSER_DEPS" |
105    xargs '-d\n' cp -v --parents -t "$outputdir/src"
106
107# other misc files
108cp -v --parents -t "$outputdir/src" \
109   lib/Word_Lib/ROOT
110
111echo "Creating ROOTS file"
112cat >"$outputdir/src/ROOTS" <<EOF
113lib/Word_Lib
114lib
115c-parser
116EOF
117
118echo "Adding ROOT file for Lib session"
119cat > "$outputdir/src/lib/ROOT" <<EOF
120(*
121 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
122 *
123 * SPDX-License-Identifier: BSD-2-Clause
124 *)
125
126session Lib = HOL +
127  directories "ml-helpers"
128  theories "MLUtils"
129EOF
130
131echo "Rearranging directories"
132/bin/mv -v "$outputdir/src/tools/c-parser/README.md" "$outputdir"
133/bin/mv -v "$outputdir/src/tools/c-parser" "$outputdir/src/"
134rmdir "$outputdir/src/tools"
135
136echo "Removing files"
137/bin/rm -v "$outputdir/src/c-parser/testfiles/many_local_vars".{c,thy}
138
139echo "Executing gen_isabelle_root to generate testfiles/\$L4V_ARCH/ROOT."
140for L4V_ARCH in $RELEASE_ARCHS; do
141    python3 misc/scripts/gen_isabelle_root.py -i "$outputdir/src/c-parser/testfiles" -i "$outputdir/src/c-parser/testfiles/${L4V_ARCH}" -o "$outputdir/src/c-parser/testfiles/$L4V_ARCH/ROOT" -s CParserTest -b CParser --dir ".." --dir "imports" ||
142        die "gen_isabelle_root failed."
143done
144
145echo "Executing gen_isabelle_root to generate testfiles/all_tests_\$L4V_ARCH.thy."
146for L4V_ARCH in $RELEASE_ARCHS; do
147    python3 misc/scripts/gen_isabelle_root.py -T -o "$outputdir/src/c-parser/all_tests_${L4V_ARCH}.thy" -b CParser -i "$outputdir/src/c-parser/testfiles" -i "$outputdir/src/c-parser/testfiles/${L4V_ARCH}" ||
148        die "gen_isabelle_root failed."
149done
150
151echo "Hacking Makefile to remove ROOT generation."
152if ! grep -q '^testfiles/\$(L4V_ARCH)/ROOT' "$outputdir/src/c-parser/Makefile"; then
153    die "failed to process c-parser/Makefile"
154fi
155sed $SEDIOPT \
156    -e '/^testfiles\/\$(L4V_ARCH)\/ROOT/,/CParserTest/d' \
157    -e '/^all_tests_\$(L4V_ARCH)\.thy/,/CParser/d' \
158    "$outputdir/src/c-parser/Makefile"
159
160echo "Hacking Makefile to change root dir."
161if ! grep -q '^L4V_ROOT_DIR = ' "$outputdir/src/c-parser/Makefile"; then
162    die "failed to process c-parser/Makefile"
163fi
164sed $SEDIOPT \
165    -e 's/^L4V_ROOT_DIR = .*$/L4V_ROOT_DIR = ../' \
166    "$outputdir/src/c-parser/Makefile"
167
168echo "Generating standalone-parser/table.ML"
169pushd "$TOPLEVEL_DIR/tools/c-parser" > /dev/null
170"$TOPLEVEL_DIR/isabelle/bin/isabelle" env make -f Makefile "$(pwd)/standalone-parser/table.ML" \
171    || die "Couldn't generate table.ML for standalone parser"
172cp standalone-parser/table.ML "$outputdir/src/c-parser/standalone-parser"
173echo "Cleaning up standalone-parser's Makefile"
174sed '
175  1i\
176  SML_COMPILER ?= mlton
177  /^include/d
178  /General\/table.ML/,/pretty-printing/d
179  /ISABELLE_HOME/d
180  /CLEAN_TARGETS/s|\$(STP_PFX)/table.ML||
181' < standalone-parser/Makefile > "$outputdir/src/c-parser/standalone-parser/Makefile"
182popd > /dev/null
183
184
185echo "Making PDF of ctranslation file."
186cd "$outputdir/src/c-parser/doc"
187make ctranslation.pdf > /dev/null
188/bin/rm ctranslation.{log,aux,blg,bbl,toc}
189mv ctranslation.pdf "$outputdir/doc"
190
191popd > /dev/null
192
193lookforlicense=$(find "$outputdir" \! -name '*.lex.sml' \! -name '*.grm.sml' \! -type d -exec grep -q @LICENSE \{\} \; -print)
194if [ -n "$lookforlicense" ]
195then
196    die "### @LICENSE detected in file(s) $lookforlicense"
197else
198    echo "No @LICENSEs remain unexpanded - good."
199fi
200
201lookformichaeln=$(find "$outputdir" \! -name RELEASES.md \! -type d -exec grep -q /michaeln \{\} \; -print)
202if [ -n "$lookformichaeln" ]
203then
204    die "### /michaeln detected in file(s) $lookformichaeln"
205else
206    echo "No occurrences of \"/michaeln\" - good."
207fi
208
209echo -n "Compressing into $stem.tar.gz: "
210mv "$tmpdir/c-parser" "$tmpdir/$stem"
211
212pushd "$tmpdir"
213"$TAR" --owner=nobody --group=nogroup -cvzf "${stem}.tar.gz" "$stem" |
214    while read ; do echo -n "." ; done
215popd
216/bin/mv -f -v "$tmpdir/${stem}.tar.gz" .
217
218echo
219echo Done.
220