We present P4Testgen, a test oracle for the P4$_{16}$ language. P4Testgen supports automatic test generation for any P4 target and is designed to be extensible to many P4 targets. It models the complete semantics of the target's packet-processing pipeline including the P4 language, architectures and externs, and target-specific extensions. To handle non-deterministic behaviors and complex externs (e.g., checksums and hash functions), P4Testgen uses taint tracking and concolic execution. It also provides path selection strategies that reduce the number of tests required to achieve full coverage. We have instantiated P4Testgen for the V1model, eBPF, PNA, and Tofino P4 architectures. Each extension required effort commensurate with the complexity of the target. We validated the tests generated by P4Testgen by running them across the entire P4C test suite as well as the programs supplied with the Tofino P4 Studio. Using the tool, we have also confirmed 25 bugs in mature, production toolchains for BMv2 and Tofino.

翻译：我们提出了P4Testgen，一种针对P4$_{16}$语言的测试预言。P4Testgen支持为任意P4目标自动生成测试，并设计为可扩展到多种P4目标。它完整地建模了目标数据包处理管道的语义，包括P4语言、架构和外部模块（extern）以及目标特定的扩展。为了处理非确定性行为和复杂的外部模块（例如校验和与哈希函数），P4Testgen采用了污点追踪（taint tracking）和符号执行（concolic execution）技术。它同时提供了路径选择策略，可在达到全覆盖率的前提下减少所需测试数量。我们已为V1model、eBPF、PNA和Tofino这四种P4架构实例化了P4Testgen。每个扩展所需的工作量与目标的复杂度成正比。我们通过在整个P4C测试套件以及Tofino P4 Studio附带的程序中运行P4Testgen生成的测试来验证其有效性。使用该工具，我们还在针对BMv2和Tofino的成熟生产工具链中确认了25个缺陷。