Improving Compilers - Githubissues

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4

Apache License 2.0

74 stars 20 forks source link

Improving Compilers #338

Closed ericthewry closed 2 years ago

ericthewry commented 2 years ago

Post-Sigcomm Sync. Supercedes #309.

Bugfixes

Extern lookups
Inlining
Eliminate StackOverflows on large programs like switch.p4

Feature adds:

Translate parsers from P4Cub -> GCL
Header Stack operations (next & last)
Elaboration of extern arguments
Slicing

Eliminate Technical Debt:

Remove Compiler tests from Coq Compilation (e.g. ToP4cubTest & ToGCLTest)
Will add these as regression/CI tests in a future PR
Commit d6a7acd syncs with poulet4