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