Features

Exhaustive, automatic input-output test generation: Given a P4 program and sufficient time, P4Testgen generates tests that cover every reachable statement in the program. Each test consists of an input packet, control-plane configuration, and the expected output packet. Test case generation is configurable using command-line flags and assertions within the P4 code. For example, it is possible to generate tests that use only TCP-IP packets as input.
Support for multiple P4 targets: P4Testgen is designed to be extensible for many P4 targets. It models the complete semantics of the target's packet-processing pipeline, including the P4 language, architectures, externs, and target-specific behaviors. Support for a P4 target is implemented in the form of an extension. The open-source version of P4Testgen supports generating tests for the v1model.p4 architecture on BMv2, the pna.p4 architecture on DPDK-SoftNIC, and the ebpf_model.p4 architecture on the Linux kernel.
Support for multiple test frameworks: P4Testgen generates abstract tests that can be serialized into formats suitable for any test framework. P4Testgen extensions can generate tests for STF, PTF, and P4Runtime Protobuf messages.
Coverage heuristics: To limit the number of generated tests, P4Testgen uses coverage heuristics. It employs coverage-guided search to generate tests that cover new nodes in the P4 program, such as statements or tables. P4Testgen also supports custom stop metrics to ensure that test case generation stops when a user-defined goal has been reached.

Installation

P4Testgen depends on the P4Tools framework and is automatically installed with P4Tools. Please follow the instructions listed here to install P4Testgen. The main binary p4testgen can be found in the build folder after a successful installation.

P4Testgen is available as part of the official P4C docker image. On Debian-based systems, it is also possible to install a P4Testgen binary by following these instructions.

Dependencies

In addition to P4Tools' own dependencies P4Testgen depends on the following external software:

inja template engine for testcase generation.

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

Extensions

P4Testgen extensions are instantiations of a particular combination of P4 architecture and the target that executes the P4 code. For example, the v1model.p4 architecture can be executed on the behavioral model. P4Testgen extension make use of the core P4Testgen framework to generate tests. Several open-source extensions are available.

v1model.p4 on BMv2

targets/bmv2

P4Testgen supports generating STF, PTF, Protobuf messages, and Metadata templates for the v1model architecture on BMv2. Almost all externs, including checksums, cloning, recirculation are supported. P4Testgen also supports P4Constraints parsing.

pna.p4 on the DPDK SoftNIC

targets/pna

The DPDK-SoftNIC is a new target implemented using the Data Plane Development Kit (DPDK). The SoftNIC can be programmed using the P4 pna.p4 architecture.

ebpf_model.p4 on the eBPF kernel target

targets/ebpf

The P4Testgen eBPF extension is a proof-of-concept implementation. It supports generating tests for P4 eBPF programs but, as the test framework and extern support is limited, so is the P4Testgen extension.

Definitions

Useful definitions to keep in mind when using P4Testgen.

Paths and Path Constraints

P4Testgen defines a path as a collection of path constraints. A path constraint is a boolean expression composed of constants and symbolic variables at a particular program point. For example, in the common case an if statement will branch into a true and a false branch. This will produce two new unique paths. P4Testgen only traverses a path if its constraints are feasible. A path constraint is feasible if an SMT solver is able to find a solution for the constraints. A path constraint such as hdr.eth.eth_type == 0x800 && hdr.eth.eth_type != 0x800 is never feasible.

Symbolic Variables

A symbolic variable is a placeholder variable which is frequently part of path constraints. SMT solvers assign values to symbolic variables to satisfy a particular set of path constraints. In P4Testgen, symbolic variables typically correspond to test inputs. For example, the input packet and port are symbolic variables.

Taint

P4Testgen uses bit-level taint tracking to keep track of nondeterminism in the P4 program. An expression is considered tainted if the value of its bits (or simply just a sub-expression) is unpredictable. This could happen because of reads from an uninitialized variable, unimplemented checksums, or simply because of random generators. P4Testgen's core framework marks some constructs tainted, for example uninitialized variables, but otherwise leaves it up to the P4Testgen extension whether to mark a particular expression or method call tainted. Similiarly, it is up to the extension how tainted values are resolved. An extension can either ignore them or throw an error.

Usage

To access the possible options for p4testgen use p4testgen --help. To generate a test for a particular target and P4 architecture, run the following command:

./p4testgen --target [TARGET] --arch [ARCH] --max-tests 10 --out-dir [OUT] prog.p4

Where ARCH specifies the P4 architecture (e.g., v1model.p4) and TARGET represents the targeted network device (e.g., BMv2). Choosing 0 as the option for max-tests will cause P4Testgen to generate tests until it has exhausted all possible paths.

