summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/cheri_prelude_common.sail63
-rw-r--r--mips/mips_insts.sail24
-rw-r--r--mips/mips_prelude.sail1
-rw-r--r--mips/mips_wrappers.sail4
4 files changed, 60 insertions, 32 deletions
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index d2b69de8..764a4ff1 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -374,29 +374,60 @@ function MEMw_conditional_wrapper(addr, size, data) =
success;
}
-val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
-function addrWrapper(addr, accessType, width) =
+val checkDDCPerms : (CapStruct, MemAccessType) -> unit effect {escape, rreg, wreg}
+function checkDDCPerms(ddc : CapStruct, accessType: MemAccessType) =
{
- capno = 0b00000;
- cap = readCapRegDDC(capno);
- if (not (cap.tag)) then
- (raise_c2_exception(CapEx_TagViolation, capno))
- else if (cap.sealed) then
- (raise_c2_exception(CapEx_SealViolation, capno));
+ if (not (ddc.tag)) then
+ raise_c2_exception(CapEx_TagViolation, 0b00000)
+ else if (ddc.sealed) then
+ raise_c2_exception(CapEx_SealViolation, 0b00000);
match accessType {
- Instruction => if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)),
- LoadData => if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)),
- StoreData => if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno))
+ Instruction => assert(false), /* Only data accesses use DDC */
+ LoadData => if (~(ddc.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, 0b00000)),
+ StoreData => if (~(ddc.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, 0b00000))
};
- cursor = getCapCursor(cap);
+ }
+
+val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
+function addrWrapper(addr, accessType, width) =
+ {
+ ddc = capRegToCapStruct(DDC);
+ checkDDCPerms(ddc, accessType);
+ cursor = getCapCursor(ddc);
vAddr = (cursor + unsigned(addr)) % pow2(64);
size = wordWidthBytes(width);
- base = getCapBase(cap);
- top = getCapTop(cap);
+ base = getCapBase(ddc);
+ top = getCapTop(ddc);
if ((vAddr + size) > top) then
- (raise_c2_exception(CapEx_LengthViolation, capno))
+ (raise_c2_exception(CapEx_LengthViolation, 0b00000))
else if (vAddr < base) then
- (raise_c2_exception(CapEx_LengthViolation, capno))
+ (raise_c2_exception(CapEx_LengthViolation, 0b00000))
+ else
+ to_bits(64, vAddr);
+ }
+
+val addrWrapperUnaligned : (bits(64), MemAccessType, WordTypeUnaligned) -> bits(64) effect {rreg, wreg, escape}
+function addrWrapperUnaligned(addr, accessType, width) =
+ {
+ ddc = capRegToCapStruct(DDC);
+ checkDDCPerms(ddc, accessType);
+ cursor = getCapCursor(ddc);
+ vAddr = (cursor + unsigned(addr)) % pow2(64);
+ woffset = vAddr % 4;
+ doffset = vAddr % 8;
+ /* Compute the address and size of the bytes touched -- this depends on alignment. */
+ let (waddr, size) : (int, int) = match width {
+ WL => (vAddr, 4 - woffset),
+ WR => (vAddr - woffset, woffset + 1),
+ DL => (vAddr, 8 - doffset),
+ DR => (vAddr - doffset, doffset + 1)
+ };
+ base = getCapBase(ddc);
+ top = getCapTop(ddc);
+ if ((waddr + size) > top) then
+ (raise_c2_exception(CapEx_LengthViolation, 0b00000))
+ else if (waddr < base) then
+ (raise_c2_exception(CapEx_LengthViolation, 0b00000))
else
to_bits(64, vAddr);
}
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 2f6b0153..84136e66 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1210,8 +1210,7 @@ function clause decode(0b100010 @ base : regno @ rt : regno @ offset : imm16) =
Some(LWL(base, rt, offset))
function clause execute(LWL(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, W);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WL);
let pAddr = (TLBTranslate(vAddr, LoadData)) in
{
mem_val = MEMr_wrapper (pAddr[63..2] @ 0b00, 4); /* read word of interest */
@@ -1231,8 +1230,7 @@ function clause decode(0b100110 @ base : regno @ rt : regno @ offset : imm16) =
Some(LWR(base, rt, offset))
function clause execute(LWR(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, W);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, WR);
let pAddr = (TLBTranslate(vAddr, LoadData)) in
{
mem_val = MEMr_wrapper(pAddr[63..2] @ 0b00, 4); /* read word of interest */
@@ -1254,8 +1252,7 @@ function clause decode(0b101010 @ base : regno @ rt : regno @ offset : imm16) =
Some(SWL(base, rt, offset))
function clause execute(SWL(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, W);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WL);
let pAddr = TLBTranslate(vAddr, StoreData) in
{
reg_val = rGPR(rt);
@@ -1274,8 +1271,7 @@ function clause decode(0b101110 @ base : regno @ rt : regno @ offset : imm16) =
Some(SWR(base, rt, offset))
function clause execute(SWR(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, W);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, WR);
let pAddr = TLBTranslate(vAddr, StoreData) in
{
wordAddr = pAddr[63..2] @ 0b00;
@@ -1296,8 +1292,7 @@ function clause decode(0b011010 @ base : regno @ rt : regno @ offset : imm16) =
Some(LDL(base, rt, offset))
function clause execute(LDL(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, D);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DL);
let pAddr = TLBTranslate(vAddr, LoadData) in
{
mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */
@@ -1322,8 +1317,7 @@ function clause decode(0b011011 @ base : regno @ rt : regno @ offset : imm16) =
Some(LDR(base, rt, offset))
function clause execute(LDR(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), LoadData, D);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), LoadData, DR);
let pAddr = TLBTranslate(vAddr, LoadData) in
{
mem_val = MEMr_wrapper(pAddr[63..3] @ 0b000, 8); /* read double of interest */
@@ -1348,8 +1342,7 @@ function clause decode(0b101100 @ base : regno @ rt : regno @ offset : imm16) =
Some(SDL(base, rt, offset))
function clause execute(SDL(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, D);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DL);
let pAddr = TLBTranslate(vAddr, StoreData) in
{
reg_val = rGPR(rt);
@@ -1374,8 +1367,7 @@ function clause decode(0b101101 @ base : regno @ rt : regno @ offset : imm16) =
Some(SDR(base, rt, offset))
function clause execute(SDR(base, rt, offset)) =
{
- /* XXX length check not quite right, but conservative */
- vAddr = addrWrapper(sign_extend(offset) + rGPR(base), StoreData, D);
+ vAddr = addrWrapperUnaligned(sign_extend(offset) + rGPR(base), StoreData, DR);
let pAddr = TLBTranslate(vAddr, StoreData) in
{
reg_val = rGPR(rt);
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index fbbe74ee..76a05791 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -565,6 +565,7 @@ function compare (cmp, valA, valB) =
LTU => valA <_u valB
}
enum WordType = { B, H, W, D}
+enum WordTypeUnaligned = { WL, WR, DL, DR }
val wordWidthBytes : WordType -> range(1, 8)
function wordWidthBytes(w) =
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 0cc098a5..43e759b9 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -60,6 +60,10 @@ val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64)
function addrWrapper(addr, accessType, width) =
addr
+val addrWrapperUnaligned : (bits(64), MemAccessType, WordTypeUnaligned) -> bits(64)
+function addrWrapperUnaligned(addr, accessType, width) =
+ addr
+
$ifdef _MIPS_TLB_STUB
val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape}
$else
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:37:54 +0000