verified-network-toolchain / petr4

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

casting of enums #369

Closed pataei closed 1 year ago

pataei commented 1 year ago

Petr4 does the following while deciding if it can cast between two enums or between an enum and its underlying type:

cast_ok ?(explicit = false) env original_type new_type =
  let original_type = saturate_type env original_type in
  let new_type = saturate_type env new_type in
  let open Typed.Type in
  match original_type, new_type with
  | Enum { name; typ = Some t; members }, Enum {typ = Some t'; _}
  | Enum { name; typ = Some t; members }, t'
  | t', Enum { name; typ = Some t; members } ->
     type_equality env [] t t'

This allows the implicit casting of two enums and the implicit casting of an underlying type to an enum. However, P4 considers both of these illegal.

jnfoster commented 1 year ago

For the three cases in this code.

Enum { name; typ = Some t; members }, Enum {typ = Some t'; _}

and

t', Enum { name; typ = Some t; members }

should only be allowed when explicit is true.

pataei commented 1 year ago

Quick fix: fix enum -> enum and t -> enum in Petr4 implementation. @pataei