diff options
Diffstat (limited to 'test')
| -rwxr-xr-x | test/aarch64_small/run_tests.sh | 57 | ||||
| -rw-r--r-- | test/c/extend_simple.expect | 2 | ||||
| -rw-r--r-- | test/c/extend_simple.sail | 10 | ||||
| -rw-r--r-- | test/c/fast_signed.expect | 12 | ||||
| -rw-r--r-- | test/c/fast_signed.sail | 30 | ||||
| -rw-r--r-- | test/c/int_struct.expect | 1 | ||||
| -rw-r--r-- | test/c/int_struct.sail | 24 | ||||
| -rw-r--r-- | test/c/int_struct_constrained.expect | 1 | ||||
| -rw-r--r-- | test/c/int_struct_constrained.sail | 24 | ||||
| -rw-r--r-- | test/c/issue37.expect | 1 | ||||
| -rw-r--r-- | test/c/issue37.sail | 9 | ||||
| -rwxr-xr-x | test/c/run_tests.py | 3 | ||||
| -rwxr-xr-x | test/run_tests.sh | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/execute_decode_hard.sail | 26 | ||||
| -rw-r--r-- | test/typecheck/pass/fpthreesimp.sail (renamed from test/typecheck/fpthreesimp.sail) | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/plus_one_unify.sail | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/recursion.sail | 15 |
17 files changed, 229 insertions, 4 deletions
diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh new file mode 100755 index 00000000..cc6f223e --- /dev/null +++ b/test/aarch64_small/run_tests.sh @@ -0,0 +1,57 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR +SAILDIR="$DIR/../.." + +RED='\033[0;91m' +GREEN='\033[0;92m' +YELLOW='\033[0;93m' +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 + +if make -B -C ../../aarch64_small SAIL="$SAILDIR/sail" +then + green "built aarch64_small to lem" "ok" +else + red "failed to build lem" "fail" +fi + +finish_suite "aarch64_small tests" + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/c/extend_simple.expect b/test/c/extend_simple.expect new file mode 100644 index 00000000..3a652eaf --- /dev/null +++ b/test/c/extend_simple.expect @@ -0,0 +1,2 @@ +x = 0xFFFFFFFF +y = 0x00000000FFFFFFFF diff --git a/test/c/extend_simple.sail b/test/c/extend_simple.sail new file mode 100644 index 00000000..23f14235 --- /dev/null +++ b/test/c/extend_simple.sail @@ -0,0 +1,10 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x = sail_sign_extend(0xFF, 32); + let y = sail_zero_extend(x, 64); + print_bits("x = ", x); + print_bits("y = ", y) +}
\ No newline at end of file diff --git a/test/c/fast_signed.expect b/test/c/fast_signed.expect new file mode 100644 index 00000000..9fcfea23 --- /dev/null +++ b/test/c/fast_signed.expect @@ -0,0 +1,12 @@ +x = -1 +y = -1 +z = -1 +w = -1 +x = -128 +y = -32768 +z = -9223372036854775808 +w = -170141183460469231731687303715884105728 +x = 127 +y = 32767 +z = 9223372036854775807 +w = 170141183460469231731687303715884105727 diff --git a/test/c/fast_signed.sail b/test/c/fast_signed.sail new file mode 100644 index 00000000..b0f16f89 --- /dev/null +++ b/test/c/fast_signed.sail @@ -0,0 +1,30 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x = signed(0xFF); + let y = signed(0xFFFF); + let z = signed(0xFFFFFFFF_FFFFFFFF); + let w = signed(0xFFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF); + print_int("x = ", x); + print_int("y = ", y); + print_int("z = ", z); + print_int("w = ", w); + let x = signed(0x80); + let y = signed(0x8000); + let z = signed(0x80000000_00000000); + let w = signed(0x80000000_00000000_00000000_00000000); + print_int("x = ", x); + print_int("y = ", y); + print_int("z = ", z); + print_int("w = ", w); + let x = signed(0x7F); + let y = signed(0x7FFF); + let z = signed(0x7FFFFFFF_FFFFFFFF); + let w = signed(0x7FFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF); + print_int("x = ", x); + print_int("y = ", y); + print_int("z = ", z); + print_int("w = ", w); +}
\ No newline at end of file diff --git a/test/c/int_struct.expect b/test/c/int_struct.expect new file mode 100644 index 00000000..f70f10e4 --- /dev/null +++ b/test/c/int_struct.expect @@ -0,0 +1 @@ +A diff --git a/test/c/int_struct.sail b/test/c/int_struct.sail new file mode 100644 index 00000000..42554593 --- /dev/null +++ b/test/c/int_struct.sail @@ -0,0 +1,24 @@ +default Order dec + +$include <prelude.sail> + +val print = "print_endline" : string -> unit + +struct Foo('n: Int) = { + field: bits('n) +} + +type Foo32 = Foo(32) + +function bar(foo: Foo32) -> unit = { + if foo.field == 0xFFFF_FFFF then { + print("A") + } else { + print("B") + } +} + +function main((): unit) -> unit = { + let x: Foo32 = struct { field = 0xFFFF_FFFF }; + bar(x) +}
\ No newline at end of file diff --git a/test/c/int_struct_constrained.expect b/test/c/int_struct_constrained.expect new file mode 100644 index 00000000..f70f10e4 --- /dev/null +++ b/test/c/int_struct_constrained.expect @@ -0,0 +1 @@ +A diff --git a/test/c/int_struct_constrained.sail b/test/c/int_struct_constrained.sail new file mode 100644 index 00000000..95cb6e9b --- /dev/null +++ b/test/c/int_struct_constrained.sail @@ -0,0 +1,24 @@ +default Order dec + +$include <prelude.sail> + +val print = "print_endline" : string -> unit + +struct Foo('n: Int), 'n <= 64 = { + field: bits('n) +} + +type Foo32 = Foo(32) + +function bar(foo: Foo32) -> unit = { + if foo.field == 0xFFFF_FFFF then { + print("A") + } else { + print("B") + } +} + +function main((): unit) -> unit = { + let x: Foo32 = struct { field = 0xFFFF_FFFF }; + bar(x) +}
\ No newline at end of file diff --git a/test/c/issue37.expect b/test/c/issue37.expect new file mode 100644 index 00000000..6e77c916 --- /dev/null +++ b/test/c/issue37.expect @@ -0,0 +1 @@ +foo = 0xE diff --git a/test/c/issue37.sail b/test/c/issue37.sail new file mode 100644 index 00000000..404c4ef4 --- /dev/null +++ b/test/c/issue37.sail @@ -0,0 +1,9 @@ +default Order dec + +$include <vector_dec.sail> + +function main () : unit->unit = { + foo = 0xf; + foo[0] = bitzero; + print_bits("foo = ", foo) +}
\ No newline at end of file diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 4a02dd78..2ee44fca 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -95,7 +95,8 @@ xml += test_c('optimized C', '-O2', '-O', True) xml += test_c('constant folding', '', '-Oconstant_fold', True) xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True) xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True) -xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False) +xml += test_c('specialization', '-O1', '-O -c_specialize', True) +xml += test_c('undefined behavior sanitised', '-O2 -fsanitize=undefined', '-O', False) xml += test_interpreter('interpreter') diff --git a/test/run_tests.sh b/test/run_tests.sh index 09e99ff2..a228e270 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -47,3 +47,9 @@ printf "==========================================\n" ./arm/run_tests.sh +printf "\n==========================================\n" +printf "aarch64_small spec tests\n" +printf "==========================================\n" + +./aarch64_small/run_tests.sh + diff --git a/test/typecheck/pass/execute_decode_hard.sail b/test/typecheck/pass/execute_decode_hard.sail new file mode 100644 index 00000000..d5e91b79 --- /dev/null +++ b/test/typecheck/pass/execute_decode_hard.sail @@ -0,0 +1,26 @@ +default Order dec + +$include <prelude.sail> + +union ast('D: Int), 'D in {32, 64, 128} = { + Instr1 : {'R, 'R in {32, 64}. (int('R), bits('D))} +} + +val execute : forall 'd, 'd in {32, 64, 128}. ast('d) -> unit + +function clause execute(Instr1(r as int('R), d)) = { + _prove(constraint('R in {32, 64})); + if length(d) == 64 then { + let _ = d[r - 1 .. 0]; + () + } +} + +function clause execute(Instr1((r as int('R), d))) = { + _prove(constraint('R in {32, 64})); + if length(d) == 64 then { + let _ = d[r - 1 .. 0]; + () + } +} + diff --git a/test/typecheck/fpthreesimp.sail b/test/typecheck/pass/fpthreesimp.sail index 3f759ba4..d0f44119 100644 --- a/test/typecheck/fpthreesimp.sail +++ b/test/typecheck/pass/fpthreesimp.sail @@ -4,11 +4,11 @@ $include <prelude.sail> val Zeros : forall 'N, 'N >= 0. int('N) -> bits('N) -type FPExponent ('N : Int) = {'E, ('N = 16 & 'E = 5) | ('N = 32 & 'E = 8) | ('N = 64 & 'E = 11). int('E)} +type FPExponent ('N : Int) = {'E, ('N == 16 & 'E == 5) | ('N == 32 & 'E == 8) | ('N == 64 & 'E == 11). int('E)} -val FPThree : forall 'N, 'N in {16, 32, 64}. bits(1) -> bits('N) +val FPThree : forall 'N, 'N in {16, 32, 64}. (implicit('N), bits(1)) -> bits('N) -function FPThree(sign) = { +function FPThree(N, sign) = { let E : FPExponent('N) = if 'N == 16 then 5 else if 'N == 32 then 8 else 11; sign @ 0b1 @ Zeros(E - 1) @ 0b1 @ Zeros('N - E - 2) }
\ No newline at end of file diff --git a/test/typecheck/pass/plus_one_unify.sail b/test/typecheck/pass/plus_one_unify.sail new file mode 100644 index 00000000..0dceaa4c --- /dev/null +++ b/test/typecheck/pass/plus_one_unify.sail @@ -0,0 +1,6 @@ + +val f2 : forall 'm, 'm in {0,1}. (int('m+1)) -> int + +function f2(_) = 3 + +let x = f2(1)
\ No newline at end of file diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail new file mode 100644 index 00000000..5ca85f53 --- /dev/null +++ b/test/typecheck/pass/recursion.sail @@ -0,0 +1,15 @@ +default Order dec + +$include <prelude.sail> + +val log2 : int -> int + +function log2(n) = + if n <= 1 then 0 else 1 + log2(n/2) + +termination_measure log2(n) = n + +val testlog2 : unit -> unit effect {escape} + +function testlog2() = + assert(log2(64) == 6) |