BitString Access Typing Limitation

[pataei]

@hackedy Petr4 forces the context of type checking low and high expressions in bitstring access exp[low:high] to be Constant. Why?

Furthermore, it doesn't allow low and/or high to be serializable enums with an underlying type of bit<w> or int<w>. However, P4 allows this.

Petr4 Code

It can be found in checker.ml:

type_bit_string_access env ctx bits lo hi : Prog.Expression.t =
  let bits_typed = type_expression env ctx bits in
  match reduce_type env bits_typed.typ with
  | Int { width }
  | Bit { width } ->
     let lo_typed = type_expression env Constant lo in
     let typ_lo = saturate_type env lo_typed.typ in
     let hi_typed = type_expression env Constant hi in
     let typ_hi = saturate_type env hi_typed.typ in
     assert (is_numeric typ_lo);
     assert (is_numeric typ_hi);
     let val_lo = compile_time_eval_bigint env lo_typed in
     let val_hi = compile_time_eval_bigint env hi_typed in
     let big_width = Bigint.of_int width in
     (* Bounds checking *)
     assert (Bigint.(<=) Bigint.zero val_lo);
     assert (Bigint.(<) val_lo big_width);
     assert (Bigint.(<=) val_lo val_hi);
     assert (Bigint.(<) val_hi big_width);
     let diff = Bigint.(-) val_hi val_lo |> Bigint.to_int_exn |> (+) 1 in
     { expr = BitStringAccess { bits = bits_typed;
                                lo = val_lo;
                                hi = val_hi;
                                tags = Info.dummy };
       typ = Bit { width = diff };
       dir = bits_typed.dir;
       tags = Info.dummy}
  | typ ->
     raise_s [%message "expected bit type, got"
                 ~expr:(bits: Types.Expression.t)
                 ~typ:(typ: Typed.Type.t)]

Text from P4 spec version 1.2.3:

Extraction of a set of contiguous bits, also known as a slice, denoted by [L:R], where L and R must be expressions that evaluate to non-negative compile-time known values, and L >= R. The types of L and R (which do not need to be identical) must be one of the following:

• int - an infinite-precision integer (section 7.1.6.5)
• bit - a W-bit unsigned integer where W >= 0 (section 7.1.6.2)
• int - a W-bit signed integer where W >= 1 (section 7.1.6.3)
• a serializable enum with an underlying type that is bit or int (section 7.2.1).

The result is a bit-string of width L - R + 1, including the bits numbered from R (which becomes the least significant bit of the result) to L (the most significant bit of the result) from the source operand. The conditions 0 <= R <= L < W are checked statically (where W is the length of the source bit-string). Note that both endpoints of the extraction are inclusive. The bounds are required to be known-at-compile-time values so that the result width can be computed at compile time. Slices are also l-values, which means that P4 supports assigning to a slice: e[L:R] = x . The effect of this statement is to set bits L through R (inclusive of both) of e to the bit-pattern represented by x, and leaves all other bits of e unchanged. A slice of an unsigned integer is an unsigned integer.

[hackedy]

So the

     assert (is_numeric typ_lo);
     assert (is_numeric typ_hi);

lines will disallow serializable enums, but we want to allow them.