bitstring access typing

[pataei]

Consider the slice expression exp [L : R].

• Petr4 allows L or R to be varbit, however, P4 spec doesn't.
• Petr4 removes the enum if the index has an enum type, however, P4 spec inserts an implicit cast (even though it states that L and R can be enums, it still inserts implicit cast in the following example). For example, x[E.a:0] becomes x[(bit<8>)E.a:0] (taken from P4 spec implicit cast section), where:

enum bit<8> E {
   a = 5
}

bit<8>  x;

Petr4 code

is_numeric (typ: Typed.Type.t) : bool =
  match typ with
  | Int _
  | Bit _
  | VarBit _
  | Integer -> true
  | _ -> false

and 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)]

P4 spec (v1.2.3)

operations on unsigned fixed-length integers

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.

operations on signed fixed-length integers

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 must be true. 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 an unsigned 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 values that are known at compile time so that the width of the result 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 of e to the bit-pattern represented by x, and leaves all other bits of e unchanged. A slice of a signed integer is treated as an unsigned integer.

How to fix

• change the assertion is_numeric to a helper that only allows the types mentioned by P4 spec.
• instead of saturating the type of indexes, insert casts if needed.

[jnfoster]

Excellent writeup!

[hackedy]

I think all of this applies to indices in array lookups as well