Merge branch 'sail2' into rmem_interpreter

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)