summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/cheri_prelude.sail6
-rw-r--r--mips/mips_insts.sail40
-rw-r--r--mips/mips_prelude.sail27
-rw-r--r--mips/mips_wrappers.sail4
-rw-r--r--src/lem_interp/run_with_elf.ml17
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml17
6 files changed, 91 insertions, 20 deletions
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 4ab99fdc..0cb2a1f3 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -407,7 +407,9 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
vAddr64;
}
-function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) =
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
+ incrementCP0Count();
+ (* XXX Sail does not allow reading fields here :-( *)
let (bit[257]) x = PCC in
let (bit[64]) base = x[127..64] in
let (bit[64]) length = x[63..0] in
@@ -418,6 +420,7 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType
exit (raise_c2_exception_noreg(CapEx_LengthViolation)) (* XXX take exception properly *)
else
TLBTranslate(absPC, accessType)
+}
function unit checkCP2usable () =
{
@@ -427,3 +430,4 @@ function unit checkCP2usable () =
exit (SignalException(CpU));
}
}
+
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 722e3d00..d8a45730 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1286,8 +1286,8 @@ function clause execute(SDR(base, rt, offset)) =
union ast member regregimm16 CACHE
function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) =
Some(CACHE(base, op, imm))
-function clause execute (CACHE(base, op, imm)) =
- () (* XXX NOP *)
+function clause execute (CACHE(base, op, imm)) =
+ checkCP0Access () (* pretty much a NOP because no caches *)
(* PREF - prefetching into (non-existent) caches *)
@@ -1317,7 +1317,8 @@ function clause decode (0b010000 : 0b00000 : (regno) rt : (regno) rd : 0b0000000
Some(MFC0(rt, rd, sel, false)) (* MFC0 *)
function clause decode (0b010000 : 0b00001 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) =
Some(MFC0(rt, rd, sel, true)) (* DMFC0 *)
-function clause execute (MFC0(rt, rd, sel, double)) =
+function clause execute (MFC0(rt, rd, sel, double)) = {
+ checkCP0Access();
let (bit[64]) result = switch (rd, sel)
{
case (0b00000,0b000) -> 0 (* 0, TLB Index *)
@@ -1327,10 +1328,10 @@ function clause execute (MFC0(rt, rd, sel, double)) =
case (0b00100,0b000) -> 0 (* 4, TLB Context *)
case (0b00101,0b000) -> 0 (* 5, TLB PageMask *)
case (0b00110,0b000) -> 0 (* 6, TLB Wired *)
- case (0b00111,0b000) -> 0 (* 6, HWREna *)
+ case (0b00111,0b000) -> EXTZ(CP0HWREna) (* 6, HWREna *)
case (0b01000,0b000) -> CP0BadVAddr (* 8, BadVAddr reg *)
case (0b01000,0b001) -> 0 (* 8, BadInstr reg XXX TODO *)
- case (0b01001,0b000) -> 0 (* 9, Count reg XXX TODO *)
+ case (0b01001,0b000) -> EXTZ(CP0Count) (* 9, Count reg *)
case (0b01010,0b000) -> 0 (* 10, TLB EntryHi *)
case (0b01011,0b000) -> EXTZ(CP0Compare) (* 11, Compare reg *)
case (0b01100,0b000) -> EXTZ(CP0Status) (* 12, Status reg *)
@@ -1356,20 +1357,24 @@ function clause execute (MFC0(rt, rd, sel, double)) =
case _ -> {exit (SignalException(ResI)); 0}
} in
wGPR(rt) := if (double) then result else EXTS(result[31..0])
-
+}
union ast member (regno, regno, bit[3], bool) MTC0
function clause decode (0b010000 : 0b00100 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) =
Some(MTC0(rt, rd, sel, false)) (* MTC0 *)
function clause decode (0b010000 : 0b00101 : (regno) rt : (regno) rd : 0b00000000 : (bit[3]) sel) =
Some(MTC0(rt, rd, sel, true)) (* DMTC0 *)
-function clause execute (MTC0(rt, rd, sel, double)) =
+function clause execute (MTC0(rt, rd, sel, double)) = {
+ checkCP0Access();
let reg_val = (rGPR(rt)) in
switch (rd, sel)
{
+ case (0b00100,0b010) -> CP0UserLocal := reg_val
+ case (0b00111,0b000) -> CP0HWREna := (reg_val[31..30] : 0b00000000000000000000000000 : reg_val[4..0])
+ case (0b01001,0b000) -> CP0Count := reg_val[31..0]
case (0b01011,0b000) -> { (* 11, sel 0: Compare reg *)
CP0Compare := reg_val[31..0];
- (CP0Cause.IP)[8] := 0
+ (CP0Cause.IP)[15] := 0
}
case (0b01100,0b000) -> { (* 12 Status *)
(CP0Status.CU) := reg_val[31..28];
@@ -1391,12 +1396,31 @@ function clause execute (MTC0(rt, rd, sel, double)) =
case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *)
case _ -> exit (SignalException(ResI))
}
+}
+
+union ast member (regno, regno) RDHWR
+function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 : 0b111011) = Some(RDHWR(rt, rd))
+function clause execute (RDHWR(rt, rd)) = {
+ let accessLevel = getAccessLevel() in
+ if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then
+ exit (SignalException(ResI));
+ let (bit[64]) temp = switch (rd) {
+ case 0b00000 -> EXTZ([bitzero]) (* CPUNum *)
+ case 0b00001 -> EXTZ([bitzero]) (* SYNCI_step *)
+ case 0b00010 -> EXTZ(CP0Count) (* Count *)
+ case 0b00011 -> EXTZ([bitone]) (* Count resolution *)
+ case 0b11101 -> CP0UserLocal (* User local register *)
+ case _ -> exit (SignalException(ResI))
+ } in
+ wGPR(rt) := temp;
+}
union ast member unit ERET
function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) =
Some(ERET)
function clause execute (ERET) =
{
+ checkCP0Access();
ERETHook();
CP0LLBit := 0b0;
if (CP0Status.ERL == bitone) then
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index a8d3f8d5..28afb156 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -30,6 +30,10 @@ register (bit[64]) CP0ErrorEPC
register (bit[1]) CP0LLBit
register (bit[64]) CP0LLAddr
register (bit[64]) CP0BadVAddr
+register (bit[32]) CP0Count
+register (bit[32]) CP0Compare
+register (bit[32]) CP0HWREna
+register (bit[64]) CP0UserLocal
typedef StatusReg = register bits [31:0] {
31 .. 28 : CU; (* co-processor enable bits *)
@@ -208,6 +212,29 @@ function AccessLevel getAccessLevel() =
case _ -> User (* behaviour undefined, assume user *)
}
+function unit checkCP0Access () =
+ {
+ let accessLevel = getAccessLevel() in
+ if ((accessLevel != Kernel) & (~((CP0Status.CU)[0]))) then
+ {
+ (CP0Cause.CE) := 0b00;
+ exit (SignalException(CpU));
+ }
+ }
+
+function unit incrementCP0Count() = {
+ CP0Count := (CP0Count + 1);
+ if (CP0Count == CP0Compare) then {
+ ((CP0Cause.IP)[15]) := bitone;
+ };
+ (* XXX Sail does not allow reading fields here :-( *)
+ let (bit[32])status = CP0Status in
+ let (bit[32])cause = CP0Cause in
+ let (bit[8]) ims = (status[15..8]) in
+ let (bit[8]) ips = (cause[15..8]) in
+ if ((CP0Status.IE) & ((ips & ims) != 0x00)) then
+ exit (SignalException(Int));
+}
function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
{
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 25b8936b..7d9e73e6 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -5,11 +5,13 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
addr
-function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) =
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
+ incrementCP0Count();
if (vAddr[1..0] != 0b00) then (* bad PC alignment *)
exit (SignalExceptionBadAddr(AdEL, vAddr))
else
TLBTranslate(vAddr, accessType)
+}
function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex)
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 0f8e86ad..7872a5b5 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -491,11 +491,15 @@ let mips_register_data_all = [
("HI", (D_decreasing, 64, 63));
("LO", (D_decreasing, 64, 63));
(* control registers *)
- ("CP0Status", (D_decreasing, 32, 31));
- ("CP0Cause", (D_decreasing, 32, 31));
- ("CP0EPC", (D_decreasing, 64, 63));
- ("CP0LLAddr", (D_decreasing, 64, 63));
- ("CP0LLBit", (D_decreasing, 1, 0));
+ ("CP0Status", (D_decreasing, 32, 31));
+ ("CP0Cause", (D_decreasing, 32, 31));
+ ("CP0EPC", (D_decreasing, 64, 63));
+ ("CP0LLAddr", (D_decreasing, 64, 63));
+ ("CP0LLBit", (D_decreasing, 1, 0));
+ ("CP0Count", (D_decreasing, 32, 31));
+ ("CP0Compare", (D_decreasing, 32, 31));
+ ("CP0HWREna", (D_decreasing, 32, 31));
+ ("CP0UserLocal", (D_decreasing, 64, 63));
]
let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
@@ -872,6 +876,9 @@ let get_addr_trans_regs _ =
Some([
(Interp_interface.Reg0("PC", 63, 64, Interp_interface.D_decreasing), Reg.find "PC" !reg);
(Interp_interface.Reg0("CP0Status", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Status" !reg);
+ (Interp_interface.Reg0("CP0Cause", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Cause" !reg);
+ (Interp_interface.Reg0("CP0Count", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Count" !reg);
+ (Interp_interface.Reg0("CP0Compare", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Compare" !reg);
(Interp_interface.Reg0("inBranchDelay", 0, 1, Interp_interface.D_decreasing), Reg.find "inBranchDelay" !reg);
])
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index f50720c5..633dda72 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -491,11 +491,15 @@ let mips_register_data_all = [
("HI", (D_decreasing, 64, 63));
("LO", (D_decreasing, 64, 63));
(* control registers *)
- ("CP0Status", (D_decreasing, 32, 31));
- ("CP0Cause", (D_decreasing, 32, 31));
- ("CP0EPC", (D_decreasing, 64, 63));
- ("CP0LLAddr", (D_decreasing, 64, 63));
- ("CP0LLBit", (D_decreasing, 1, 0));
+ ("CP0Status", (D_decreasing, 32, 31));
+ ("CP0Cause", (D_decreasing, 32, 31));
+ ("CP0EPC", (D_decreasing, 64, 63));
+ ("CP0LLAddr", (D_decreasing, 64, 63));
+ ("CP0LLBit", (D_decreasing, 1, 0));
+ ("CP0Count", (D_decreasing, 32, 31));
+ ("CP0Compare", (D_decreasing, 32, 31));
+ ("CP0HWREna", (D_decreasing, 32, 31));
+ ("CP0UserLocal", (D_decreasing, 64, 63));
]
let cheri_register_data_all = mips_register_data_all @ [
@@ -960,6 +964,9 @@ let get_addr_trans_regs _ =
(Interp_interface.Reg0("PCC", 256, 257, Interp_interface.D_decreasing), Reg.find "PCC" !reg);
(Interp_interface.Reg0("C29", 256, 257, Interp_interface.D_decreasing), Reg.find "C29" !reg);
(Interp_interface.Reg0("CP0Status", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Status" !reg);
+ (Interp_interface.Reg0("CP0Cause", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Cause" !reg);
+ (Interp_interface.Reg0("CP0Count", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Count" !reg);
+ (Interp_interface.Reg0("CP0Compare", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Compare" !reg);
(Interp_interface.Reg0("inBranchDelay", 0, 1, Interp_interface.D_decreasing), Reg.find "inBranchDelay" !reg);
])
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:27:38 +0000