verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

array access for tuples is missing #384

Open pataei opened 1 year ago

pataei commented 1 year ago

Petr4 doesn't support array access for tuples. It only supports array access for expressions that have the type array using Petr4's type system while P4 specifies that elements of a tuple can also be accessed by array indexing.

Petr4 code

The only type checking for array access expressions is done by the following function. Note that both the type of an input expression to this function (which is types.type.t) and the type of an output expression (which is typed.type.t) can be either tuple or headerstack. However, only the latter one can be an array.

Also, note that when initializing a tuple, petr4 assigns it the tuple type (see function type_assignment). But then, the elements of the tuple cannot be accessed because such expression will never type check.

type_array_access env ctx (array: Types.Expression.t) index : Prog.Expression.t =
  let array_typed = type_expression env ctx array in
  let array_typ = array_typed.typ in
  let idx_typed = type_expression env ctx index in
  let element_typ = (assert_array (Types.Expression.tags array) array_typ).typ in
  assert_numeric (Types.Expression.tags index) idx_typed.typ |> ignore;
  { expr = ArrayAccess { array = array_typed; index = idx_typed; tags=Types.Expression.tags array };
    typ = element_typ;
    dir = array_typed.dir;
    tags = Types.Expression.tags array}

let assert_array = make_assert "array"
  begin function
  | Array array_typ -> Some array_typ
  | _ -> None
  end

type_assignment env ctx lhs rhs =
  let open Expression in 
  let open Prog.Statement in
  let expr_ctx = ExprContext.of_stmt_context ctx in
  let lhs_typed = type_expression env expr_ctx lhs in
  if not @@ is_lvalue env lhs_typed
  then raise_s [%message "Must be an lvalue"
                   ~lhs:(lhs:Types.Expression.t)]
  else
    let rhs_typed = cast_expression env expr_ctx lhs_typed.typ rhs in
    ignore (assert_same_type env (tags lhs) (tags rhs)
              lhs_typed.typ rhs_typed.typ);
    { stmt = Assignment { lhs = lhs_typed; rhs = rhs_typed; tags = Info.merge (tags lhs) (tags rhs) };
      typ = StmType.Unit },
    env

P4 spec (v1.2.3)

Example of initializing a tuple: tuple<bit<32>, bool> x = { 10, false };

The fields of a tuple can be accessed using array index syntax x[0], x[1]. The array indexes must be compile-time constants, to enable the type-checker to identify the field types statically.