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

22 files changed, 222 insertions, 5 deletions

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