diff options
| author | Alasdair Armstrong | 2017-07-25 15:06:23 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-25 15:06:23 +0100 |
| commit | 3ff8009f1dc81593a972eb2050f7e1159aba718a (patch) | |
| tree | 6cad4b9def8550d02fb67032a6598c3985ddfc19 /test/typecheck | |
| parent | 5c306614427179282c8747a6fa6c34637c64ca68 (diff) | |
Improved l-expressions
- Fixed a bug where some l-expressions which wrote registers wern't
picking up register writes.
- Can now write to registers with record types. e.g. ARM's ProcState
record from ASL.
Diffstat (limited to 'test/typecheck')
| -rw-r--r-- | test/typecheck/fail/procstate1.sail | 16 | ||||
| -rw-r--r-- | test/typecheck/pass/arm_FPEXC1.sail | 53 | ||||
| -rw-r--r-- | test/typecheck/pass/procstate1.sail | 16 |
3 files changed, 85 insertions, 0 deletions
diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail new file mode 100644 index 00000000..00dc1ab1 --- /dev/null +++ b/test/typecheck/fail/procstate1.sail @@ -0,0 +1,16 @@ +default Order dec + +typedef ProcState = const struct forall Num 'n. +{ + bit['n] N; + bit[1] Z; + bit[1] C; + bit[1] V +} + +register ProcState<2> PSTATE + +function unit test () = +{ + PSTATE.N := 0b1 +} diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail new file mode 100644 index 00000000..cfae86a1 --- /dev/null +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -0,0 +1,53 @@ +default Order dec + +val forall Num 'n. (bit['n], int) -> bit effect pure vector_access + +val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1. + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange + +register vector<32 - 1, 32, dec, bit> _FPEXC32_EL2 + +val vector<32 - 1, 32, dec, bit> -> unit effect {wreg} set_FPEXC32_EL2 + +function set_FPEXC32_EL2 value_name = + { + _FPEXC32_EL2[0..0] := [value_name[0]]; + _FPEXC32_EL2[1..1] := [value_name[1]]; + _FPEXC32_EL2[2..2] := [value_name[2]]; + _FPEXC32_EL2[3..3] := [value_name[3]]; + _FPEXC32_EL2[4..4] := [value_name[4]]; + _FPEXC32_EL2[6..5] := value_name[6 .. 5]; + _FPEXC32_EL2[7..7] := [value_name[7]]; + _FPEXC32_EL2[20..11] := value_name[20 .. 11]; + _FPEXC32_EL2[29..29] := [value_name[29]]; + _FPEXC32_EL2[30..30] := [value_name[30]] + } + +val unit -> vector<32 - 1, 32, dec, bit> effect {rreg} get_FPEXC32_EL2 + +function get_FPEXC32_EL2 () = + { + (vector<32 - 1, 32, dec, bit> ) value_name := 0x04000700; + value_name[0..0] := [_FPEXC32_EL2[0]]; + value_name[1..1] := [_FPEXC32_EL2[1]]; + value_name[2..2] := [_FPEXC32_EL2[2]]; + value_name[3..3] := [_FPEXC32_EL2[3]]; + value_name[4..4] := [_FPEXC32_EL2[4]]; + value_name[6..5] := _FPEXC32_EL2[6 .. 5]; + value_name[7..7] := [_FPEXC32_EL2[7]]; + value_name[20..11] := _FPEXC32_EL2[20 .. 11]; + value_name[26..26] := [_FPEXC32_EL2[26]]; + value_name[29..29] := [_FPEXC32_EL2[29]]; + value_name[30..30] := [_FPEXC32_EL2[30]]; + value_name + } + +val vector<32 - 1, 32, dec, bit> -> unit effect {rreg, wreg} set_FPEXC + +function set_FPEXC val_name = + { + (vector<32 - 1, 32, dec, bit> ) r := val_name; + (vector<32 - 1, 32, dec, bit> ) __tmp_45 := get_FPEXC32_EL2(); + __tmp_45[31..0] := r; + set_FPEXC32_EL2(__tmp_45) + } diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail new file mode 100644 index 00000000..95ba97db --- /dev/null +++ b/test/typecheck/pass/procstate1.sail @@ -0,0 +1,16 @@ +default Order dec + +typedef ProcState = const struct forall Num 'n. +{ + bit['n] N; + bit[1] Z; + bit[1] C; + bit[1] V +} + +register ProcState<1> PSTATE + +function unit test () = +{ + PSTATE.N := 0b1 +} |
