22 files changed, 249 insertions, 18 deletions

diff --git a/test/aarch64_small/run_tests.sh b/test/aarch64_small/run_tests.sh
index cc6f223e..dc2bdde4 100755
--- a/test/aarch64_small/run_tests.sh
+++ b/test/aarch64_small/run_tests.sh
@@ -45,7 +45,7 @@ function finish_suite {
 
 printf "<testsuites>\n" >> $DIR/tests.xml
 
-if make -B -C ../../aarch64_small SAIL="$SAILDIR/sail"
+if make -B -C ../../aarch64_small armV8.lem SAIL="$SAILDIR/sail"
 then
     green "built aarch64_small to lem" "ok"
 else
diff --git a/test/builtins/slice_mask.sail b/test/builtins/slice_mask.sail
new file mode 100644
index 00000000..e694f029
--- /dev/null
+++ b/test/builtins/slice_mask.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <exception_basic.sail>
+$include <flow.sail>
+$include <vector_dec.sail>
+
+function main (() : unit) -> unit = {
+  assert(slice_mask(32, 8, 4)   == 0x00000F00);
+  assert(slice_mask(32, 16, 8)  == 0x00FF0000);
+  assert(slice_mask(32, 15, 3)  == 0x00038000);
+  assert(slice_mask(32, 16, 32) == 0xFFFF0000);
+}
diff --git a/test/c/single_guard.expect b/test/c/single_guard.expect
new file mode 100644
index 00000000..070cdc2c
--- /dev/null
+++ b/test/c/single_guard.expect
@@ -0,0 +1,2 @@
+In main
+In test
diff --git a/test/c/single_guard.sail b/test/c/single_guard.sail
new file mode 100644
index 00000000..017ed8a5
--- /dev/null
+++ b/test/c/single_guard.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+val test : unit -> unit
+
+function test(_ if true) = {
+  print_endline("In test")
+}
+
+function main() -> unit = {
+  print_endline("In main");
+  test()
+}
\ No newline at end of file
diff --git a/test/coq/pass/non_exh_exc.sail b/test/coq/pass/non_exh_exc.sail
new file mode 100644
index 00000000..8ce99163
--- /dev/null
+++ b/test/coq/pass/non_exh_exc.sail
@@ -0,0 +1,18 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  Error_foo : unit,
+  Error_bar : int
+}
+
+val f : int -> int effect {escape}
+
+function f(n) = {
+  try {
+    let m : int = if n > 5 then n - 3 else throw(Error_bar(n)) in
+    m + 1
+  } catch {
+    Error_bar(n) => n
+  }
+}
diff --git a/test/coq/pass/throw_fact.sail b/test/coq/pass/throw_fact.sail
new file mode 100644
index 00000000..e40267b1
--- /dev/null
+++ b/test/coq/pass/throw_fact.sail
@@ -0,0 +1,25 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+  BadInput : int
+}
+
+val test1 : int -> nat effect {escape}
+
+function test1(n) = {
+  if (n < 0) then {
+    throw (BadInput(n))
+  };
+  n
+}
+
+val test2 : int -> nat effect {escape}
+
+function test2(n) = {
+  m : nat = 0;
+  if (n < 0) then {
+    throw (BadInput(n))
+  } else { m = 1 };
+  n+m
+}
diff --git a/test/coq/pass/var_type_autocast.sail b/test/coq/pass/var_type_autocast.sail
new file mode 100644
index 00000000..6c65b978
--- /dev/null
+++ b/test/coq/pass/var_type_autocast.sail
@@ -0,0 +1,13 @@
+default Order dec
+$include <prelude.sail>
+$include <smt.sail>
+
+val load_bytes : forall 'n, 'n >= 0. int('n) -> bits(8 * 'n)
+
+val foo : forall 'n, 'n in {8,16}. (int('n),bool) -> bits('n)
+
+function foo(n,b) = {
+  let 'bytes = ediv_int(n,8);
+  let data = load_bytes(bytes);
+  if b then data else sail_zeros(n)
+}
diff --git a/test/smt/arith_LC32L.unsat.sail b/test/smt/arith_LC32L.unsat.sail
index 547a5cb1..82184bf8 100644
--- a/test/smt/arith_LC32L.unsat.sail
+++ b/test/smt/arith_LC32L.unsat.sail
@@ -2,26 +2,11 @@ default Order dec
 
 $include <prelude.sail>
 
-$option -smt_ignore_overflow
-
 $property
 function prop(x: int, y: int(32), z: int) -> bool = {
   let add_comm  = x + y == y + x;
   let add_assoc = (x + y) + z == x + (y + z);
   let add_id  = x + 0 == x;
 
-  let mul_comm = x * y == y * x;
-  let mul_assoc = (x * y) * z == x * (y * z);
-  let mul_zero = x * 0 == 0;
-
-  let add_mul_distrib = x * (y + z) == (x * y) + (x * z);
-
-  let add_neg_zero = x + negate(x) == 0;
-  let add_neg_sub  = x + negate(y) == x - y;
-  let neg_neg = negate(negate(x)) == x;
-
   add_comm & add_assoc & add_id
-  & mul_comm & mul_assoc & mul_zero
-  & add_mul_distrib
-  & add_neg_zero & add_neg_sub & neg_neg
-}
\ No newline at end of file
+}
diff --git a/test/smt/arith_LC32L_1.unsat.sail b/test/smt/arith_LC32L_1.unsat.sail
new file mode 100644
index 00000000..82184bf8
--- /dev/null
+++ b/test/smt/arith_LC32L_1.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let add_comm  = x + y == y + x;
+  let add_assoc = (x + y) + z == x + (y + z);
+  let add_id  = x + 0 == x;
+
+  add_comm & add_assoc & add_id
+}
diff --git a/test/smt/arith_LC32L_2.unsat.sail b/test/smt/arith_LC32L_2.unsat.sail
new file mode 100644
index 00000000..9a29fe13
--- /dev/null
+++ b/test/smt/arith_LC32L_2.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  let mul_comm = x * y == y * x;
+  let mul_zero1 = x * 0 == 0;
+  let mul_zero2 = y * 0 == 0;
+
+  mul_comm & mul_zero1 & mul_zero2
+}
\ No newline at end of file
diff --git a/test/smt/arith_LC32L_3.unsat.sail b/test/smt/arith_LC32L_3.unsat.sail
new file mode 100644
index 00000000..7d97a76b
--- /dev/null
+++ b/test/smt/arith_LC32L_3.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -smt_ignore_overflow
+
+$property
+function prop(x: int, y: int(32), z: int) -> bool = {
+  if  -10000 <= x & x <= 10000 & -10000 <= z & z <= 10000 then
+    (x * y) * z == x * (y * z)
+  else true
+}
diff --git a/test/smt/arith_LC32L_4.unsat.sail b/test/smt/arith_LC32L_4.unsat.sail
new file mode 100644
index 00000000..e94ab2c3
--- /dev/null
+++ b/test/smt/arith_LC32L_4.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop(x: int, y: int(32)) -> bool = {
+  let add_neg_zero = x + negate(x) == 0;
+  let add_neg_sub  = x + negate(y) == x - y;
+  let neg_neg = negate(negate(x)) == x;
+
+  add_neg_zero & add_neg_sub & neg_neg
+}
diff --git a/test/smt/load_store_dep.sat.sail b/test/smt/load_store_dep.sat.sail
new file mode 100644
index 00000000..bb35c6f7
--- /dev/null
+++ b/test/smt/load_store_dep.sat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+$include "test/arch.sail"
+
+/* Default memory model is as weak as possible, so this is not true */
+$counterexample
+function prop() -> bool = {
+  let _ = arch_load(0b00, 0b01);
+  let _ = arch_store(0b10, 0b00);
+  X(0b01) == X(0b10)
+}
diff --git a/test/smt/minmax.unsat.sail b/test/smt/minmax.unsat.sail
new file mode 100644
index 00000000..f1bdf55a
--- /dev/null
+++ b/test/smt/minmax.unsat.sail
@@ -0,0 +1,20 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$property
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(3, 2) == 3);
+  assert(min_int(3, 2) == 2);
+  assert(max_int(-132542345, 3) == 3);
+
+  assert(max_int(a, b) == max_int(b, a));
+  assert(min_int(a, b) == min_int(b, a));
+
+  assert(max_int(0, 0) == 0);
+
+  true
+}
diff --git a/test/smt/minmax_1.sat.sail b/test/smt/minmax_1.sat.sail
new file mode 100644
index 00000000..09119db0
--- /dev/null
+++ b/test/smt/minmax_1.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, a) == max_int(b, a));
+  true
+}
diff --git a/test/smt/minmax_2.sat.sail b/test/smt/minmax_2.sat.sail
new file mode 100644
index 00000000..dd773058
--- /dev/null
+++ b/test/smt/minmax_2.sat.sail
@@ -0,0 +1,12 @@
+
+val operator == = "eq_int" : (int, int) -> bool
+
+val "max_int" : (int, int) -> int
+
+val "min_int" : (int, int) -> int
+
+$counterexample
+function prop(a: int, b: int) -> bool = {
+  assert(max_int(a, b) == min_int(a, b));
+  true
+}
diff --git a/test/smt/sail_mask.unsat.sail b/test/smt/sail_mask.unsat.sail
new file mode 100644
index 00000000..4afbab90
--- /dev/null
+++ b/test/smt/sail_mask.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 0 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b0);
+  assert(x == sail_zeros(n));
+  true
+}
diff --git a/test/smt/sail_mask_2.unsat.sail b/test/smt/sail_mask_2.unsat.sail
new file mode 100644
index 00000000..8904bbe9
--- /dev/null
+++ b/test/smt/sail_mask_2.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 1 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0b1);
+  assert(x == sail_zero_extend(0b1, n));
+  true
+}
diff --git a/test/smt/sail_mask_3.unsat.sail b/test/smt/sail_mask_3.unsat.sail
new file mode 100644
index 00000000..5f4b5fe4
--- /dev/null
+++ b/test/smt/sail_mask_3.unsat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 32 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  assert(x == sail_zero_extend(0xdeadbeef, n));
+  true
+}
diff --git a/test/smt/sail_mask_4.unsat.sail b/test/smt/sail_mask_4.unsat.sail
new file mode 100644
index 00000000..368a3f2d
--- /dev/null
+++ b/test/smt/sail_mask_4.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(x == 0b1011110101011011011111011101111);
+  true
+}
diff --git a/test/smt/sail_mask_5.unsat.sail b/test/smt/sail_mask_5.unsat.sail
new file mode 100644
index 00000000..452c7f6c
--- /dev/null
+++ b/test/smt/sail_mask_5.unsat.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+function prop forall 'n, 31 <= 'n <= 128. (n: int('n)) -> bool = {
+  let x = sail_mask(n, 0xdeadbeef);
+  if n >= 32 then
+     assert(x == sail_zero_extend(0xdeadbeef, n))
+  else
+     assert(0b1011110101011011011111011101111 == x);
+  true
+}
diff --git a/test/typecheck/pass/constant_nexp/v2.expect b/test/typecheck/pass/constant_nexp/v2.expect
index 3c4dcc16..7c0e8093 100644
--- a/test/typecheck/pass/constant_nexp/v2.expect
+++ b/test/typecheck/pass/constant_nexp/v2.expect
@@ -3,6 +3,6 @@ Type error:
 12 |  let _ = czeros(sizeof('n - 10) + 20);
    |          ^--------------------------^
    | Could not resolve quantifiers for czeros
-   | * is_constant(('fv47#n : Int))
+   | * is_constant(('fv50#n : Int))
    | * (('n - 10) + 20) >= 0
    |