Translation Validation for the P4 compiler

[fruffy]

Gauntlet (cough) has show that it is possible to use translation validation at scale and effectively for P4 programs. This is because the P4 language itself is restricted enough that you can easily convert it to pure SMT expressions and then use these expressions for equality checks in a solver like Z3.

The problem with Gauntlet is that it is an external tool, and not well integrated with the current P4 compiler. Particularly because Gauntlet uses its own type inference and state tracking it is difficult to maintain with developments to the P4 language.

Ideally, we should have a translation validation library as part of P4C, which we can call into to convert a particular P4 construct (e.g., IR:Expression, IR::P4Control, IR::P4Parser) into SMT logic and then use this representation for various validation tasks.

Use case 1: You could use this representation to check whether a particular language construction is "semantically equivalent" before and after a compiler transformation. This is similar to Credible Compilation, which validates that a particular compile step is semantically correct.

Use case 2: Another use case is superoptimization. We can use this SMT representation to transform basic blocks into "better", and semantically equivalent structures.

[jnfoster]

Cool ideas! Would any of the p4testgen infrastructure be useful for this?

[fruffy]

Cool ideas! Would any of the p4testgen infrastructure be useful for this?

I think so, but it requires work. One problem is that the P4Testgen is build as a monolith, it is designed to consume a P4 program as a whole. Ideally, we want to check single basic blocks.

The symbolic executor interface requires ProgramInfo, which in turn requires compiler information.

Carrying this information along could be onerous.