P4-SpecTec
A mechanized formal specification for the P4 programming language, using the SpecTec framework. This reuses parts of the Petr4 codebase, especially the parser and numerics implementation. This also reuses parts of the Wasm-SpecTec codebase, especially the specification parser and the high-level architecture of the tool.
Table of Contents
Building the Project
Building from Source
Submodule(s)
p4c is a submodule of this project, as we reuse the tests and the P4 include files from p4c. You can initialize it by running:
$ git submodule update --init
Prerequisites (Linux)
Install opam version 2.0.5 or higher.
$ apt-get install opam
$ opam init
creduce is used in the test generation beckend to reduce the generated test cases. You can install it by running:
$ apt-get install creduce
Note that creduce is only necessary for the test generation backend, so you can skip this step if you only want to use the specification and the simulation features.
asciidoctor is used to generate HTML/PDF document from the AsciiDoc source files. Use docs/install-asciidoctor-linux.sh to install it on Linux.
Prerequisites (MacOS)
- Install
opam version 2.0.5 or higher following the instructions here. Install creduce using Homebrew.
Note that creduce is only necessary for the test generation backend, so you can skip this step if you only want to use the specification and the simulation features.
- Install
asciidoctor following the instructions here.
Prerequisites (Windows)
- For now, we do not have instructions for building on Windows. We recommend using WSL2 or using Docker to build and run P4-SpecTec on Windows.
OCaml compiler and packages
Create OCaml switch for version 5.1.0 Install dune version 3.16.1, bignum version v0.17.0, menhir version 20240715, core version v0.17.1, core_unix version v0.17.0, and bisect_ppx version 2.8.3 via opam.
$ opam switch create 5.1.0
$ eval $(opam env)
$ opam install dune bignum 'menhir=20240715' 'menhirLib=20240715' core core_unix bisect_ppx yojson ppx_deriving_yojson
Compiling the Project
$ make build
This creates an executable p4spectec in the project root.
Additional Notes
You may also need libgmp-dev and pkg-config, depending on your system.
Docker builds
We provide two dockerfiles, p4spectec.dockerfile for P4-SpecTec and p4spectec_p4c.dockerfile for both P4-SpecTec and p4c. The former is useful for users who only want to use P4-SpecTec, while the latter is useful for users who also want to use p4c tools.
# without p4c
$ docker build -f p4spectec.dockerfile -t p4spectec:latest .
# with p4c, for RQ3-b branch coverage measurement
$ docker build -f p4spectec_p4c.dockerfile -t p4spectec_with_p4c:latest .
Nix Flake
A flake.nix is provided for reproducible development environments via Nix. It sets up OCaml 5.1 and all project dependencies without requiring manual opam configuration.
Prerequisites: Nix with flakes enabled. If you haven't enabled flakes, add this to /etc/nix/nix.conf or ~/.config/nix/nix.conf:
experimental-features = nix-command flakes
Enter the dev shell:
$ nix develop
This drops you into a shell with OCaml 5.1, dune, menhir, core, and all other required packages available. It also includes development tooling: ocaml-lsp-server, utop, and ocamlformat.
Automatic shell activation with direnv:
Create a .envrc at the project root with use flake, then run direnv allow once to activate the dev shell automatically on cd.
P4-SpecTec: A language specification framework for P4
The spec source files are located in the spec directory.
Processing the specification
The specification is processed in multiple stages: parsing, elaboration, structuring, and prose generation.
- Parsing: The input spec files are parsed. At this stage, the spec is called EL (external language).
Elaboration: The parsed spec files are type checked, and auxiliary information is annotated on the spec. At this stage, the spec is called IL (internal language).
$ ./p4spectec elab spec
Structuring: The elaborated spec is structured, where structured control flow is introduced. At this stage, the spec is called SL (structured language).
$ ./p4spectec struct spec
Prose generation: The structured spec is converted to a human-readable format, in AsciiDoc format. At this stage, the spec is called PL (prose language).
$ ./p4spectec prose spec
Generating the specification document
From the project root, run the following command to generate the specification document in HTML and PDF format.
# Only HTML
make spec-release-html
# Both HTML and PDF (takes more time)
make spec-release
The generated documents can be found in the docs directory.
Running the specification
Given a P4 program, below command runs a particular relation on it. RELNAME may be Program_ok (for typing) or Program_inst (for instantiation).
# To run the IL
$ ./p4spectec run spec -rel [RELNAME] -i p4c/p4include -p [FILENAME].p4 -il
# To run the SL
$ ./p4spectec run spec -rel [RELNAME] -i p4c/p4include -p [FILENAME].p4 -sl
e.g., $ ./p4spectec run spec/*/*.watsup -rel Program_ok -i p4c/p4include -p p4c/testdata/p4_16_samples/basic_routing-bmv2.p4 -sl type checks the basic_routing-bmv2.p4 program using the relation Program_ok specified in the spec.
We currently support the V1Model and eBPF architectures, and the STF format for specifying input/output packets. ARCH may be v1model or ebpf.
# To run the IL
$ ./p4spectec sim spec -arch [ARCH] -i p4c/p4include -p [FILENAME].p4 -stf [STF_FILENAME].stf -il
# To run the SL
$ ./p4spectec sim spec -arch [ARCH] -i p4c/p4include -p [FILENAME].p4 -stf [STF_FILENAME].stf -sl
e.g., $ ./p4spectec sim spec/*/*.watsup -arch v1model -i p4c/p4include -p p4c/testdata/p4_16_samples/basic_routing-bmv2.p4 -stf testdata/p4testgen/basic_routing-bmv2/basic_routing-bmv2_1.stf -sl runs the basic_routing-bmv2.p4 program on the input packet specified in basic_routing-bmv2_1.stf, and checks if the output packet matches the expected output specified in the same STF file.
To initiate a fuzz loop generating (intentionally) ill-typed P4 programs
P4-SpecTec also supports fuzzing negative type checker tests for P4 type checkers. i.e., it can generate various ill-typed P4 programs that should be rejected by the type checker.
$ mkdir [GEN_DIR]
$ ./p4spectec testgen spec -rel Program_ok -i p4c/p4include -gen [GEN_DIR] -fuel [NUM] -boot-dir [BOOT_DIR]
This will generate P4 programs in the directory [GEN_DIR] using the seed files in the directory [BOOT_DIR]. [NUM] is the number of fuzz cycles to run. For instance, you may set [BOOT_DIR] to p4c/testdata/p4_16_samples, and [NUM] to 10 to run 10 fuzzing iterations starting from the sample P4 programs in p4c/testdata/p4_16_samples.
After the fuzz loop, you may find the generated P4 programs in the directory [GEN_DIR], with the log file fuzz.log, query files for mutations query.log and an initial coverage file boot.coverage.
In later runs with the same boot directory, you can use warm boot to skip the initial coverage collection phase, and directly start with the fuzz loop.
$ ./p4spectec testgen spec -rel Program_ok -i p4c/p4include -gen [GEN_DIR] -fuel [NUM] -boot-file [BOOT_FILE].coverage
Read this document for how to apply meta-circular interpretation to the P4-SpecTec framework, intuitively, running the specification-of-specification on P4-SpecTec.
Contributing
P4-SpecTec is an open-source project. Please feel free to contribute by opening issues or pull requests.
License
P4-SpecTec is released under the Apache 2.0 license.