Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add P4Smith, a random program generator to the P4Tools framework #4182

Merged
merged 2 commits into from
Jun 7, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions backends/p4tools/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,20 +6,22 @@
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.
─ 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.

```

## P4Tools
P4Tools is a collection of tools that make testing P4 targets and programs a little easier. So far the platform supports the following tools and projects:

- [P4Testgen](https://github.com/p4lang/p4c/tree/main/backends/p4tools/modules/testgen): An input-output test case generator for P4.

- [P4Smith](https://github.com/p4lang/p4c/tree/main/backends/p4tools/modules/smith): A random P4 program generator in the spirit of Csmith.

## Building
Please see the general installation instructions [here](https://github.com/p4lang/p4c#installing-p4c-from-source). P4Tools can be built using the following CMAKE configuration in the P4C repository.

Expand All @@ -31,7 +33,6 @@ make
```

## Dependencies
* [inja](https://github.com/pantor/inja) template engine for testcase generation.
* [z3](https://github.com/Z3Prover/z3) SMT solver to compute path constraints.
* Important: We currently only support Z3 versions 4.8.14 to 4.12.0.

Expand Down
41 changes: 37 additions & 4 deletions backends/p4tools/common/lib/util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
#include <cstdint>
#include <ctime>
#include <iomanip>
#include <numeric>
#include <optional>
#include <ratio>

#include <boost/multiprecision/cpp_int.hpp>
#include <boost/multiprecision/cpp_int/add.hpp>
Expand Down Expand Up @@ -64,14 +64,45 @@ uint64_t Utils::getRandInt(uint64_t max) {
return dist(rng);
}

big_int Utils::getRandBigInt(big_int max) {
int64_t Utils::getRandInt(int64_t min, int64_t max) {
boost::random::uniform_int_distribution<int64_t> distribution(min, max);
return distribution(rng);
}

int64_t Utils::getRandInt(const std::vector<int64_t> &percent) {
int sum = std::accumulate(percent.begin(), percent.end(), 0);

// Do not pick zero since that conflicts with zero percentage values.
auto randNum = getRandInt(1, sum);
int ret = 0;

int64_t retSum = 0;
for (auto i : percent) {
retSum += i;
if (retSum >= randNum) {
break;
}
ret = ret + 1;
}
return ret;
}

big_int Utils::getRandBigInt(const big_int &max) {
if (!currentSeed) {
return 0;
}
boost::random::uniform_int_distribution<big_int> dist(0, max);
return dist(rng);
}

big_int Utils::getRandBigInt(const big_int &min, const big_int &max) {
if (!currentSeed) {
return 0;
}
boost::random::uniform_int_distribution<big_int> dist(min, max);
return dist(rng);
}

const IR::Constant *Utils::getRandConstantForWidth(int bitWidth) {
auto maxVal = IR::getMaxBvVal(bitWidth);
auto randInt = Utils::getRandBigInt(maxVal);
Expand Down Expand Up @@ -145,8 +176,10 @@ std::vector<const IR::Type_Declaration *> argumentsToTypeDeclarations(

const IR::IDeclaration *findProgramDecl(const IR::IGeneralNamespace *ns, const IR::Path *path) {
auto name = path->name.name;
auto *decl = ns->getDeclsByName(name)->singleOrDefault();
if (decl != nullptr) return decl;
const auto *decl = ns->getDeclsByName(name)->singleOrDefault();
if (decl != nullptr) {
return decl;
}
BUG("Variable %1% not found in the available namespaces.", path);
}

Expand Down
11 changes: 10 additions & 1 deletion backends/p4tools/common/lib/util.h
Original file line number Diff line number Diff line change
Expand Up @@ -70,9 +70,18 @@ class Utils {
/// @returns a random integer in the range [0, @param max]. Always return 0 if no seed is set.
static uint64_t getRandInt(uint64_t max);

/// @returns a random integer between min and max.
static int64_t getRandInt(int64_t min, int64_t max);

/// @returns a random integer based on the percent vector.
static int64_t getRandInt(const std::vector<int64_t> &percent);

/// @returns a random big integer in the range [0, @param max]. Always return 0 if no seed is
/// set.
static big_int getRandBigInt(big_int max);
static big_int getRandBigInt(const big_int &max);

/// This is a big_int version of getRndInt.
static big_int getRandBigInt(const big_int &min, const big_int &max);

/// @returns a IR::Constant with a random big integer that fits the specified bit width.
/// The type will be an unsigned Type_Bits with @param bitWidth.
Expand Down
3 changes: 1 addition & 2 deletions backends/p4tools/common/p4ctool.h
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,11 @@ class AbstractP4cTool {
auto &toolOptions = Options::get();
auto compileContext = toolOptions.process(args);
if (!compileContext) {
return 1;
return EXIT_FAILURE;
}

// Set up the compilation context.
AutoCompileContext autoContext(*compileContext);

// If not explicitly disabled, print basic information to standard output.
if (!toolOptions.disableInformationLogging) {
enableInformationLogging();
Expand Down
84 changes: 84 additions & 0 deletions backends/p4tools/modules/smith/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
# CMake file for P4Smith.

include(common)

project(smith)

# Declare common P4Testgen variables.
set(P4SMITH_DIR ${P4C_BINARY_DIR}/smith)
set(P4SMITH_DRIVER "${CMAKE_CURRENT_BINARY_DIR}/p4smith")

configure_file(
"${CMAKE_CURRENT_SOURCE_DIR}/version.h.cmake" "${CMAKE_CURRENT_BINARY_DIR}/version.h" @ONLY
)
# Source files for smith.
set(SMITH_SOURCES
core/target.cpp
common/declarations.cpp
common/expressions.cpp
common/parser.cpp
common/scope.cpp
common/statements.cpp
common/table.cpp
util/util.cpp
util/wordlist.cpp
options.cpp
smith.cpp
)

set(SMITH_LIBS
PRIVATE p4tools-common
)

file(GLOB tools_targets RELATIVE ${CMAKE_CURRENT_SOURCE_DIR}/targets
${CMAKE_CURRENT_SOURCE_DIR}/targets/*
)

foreach(ext ${tools_targets})
if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/targets/${ext}/CMakeLists.txt)
# Generate an option that makes it possible to disable this extension.
string(MAKE_C_IDENTIFIER ${ext} EXT_AS_IDENTIFIER)
string(TOUPPER ${EXT_AS_IDENTIFIER} EXT_AS_OPTION_NAME)
string(CONCAT ENABLE_EXT_OPTION "ENABLE_TOOLS_TARGET_" ${EXT_AS_OPTION_NAME})
string(CONCAT EXT_HELP_TEXT "Build the " ${ext} " target")
option(${ENABLE_EXT_OPTION} ${EXT_HELP_TEXT} ON)
if(${ENABLE_EXT_OPTION})
message("-- Enabling target ${ext}")
add_subdirectory(${CMAKE_CURRENT_SOURCE_DIR}/targets/${ext})
set(include_statements_var
"${include_statements_var}#include \"backends/p4tools/modules/smith/targets/${ext}/register.h\"\n"
)
set(smith_targets_var "${smith_targets_var} ${ext}RegisterSmithTarget();\n")
endif()
endif()
endforeach(ext)

# Fill the template
configure_file(register.h.in register.h)

add_library(smith ${SMITH_SOURCES})
target_link_libraries(smith
${SMITH_LIBS}
# For Abseil includes.
PRIVATE frontend
)

add_dependencies(smith p4tools-common)

add_p4tools_executable(p4smith main.cpp)

target_link_libraries(
p4smith
PRIVATE smith
${SMITH_LIBS}
PRIVATE ${P4C_LIBRARIES}
PRIVATE ${P4C_LIB_DEPS}
)

add_custom_target(
linkp4smith # Add some convenience links for invoking p4smith.
COMMAND ${CMAKE_COMMAND} -E create_symlink ${CMAKE_CURRENT_BINARY_DIR}/p4smith
${CMAKE_BINARY_DIR}/p4smith
)

add_dependencies(p4smith linkp4smith)
79 changes: 79 additions & 0 deletions backends/p4tools/modules/smith/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
[![Status](https://github.com/p4lang/p4c/actions/workflows/ci-p4tools.yml/badge.svg)](https://github.com/p4lang/p4c/actions/workflows/ci-p4tools.yml)

# <img src="https://p4.org/wp-content/uploads/2021/05/Group-81.png" width="40">P4Smith

## Table of Contents

- [Installation](#installation)
- [Extensions](#extensions)
- [Usage](#usage)
- [Limitations](#limitations)
- [Further Reading](#further-reading)
- [Contributing](#contributing)
- [License](#license)

P4Smith is an extensible random P4 program generator in the spirit of [CSmith](https://en.wikipedia.org/wiki/Csmith). P4Smith generates random, but valid P4 programs for various P4 targets, for example the [v1model.p4](https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md) architecture on [BMv2](https://github.com/p4lang/behavioral-model) or `tna.p4` running on Tofino 1. P4Smiths generates programs that are valid according to the latest version of the (P4 specification)[https://p4.org/p4-spec/docs/P4-16-working-spec.html] or the restrictions of the specific target.

## Installation

P4Smith depends on the P4Tools framework and is automatically installed with P4Tools. Please follow the instructions listed [here](https://github.com/p4lang/p4c/tree/main/backends/p4tools#building) to install P4Smith. The main binary `p4smith` can be found in the `build` folder after a successful installation.

P4Smith is available as part of the [official P4C docker image](https://hub.docker.com/r/p4lang/p4c/). On Debian-based systems, it is also possible to install a P4Smith binary by following [these](https://github.com/p4lang/p4c#installing-packaged-versions-of-p4c) instructions.

## Extensions
P4Smith 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. P4Smith extension make use of the core P4Smith framework to generate programs. Several open-source extensions are available.

### core.p4 using the test compiler p4test
[targets/generic](targets/generic)

This random program generator generates random packages and tries to produce all valid P4 code according to the latest P4 specification. Programs should be compiled using [p4test](https://github.com/p4lang/p4c/tree/main/backends/p4est).

### v1model.p4 and psa.p4 on BMv2
[targets/bmv2](targets/bmv2)

P4Smith supports generating P4 programs for the `v1model` and `psa` architecture on [BMv2](https://github.com/p4lang/behavioral-model).

### pna.p4 on the DPDK SoftNIC
[targets/pna](targets/pna)

The [DPDK-SoftNIC](https://github.com/p4lang/p4-dpdk-target) is a new target implemented using the [Data Plane Development Kit (DPDK)](https://www.dpdk.org/). The SoftNIC can be programmed using the P4 `pna.p4` architecture.

### tna.p4 on Tofino 1
[targets/ebpf](targets/ebpf)

P4Smith can also generate programs for the `tna` architecture on Tofino 1. The programs are intended to be compiled on the proprietary Barefoot Tofino compiler.

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

```bash
./p4smith --target [TARGET] --arch [ARCH] prog.p4
```
Where `ARCH` specifies the P4 architecture (e.g., v1model.p4) and `TARGET` represents the targeted network device (e.g., BMv2). `prog.p4` is the name of the generated program.

## Further Reading
P4Smith was originally titled Bludgeon and part of the Gauntlet compiler testing framework. Section 4 of the [paper](https://arxiv.org/abs/2006.01074) provides a high-level overview of the tool.


If you would like to cite this tool please use this citation format:
```latex
@inproceedings{ruffy-osdi2020,
author = {Ruffy, Fabian and Wang, Tao and Sivaraman, Anirudh},
title = {Gauntlet: Finding Bugs in Compilers for Programmable Packet Processing},
booktitle = {14th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 20)},
year = {2020},
publisher = {{USENIX} Association},
month = nov,
abstract = {
Programmable packet-processing devices such as programmable switches and network interface cards are becoming mainstream. These devices are configured in a domain-specific language such as P4, using a compiler to translate packet-processing programs into instructions for different targets. As networks with programmable devices become widespread, it is critical that these compilers be dependable. This paper considers the problem of finding bugs in compilers for packet processing in the context of P4-16. We introduce domain-specific techniques to induce both abnormal termination of the compiler (crash bugs) and miscompilation (semantic bugs). We apply these techniques to (1) the opensource P4 compiler (P4C) infrastructure, which serves as a common base for different P4 back ends; (2) the P4 back end for the P4 reference software switch; and (3) the P4 back end for the Barefoot Tofino switch. Across the 3 platforms, over 8 months of bug finding, our tool Gauntlet detected 96 new and distinct bugs (62 crash and 34 semantic), which we confirmed with the respective compiler developers. 54 have been fixed (31 crash and 23 semantic); the remaining have been assigned to a developer. Our bug-finding efforts also led to 6 P4 specification changes. We have open sourced Gauntlet at p4gauntlet.github.io and it now runs within P4C’s continuous integration pipeline.}
}

```

## Contributing

Contributions to P4Smith in any form are welcome! Please follow the guidelines listed [here](https://github.com/p4lang/p4c/blob/main/CONTRIBUTING.md) to contribute.

## License

This project is licensed under the Apache License 2.0. See the [LICENSE](https://github.com/p4lang/p4c/blob/main/backends/p4tools/LICENSE) file for details.
Loading
Loading