blob: 1fe2d182a412a2257289d17d0f482ba2989a546e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
#!/usr/bin/env bash
set -e
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
cd $DIR
SAILDIR="$DIR/../.."
LEMBUILDDIR="$DIR/_lembuild"
RED='\033[0;31m'
GREEN='\033[0;32m'
YELLOW='\033[0;33m'
NC='\033[0m'
rm -f $DIR/tests.xml
pass=0
fail=0
XML=""
function green {
(( pass += 1 ))
printf "$1: ${GREEN}$2${NC}\n"
XML+=" <testcase name=\"$1\"/>\n"
}
function yellow {
(( fail += 1 ))
printf "$1: ${YELLOW}$2${NC}\n"
XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n"
}
function red {
(( fail += 1 ))
printf "$1: ${RED}$2${NC}\n"
XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n"
}
function finish_suite {
printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n"
printf "$XML" >> $DIR/tests.xml
XML=""
pass=0
fail=0
}
printf "<testsuites>\n" >> $DIR/tests.xml
shopt -s nullglob;
for file in $DIR/*.sail;
do
if $SAILDIR/sail -no_warn -c $file 1> ${file%.sail}.c 2> /dev/null;
then
green "compiling $(basename $file) (C)" "ok";
if gcc -I $SAILDIR/lib/ ${file%.sail}.c -lgmp;
then
green "compiling $(basename ${file%.sail}.c)" "ok";
if $DIR/a.out;
then
green "tested $(basename ${file%.sail}) (C)" "ok"
else
red "tested $(basename ${file%.sail}) (C)" "fail"
fi
else
red "compiling $file" "fail"
fi
else
red "compiling $file" "fail"
fi;
if $SAILDIR/sail -no_warn -o out -ocaml $file 1> /dev/null 2> /dev/null;
then
green "compiling $(basename $file) (OCaml)" "ok"
if $DIR/out;
then
green "tested $(basename ${file%.sail}) (OCaml)" "ok"
else
red "tested $(basename ${file%.sail}) (OCaml)" "fail"
fi
else
red "compiling $(basename $file) (OCaml)" "fail"
fi;
mkdir -p "$LEMBUILDDIR"
if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null;
then
mv out.lem out_types.lem "$LEMBUILDDIR"
if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
-outdir "$LEMBUILDDIR" \
"$SAILDIR/src/gen_lib/sail_values.lem" \
"$SAILDIR/src/gen_lib/sail_operators.lem" \
"$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
"$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
"$SAILDIR/src/gen_lib/prompt.lem" \
"$SAILDIR/src/gen_lib/state_monad.lem" \
"$SAILDIR/src/gen_lib/state.lem" \
"$SAILDIR/src/gen_lib/prompt_monad.lem" \
"test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null;
then
cd "$LEMBUILDDIR"
if ocamlfind ocamlc -linkpkg -package zarith -package lem \
sail_values.ml sail_operators.ml \
sail_instr_kinds.ml prompt_monad.ml prompt.ml \
sail_operators_mwords.ml state_monad.ml state.ml \
test_extras.ml out_types.ml out.ml ../test.ml \
-o test 1> /dev/null 2> /dev/null
then
green "compiling $(basename $file) (Lem)" "ok"
if ./test 1> /dev/null 2> /dev/null
then
green "tested $(basename ${file%.sail}) (Lem)" "ok"
else
red "tested $(basename ${file%.sail}) (Lem)" "fail"
fi
else
red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail"
fi
cd "$DIR"
else
red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail"
fi
else
red "compiling $(basename $file) (Sail->Lem)" "fail"
fi;
rm -rf $DIR/_sbuild/;
rm -rf "$LEMBUILDDIR";
rm -f Out_lemmas.thy;
rm -f out_types.lem;
rm -f out.lem;
rm -f ${file%.sail}.c;
rm -f a.out;
rm -f out
done
finish_suite "builtin testing"
printf "</testsuites>\n" >> $DIR/tests.xml
|
