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