Coverage

P4Testgen is able to track the (source code) coverage of the program it is generating tests for. With each test, P4Testgen can emit the cumulative program coverage it has achieved so far. Test 1 may have covered 2 out 10 P4 nodes, test 2 5 out of 10 P4 nodes, and so on. To enable program coverage, P4Testgen provides the --track-coverage [NODE_TYPE] option where NODE_TYPE refers to a particular P4 source node. Currently, STATEMENTS for P4 program statements and TABLE_ENTRIES for constant P4 table entries are supported. Multiple uses of --track-coverage are possible.

The option --stop-metric MAX_NODE_COVERAGE makes P4Testgen stop once it has hit 100% coverage as determined by --track-coverage.

Generating Specific Tests

P4Testgen supports the use of custom externs to restrict the breadth of possible input-output tests. These externs are testgen_assume and testgen_assert, which serve two different use cases: Generating restricted tests and finding assertion violations.

Restricted Tests

testgen_assume(expr) will add expr as a necessary path constraints to all subsequent execution. For example, for the following snippet

 P4
 
state parse_ethernet {
    packet.extract(headers.ethernet);
    testgen_assume(headers.ethernet.ether_type == 0x800);
    transition select(headers.ethernet.ether_type) {
        0x800: parse_ipv4;
        0x86dd: parse_ipv6;
        default: accept;
    }
}

only inputs which have 0x800 as Ethertype will be generated. This mode is enable by default and can be disabled with the flag --disable-assumption-mode.

Finding Assertion Violations

Conversely, testgen_assert(expr) can be used to find violations in a particular P4 program. By default, testgen_assert behaves like testgen_assume. If the flag --assertion-mode is enabled, P4Testgen will only generate tests that will cause expr to be false and, hence, violate the assertion. For example, for

 P4
 
state parse_ethernet {
    packet.extract(headers.ethernet);
    transition select(headers.ethernet.ether_type) {
        0x800: parse_ipv4;
        0x86dd: parse_ipv6;
        default: accept;
    }
}
state parse_ipv4 {
    packet.extract(headers.ipv4);
    testgen_assert(!headers.ipv6.isValid());
    transition select(headers.ethernet.ether_type) {
        0x800: parse_ipv4;
        0x86dd: parse_ipv6;
        default: accept;
    }
}

with --assertion-mode enabled, P4Testgen will try to generate tests that violated the condition testgen_assert(!headers.ipv6.isValid());.

Interacting with Test Frameworks

Generally, P4Testgen only generates tests. It does not invoke test frameworks or run end-to-end tests. However, many of the extensions supply tests that do so. Each extension has their own scripts and CMake implementation for these test scripts. These can be run with ctest -R testgen-p4c-[extension]. Concretely, ctest -V -R testgen-p4c-bmv2/ will run the v1model BMv2 STF tests.

Detecting P4 Program Flaws

P4Testgen can also be used to detect flaws in P4 program. P4Testgen supplies a strict mode (enabled with the flag --strict), which fails when the interpreter encounters unrecoverable tainted behavior in the program.

Coverage tracking can also be used to identify dead code in the program. If P4Testgen does not achieve 100% coverage within a reasonable amount of time (say 10k tests or an hour of test generation) one can use the --print-coverage to emit the nodes which can not be covered. Often, P4Testgen simply does have control-plane support for the node, but in many cases the code may simply not executable.

Limitations

P4Testgen only performs functional validation for single inputs. It does not support tests which involve multiple packets as input. It also does not support generating any performance or resource usage tests. Target-specific limitations are documented in the corresponding relevant target-folder or Github issue.

P4Testgen Benchmarks

The backends\p4tools\modules\testgen\benchmarks folder contains utility scripts to benchmark P4Testgen. test_coverage.py measures coverage of various path selection strategies. plot.py creates plots of the results.

P4Testgen BMv2 target tests

CMake Files

P4Tests.cmake - Common test suite to add P4 tests from P4C submodules.
- Run p4testgen on P4-16 V1Model p4s with the BMv2 target.
BMV2...Xfail.cmake - BMv2 xfails for the various BMv2 V1Model back ends.

How to Run tests

All P4C submodule tests are tagged with 'testgen-p4c-bmv2' label

bash cd build/testgen ctest -R testgen-p4c-bmv2

Contributing

Contributions to P4Testgen in any form are welcome! Please follow the guidelines listed here to contribute.

License

This project is licensed under the Apache License 2.0. See the LICENSE file for details.

Table of Contents