bf4

bf4 is an analysis backend for P4. It translates P4 code (for the moment V1Model) into a CFG, performs optimization passes and then converts it into a verification condition which is checked using Z3.

bf4 is described in the following SIGCOMM'20 paper: "bf4: towards bug-free P4 programs".

Building bf4

0. Install p4c prerequisites

1. Install z3. Currently tested with version 4.8.7 from official repo.

2. Install inja. Tested with version 2.2.0. Copy inja.hpp to include path (e.g. /usr/include)

3. Install json. Tested with version 3.7.3. Copy json.hpp to include path / nlohmann (e.g. /usr/include/nlohmann)

4. Build:

mkdir build
cd build
cmake -DENABLE_UNIFIED_COMPILATION=OFF ..
make
make install

5. Preprocess

cd build/
make cptemplate
python3 ../sigcomm-2020/cleanup_v1.py sample.p4

6. Run bf4

p4c-analysis sample-integrated.p4

7. Making sense of the output (assume output of previous command was redirected to log.txt)

Getting specs:

grep -e "WHEN" -e "AND" log.txt

Getting fixes:

grep -o "missing fixes.*" log.txt | sort -u

bf4 infers required missing keys as described in the SIGCOMM paper. Altering the original program to add missing keys is not implemented in this version.

Known limitations

• For the moment, bf4 has only limited support for parser loops (it may not scale well or loop indefinitely)

• Support for automatically modifying the original program to add missing keys is not implemented. Thus, adding keys should be performed manually

• Due to optimzations (e.g. dominator tree) and ssa conversion some fields/variables may be hard to trace back in the original program

• In general tracing back things in the original program is far from ideal

p4c

p4c is a new, alpha-quality reference compiler for the P4 programming language. It supports both P4-14 and P4-16; you can find more information about P4 here and the specifications for both versions of the language here.

p4c is modular; it provides a standard frontend and midend which can be combined with a target-specific backend to create a complete P4 compiler. The goal is to make adding new backends easy.

The code contains four sample backends:

• p4c-bm2-ss: can be used to target the P4 simple_switch written using the BMv2 behavioral model https://github.com/p4lang/behavioral-model
• p4c-ebpf: can be used to generate C code which can be compiled to EBPF https://en.wikipedia.org/wiki/Berkeley_Packet_Filter and then loaded in the Linux kernel for packet filtering
• p4test: a source-to-source P4 translator which can be used for testing, learning compiler internals and debugging.
• p4c-graphs: can be used to generate visual representations of a P4 program; for now it only supports generating graphs of top-level control flows.

Sample command lines:

Compile P4_16 or P4_14 source code. If your program successfully compiles, the command will create files with the same base name as the P4 program you supplied, and the following suffixes instead of the .p4:

• a file with suffix .p4i, which is the output from running the preprocessor on your P4 program.
• a file with suffix .json that is the JSON file format expected by BMv2 behavioral model simple_switch.

p4c --target bmv2 --arch v1model my-p4-16-prog.p4
p4c --target bmv2 --arch v1model --std p4-14 my-p4-14-prog.p4

By adding the option --p4runtime-files <filename>.txt as shown in the example commands below, p4c will also create a file <filename>.txt. This is a text format "P4Info" file, containing a description of the tables and other objects in your P4 program that have an auto-generated control plane API.

p4c --target bmv2 --arch v1model --p4runtime-files my-p4-16-prog.p4info.txt my-p4-16-prog.p4
p4c --target bmv2 --arch v1model --p4runtime-files my-p4-14-prog.p4info.txt --std p4-14 my-p4-14-prog.p4

All of these commands take the --help argument to show documentation of supported command line options. p4c --target-help shows the supported "target, arch" pairs.

p4c --help
p4c --target-help

Auto-translate P4_14 source to P4_16 source:

p4test --std p4-14 my-p4-14-prog.p4 --pp auto-translated-p4-16-prog.p4

Check syntax of P4_16 or P4_14 source code, without limitations that might be imposed by any particular compiler back end. There is no output for these commands other than error and/or warning messages.

p4test my-p4-16-prog.p4
p4test --std p4-14 my-p4-14-prog.p4

Generate GraphViz ".dot" files for parsers and controls of a P4_16 or P4_14 source program.

p4c-graphs my-p4-16-prog.p4
p4c-graphs --std p4-14 my-p4-14-prog.p4

