search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
462 stars 168 forks source link

Improve `to_bits` type checking #614

Open Timmmm opened 1 week ago

Timmmm commented 1 week ago

Currently to_bits just silently accepts larger integers than will fit in the bitvector and slices off the top. That's a bit sad from a type checking point of view. Sail can perfectly happily check this at compile time:

val to_bits : forall 'l 'x, 'l >= 0 & 0 <= 'x < 2 ^ 'l . (int('l), int('x)) -> bits('l)
function to_bits (l, n) = get_slice_int(l, n, 0)

I think we should change the definition to that. There are some places where the slicing is intentional (e.g. the bit rotate functions), where we can probably introduce an explicit function:

val to_bits_truncate : forall 'l, 'l >= 0 . (int('l), int) -> bits('l)
function to_bits_truncate (l, n) = get_slice_int(l, n, 0)

And there are a lot of places where it probably isn't intentional, where we could add

val to_bits_unsafe : forall 'l, 'l >= 0 . (int('l), int) -> bits('l)
function to_bits_unsafe (l, n) = get_slice_int(l, n, 0)

with TODOs to add the appropriate assertions & types. A lot of them are in the vector extension which has very loose typing so it will take a while to fix them there.

jordancarlin commented 1 week ago

Seems like a great type safety improvement that makes a lot of sense.On Nov 11, 2024, at 8:54 AM, Tim Hutt @.***> wrote: Currently to_bits just silently accepts larger integers than will fit in the bitvector and slices off the top. That's a bit sad from a type checking point of view. Sail can perfectly happily check this at compile time: val to_bits : forall 'l 'x, 'l >= 0 & 0 <= 'x < 2 ^ 'l . (int('l), int('x)) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0)

I think we should change the definition to that. There are some places where the slicing is intentional (e.g. the bit rotate functions), where we can probably introduce an explicit function: val to_bits_truncate : forall 'l, 'l >= 0 . (int('l), int) -> bits('l) function to_bits_truncate (l, n) = get_slice_int(l, n, 0)

And there are a lot of places where it probably isn't intentional, where we could add val to_bits_unsafe : forall 'l, 'l >= 0 . (int('l), int) -> bits('l) function to_bits_unsafe (l, n) = get_slice_int(l, n, 0)

with TODOs to add the appropriate assertions & types. A lot of them are in the vector extension which has very loose typing so it will take a while to fix them there.

—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: @.***>