diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/ocaml/lsl/expect | 4 | ||||
| -rw-r--r-- | test/ocaml/lsl/lsl.sail | 31 | ||||
| -rw-r--r-- | test/ocaml/pattern1/expect | 1 | ||||
| -rw-r--r-- | test/ocaml/pattern1/pattern.sail | 11 | ||||
| -rw-r--r-- | test/ocaml/prelude.sail | 4 | ||||
| -rwxr-xr-x | test/ocaml/run_tests.sh | 5 | ||||
| -rwxr-xr-x | test/run_tests.sh | 7 | ||||
| -rwxr-xr-x | test/typecheck/run_tests.sh | 66 |
8 files changed, 95 insertions, 34 deletions
diff --git a/test/ocaml/lsl/expect b/test/ocaml/lsl/expect new file mode 100644 index 00000000..c72d1eb8 --- /dev/null +++ b/test/ocaml/lsl/expect @@ -0,0 +1,4 @@ +pass +pass +pass +pass diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail new file mode 100644 index 00000000..fdb9dc43 --- /dev/null +++ b/test/ocaml/lsl/lsl.sail @@ -0,0 +1,31 @@ + +val forall Num 'n, 'n >= 0. [:'n:] -> bit['n] effect pure zeros + +function zeros n = replicate_bits(0b0, sizeof 'n) + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> (bit['n], bit) effect pure lslc + +function lslc (vec, shift) = { + assert(constraint('shift >= 1), "shift must be positive"); + (bit['shift + 'n]) extended := vec : zeros(shift); + (bit['n]) result := extended[sizeof 'n - 1 .. 0]; + (bit) c := extended[sizeof 'n]; + return (result, c) +} + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> bit['n] effect pure lsl + +function lsl (vec, shift) = + if shift == 0 + then vec + else let (result, _) = lslc(vec, shift) in result + +val unit -> unit effect pure main + +function main () = { + print(if lsl(0b0110,1) == 0b1100 then "pass" else "fail"); + print(if lsl(0b1111,2) == 0b1100 then "pass" else "fail"); + print(if lsl(0x0F,4) == 0xF0 then "pass" else "fail"); + let (result, c) = lslc(0xF000,2) in + print(if result == 0xC000 & c == bitone then "pass" else "fail") +} diff --git a/test/ocaml/pattern1/expect b/test/ocaml/pattern1/expect new file mode 100644 index 00000000..2ae28399 --- /dev/null +++ b/test/ocaml/pattern1/expect @@ -0,0 +1 @@ +pass diff --git a/test/ocaml/pattern1/pattern.sail b/test/ocaml/pattern1/pattern.sail new file mode 100644 index 00000000..a2314adc --- /dev/null +++ b/test/ocaml/pattern1/pattern.sail @@ -0,0 +1,11 @@ + +val unit -> unit effect pure main + +function main () = { + vec := 0x4F; + switch vec { + case (0b01 : (bit[2]) x : 0xF) -> + if (x == 0b00) then print("pass") else print("x is incorrect") + case _ -> print("pattern fail") + } +} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 2526d109..cbe1927d 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -15,6 +15,10 @@ val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange" +(* FIXME: rewriter shouldn't assume this exists *) +val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure bitvector_subrange_dec = "subrange" + val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access" val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update" diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index d01535b6..4454aa48 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -2,6 +2,7 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR SAILDIR="$DIR/../.." RED='\033[0;31m' @@ -49,7 +50,7 @@ printf "<testsuites>\n" >> $DIR/tests.xml for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail`; + if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null; then ./out > result; if diff expect result; @@ -66,4 +67,6 @@ do fi done +finish_suite "Ocaml testing" + printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/run_tests.sh b/test/run_tests.sh new file mode 100755 index 00000000..380ebb18 --- /dev/null +++ b/test/run_tests.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +$DIR/typecheck/run_tests.sh +$DIR/ocaml/run_tests.sh diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index e83cc20b..41a19cb4 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -97,43 +97,43 @@ done finish_suite "Expecting fail" -function test_lem { - for i in `ls $DIR/pass/`; - do - # MIPS requires an additional library, Mips_extras_embed. - # It might be useful to allow adding options for specific test cases. - # For now, include the library for all test cases, which doesn't seem to hurt. - if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null - then - green "generated lem for $1/$i" "pass" - - cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ - # Test sequential embedding for now - # TODO: Add tests for the free monad - if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null - then - green "typechecking lem for $1/$i" "pass" - else - red "typechecking lem for $1/$i" "fail" - fi - else - red "generated lem for $1/$i" "fail" - red "typechecking lem for $1/$i" "fail" - fi - done -} +# function test_lem { +# for i in `ls $DIR/pass/`; +# do +# # MIPS requires an additional library, Mips_extras_embed. +# # It might be useful to allow adding options for specific test cases. +# # For now, include the library for all test cases, which doesn't seem to hurt. +# if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null +# then +# green "generated lem for $1/$i" "pass" + +# cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ +# mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ +# # Test sequential embedding for now +# # TODO: Add tests for the free monad +# if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null +# then +# green "typechecking lem for $1/$i" "pass" +# else +# red "typechecking lem for $1/$i" "fail" +# fi +# else +# red "generated lem for $1/$i" "fail" +# red "typechecking lem for $1/$i" "fail" +# fi +# done +# } -test_lem pass +# test_lem pass -finish_suite "Lem generation 1" +# finish_suite "Lem generation 1" -test_lem rtpass +# test_lem rtpass -finish_suite "Lem generation 2" +# finish_suite "Lem generation 2" # function test_ocaml { # for i in `ls $DIR/pass/`; |