From 454084884c7a0bbe6c00ea46349962e8d5228118 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 23 Jun 2017 18:13:33 +0100 Subject: Support for more sail constructs Added support for: * Register type declarations * Undefined literals * Exit statement * Toplevel let statements * Vector literals i.e. [a, b, c] * Binary bitvector literals * Hex bitvector literals Patched the parser so you can actually write 2**'n - 1 in a nexp. The parser rules for nexps are a bit strange, and there didn't seem to be anyway to write this before without it causing a parse error. Can now typecheck up to line 332 of mips_prelude in mips/, but need to add support for the implict passing of registers by names to go any further, which should be fun... --- test/typecheck/fail/mips_CauseReg1.sail | 14 ++++++++ test/typecheck/fail/mips_CauseReg2.sail | 14 ++++++++ test/typecheck/fail/mips_CauseReg3.sail | 14 ++++++++ test/typecheck/fail/mips_CauseReg4.sail | 14 ++++++++ test/typecheck/fail/mips_CauseReg5.sail | 14 ++++++++ test/typecheck/fail/mips_CauseReg6.sail | 14 ++++++++ test/typecheck/fail/my_unsigned1.sail | 8 +++++ test/typecheck/pass/cast_lexp2.sail | 7 ++++ test/typecheck/pass/cast_lexp2].sail | 7 ---- test/typecheck/pass/exit1.sail | 8 +++++ test/typecheck/pass/exit2.sail | 7 ++++ test/typecheck/pass/exit3.sail | 7 ++++ test/typecheck/pass/mips_CauseReg1.sail | 14 ++++++++ test/typecheck/pass/mips_CauseReg2.sail | 14 ++++++++ test/typecheck/pass/mips_CauseReg3.sail | 14 ++++++++ test/typecheck/pass/mips_regtyps.sail | 53 +++++++++++++++++++++++++++++ test/typecheck/pass/mips_tlbindext_dec.sail | 5 +++ test/typecheck/pass/mips_tlbindext_inc.sail | 5 +++ 18 files changed, 226 insertions(+), 7 deletions(-) create mode 100644 test/typecheck/fail/mips_CauseReg1.sail create mode 100644 test/typecheck/fail/mips_CauseReg2.sail create mode 100644 test/typecheck/fail/mips_CauseReg3.sail create mode 100644 test/typecheck/fail/mips_CauseReg4.sail create mode 100644 test/typecheck/fail/mips_CauseReg5.sail create mode 100644 test/typecheck/fail/mips_CauseReg6.sail create mode 100644 test/typecheck/fail/my_unsigned1.sail create mode 100644 test/typecheck/pass/cast_lexp2.sail delete mode 100644 test/typecheck/pass/cast_lexp2].sail create mode 100644 test/typecheck/pass/exit1.sail create mode 100644 test/typecheck/pass/exit2.sail create mode 100644 test/typecheck/pass/exit3.sail create mode 100644 test/typecheck/pass/mips_CauseReg1.sail create mode 100644 test/typecheck/pass/mips_CauseReg2.sail create mode 100644 test/typecheck/pass/mips_CauseReg3.sail create mode 100644 test/typecheck/pass/mips_regtyps.sail create mode 100644 test/typecheck/pass/mips_tlbindext_dec.sail create mode 100644 test/typecheck/pass/mips_tlbindext_inc.sail (limited to 'test/typecheck') 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 new file mode 100644 index 00000000..a6f6d299 --- /dev/null +++ b/test/typecheck/pass/cast_lexp2.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := 10; + y +} diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2].sail deleted file mode 100644 index a6f6d299..00000000 --- a/test/typecheck/pass/cast_lexp2].sail +++ /dev/null @@ -1,7 +0,0 @@ - -val unit -> int effect pure test - -function int test () = { - (nat) y := 10; - y -} 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 -- cgit v1.2.3