review the uses of mpz_get_ui in sail.c

[cfbolz]

After the specific problem in #300 I thought I'd make an issue to keep track of the general problem. sail.c uses mpz_get_ui in a whole bunch of places, but that GMP function will silently drop the sign of the argument. A few of the use cases of the function in sail.c are therefore potentially risky.

In my opinion all of them should be replaced with a sail-specific helper function that at least contains an assert that the argument is not negative (and not larger than an unsigned int either), to defend against bugs in other parts of the system. I think most of the problems in theory can't occur because the type system says that the involved integers can't be negative, but still.

I didn't do an in-depth review, but here are some of the calls that look potentially wrong to me:

mach_int CREATE_OF(mach_int, sail_int)(const sail_int op)
{
  return mpz_get_ui(op);
}

mach_int is signed, so that conversion looks quite wrong.

A whole bunch of functions where mpz_get_ui is used for shift amounts, bit widths, and indexes:

• shr_int
• shl_int
• pow_int
• pow2
• zeros
• zero_extend
• sign_extend
• vector_subrange_lbits
• sail_truncate
• sail_truncateLSB
• bitvector_access
• replicate_bits
• get_slice_int
• set_slice_int
• update_lbits
• vector_update_subrange_lbits
• slice
• set_slice
• shift_bits_left
• shift_bits_right
• shift_bits_right_arith
• arith_shiftr
• shiftl
• shiftr
• reverse_endianness

Does the general approach of switching to a helper function with an assert make sense? If yes, I might try to find some time to write a PR to do that.

[Alasdair]

For indices and suchlike I think we should be safe because they should be checked to be non negative, unless we weren't strict enough with the types which may be the case for primitives copied from ASL

We haven't generated any calls to CREATE_OF macros since about 2018, so it's probably time to remove them from that C file.

[cfbolz]

"we should be safe" – the "should" makes me a bit wary in that statement :wink: . Particularly given that #300 was really a case where having such an assert even for index manipulation would have caught a real bug much earlier.

So an equivalent way to address this issue is to review the uses of mpz_get_ui and check that the corresponding declarations have strict enough types. This is eg not the case for shiftl, shiftr and arith_shiftr:

val sail_shiftleft = pure "shiftl" : forall 'n ('ord : Order).
    (bitvector('n, 'ord), int) -> bitvector('n, 'ord)

val sail_shiftright = pure "shiftr" : forall 'n ('ord : Order).
    (bitvector('n, 'ord), int) -> bitvector('n, 'ord)

val sail_arith_shiftright = pure "arith_shiftr" : forall 'n ('ord : Order).
    (bitvector('n, 'ord), int) -> bitvector('n, 'ord)