[DeepTest] UInt8/UInt16 switch scrutinee not masked after wrapping arithmetic

[elefthei]

Bug Description

Category: Wrong control flow (wrong branch taken)

When F* match on UInt8/UInt16 is compiled as a C switch statement, the scrutinee expression retains its widened uint32 value. The switch compares the uint32 value against uint8 case labels, taking the wrong branch when wrapping arithmetic overflows 8 bits.

Expected vs Actual

let via_switch (a b: UInt8.t) : UInt32.t =
  match (a +%^ b) with
  | 0uy -> 10ul
  | 1uy -> 20ul
  | _   -> 30ul

With a=200, b=56: F* computes (200+56) mod 256 = 0, matches 0uy, returns 10.

Generated C:

switch ((uint32_t)a + (uint32_t)b) {  // 256, not 0!
  case 0U: return 10U;
  case 1U: return 20U;
  default: return 30U;              // takes this branch
}

C returns 30 (WRONG, F* says 10).

Why this is distinct from #694

Bug #694 fixed comparisons (==, <, etc.) by adding them to mk_arith. But the switch scrutinee path is different: try_mk_switch in DataTypes.ml puts the raw expression into ESwitch, bypassing mk_arith entirely. The if-else compilation path (compile_match) is correct because it binds the scrutinee to a uint8_t variable first.

Root Cause

DataTypes.ml try_mk_switch extracts the scrutinee expression without masking. AstToCStar.ml defers masking for Add/Sub/Mul (relying on the consumer to truncate), but switch is not a truncating consumer.

Impact

Any F* match on UInt8/UInt16 that involves wrapping arithmetic in the scrutinee may take the wrong branch in extracted C code.

[elefthei]

krml-707.sh