verified-network-toolchain / petr4

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

why are error and match_kind types categorized as base types in P4? #386

Closed pataei closed 1 year ago

pataei commented 1 year ago

P4 spec categories error and match_kind types as baseType, however, they both have to be declared by a P4 program. Here is the grammar for baseType and declaration:

baseType
    : BOOL
    | ERROR
    | MATCH_KIND
    | STRING
    | INT
    | BIT
    | BIT '<' INTEGER '>'
    | INT '<' INTEGER '>'
    | VARBIT '<' INTEGER '>'
    | BIT '<' '(' expression ')' '>'
    | INT '<' '(' expression ')' '>'
    | VARBIT '<' '(' expression ')' '>'
    ;

declaration
    : constantDeclaration
    | externDeclaration
    | actionDeclaration
    | parserDeclaration
    | typeDeclaration
    | controlDeclaration
    | instantiation
    | errorDeclaration
    | matchKindDeclaration
    | functionDeclaration
    ;

errorDeclaration
    : ERROR '{' identifierList '}'
    ;

matchKindDeclaration
    : MATCH_KIND '{' identifierList '}'
    ;

identifierList
    : name
    | identifierList ',' name
    ;

A quick look through P4 spec and where these types are used resulted only in one example which uses error type in arguments:

extern void verify(in bool condition, in error err);

ParserModel.verify(bool condition, error err) {
    if (condition == false) {
        ParserModel.parserError = err;
        goto reject;
    }
}

@jnfoster and @hackedy Any other examples of using these types where baseType is used?

hackedy commented 1 year ago

I don't think the error type has to be declared. But members of the error type do need to be declared. It's like error exists but new members can be added to it by error {member1; member2 } declarations. Likewise for match_kind.

hackedy commented 1 year ago

Also where I usually see error used is as a field of the standard_metadata_t struct in V1Model. I don't know if that's the kind of use you're looking for though?

pataei commented 1 year ago

Yeah, error itself doesn't have to be declared but its member does. And yes, standard_metadata_t is a great example. Thx Ryan!

hackedy commented 1 year ago

yw!

jnfoster commented 1 year ago

In the same vein, you can also declare variables of type match_kind or error. Not incredibly useful, but legal.