summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/typecheck/fail/mips_CauseReg1.sail14
-rw-r--r--test/typecheck/fail/mips_CauseReg2.sail14
-rw-r--r--test/typecheck/fail/mips_CauseReg3.sail14
-rw-r--r--test/typecheck/fail/mips_CauseReg4.sail14
-rw-r--r--test/typecheck/fail/mips_CauseReg5.sail14
-rw-r--r--test/typecheck/fail/mips_CauseReg6.sail14
-rw-r--r--test/typecheck/fail/my_unsigned1.sail8
-rw-r--r--test/typecheck/pass/cast_lexp2.sail (renamed from test/typecheck/pass/cast_lexp2].sail)0
-rw-r--r--test/typecheck/pass/exit1.sail8
-rw-r--r--test/typecheck/pass/exit2.sail7
-rw-r--r--test/typecheck/pass/exit3.sail7
-rw-r--r--test/typecheck/pass/mips_CauseReg1.sail14
-rw-r--r--test/typecheck/pass/mips_CauseReg2.sail14
-rw-r--r--test/typecheck/pass/mips_CauseReg3.sail14
-rw-r--r--test/typecheck/pass/mips_regtyps.sail53
-rw-r--r--test/typecheck/pass/mips_tlbindext_dec.sail5
-rw-r--r--test/typecheck/pass/mips_tlbindext_inc.sail5
17 files changed, 219 insertions, 0 deletions
diff --git a/test/typecheck/fail/mips_CauseReg1.sail b/test/typecheck/fail/mips_CauseReg1.sail
new file mode 100644
index 00000000..ae99e625
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg1.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 30 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg2.sail b/test/typecheck/fail/mips_CauseReg2.sail
new file mode 100644
index 00000000..683f5a2a
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg2.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 3 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg3.sail b/test/typecheck/fail/mips_CauseReg3.sail
new file mode 100644
index 00000000..09e27e27
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg3.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 32 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg4.sail b/test/typecheck/fail/mips_CauseReg4.sail
new file mode 100644
index 00000000..1f14981f
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg4.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 8 .. 15 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg5.sail b/test/typecheck/fail/mips_CauseReg5.sail
new file mode 100644
index 00000000..98fc614a
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg5.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 22 : IV; (* special interrupt vector not supported *)
+ 23 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg6.sail b/test/typecheck/fail/mips_CauseReg6.sail
new file mode 100644
index 00000000..ecb8322e
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg6.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : BD; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/fail/my_unsigned1.sail b/test/typecheck/fail/my_unsigned1.sail
new file mode 100644
index 00000000..958340ff
--- /dev/null
+++ b/test/typecheck/fail/my_unsigned1.sail
@@ -0,0 +1,8 @@
+
+default Order inc
+
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o >= 0, 'o + 1 <= 2**'m. vector<'n,'m,'ord,bit> -> [:'o:] effect pure my_unsigned
+
+let MAX = my_unsigned(0xff)
+
+let ([:0:]) MIN = MAX \ No newline at end of file
diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2.sail
index a6f6d299..a6f6d299 100644
--- a/test/typecheck/pass/cast_lexp2].sail
+++ b/test/typecheck/pass/cast_lexp2.sail
diff --git a/test/typecheck/pass/exit1.sail b/test/typecheck/pass/exit1.sail
new file mode 100644
index 00000000..fa1de7e0
--- /dev/null
+++ b/test/typecheck/pass/exit1.sail
@@ -0,0 +1,8 @@
+
+val unit -> [:6:] effect pure test
+
+function [:6:] test () =
+{
+ exit ();
+ 6
+} \ No newline at end of file
diff --git a/test/typecheck/pass/exit2.sail b/test/typecheck/pass/exit2.sail
new file mode 100644
index 00000000..40bf7da3
--- /dev/null
+++ b/test/typecheck/pass/exit2.sail
@@ -0,0 +1,7 @@
+
+val unit -> [:6:] effect pure test
+
+function [:6:] test () =
+{
+ exit ();
+} \ No newline at end of file
diff --git a/test/typecheck/pass/exit3.sail b/test/typecheck/pass/exit3.sail
new file mode 100644
index 00000000..9ac0aa78
--- /dev/null
+++ b/test/typecheck/pass/exit3.sail
@@ -0,0 +1,7 @@
+
+val forall Type 'a. unit -> 'a effect pure test
+
+function forall Type 'a. 'a test () =
+{
+ exit ();
+} \ No newline at end of file
diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail
new file mode 100644
index 00000000..e05d0af8
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg1.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail
new file mode 100644
index 00000000..f62824f1
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg2.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 1 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/pass/mips_CauseReg3.sail b/test/typecheck/pass/mips_CauseReg3.sail
new file mode 100644
index 00000000..24b07fcd
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg3.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 23 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
diff --git a/test/typecheck/pass/mips_regtyps.sail b/test/typecheck/pass/mips_regtyps.sail
new file mode 100644
index 00000000..f7a3ce91
--- /dev/null
+++ b/test/typecheck/pass/mips_regtyps.sail
@@ -0,0 +1,53 @@
+
+(* mips_prelude.sail: declarations of mips registers, and functions common
+ to mips instructions (e.g. address translation) *)
+
+(* bit vectors have indices decreasing from left i.e. msb is highest index *)
+default Order dec
+
+register (bit[64]) PC
+register (bit[64]) nextPC
+
+(* CP0 Registers *)
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+ 31 : BD; (* branch delay *)
+ (*30 : Z0;*)
+ 29 .. 28 : CE; (* for coprocessor enable exception *)
+ (*27 .. 24 : Z1;*)
+ 23 : IV; (* special interrupt vector not supported *)
+ 22 : WP; (* watchpoint exception occurred *)
+ (*21 .. 16 : Z2; *)
+ 15 .. 8 : IP; (* interrupt pending bits *)
+ (*7 : Z3;*)
+ 6 .. 2 : ExcCode; (* code of last exception *)
+ (*1 .. 0 : Z4;*)
+}
+
+typedef TLBEntryLoReg = register bits [63 : 0] {
+ 63 : CapS;
+ 62 : CapL;
+ 29 .. 6 : PFN;
+ 5 .. 3 : C;
+ 2 : D;
+ 1 : V;
+ 0 : G;
+}
+
+typedef TLBEntryHiReg = register bits [63 : 0] {
+ 63 .. 62 : R;
+ 39 .. 13 : VPN2;
+ 7 .. 0 : ASID;
+}
+
+typedef ContextReg = register bits [63 : 0] {
+ 63 .. 23 : PTEBase;
+ 22 .. 4 : BadVPN2;
+ (*3 .. 0 : ZR;*)
+}
+
+typedef XContextReg = register bits [63 : 0] {
+ 63 .. 33: PTEBase;
+ 32 .. 31: R;
+ 30 .. 4: BadVPN2;
+}
diff --git a/test/typecheck/pass/mips_tlbindext_dec.sail b/test/typecheck/pass/mips_tlbindext_dec.sail
new file mode 100644
index 00000000..af98cd85
--- /dev/null
+++ b/test/typecheck/pass/mips_tlbindext_dec.sail
@@ -0,0 +1,5 @@
+
+default Order dec
+
+typedef TLBIndexT = (bit[6])
+let (TLBIndexT) TLBIndexMax = 0b111111
diff --git a/test/typecheck/pass/mips_tlbindext_inc.sail b/test/typecheck/pass/mips_tlbindext_inc.sail
new file mode 100644
index 00000000..d64ffd68
--- /dev/null
+++ b/test/typecheck/pass/mips_tlbindext_inc.sail
@@ -0,0 +1,5 @@
+
+default Order inc
+
+typedef TLBIndexT = (bit[6])
+let (TLBIndexT) TLBIndexMax = 0b111111
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:07:29 +0000