search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
76 stars 21 forks source link

Built-in functions #302

Open QinshiWang opened 2 years ago

QinshiWang commented 2 years ago

Currently, the semantics of built-in functions only supports the case that the "this" object to be an lvalue. Maybe we want to support rvalue in some cases. If so, then I think we should convert built-in function calls into kind of normal function calls with built-in operations. For example, we can have function prototypes

bool isValid(in hdr);
void setValid(inout hdr);
void setInvalid(inout hdr);

And the calls are converted as

hdr.isValid() -> isValid(hdr)
hdr.setValid() -> setValid(hdr)
hdr.setInvalid() -> setInvalid(hdr)
hackedy commented 2 years ago

Yeah I think being able to place a direction annotation on the this parameter would be useful.