2 files changed, 228 insertions, 0 deletions
diff --git a/test/ocaml/reg_ref/expect b/test/ocaml/reg_ref/expect
new file mode 100644
index 00000000..904fc765
--- /dev/null
+++ b/test/ocaml/reg_ref/expect
@@ -0,0 +1,51 @@
+Testing register references
+Register 1
+Assigning 0x00000000
+Register 2
+Assigning 0x00000000
+Register 3
+Assigning 0x00000000
+1 = 0x00000000
+2 = 0x00000000
+3 = 0x00000000
+Register 1
+Assigning 0xCAFEBEEF
+1 = 0xCAFEBEEF
+2 = 0x00000000
+3 = 0x00000000
+Reading 1 to variable
+v = 0xCAFEBEEF
+Register 3
+Assigning 0x00BEEF00
+1 = 0xCAFEBEEF
+2 = 0x00000000
+3 = 0x00BEEF00
+Reading zero register
+0 = 0x00000000
+Register 2
+Assigning 0xDEADCAFE
+2 = 0xDEADCAFE
+Assigning register 2 to register 1
+Register 2
+Assigning 0xCAFEBEEF
+1 = 0xCAFEBEEF
+2 = 0xCAFEBEEF
+3 = 0x00BEEF00
+
+Testing slicing
+s = 0b111
+s = 0b01110
+s = 0xE
+b = 0b01110
+b = 0b01010
+b = 0b01111
+
+Testing bit aliasing
+CR0 = 0x0
+LT = 0b0
+Setting LT to bitone
+CR0 = 0x8
+LT = 0b1
+Setting CR0 to 0b0111
+CR0 = 0x7
+LT = 0b0
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
new file mode 100644
index 00000000..3c11dcb8
--- /dev/null
+++ b/test/ocaml/reg_ref/rr.sail
@@ -0,0 +1,177 @@
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val deref = "reg_deref" : forall ('a : Type). ref('a) -> 'a
+
+/* *** Register reference list example *** */
+
+type regno ('n : Int), 0 <= 'n < 4 = atom('n)
+
+/* regiser x0 : bits(32) is always 0 */
+register x1 : bits(32)
+register x2 : bits(32)
+register x3 : bits(32)
+
+let GPRs : vector(3, dec, register(bits(32))) =
+  [ ref x3, ref x2, ref x1 ]
+
+val rGPR : forall 'n, 0 <= 'n < 4. regno('n) -> bits(32) effect {rreg}
+
+function rGPR 0 = 0x00000000
+and rGPR (r if r > 0) = reg_deref(GPRs[r - 1])
+
+val wGPR : forall 'n, 1 <= 'n < 4. (regno('n), bits(32)) -> unit effect {wreg}
+
+function wGPR (r, v) = {
+  print_int("Register ", r);
+  print_bits("Assigning ", v);
+  (*GPRs[r - 1]) = v
+}
+
+overload _mod_GPR = { rGPR, wGPR }
+
+/* *** Power style vector slicing *** */
+
+/* Create a new type which is a pair of a bitvector and a start index
+
+   slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
+newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m))
+
+/* Extract the bitvector from a slice */
+val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
+
+function slice_bits MkSlice(_, xs) = xs
+
+/* Take a slice from a bitvector */
+val vector_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+  (bits('n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
+
+function vector_slice (v, to, from) = MkSlice(from, v[to .. from])
+
+val slice_slice : forall 'n 'm 'o 'p.
+  (slice('p, 'n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
+
+function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
+
+/* We can update a bitvector from another bitvector or a slice */
+val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+  (ref(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit
+
+function _set_slice (v, stop, start, update) = {
+  v2 = deref(v);
+  v2[stop .. start] = update;
+  (*v) = v2;
+}
+
+val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n.
+  (ref(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit
+
+function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
+
+val slice_bit : forall 'n. slice('n, 1) -> bit
+
+function slice_bit MkSlice(_, [b]) = b
+
+/* Overload slice modifier */
+overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
+
+/* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
+infix 1 ...
+
+type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1))
+
+struct cr = {
+  CR0 : 7 ... 4,
+  /* 7 : LT; 6 : GT; 5 : EQ; 4 : SO; */
+  CR1 : 3 ... 2,
+  CR3 : 1 ... 0,
+}
+
+register CR : cr
+
+val _get_LT : cr -> bit
+val _set_LT : (register(cr), bit) -> unit effect {rreg, wreg}
+
+function _get_LT cr = slice_bit(cr.CR0.slice(7, 7))
+function _set_LT (cr_ref, b) = {
+  cr = reg_deref(cr_ref);
+  cr.CR0 = MkSlice(4, [slice_bits(cr.CR0) with (7 - 4) = b]);
+  (*cr_ref) = cr;
+}
+
+overload _mod_LT = {_get_LT, _set_LT}
+
+/* *** Test Program *** */
+
+val main : unit -> unit effect {wreg, rreg}
+
+val print_regs : unit -> unit effect {rreg}
+
+function print_regs () = {
+  print_bits("1 = ", rGPR(1));
+  print_bits("2 = ", rGPR(2));
+  print_bits("3 = ", rGPR(3));
+}
+
+function main () = {
+  print("Testing register references");
+  wGPR(1) = 0x00000000;
+  wGPR(2) = 0x00000000;
+  wGPR(3) = 0x00000000;
+
+  print_regs ();
+
+  /* Assign to lowest assignable register */
+  wGPR(1) = 0xCAFEBEEF;
+  print_regs ();
+
+  /* Reading to variable */
+  print("Reading 1 to variable");
+  v = rGPR(1);
+  print_bits("v = ", v);
+
+  /* Assign to highest register */
+  wGPR(3) = 0x00BEEF00;
+  print_regs ();
+
+  print("Reading zero register");
+  print_bits("0 = ", rGPR(0));
+
+  /* Test overloaded version */
+  _mod_GPR(2) = 0xDEADCAFE;
+  print_bits("2 = ", _mod_GPR(2));
+
+  /* Method syntax */
+  print("Assigning register 2 to register 1");
+  2.GPR() = 1.GPR();
+  print_regs();
+
+  /* Slice testing */
+  print("\nTesting slicing");
+  let s = 0b01110.slice(3, 1);
+  print_bits("s = ", slice_bits(s));
+  let s = 0b01110.slice(4, 0);
+  print_bits("s = ", slice_bits(s));
+  let s = 0b01110.slice(3, 0);
+  print_bits("s = ", slice_bits(s));
+
+  /* Updating slices */
+  b = 0b01110;
+  print_bits("b = ", b);
+  b->slice(3, 1) = 0b101;
+  print_bits("b = ", b);
+  b->slice(2, 0) = 0xFF.slice(5, 3);
+  print_bits("b = ", b);
+
+  /* Bit aliasing */
+  print("\nTesting bit aliasing");
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+  print("Setting LT to bitone");
+  CR->LT() = bitone;
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+  print("Setting CR0 to 0b0111");
+  CR.CR0 = MkSlice(4, 0b0111);
+  print_bits("CR0 = ", slice_bits(CR.CR0));
+  print_bits("LT = ", [CR.LT()]);
+}