add support for experimental CHasSpace instruction

[brettferdosi]

No description provided.

[jrtc27]

Suggested change

	function clause execute (CHasSpace (rd, cb, rs)) =
	function clause execute (CHasSpace(rd, cb, rs)) =

[jrtc27]

This might be nicer using n+1-bit arithmetic for the top check. Something like:

Suggested change

	if ((cb_cursor + rs_val) <= cb_top) &
	(cb_cursor < cb_top) &
	(cb_cursor >= cb_base) then
	let req_top : CapLenBits = zero_extend(cb_cursor) + zero_extend(rs_val);
	if (cb_cursor >= cb_base) & (req_top <= cb_top) then

[rmn30]

Note that cb_cursor is an int so you can't use zero_extend on it (you could use cb.address but you need the base and top as bits to compare with). The cheri-mips spec as whole uses ints rather than bits because that's what the original pseudocode did but cheri-riscv has moved to bits in some places. The advantage of ints when bounds checking is you don't have to worry about overflow (ints are unbounded in sail) but obviously hardware has to use a fixed width.

On cheri-riscv I factored the bounds check into a inCapBounds function which might be nicer.

[brettferdosi]

Thanks. I'll refactor into an inCapBounds function and use unbounded integers to be in line with the rest of cheri-mips. Please let me know whether the types etc. look OK.

I noticed that the cheri-riscv inCapBounds doesn't check that cursor < top, so that an invocation of inCapBounds with addr == top and size == 0 will return true even though the address isn't in bounds for the capability. Was this done intentionally? I was thinking that it would make more sense for CHasSpace to return false in that case, so I have implemented the mips inCapBounds accordingly.

[rmn30]

That is a good point. I'm just wondering whether there is a bug in CSetBounds (and others) on cheri-riscv because of it.

[jrtc27]

The behaviour of allowing that seems perfectly natural to me, and special-casing it would be strange. There's nothing wrong architecturally with a [top, top) capability. Microarchitecturally, adding that extra check would just make the (already expensive) bounds check longer. From a software perspective, this allows you to take any valid C pointer and CSetBounds it with length <= remaining_length, which includes one-past-the-end pointers. Purely abstractly, the [top, top) capabilities are a subset of [bot, top), and other than precision issues, we should be able to get any subset of [bot, top), even the trivial ones.

[brettferdosi]

To summarize the discussion from yesterday, I believe we decided that it is fine in general for instructions to allow for the creation of capabilities of zero length and base equal to the parent capability's top. The functionality of CHasSpace should be similar and return true if the given address is equal to the given capability's top and the size is 0. However, checking whether a cursor is in bounds should return false when the cursor is equal to top.

In line with this, I have modified the helper function for sail-mips to have the same checks as the sail-riscv inCapBounds function. But I have named it capHasSpace to make the difference between this check and the in-bounds check more clear.

CInBounds for a capability can be implemented as CHasSpace with the capability's cursor and a size of 1.

[jrtc27]

Suggested change

	wGPR(rd) = zero_extend(to_bits(1,1))
	wGPR(rd) = zero_extend(0b1)

And maybe do something like either CTestSubset or CGetType/CToPtr to avoid multiple wGPR(rd) = statements.