1#!/bin/bash 2# 3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 4# 5# SPDX-License-Identifier: BSD-2-Clause 6# 7 8set -e 9 10ORIG_PWD="$PWD" 11 12function find_dir () { 13 cd $ORIG_PWD 14 while [[ "/$PWD" != '//' ]] 15 do 16 if [[ -d "./$1" ]] 17 then 18 FOUND_PWD="$(pwd)/$1" 19 if [[ ! -z "$V" ]] 20 then echo "Found $FOUND_PWD" 1>&2 21 fi 22 echo "$FOUND_PWD" 23 return 0 24 fi 25 cd .. 26 done 27 echo "Could not find a directory containing $1" 1>&2 28 echo " in any parent directory." 1>&2 29 exit 1 30} 31 32TRANSLATOR=$(find_dir "tools/haskell-translator") 33 34SPEC=$(find_dir "spec/design") 35 36if [[ -z $L4CAP ]] 37then 38 L4CAP=$(find_dir "spec/haskell") 39 export L4CAP 40fi 41 42if [[ ! -d $L4CAP/src/SEL4 ]] 43then 44 echo "This script is using L4CAP == $L4CAP" 45 echo Set the L4CAP environment variable to the location 46 echo of the haskell kernel source. 47 exit 1 48fi 49 50SKEL="$SPEC/skel" 51MSKEL="$SPEC/m-skel" 52 53MACH="$SPEC/../machine" 54 55if [[ ! -d $SKEL ]] 56then 57 echo Error: $SKEL is not a directory. 58 echo "(this script may have found the wrong spec $SPEC)" 59 exit 60fi 61 62# which architectures to process 63ARCHES=("ARM" "RISCV64" "X64" "ARM_HYP") 64 65# Match the CPP configuration used by SEL4.cabal and Setup.hs for Haskell build 66# Note: these should be in sync with both the Haskell .cabal and Setup.hs, 67# If these are not in sync, expect the unexpected. 68# spec_check.sh has a copy of these, which should be updated in tandem. 69# FIXME: move to a common location in haskell-translator (D.R.Y.) 70function cpp_opts () { 71 case ${1} in 72 ARM) 73 L4CPP="-DPLATFORM=QEmu -DPLATFORM_QEmu -DTARGET=ARM -DTARGET_ARM" 74 ;; 75 ARM_HYP) 76 L4CPP="-DPLATFORM=TK1 -DPLATFORM_TK1 -DTARGET=ARM -DTARGET_ARM -DCONFIG_ARM_HYPERVISOR_SUPPORT" 77 ;; 78 RISCV64) 79 L4CPP="-DPLATFORM=HiFive -DPLATFORM_HiFive -DTARGET=RISCV64 -DTARGET_RISCV64" 80 ;; 81 *) 82 echo "Warning: No CPP configuration for achitecture ${1}" 83 L4CPP="" 84 esac 85 export L4CPP 86} 87 88NAMES=`cd $SKEL; ls *.thy` 89 90SPECNONARCH="/tmp/make_spec_temp_nonarch_$$" 91TMPFILE="/tmp/make_spec_temp_$$" 92 93# Delete on exit 94trap "rm -fr $SPECNONARCH $TMPFILE" EXIT 95 96function send_filenames () { 97 local arch=${1} 98 local archnames=`cd $SKEL/${arch}; ls *.thy` 99 local archmnames=`cd $MSKEL/${arch}; ls *.thy` 100 mkdir -p "$SPEC/${arch}" 101 mkdir -p "$SPECNONARCH/${arch}" 102 103 # Theory files common to all haskell specifications 104 for NAME in $NAMES 105 do 106 echo "$SKEL/$NAME --> $SPECNONARCH/${arch}/$NAME" 107 done 108 109 # Arch-specific haskell specifications 110 for NAME in ${archnames} 111 do 112 echo "$SKEL/${arch}/$NAME --> $SPEC/${arch}/$NAME" 113 done 114 115 # Arch-specific machine theories, imported by haskell and abstract 116 for MNAME in ${archmnames} 117 do 118 echo "$MSKEL/${arch}/$MNAME --> $MACH/${arch}/$MNAME" 119 done 120} 121 122# Ensure that non-arch-specific theories are identical after preprocessing 123for ARCH in ${ARCHES[@]} 124do 125 send_filenames $ARCH > $TMPFILE 126 cpp_opts $ARCH 127 cd $TRANSLATOR 128 python3 pars_skl.py $TMPFILE 129done 130 131for ARCH in ${ARCHES[@]} 132do 133 specdiff=`diff "$SPECNONARCH/${ARCHES[0]}" "$SPECNONARCH/$ARCH"` 134 if [ -n "${specdiff}" ]; then 135 echo "Non arch-specific haskell translations differ:" 1>&2 136 echo "${specdiff}" 1>&2 137 exit 1 138 fi 139done 140 141for thy in $SPECNONARCH/${ARCHES[0]}/*.thy; do rsync -c "$thy" "$SPEC/"; done 142 143echo Built from git repo at $L4CAP by $USER > $SPEC/version 144echo >> $SPEC/version 145echo Generated from changeset: >> $SPEC/version 146(cd $L4CAP && git show --oneline | head -1) >> $SPEC/version 147echo >> $SPEC/version 148if [ "$(cd $L4CAP && git status --short)" != "" ] 149then 150 echo >> $SPEC/version 151 echo Warning - uncomitted changes used: >> $SPEC/version 152 (cd $L4CAP && git status --short) >> $SPEC/version 153fi 154