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