out of range top detection

[tariqkurd-repo]

cases where the top is greater than the infinite top are hard to detect without expanding the bounds
they are in the same category as malformed bounds, i.e. can not be created by correct hardware

#521

The PR has a suggestion of how to detect them and clear the tag in hardware

[tariqkurd-repo]

we've discussed this locally - we think the main issue is to prevent cases where the top overflows from allowing accesses to wrap the address space and allow access to byte 0, which the SAIL curently does, even though byte 0 is out of bounds

[PeterRugg]

we think the main issue is to prevent cases where the top overflows from allowing accesses to wrap the address space and allow access to byte 0, which the SAIL curently does, even though byte 0 is out of bounds

I'm not sure if I'm reading that right: the SAIL currently allows the access, or doesn't allow it? I would have thought it would not allow it. Broadly, the way I thought of it currently is that addresses wrap but bounds don't.

[tomaird]

@PeterRugg - If you have a cap with top bounds greater than "max top" (2^mxlen) and base bound non-zero (so it's not classified as infinite bounds), and you use it to authorise a memory access that wraps over the top of the address space, the Sail inCapBounds() function currently allows this access. Obviously this kind of cap can never be generated by a correctly operating core, but is possible if say there is a memory error and you load this kind of capability from memory.

Current Sail function:

function inCapBounds(cap : Capability, addr : CapAddrBits, size : CapLenInt) -> bool = {
  let a = unsigned(addr);
  match getCapBounds(cap) {
    None() => false,
    Some(base, top) => ((a >= base) & ((a + size) <= top)) | decodedBoundsInfinite(base, top)
  }
}

This was modified to the following, which solved the issue:

function inCapBounds(cap : Capability, addr : CapAddrBits, size : CapLenInt) -> bool = {
  let a = unsigned(addr);
  let max_top = 2 ^ xlen;
  match getCapBounds(cap) {
    None() => false,
    Some(base, top) => ((a >= base) & ((a + size) <= min(top,max_top))) | decodedBoundsInfinite(base, top)
  }
}

So for a non-infinite bounds case, the top must be less than the max_top, which enforces the requirement that wrapping accesses are only legal when you have infinite bounds