2 files changed, 86 insertions, 0 deletions
diff --git a/test/ocaml/reg_alias/expect b/test/ocaml/reg_alias/expect
new file mode 100644
index 00000000..21493790
--- /dev/null
+++ b/test/ocaml/reg_alias/expect
@@ -0,0 +1,7 @@
+CR = 0x00
+CR = 0xCA
+CR.CR0 = 0xC
+CR.CR1 = 0b10
+CR.CR2 = 0b10
+CR = 0xFA
+CR = 0xF8
diff --git a/test/ocaml/reg_alias/ra.sail b/test/ocaml/reg_alias/ra.sail
new file mode 100644
index 00000000..f4e6d529
--- /dev/null
+++ b/test/ocaml/reg_alias/ra.sail
@@ -0,0 +1,79 @@
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+struct cr = {
+  CR0 : bits(4),
+  CR1 : bits(2),
+  CR2 : bits(2)
+}
+
+val _set_CR0 : (register(cr), bits(4)) -> unit effect {wreg}
+val _get_CR0 : register(cr) -> bits(4) effect {rreg}
+
+val _set_CR1 : (register(cr), bits(2)) -> unit effect {wreg}
+val _get_CR1 : register(cr) -> bits(2) effect {rreg}
+
+val _set_CR2 : (register(cr), bits(2)) -> unit effect {wreg}
+val _get_CR2 : register(cr) -> bits(2) effect {rreg}
+
+function _set_CR0 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR0 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR0 cr = reg_deref(cr).CR0
+
+function _set_CR1 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR1 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR1 cr = reg_deref(cr).CR1
+
+function _set_CR2 (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR2 = v;
+  (*cr_ref) = cr;
+}
+function _get_CR2 cr = reg_deref(cr).CR2
+
+overload _mod_CR0 = {_set_CR0, _get_CR0}
+overload _mod_CR1 = {_set_CR1, _get_CR1}
+overload _mod_CR2 = {_set_CR2, _get_CR2}
+
+val _get_cr : register(cr) -> bits(8) effect {rreg}
+
+function _get_cr cr_ref =
+  let cr = reg_deref(cr_ref) in cr.CR0 @ cr.CR1 @ cr.CR2
+
+val _set_cr : (register(cr), bits(8)) -> unit effect {wreg}
+
+function _set_cr (cr_ref, v) = {
+  cr = _reg_deref(cr_ref);
+  cr.CR0 = v[7 .. 4];
+  cr.CR1 = v[3 .. 2];
+  cr.CR2 = v[1 .. 0];
+  (*cr_ref) = cr
+}
+
+overload _mod_cr = {_set_cr, _get_cr}
+
+register CR : cr
+
+val main : unit -> unit effect {wreg, rreg}
+
+function main () = {
+  CR->cr() = 0x00;
+  print_bits("CR = ", CR->cr());
+  CR->cr() = 0xCA;
+  print_bits("CR = ", CR->cr());
+  print_bits("CR.CR0 = ", CR->CR0());
+  print_bits("CR.CR1 = ", CR->CR1());
+  print_bits("CR.CR2 = ", CR->CR2());
+  CR->CR0() = 0xF;
+  print_bits("CR = ", CR->cr());
+  CR->CR2() = 0b00;
+  print_bits("CR = ", CR->cr());
+  ()
+}
+\ No newline at end of file