Directory Structure

p4tools
 ├─ cmake            ── common P4Tools CMake modules.
 ├─ common           ── common code for the various P4Tools modules.
 │  ├─ compiler      ── transformation passes for P4 code.
 │  ├─ control_plane ── code concerning P4Tool's control plane semantics.
 │  ├─ core          ── definitions for core parts of the P4Tools modules.
 │  └─ lib           ── helper functions and utilities for P4Tools modules.  
 └─  modules         ── P4Tools extensions.
    ├─ smith       ── P4Smith: a random P4 program generator.
    └─ testgen       ── P4Testgen: a test-case generator for P4 programs.

Building

Please see the general installation instructions here. P4Tools can be built using the following CMAKE configuration in the P4C repository.

mkdir build
cd build
cmake .. -DCMAKE_EXPORT_COMPILE_COMMANDS=ON -DENABLE_TEST_TOOLS=ON
make

Dependencies

z3 SMT solver to compute path constraints.
- Important: We currently only support Z3 versions 4.8.14 to 4.12.0.

These dependencies are automatically installed via CMakelist's FetchContent module.

Development Style

Currently, each C++ source directory has a few subdirectories, including:

core, containing the core functionality of the submodule; and
lib, containing supporting data structures.

The distinction between the two can be fuzzy. Here are some guiding principles for where to find/put what:

If it depends on anything in core, it belongs in core.
If it's something that resembles a general-purpose data structure (e.g., an environment or a symbol table), it's probably in lib.

C++ Coding style

P4Tools in general follows the P4C coding style. Some deviations from the Style Guide are highlighted below.

Comments are important. The Style Guide's section on comments is required reading.
- Classes, methods, and fields are documented with triple-slash Doxygen-style comments: /// An example class demonstrating a documentation comment. class C {};
- We do not use copyright headers or license boilerplate in our source files. Where needed, these will be auto-generated during release packaging.
Generally prefer a single class declaration per .h file, unless providing a library of related classes. Multiple classes may be declared in a .cpp file.

P4Tools Contributors

P4Testgen is a test oracle for the P4 language. Given a P4_16 program and a specification of the underlying architecture, it automatically generates a comprehensive set of input/output tests that can be executed to validate a target device.

Core Developers

History

Jed Liu was the original architect of P4Testgen and designed the abstract machine that allows using P4C's visitors to implement arbitrary traversals of the program IR. Building on Jed's design, Fabian Ruffy completed the symbolic interpreter for P4_16's core features and designed extensions for common open-source architectures. He also developed the model of packets, taint tracking, and concolic execution. Prathima Kotikalapudi developed the extensible test backend, with instantiations for PTF and STF. Vojtěch Havel assisted with the implementation of the symbolic interpreter and the development of P4Testgen extensions for several Intel architectures. Hanneli Tavante added support for strategies that guide the exploration of paths that maximize various notions of coverage. Volodymyr Peschanenko, and Vlad Dubina developed the SMT-LIB interface to Z3, implemented front-end and mid-end passes such as parser unrolling, and completed the back end for the V1Model architecture on the BMv2 simple switch. Nate Foster guided the design of P4Testgen and contributed to various aspects of the symbolic interpreter.

Table of Contents