summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/ocaml/prelude.sail14
-rw-r--r--test/ocaml/reg_alias/expect7
-rw-r--r--test/ocaml/reg_alias/ra.sail79
-rw-r--r--test/ocaml/reg_passing/reg_passing.sail6
-rw-r--r--test/ocaml/reg_ref/expect51
-rw-r--r--test/ocaml/reg_ref/rr.sail177
-rw-r--r--test/ocaml/vec_32_64/vec_32_64.sail6
7 files changed, 327 insertions, 13 deletions
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index b56ce7e2..9bdfdc33 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -1,6 +1,6 @@
default Order dec
-type bits ('n : Int) = vector('n - 1, 'n, dec, bit)
+type bits ('n : Int) = vector('n, dec, bit)
infix 4 ==
@@ -20,7 +20,7 @@ val eq_real = "eq_real" : (real, real) -> bool
val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool
-val length = "length" : forall 'n ('a : Type). vector('n - 1, 'n, dec, 'a) -> atom('n)
+val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
@@ -33,24 +33,24 @@ val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int).
overload vector_subrange = {vector_subrange_A, vector_subrange_B}
val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
- (vector('n - 1, 'n, dec, 'a), atom('m)) -> 'a
+ (vector('n, dec, 'a), atom('m)) -> 'a
val vector_access_B = "access" : forall ('n : Int) ('a : Type).
- (vector('n - 1, 'n, dec, 'a), int) -> 'a
+ (vector('n, dec, 'a), int) -> 'a
overload vector_access = {vector_access_A, vector_access_B}
val vector_update = "update" : forall 'n ('a : Type).
- (vector('n - 1, 'n, dec, 'a), int, 'a) -> vector('n - 1, 'n, dec, 'a)
+ (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
val vector_update_subrange = "update_subrange" : forall 'n 'm 'o.
(bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
val vcons : forall ('n : Int) ('a : Type).
- ('a, vector('n - 1, 'n, dec, 'a)) -> vector('n, 'n + 1, dec, 'a)
+ ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
val append = "append" : forall ('n : Int) ('m : Int) ('a : Type).
- (vector('n - 1, 'n, dec, 'a), vector('m - 1, 'm, dec, 'a)) -> vector('n + 'm - 1, 'n + 'm, dec, 'a)
+ (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
val not_bool = "not" : bool -> bool
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
diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail
index 94acdf7e..d84f98e0 100644
--- a/test/ocaml/reg_passing/reg_passing.sail
+++ b/test/ocaml/reg_passing/reg_passing.sail
@@ -17,8 +17,8 @@ function f R = {
val g : unit -> unit effect {rreg, wreg}
function g () = {
- f(R1);
- f(R2);
+ f(ref R1);
+ f(ref R2);
}
val main : unit -> unit effect {rreg, wreg}
@@ -28,7 +28,7 @@ function main () = {
R2 = 5;
g ();
R3 = 10;
- f(R3);
+ f(ref R3);
R2 = 20;
output("R1 = ", R1);
output("R2 = ", R2);
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()]);
+}
diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail
index eb518515..60fa0e46 100644
--- a/test/ocaml/vec_32_64/vec_32_64.sail
+++ b/test/ocaml/vec_32_64/vec_32_64.sail
@@ -1,6 +1,6 @@
-(* This example is more testing the typechecker flow typing rather
+/* This example is more testing the typechecker flow typing rather
than the ocaml backend, but it does test that recursive functions work
-correctly *)
+correctly */
val get_size : unit -> {|32, 64|}
@@ -8,7 +8,7 @@ function get_size () = 32
val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit
-val zeros : forall 'n. atom('n) -> vector('n - 1, 'n, dec, bit)
+val zeros : forall 'n. atom('n) -> vector('n, dec, bit)
function zeros n =
if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 03:34:52 +0000