Missing cast in left operand of right shift

[s-zanella]

The following program outputs z = 255 despite assert (z == 1uy) being provable in F*:

module M

open FStar.HyperStack.All
open FStar.UInt8

val discard: bool -> St unit
let discard _ = ()

let print s = discard (IO.debug_print_string s)

val main: unit -> St C.exit_code
let main _ =
  let z = (0uy -%^ 1uy) >>^ 7ul in
  assert (z == 1uy);
  print (Printf.sprintf "z = %uy\n" z);
  C.EXIT_SUCCESS

(compiled with krml -no-prefix M -add-include '"extracted/FStar_String.h"' -drop WasmSupport M.fst -o M.exe.)

The generated C code uses
uint8_t z = (uint8_t)0U - (uint8_t)1U >> (uint32_t)7U;
while I think it should use
uint8_t z = (uint8_t)((uint8_t)0U - (uint8_t)1U) >> (uint32_t)7U;

Note also that the C11 standard says that the semantics of a right shift with a negative left operand is implementation-defined:

The result of E1 >> E2 is E1 right-shifted E2 bit positions. If E1 has an unsigned type or if E1 has a signed type and a nonnegative value, the value of the result is the integral part of the quotient of E1/2^E2. If E1 has a signed type and a negative value, the resulting value is implementation-defined.

[s-zanella]

Also in the case of left shifts, the left operand in the generated C code may be negative, which is undefined behavior in C11.

[msprotz]

I think the relative precedence of - and >> is counter-intuitive, but the printing is correct (https://en.cppreference.com/w/c/language/operator_precedence). I don't think the parentheses you suggest would change anything.

My understanding of this is that shifting when E1 is negative is implementation-defined, and we just shouldn't expose it, period. Is it time to change the signature of the >>^ operators?

[msprotz]

Oh ok got it. You're talking about the implicit integer promotion that happens for uint8_t because it is smaller than it.