summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/mono/.gitignore2
-rw-r--r--test/mono/pass/assert1
-rw-r--r--test/mono/pass/assert21
-rw-r--r--test/mono/pass/atomsplit1
-rw-r--r--test/mono/pass/castreq1
-rw-r--r--test/mono/pass/control_deps1
-rw-r--r--test/mono/pass/exint1
-rw-r--r--test/mono/pass/feature1
-rw-r--r--test/mono/pass/feature_no_effects1
-rw-r--r--test/mono/pass/fnreduce1
-rw-r--r--test/mono/pass/fnreduce_manual1
-rw-r--r--test/mono/pass/set1
-rw-r--r--test/mono/pass/time8_continue1
-rw-r--r--test/mono/pass/times81
-rw-r--r--test/mono/pass/times8div81
-rw-r--r--test/mono/pass/union-exist1
-rw-r--r--test/mono/pass/union-exist_manual1
-rw-r--r--test/mono/pass/varmatch1
-rw-r--r--test/mono/pass/varmatch_manual1
-rw-r--r--test/mono/pass/vector1
-rw-r--r--test/mono/pass/vector_manual1
-rwxr-xr-xtest/mono/run_tests.sh103
-rw-r--r--test/mono/test.ml6
-rwxr-xr-xtest/mono/test.sh37
24 files changed, 127 insertions, 41 deletions
diff --git a/test/mono/.gitignore b/test/mono/.gitignore
index 2dd3daa3..bb7f92e1 100644
--- a/test/mono/.gitignore
+++ b/test/mono/.gitignore
@@ -1 +1 @@
-test-out \ No newline at end of file
+test-output \ No newline at end of file
diff --git a/test/mono/pass/assert b/test/mono/pass/assert
new file mode 100644
index 00000000..f24b885a
--- /dev/null
+++ b/test/mono/pass/assert
@@ -0,0 +1 @@
+assert.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/assert2 b/test/mono/pass/assert2
new file mode 100644
index 00000000..491a98b6
--- /dev/null
+++ b/test/mono/pass/assert2
@@ -0,0 +1 @@
+assert2.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/atomsplit b/test/mono/pass/atomsplit
new file mode 100644
index 00000000..d224fcfd
--- /dev/null
+++ b/test/mono/pass/atomsplit
@@ -0,0 +1 @@
+atomsplit.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/castreq b/test/mono/pass/castreq
new file mode 100644
index 00000000..e2fc1d55
--- /dev/null
+++ b/test/mono/pass/castreq
@@ -0,0 +1 @@
+castreq.sail -auto_mono -undefined_gen \ No newline at end of file
diff --git a/test/mono/pass/control_deps b/test/mono/pass/control_deps
new file mode 100644
index 00000000..e173c42f
--- /dev/null
+++ b/test/mono/pass/control_deps
@@ -0,0 +1 @@
+control_deps.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/exint b/test/mono/pass/exint
new file mode 100644
index 00000000..8de7c0bf
--- /dev/null
+++ b/test/mono/pass/exint
@@ -0,0 +1 @@
+exint.sail -auto_mono -undefined_gen \ No newline at end of file
diff --git a/test/mono/pass/feature b/test/mono/pass/feature
new file mode 100644
index 00000000..9363dd68
--- /dev/null
+++ b/test/mono/pass/feature
@@ -0,0 +1 @@
+feature -auto_mono -undefined_gen \ No newline at end of file
diff --git a/test/mono/pass/feature_no_effects b/test/mono/pass/feature_no_effects
new file mode 100644
index 00000000..098d7f94
--- /dev/null
+++ b/test/mono/pass/feature_no_effects
@@ -0,0 +1 @@
+feature.sail -auto_mono -undefined_gen -no_effects
diff --git a/test/mono/pass/fnreduce b/test/mono/pass/fnreduce
new file mode 100644
index 00000000..4237c34a
--- /dev/null
+++ b/test/mono/pass/fnreduce
@@ -0,0 +1 @@
+fnreduce.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/fnreduce_manual b/test/mono/pass/fnreduce_manual
new file mode 100644
index 00000000..25d8256c
--- /dev/null
+++ b/test/mono/pass/fnreduce_manual
@@ -0,0 +1 @@
+fnreduce.sail -mono_split fnreduce.sail:43:x \ No newline at end of file
diff --git a/test/mono/pass/set b/test/mono/pass/set
new file mode 100644
index 00000000..700d1752
--- /dev/null
+++ b/test/mono/pass/set
@@ -0,0 +1 @@
+set.sail -auto_mono
diff --git a/test/mono/pass/time8_continue b/test/mono/pass/time8_continue
new file mode 100644
index 00000000..eb8d043b
--- /dev/null
+++ b/test/mono/pass/time8_continue
@@ -0,0 +1 @@
+times8.sail -auto_mono -dmono_continue -dall_split_errors \ No newline at end of file
diff --git a/test/mono/pass/times8 b/test/mono/pass/times8
new file mode 100644
index 00000000..1315855d
--- /dev/null
+++ b/test/mono/pass/times8
@@ -0,0 +1 @@
+times8.sail -auto_mono \ No newline at end of file
diff --git a/test/mono/pass/times8div8 b/test/mono/pass/times8div8
new file mode 100644
index 00000000..5f3a973f
--- /dev/null
+++ b/test/mono/pass/times8div8
@@ -0,0 +1 @@
+times8div8.sail -auto_mono -undefined_gen
diff --git a/test/mono/pass/union-exist b/test/mono/pass/union-exist
new file mode 100644
index 00000000..ebb89267
--- /dev/null
+++ b/test/mono/pass/union-exist
@@ -0,0 +1 @@
+union-exist.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
new file mode 100644
index 00000000..d35c3d48
--- /dev/null
+++ b/test/mono/pass/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:9:v \ No newline at end of file
diff --git a/test/mono/pass/varmatch b/test/mono/pass/varmatch
new file mode 100644
index 00000000..e1402863
--- /dev/null
+++ b/test/mono/pass/varmatch
@@ -0,0 +1 @@
+varmatch.sail -auto_mono
diff --git a/test/mono/pass/varmatch_manual b/test/mono/pass/varmatch_manual
new file mode 100644
index 00000000..f2870060
--- /dev/null
+++ b/test/mono/pass/varmatch_manual
@@ -0,0 +1 @@
+varmatch.sail -mono_split varmatch.sail:7:x \ No newline at end of file
diff --git a/test/mono/pass/vector b/test/mono/pass/vector
new file mode 100644
index 00000000..82435ef5
--- /dev/null
+++ b/test/mono/pass/vector
@@ -0,0 +1 @@
+vector.sail -auto_mono
diff --git a/test/mono/pass/vector_manual b/test/mono/pass/vector_manual
new file mode 100644
index 00000000..d0712dbc
--- /dev/null
+++ b/test/mono/pass/vector_manual
@@ -0,0 +1 @@
+vector.sail -mono_split vector.sail:7:sel \ No newline at end of file
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
new file mode 100755
index 00000000..4be1f434
--- /dev/null
+++ b/test/mono/run_tests.sh
@@ -0,0 +1,103 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+TESTSDIR="$DIR"
+OUTPUTDIR="$DIR/test-output"
+
+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"
+
+cd "$DIR"
+mkdir -p "$OUTPUTDIR"
+
+echo > log
+
+for i in `ls $TESTSDIR/pass`;
+do
+ echo "Running test $i" >> log
+ cd "$DIR"
+ if "$SAILDIR/sail" -lem -lem_mwords -lem_lib Test_extra -o out $(< "$TESTSDIR/pass/$i") &>>log;
+ then
+ mv out.lem out_types.lem "$OUTPUTDIR"
+ if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
+ -outdir "$OUTPUTDIR" \
+ "$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" \
+ "$DIR/test_extra.lem" \
+ "$OUTPUTDIR/out_types.lem" "$OUTPUTDIR/out.lem" &>>log;
+ then
+ cd "$OUTPUTDIR"
+ if ocamlfind ocamlc -linkpkg -package zarith -package lem \
+ sail_values.ml sail_operators.ml \
+ sail_operators_mwords.ml sail_instr_kinds.ml \
+ prompt_monad.ml prompt.ml state_monad.ml state.ml \
+ test_extra.ml out_types.ml out.ml ../test.ml \
+ -o test &>>log
+ then
+ if ./test &>>log
+ then
+ green "tested $i expecting pass" "pass"
+ else
+ red "tested $i expecting pass" "running generated test failed"
+ fi
+ else
+ red "tested $i expecting pass" "compiling generated OCaml failed"
+ fi
+ else
+ red "tested $i expecting pass" "failed to generate OCaml from Lem"
+ fi
+ else
+ red "tested $i expecting pass" "failed to generate Lem"
+ fi
+ echo >> log
+done
+
+finish_suite "monomorphisation tests"
+
+printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/mono/test.ml b/test/mono/test.ml
index dc194792..32d3b2ed 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1,3 +1,3 @@
-match Testout.run() with
-| Done _ -> print_endline "OK"
-| _ -> print_endline "Failed";;
+match Out.run() with
+| Done _ -> exit 0
+| _ -> exit 1
diff --git a/test/mono/test.sh b/test/mono/test.sh
deleted file mode 100755
index 5bf72828..00000000
--- a/test/mono/test.sh
+++ /dev/null
@@ -1,37 +0,0 @@
-#!/bin/bash
-
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-SAILDIR="$DIR/../.."
-LEMDIR="$DIR/../../../lem"
-OUTDIR="$DIR/test-out"
-ZARITH="$LEMDIR/ocaml-lib/dependencies/zarith"
-
-if [ ! -d "$OUTDIR" ]; then
- mkdir -- "$OUTDIR"
-fi
-cd "$OUTDIR"
-
-TESTONLY="$1"
-if [ -n "$TESTONLY" ]; then shift; fi
-
-LOG="$DIR/log"
-date > "$LOG"
-
-exec 3< "$DIR/tests"
-set +e
-
-while read -u 3 TEST ARGS; do
- if [ -z "$TESTONLY" -o "$TEST" = "$TESTONLY" ]; then
-
- echo "$TEST lem - ocaml" | tee -a -- "$LOG"
- rm -f -- "$OUTDIR"/*
- "$SAILDIR/sail" -lem -lem_mwords -lem_lib Test_extra "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
- "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$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" "$DIR/test_extra.lem" testout_types.lem testout.lem -outdir "$OUTDIR" &>> "$LOG" && \
- cp -- "$DIR"/test.ml "$OUTDIR" && \
- ocamlfind ocamlc -linkpkg -package zarith -package lem sail_values.ml sail_operators.ml sail_operators_mwords.ml sail_instr_kinds.ml prompt_monad.ml prompt.ml state_monad.ml state.ml test_extra.ml testout_types.ml testout.ml test.ml -o test &>> "$LOG" && \
- ./test |& tee -a -- "$LOG" || \
- (echo "Failed:"; echo; tail -- "$LOG"; echo; echo)
- fi
-done
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 09:31:37 +0000