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