Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

41 files changed, 387 insertions, 6 deletions

diff --git a/test/c/bitvector_update.expect b/test/c/bitvector_update.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/bitvector_update.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/bitvector_update.sail b/test/c/bitvector_update.sail
new file mode 100644
index 00000000..6f506e23
--- /dev/null
+++ b/test/c/bitvector_update.sail
@@ -0,0 +1,13 @@
+default Order dec
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main() -> unit = {
+  let x = bitzero;
+  let y = bitone;
+  let z = bitzero;
+  let bv = [x, y, z];
+  assert(bv == 0b010);
+  print_endline("ok")
+}
\ No newline at end of file
diff --git a/test/c/bitvector_update2.expect b/test/c/bitvector_update2.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/bitvector_update2.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/bitvector_update2.sail b/test/c/bitvector_update2.sail
new file mode 100644
index 00000000..8e5e9918
--- /dev/null
+++ b/test/c/bitvector_update2.sail
@@ -0,0 +1,14 @@
+default Order dec
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main() -> unit = {
+  var bv = 0b101;
+  let x = bitzero;
+  let y = bitone;
+  let z = bitzero;
+  bv = [x, y, z];
+  assert(bv == 0b010);
+  print_endline("ok")
+}
diff --git a/test/c/nested_fields.expect b/test/c/nested_fields.expect
new file mode 100644
index 00000000..0cfbf088
--- /dev/null
+++ b/test/c/nested_fields.expect
@@ -0,0 +1 @@
+2
diff --git a/test/c/nested_fields.sail b/test/c/nested_fields.sail
new file mode 100644
index 00000000..1e26dac9
--- /dev/null
+++ b/test/c/nested_fields.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct B = {
+  f3: int,
+  f4: int,
+}
+
+struct A = {
+  f1: B,
+  f2: int,
+}
+
+register R : A
+
+function main() -> unit = {
+  R.f1.f3 = 2;
+  print_int("", R.f1.f3)
+}
\ No newline at end of file
diff --git a/test/c/scattered_mapping.expect b/test/c/scattered_mapping.expect
new file mode 100644
index 00000000..6a452c18
--- /dev/null
+++ b/test/c/scattered_mapping.expect
@@ -0,0 +1 @@
+()
diff --git a/test/c/scattered_mapping.sail b/test/c/scattered_mapping.sail
new file mode 100644
index 00000000..4f523e45
--- /dev/null
+++ b/test/c/scattered_mapping.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+val "print_endline" : string -> unit
+
+val unit_str_map : unit <-> string
+scattered mapping unit_str_map
+val unit_str : unit -> string
+function unit_str () = unit_str_map_forwards(())
+mapping clause unit_str_map = () <-> "()"
+
+function main () : unit -> unit = {
+  print_endline(unit_str())
+}
diff --git a/test/c/undefined_union.expect b/test/c/undefined_union.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/undefined_union.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/undefined_union.sail b/test/c/undefined_union.sail
new file mode 100644
index 00000000..9b652b34
--- /dev/null
+++ b/test/c/undefined_union.sail
@@ -0,0 +1,11 @@
+
+union Test = {
+  Ctor1 : int,
+  Ctor2 : (int, int)
+}
+
+val "print_endline" : string -> unit
+
+function main() -> unit = {
+  print_endline("ok")
+}
diff --git a/test/coq/pass/booltyparam.sail b/test/coq/pass/booltyparam.sail
new file mode 100644
index 00000000..423c2720
--- /dev/null
+++ b/test/coq/pass/booltyparam.sail
@@ -0,0 +1,11 @@
+/* Test a boolean type parameter.  Not sure that this is terribly useful,
+   but it fills a gap in coverage... */
+
+$include <prelude.sail>
+
+union perhaps('b : Bool) = {No : unit, Yes : {'n, 'b. atom('n)}}
+
+val foo : forall 'n. atom('n) -> perhaps('n >= 0)
+
+function foo(n) =
+  if n >= 0 then Yes(n) else No()
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index b1df7010..75791bfd 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -93,6 +93,33 @@ function assign3(x) = {
   y
 }
 
+/* Test that matching on a variable which happens to fix a bitvector variable's
+   size updates the environment properly. */
+
+val assign4 : forall 'm, 'm in {1,2}. (implicit('m),bits(8*'m)) -> bits(8*'m)
+
+function assign4(m,x) = {
+  y : bits(8*'m) = x;
+  match m {
+    1 => y = y + 0x01,
+    2 => y[7..0] = 0x89
+  };
+  y
+}
+
+/* The same as assign4, except with a distinct type variable. */
+
+val assign5 : forall 'm 'n, 'm in {1,2} & 'n == 8 * 'm. (implicit('m),bits('n)) -> bits('n)
+
+function assign5(m,x) = {
+  y : bits('n) = x;
+  match m {
+    1 => y = y + 0x01,
+    2 => y[7..0] = 0x89
+  };
+  y
+}
+
 /* Adding casts for top-level pattern matches */
 
 val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (atom('n), bits('m)) -> bits('n) effect pure
@@ -140,6 +167,10 @@ function run () = {
     assert(assign2(0x1234) == 0x00001234);
     assert(assign3(0x12) == 0x13);
     assert(assign3(0x1234) == 0x1289);
+    assert(assign4(0x12) == 0x13);
+    assert(assign4(0x1234) == 0x1289);
+    assert(assign5(0x12) == 0x13);
+    assert(assign5(0x1234) == 0x1289);
     assert(foo2(32,0x12) == 0x00120012);
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
diff --git a/test/mono/nonlinearpat.sail b/test/mono/nonlinearpat.sail
new file mode 100644
index 00000000..e0aaeff3
--- /dev/null
+++ b/test/mono/nonlinearpat.sail
@@ -0,0 +1,17 @@
+default Order dec
+$include <prelude.sail>
+
+val test : forall 'n, 'n in {8,16}. (int('n),int('n),bits(1)) -> bits(64) effect pure
+
+function test(x,y,b) = {
+  let 'z = x + y in
+  let v : bits('z) = sail_zero_extend(b,z) in
+  sail_zero_extend(v,64)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test(8,8,0b0) == 0x0000000000000000);
+  assert(test(16,16,0b1) == 0x0000000000000001);
+}
diff --git a/test/mono/pass/nonlinearpat b/test/mono/pass/nonlinearpat
new file mode 100644
index 00000000..3f235d60
--- /dev/null
+++ b/test/mono/pass/nonlinearpat
@@ -0,0 +1 @@
+nonlinearpat.sail -auto_mono
diff --git a/test/mono/pass/union_split b/test/mono/pass/union_split
new file mode 100644
index 00000000..cdd2763d
--- /dev/null
+++ b/test/mono/pass/union_split
@@ -0,0 +1 @@
+union_split.sail -auto_mono
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
index d2023229..f95dc7d5 100755
--- a/test/mono/run_tests.sh
+++ b/test/mono/run_tests.sh
@@ -72,7 +72,7 @@ do
                "$SAILDIR/src/gen_lib/sail2_values.lem" \
                "$SAILDIR/src/gen_lib/sail2_operators.lem" \
                "$SAILDIR/src/gen_lib/sail2_operators_mwords.lem" \
-               "$SAILDIR/src/lem_interp/sail2_instr_kinds.lem" \
+               "$SAILDIR/src/gen_lib/sail2_instr_kinds.lem" \
                "$SAILDIR/src/gen_lib/sail2_prompt.lem" \
                "$SAILDIR/src/gen_lib/sail2_state_monad.lem" \
                "$SAILDIR/src/gen_lib/sail2_state.lem" \
diff --git a/test/mono/union_split.sail b/test/mono/union_split.sail
new file mode 100644
index 00000000..2403e644
--- /dev/null
+++ b/test/mono/union_split.sail
@@ -0,0 +1,23 @@
+default Order dec
+$include <prelude.sail>
+
+/* Simple case split example on a variant datatype */
+
+union ast = {
+  SomeOp : {'n, 'n in {8,16}. (int('n),bits('n))}
+}
+
+val execute : ast -> bits(32)
+
+function execute(SomeOp(n as int('n),v)) = {
+  a : bits('n) = sail_zero_extend(0x12,n);
+  b : bits('n) = and_vec(v, a);
+  sail_zero_extend(b,32)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(execute(SomeOp(8,0x11)) == 0x00000010);
+  assert(execute(SomeOp(16,0x3333)) == 0x00000012);
+}
diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.unsat.sail
index f792871f..f792871f 100644
--- a/test/smt/revrev_endianness.sail
+++ b/test/smt/revrev_endianness.unsat.sail
diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.unsat.sail
index 33ba93a2..33ba93a2 100644
--- a/test/smt/revrev_endianness2.sail
+++ b/test/smt/revrev_endianness2.unsat.sail
diff --git a/test/typecheck/fail/scattered_union_rec.expect b/test/typecheck/fail/scattered_union_rec.expect
new file mode 100644
index 00000000..cbc9f70a
--- /dev/null
+++ b/test/typecheck/fail/scattered_union_rec.expect
@@ -0,0 +1,16 @@
+Type error:
+[scattered_union_rec.sail]:6:24-25
+6 |union clause U = Ctor : E
+  |                        ^
+  | Undefined type E
+  | This error was caused by:
+  | [scattered_union_rec.sail]:6:0-25
+  | 6 |union clause U = Ctor : E
+  |   |^-----------------------^
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | This error was caused by:
+  | [scattered_union_rec.sail]:6:13-14
+  | 6 |union clause U = Ctor : E
+  |   |             ^
+  |   | As this is a scattered union clause, this could also be caused by using a type defined after the 'scattered union' declaration
+  | 
diff --git a/test/typecheck/fail/scattered_union_rec.sail b/test/typecheck/fail/scattered_union_rec.sail
new file mode 100644
index 00000000..9f005f4e
--- /dev/null
+++ b/test/typecheck/fail/scattered_union_rec.sail
@@ -0,0 +1,6 @@
+
+scattered union U
+
+enum E = A | B | C
+
+union clause U = Ctor : E
diff --git a/test/typecheck/fail/shadow_leak_check.expect b/test/typecheck/fail/shadow_leak_check.expect
new file mode 100644
index 00000000..a92e0078
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_check.expect
@@ -0,0 +1,8 @@
+Type error:
+[shadow_leak_check.sail]:17:5-18:6
+17 |     let 'x = some_other_int();
+   |     ^-------------------------
+18 |     x
+   |-----^
+   | Type variable 'x would leak into a scope where it is shadowed
+   | 
diff --git a/test/typecheck/fail/shadow_leak_check.sail b/test/typecheck/fail/shadow_leak_check.sail
new file mode 100644
index 00000000..266a0469
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_check.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+function some_int() -> int = {
+  4
+}
+
+function some_other_int() -> int = {
+  5
+}
+
+val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit
+
+function main() -> unit = {
+  let 'x = some_int();
+
+  let 'y: int('x) = {
+     let 'x = some_other_int();
+     x
+  };
+
+  _prove(constraint('x == 'y));
+
+  test(x, y)
+}
diff --git a/test/typecheck/fail/shadow_leak_infer.expect b/test/typecheck/fail/shadow_leak_infer.expect
new file mode 100644
index 00000000..63aba5d7
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_infer.expect
@@ -0,0 +1,8 @@
+Type error:
+[shadow_leak_infer.sail]:17:5-18:6
+17 |     let 'x = some_other_int();
+   |     ^-------------------------
+18 |     x
+   |-----^
+   | Type variable '_x would leak into a scope where it is shadowed
+   | 
diff --git a/test/typecheck/fail/shadow_leak_infer.sail b/test/typecheck/fail/shadow_leak_infer.sail
new file mode 100644
index 00000000..cb122cf9
--- /dev/null
+++ b/test/typecheck/fail/shadow_leak_infer.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+function some_int() -> int = {
+  4
+}
+
+function some_other_int() -> int = {
+  5
+}
+
+val test : forall 'n 'm, 'n == 'm. (int('n), int('m)) -> unit
+
+function main() -> unit = {
+  let 'x = some_int();
+
+  let 'y = {
+     let 'x = some_other_int();
+     x
+  };
+
+  _prove(constraint('x == 'y));
+
+  test(x, y)
+}
diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect
new file mode 100644
index 00000000..2b5b1852
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[struct_rec.sail]:3:10-11
+3 |  field : S
+  |          ^
+  | Undefined type S
+  | This error was caused by:
+  | [struct_rec.sail]:2:0-4:1
+  | 2 |struct S = {
+  |   |^-----------
+  | 4 |}
+  |   |^
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
diff --git a/test/typecheck/fail/struct_rec.sail b/test/typecheck/fail/struct_rec.sail
new file mode 100644
index 00000000..01c29d6d
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.sail
@@ -0,0 +1,4 @@
+
+struct S = {
+  field : S
+}
diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect
new file mode 100644
index 00000000..3d482f40
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.expect
@@ -0,0 +1,11 @@
+Type error:
+[synonym_rec.sail]:2:9-10
+2 |type T = T
+  |         ^
+  | Undefined type T
+  | This error was caused by:
+  | [synonym_rec.sail]:2:0-10
+  | 2 |type T = T
+  |   |^--------^
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
diff --git a/test/typecheck/fail/synonym_rec.sail b/test/typecheck/fail/synonym_rec.sail
new file mode 100644
index 00000000..54906418
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.sail
@@ -0,0 +1,2 @@
+
+type T = T
diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect
new file mode 100644
index 00000000..7fd07169
--- /dev/null
+++ b/test/typecheck/fail/union_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_rec.sail]:3:9-10
+3 |  Ctor : U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_rec.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
diff --git a/test/typecheck/fail/union_rec.sail b/test/typecheck/fail/union_rec.sail
new file mode 100644
index 00000000..7ca7b8e9
--- /dev/null
+++ b/test/typecheck/fail/union_rec.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U
+}
diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect
new file mode 100644
index 00000000..ec610ae6
--- /dev/null
+++ b/test/typecheck/fail/union_recf.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_recf.sail]:3:9-10
+3 |  Ctor : U -> U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_recf.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
diff --git a/test/typecheck/fail/union_recf.sail b/test/typecheck/fail/union_recf.sail
new file mode 100644
index 00000000..f64ca675
--- /dev/null
+++ b/test/typecheck/fail/union_recf.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U -> U
+}
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index 8c95193d..0b0dda29 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -3,4 +3,9 @@ Type error:
 10 |type MyStruct64 = MyStruct(65)
    |                  ^------^
    | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   | This error was caused by:
+   | [constrained_struct/v1.sail]:10:0-30
+   | 10 |type MyStruct64 = MyStruct(65)
+   |    |^----------------------------^
+   |    | Types are not well-formed within this type definition. Note that recursive types are forbidden.
    | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index e2823692..8d061933 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex270#)
+   | * datasize('ex276#)
    | 
diff --git a/test/typecheck/pass/mapping_rreg.sail b/test/typecheck/pass/mapping_rreg.sail
new file mode 100644
index 00000000..1f3e1212
--- /dev/null
+++ b/test/typecheck/pass/mapping_rreg.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <prelude.sail>
+
+register enabled : bits(1)
+
+union ast = {
+  I: bits(1)
+}
+
+val encdec : ast <-> bits(2) effect {rreg}
+
+scattered mapping encdec
+
+mapping clause encdec = I(imm) if enabled == 0b0 <-> 0b0 @ imm if enabled == 0b0
+
+end encdec
diff --git a/test/typecheck/pass/new_bitfields.sail b/test/typecheck/pass/new_bitfields.sail
new file mode 100644
index 00000000..fdb17576
--- /dev/null
+++ b/test/typecheck/pass/new_bitfields.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option -new_bitfields
+
+bitfield B : bits(32) = {
+  Field: 7..0
+}
+
+register R : B
+
+function main() -> unit = {
+  R[Field] = 0xFF;
+  assert(R[Field] == 0xFF)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index 24439bed..90166904 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -5,7 +5,7 @@ Type error:
    | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
    | Coercion failed because:
    | Mismatched argument types in subtype check
-   | This error occured because of a previous error:
+   | This error was caused by:
    | [reg_32_64/v2.sail]:21:2-15
    | 21 |  (*R)['d .. 0] = data
    |    |  ^-----------^
diff --git a/test/typecheck/pass/union_recf_ok.sail b/test/typecheck/pass/union_recf_ok.sail
new file mode 100644
index 00000000..0f415601
--- /dev/null
+++ b/test/typecheck/pass/union_recf_ok.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : int -> U
+}
\ No newline at end of file
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index e5650646..adc30c42 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -87,6 +87,24 @@ do
     done
 done
 
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    if $SAILDIR/sail -no_memo_z3 $(basename $file) 2> result
+    then
+        red "Expected failure, but $i $(basename $file) passed" "fail"
+    else
+        if diff ${file%.sail}.expect result;
+        then
+            green "failing $i $(basename $file)" "pass"
+        else
+            yellow "failing $i $(basename $file)" "unexpected error"
+        fi
+    fi;
+    rm -f result;
+    popd > /dev/null
+done
+
 finish_suite "Typechecking tests"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
index ba436daf..1d174797 100755
--- a/test/typecheck/update_errors.sh
+++ b/test/typecheck/update_errors.sh
@@ -10,8 +10,15 @@ do
     shopt -s nullglob;
     for file in $DIR/pass/${i%.sail}/*.sail;
     do
-	pushd $DIR/pass > /dev/null;
-	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
-	popd > /dev/null
+        pushd $DIR/pass > /dev/null;
+        $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+        popd > /dev/null
     done
 done
+
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    $SAILDIR/sail -no_memo_z3 $(basename $file) 2> ${file%.sail}.expect || true;
+    popd > /dev/null
+done