Capability to integer casts on CheriBSD

[Richard Kettlewell]

On 30/10/2023 21:10, Julien ÉLIE wrote:
> Hi Richard,
> 
>> The idea of the code in question seems to be to convert region 
>> expressed by a pointer and length into the slightly wider region 
>> containing it consisting of whole pages.
> 
> Yes, indeed.
> And your proposal even optimizes the initial code which always takes an 
> extra pagesize.
> 
> 
>> An alternative approach that does not synthesize any pointers (but 
>> still relies on a pointer-to-integer conversion):
>>
>>    size_t page_mask = pagesize - 1;
>>
>>    // Offset of p from start of first page
>>    size_t start_offset = (size_t)p & page_mask;
>>
>>    // Start of first page
>>    char *start = p - start_offset;
>>
>>    // Offset of (p+length) from start of last page, or 0
>>    // if (p+length) is exactly on a page boundary
>>    size_t end_offset = (start_offset + length) & page_mask;
>>
>>    // Offset _backwards_ of (p+length) from end of last page
>>    if(end_offset > 0)
>>      end_offset = page_mask - end_offset;
> 
> I see the idea, thanks.
> As for pointer-to-integer conversion, maybe casting to (uintptr_t) could 
> be of help?  I've googled a bit and found out that it is in the C99 
> standard
All the sizes are bounded by the size of whatever the containing memory 
mapping is, which has to fit in a size_t since that's what the argument 
to mmap() was when the mapping was created.

So I don't think uintptr_t will make much difference.

> Maybe we could check for its being available via Autoconf 
> (AC_TYPE_UINTPTR_T macro) and use (uintptr_t) instead of (size_t) if 
> that's the case?
> 
> 
>>    // Total length of pages
>>    size_t total_length = start_offset + length + end_offset;
> 
> I'm unsure total_length always has the right value.  If end_offset is 0, 
> total_length should be pagesize I think.

Are you sure?

As a concrete example, suppose:
   pagesize = 4096
   p is at the start of a page
   length = 8192
Then:
   start_offset = 0
   start = p
   end_offset = (0+8192)&4095 = 0
   total_length = 0+8192+0 = 8192
which is surely what we want.

ttfn/rjk