Generate PDF of parser instance named "ParserImpl" generated by the p4c-graphs command above (search for graphviz below for its install instructions):

dot -Tpdf ParserImpl.dot > ParserImpl.pdf

Getting started

1. Clone the repository. It includes submodules, so be sure to use --recursive to pull them in:

   git clone --recursive https://github.com/p4lang/p4c.git
   

   If you forgot --recursive, you can update the submodules at any time using:

   git submodule update --init --recursive
   

2. Install dependencies. You can find specific instructions for Ubuntu 16.04 here and for macOS 10.12 here.

3. Build. Building should also take place in a subdirectory named build.

   mkdir build
   cd build
   cmake .. <optional arguments>
   make -j4
   make -j4 check
   

   The cmake command takes the following optional arguments to further customize the build:

   • -DCMAKE_BUILD_TYPE=RELEASE|DEBUG -- set CMAKE_BUILD_TYPE to RELEASE or DEBUG to build with optimizations or with debug symbols to run in gdb. Default is RELEASE.
   • -DCMAKE_INSTALL_PREFIX=<path> -- set the directory where make install installs the compiler. Defaults to /usr/local.
   • -DENABLE_BMV2=ON|OFF. Enable the bmv2 backend. Default ON.
   • -DENABLE_EBPF=ON|OFF. Enable the ebpf backend. Default ON.
   • -DENABLE_P4C_GRAPHS=ON|OFF. Enable the p4c-graphs backend. Default ON.
   • -DENABLE_P4TEST=ON|OFF. Enable the p4test backend. Default ON.
   • -DENABLE_DOCS=ON|OFF. Build documentation. Default is OFF.
   • -DENABLE_GC=ON|OFF. Enable the use of the garbage collection library. Default is ON.
   • -DENABLE_GTESTS=ON|OFF. Enable building and running GTest unit tests. Default is ON.
   • -DENABLE_PROTOBUF_STATIC=ON|OFF. Enable the use of static protobuf libraries. Default is ON.

   If adding new targets to this build system, please see instructions.

4. (Optional) Install the compiler and the P4 shared headers globally.

   sudo make install
   

   The compiler driver p4c and binaries for each of the backends are installed in /usr/local/bin by default; the P4 headers are placed in /usr/local/share/p4c.

5. You're ready to go! You should be able to compile a P4-16 program for BMV2 using:

   p4c -b bmv2-ss-p4org program.p4 -o program.bmv2.json
   

If you plan to contribute to p4c, you'll find more useful information here.

Dependencies

Ubuntu 16.04 is the officially supported platform for p4c. There's also unofficial support for macOS 10.12. Other platforms are untested; you can try to use them, but YMMV.

• A C++11 compiler. GCC 4.9 or later or Clang 3.3 or later is required.

• git for version control

• GNU autotools for the build process

• CMake 3.0.2 or higher

• Boehm-Weiser garbage-collector C++ library

• GNU Bison and Flex for the parser and lexical analyzer generators.

• Google Protocol Buffers 3.0 or higher for control plane API generation

• GNU multiple precision library GMP

• C++ boost library (minimally used)

• Python 2.7 for scripting and running tests

• Optional: Documentation generation (enabled when configuring with --enable-doxygen-doc) requires Doxygen (1.8.10 or higher) and Graphviz (2.38.0 or higher).

Backends may have additional dependencies. The dependencies for the backends included with p4c are documented here:

• BMv2
• eBPF
• graphs

Ubuntu dependencies

Most dependencies can be installed using apt-get install:

sudo apt-get install cmake g++ git automake libtool libgc-dev bison flex libfl-dev libgmp-dev libboost-dev libboost-iostreams-dev libboost-graph-dev llvm pkg-config python python-scapy python-ipaddr python-ply tcpdump

For documentation building: sudo apt-get install -y doxygen graphviz texlive-full

An exception is Google Protocol Buffers; p4c depends on version 3.0 or higher, which is not available until Ubuntu 16.10. For earlier releases of Ubuntu, you'll need to install from source. You can find instructions here. We recommend that you use version 3.2.0. Earlier versions in the 3 series may not be supported by other p4lang projects, such as p4lang/PI. More recent versions may work as well, but all our CI testing is done with version 3.2.0. After cloning protobuf and before you build, check-out version 3.2.0:

git checkout v3.2.0

Please note that while all protobuf versions newer than 3.0 should work for p4c itself,