pataei
commented
1 year ago Some of the castings that Petr4 allows make sense as going through P4 spec. Specifically, P4 uses lists and records on the rhs of assignments for structs, headers, and tuples. This results in requiring an either implicit or explicit cast of list/record types to struct/header/tuple types.
The following recognizes the cast needed using examples and explanation from P4 spec along with todos needed to be applied to P4 spec.
list --> tuple (implicit)
P4 spec states that: "Tuples can be assigned to other tuples with the same type, passed as arguments and returned from functions, and can be initialized with list expressions."
tuple<bit<32>, bool> x = { 10, false };
We don't need such cast in our formalization since lists are actually of type list.
list --> struct/header
[P4 spec]() states that: "List expressions can be assigned to expressions of type tuple, struct or header, and can also be passed as arguments to methods. A list may be used to initialize a structure if the list has the same number of elements as fields in the structure. The effect of such an initializer is to assign the nth element of the list to the nth field in the structure:"
bit<32> a;
bit<32> b;
}
const S x = { 10, 20 }; //a = 10, b = 20It continues: "A list expression can have an explicit structure or header type specified, and then it is converted automatically to a structure-valued expression (see 8.13):"
bit<32> a;
bit<32> b;
}
extern void f<T>(in T data);
f((S){ 10, 20 }); // automatically converted to f((S){a = 10, b = 20});The first example requires an implicit cast of list to struct to be legal while the second one requires the explicit cast of list to struct to be legal.
record --> struct/header
Somehow P4 spec (v1.2.3. section 8.13) fails to categorize '(' typeRef ')' expression as an explicit casting expression. Instead, it puts it as part of structure-valued expressions as follows:
expression ...
| '{' kvList '}'
| '(' typeRef ')' expression
;
kvList
: kvPair
| kvList "," kvPair
;
kvPair
: name "=" expression
;P4 spec states that: "For a structure-valued expression typeRef is the name of a struct or header type. The typeRef can be omitted if it can be inferred from context, e.g., when initializing a variable with a struct type. The following example shows a structure-valued expression used in an equality comparison expression:"
Example 1:
struct S {
bit<32> a;
bit<32> b;
}
S s;
// Compare s with a structure-valued expression
bool b = s == (S) { a = 1, b = 2 };It continues: "Structure-valued expressions can be used in the right-hand side of assignments, in comparisons, in field selection expressions, and as arguments to functions, method or actions. Structure-valued expressions are not left values."
This means that we need to add the following explicit (becuase of example 1) and implicit (because of saying "the typeRef can be omitted if it can be inferred from the context") casts to P4 spec in order to allow the expression '(' typeRef ')' expression to make up the rhs of an assignment:
- record type --> header type
- record type --> struct type
Fix informal P4 spec
I'm not sure why P4 doesn't consider these casts at the moment. It might be how it categorizes its types, however, this can easily be resolved by stating that a cast of the type name to a type is legal if the type assigned to the name can be casted to the other type. Then, include a list of such underlying types casted to other types.
Casts to be added to informal P4 spec:
- [x] list --> header (explicit and implicit)
- [x] list --> struct (explicit and implicit)
- [ ] record --> header (explicit and implicit)
- [ ] record --> struct (explicit and implicit)
Note: As of now, the formalization of these casts checks for a recursive cast (e.g., the rule TupleToHeader-AE-1 below)or the type equality of the elements e.g., the rule TupleToHeader-AE-2 below). As an example, consider the rules for casting a tuple type to a header type:
@jnfoster and @hackedy This note makes sense. However, to the extent that I've read the P4 spec, P4 spec doesn't talk about allowing recursive cast. I want to double-check that 1) such recursion is legal in P4 and 2) we want to keep this recursion in our formalization.
For reference, here's how P4 categorizes its types:
typeRef
: baseType
| typeName
| specializedType
| headerStackType
| tupleType
;
baseType
: BOOL
| ERROR
| MATCH_KIND
| STRING
| INT
| BIT
| BIT '<' INTEGER '>'
| INT '<' INTEGER '>'
| VARBIT '<' INTEGER '>'
| BIT '<' '(' expression ')' '>'
| INT '<' '(' expression ')' '>'
| VARBIT '<' '(' expression ')' '>'
;
typeName
: prefixedType
;
prefixedType
: TYPE_IDENTIFIER
| dotPrefix TYPE_IDENTIFIER
;
tupleType
: TUPLE '<' typeArgumentList '>'
;
headerStackType
: typeName '[' expression ']'
| specializedType '[' expression ']'
;
specializedType
: prefixedType '<' typeArgumentList '>'
;Additionally, it defines type declarations as:
typeDeclaration
: derivedTypeDeclaration
| typedefDeclaration
| parserTypeDeclaration ';'
| controlTypeDeclaration ';'
| packageTypeDeclaration ';'
;
derivedTypeDeclaration
: headerTypeDeclaration
| headerUnionDeclaration
| structTypeDeclaration
| enumDeclaration
;
Petr4 allows the following casts while P4 spec doesn't (however, as the formalization continues some of these make lots of sense to have. Such casts are italicized.):
On the other hand, Petr4 is missing the cast
int --> bool. P4 spec states that "int → bool: only if the int value is 0 (converted to false) or 1 (converted to true)".Quick fix
For the one that Petr4 is missing, just add it. And remove the ones that aren't allowed by P4 spec or check the explicit flag if it's only allowed when the cast is explicit.
Note that the formalization considers lists to have a tuple type. So the cast from a list to a tuple is not required.
Petr4 code
P4 spce (v1.2.3)
Look at section 8.10. Additionally, some examples such as examples in section 8.3 are helpful.