9 files changed, 231 insertions, 0 deletions

diff --git a/test/c/reg_32_64.expect b/test/c/reg_32_64.expect
new file mode 100644
index 00000000..c381486c
--- /dev/null
+++ b/test/c/reg_32_64.expect
@@ -0,0 +1,2 @@
+R = 0xCAFECAFEFFFFFFFF
+R = 0xFFFFFFFF
diff --git a/test/c/reg_32_64.sail b/test/c/reg_32_64.sail
new file mode 100644
index 00000000..79dfc862
--- /dev/null
+++ b/test/c/reg_32_64.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64.sail b/test/typecheck/pass/reg_32_64.sail
new file mode 100644
index 00000000..79dfc862
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect
new file mode 100644
index 00000000..eb398991
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v1.expect
@@ -0,0 +1,11 @@
+Type error:
+[reg_32_64/v1.sail]:35:9-28
+35 |  R(0) = 0xCAFE_CAFE_0000_00;
+   |         ^-----------------^
+   | No overloading for R, tried:
+   | * set_R
+   |    Could not resolve quantifiers for set_R
+   |    * (regno(0) & (56 == 32 | 56 == 64))
+   | * get_R
+   |    No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v1.sail b/test/typecheck/pass/reg_32_64/v1.sail
new file mode 100644
index 00000000..8c0e980b
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v1.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_00;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
new file mode 100644
index 00000000..f007c917
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -0,0 +1,13 @@
+Type error:
+[reg_32_64/v2.sail]:21:18-22
+21 |  (*R)['d .. 0] = data
+   |                  ^--^
+   | Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | This error occured because of a previous error:
+   | [reg_32_64/v2.sail]:21:2-15
+   | 21 |  (*R)['d .. 0] = data
+   |    |  ^-----------^
+   |    | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v2.sail b/test/typecheck/pass/reg_32_64/v2.sail
new file mode 100644
index 00000000..64daea4a
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v2.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect
new file mode 100644
index 00000000..cea45127
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v3.expect
@@ -0,0 +1,10 @@
+Type error:
+[reg_32_64/v3.sail]:29:15-21
+29 |  reg_deref(R)['d - 1 .. 0]
+   |               ^----^
+   | No overloading for (operator -), tried:
+   | * sub_atom
+   |    Cannot re-write sizeof('d)
+   | * sub_int
+   |    Cannot re-write sizeof('d)
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v3.sail b/test/typecheck/pass/reg_32_64/v3.sail
new file mode 100644
index 00000000..dda787ab
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v3.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(_, r) = {
+  let R = GPRs[r];
+  reg_deref(R)['d - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}