The Petr4 project is developing the formal semantics of the P4 Language backed by an independent reference implementation.
See https://verified-network-toolchain.github.io/petr4/ or check out the gh-pages
branch
for information on the Petr4 artifact.
-
Install OPAM 2 following the official OPAM installation instructions. Make sure
opam --version
reports version 2 or later. -
(on Linux) Install external dependencies:
sudo apt-get install m4 libgmp-dev
-
(on MacOS) Install external dependencies:
brew install m4 brew install gmp
You can use the scripts to install Petr4. Alternatively, follow theses steps:
-
Check the installed version of OCaml:
ocamlc -v
If the version is less than 4.14.0, upgrade:
opam switch create <name> ocaml-base-compiler.4.14.0
-
Install p4pp from source.
opam pin add p4pp https://github.com/cornell-netlab/p4pp.git
-
Install Coq and Bignum.
opam install coq opam install bignum
If this doesn't work, install the dependencies manually. This step shouldn't be needed.
opam install ANSITerminal alcotest bignum cstruct-sexp pp ppx_deriving ppx_deriving_yojson yojson js_of_ocaml js_of_ocaml-lwt js_of_ocaml-ppx
-
Build bundled dependencies.
opam repo add coq-released https://coq.inria.fr/opam/released opam pin add coq-vst-zlist https://github.com/PrincetonUniversity/VST.git opam install . --deps-only
-
Use dune to build and install petr4.
dune build dune install
-
[Optional] Run tests
make test
-
[Optional] Install helper packages
opam install utop ocaml-lsp-server ocamlformat ocamlformat-rpc
-
[Optional] Run one of the following commands
dune utop
ORdune utop -p petr4
. Check if you can run the following command in the toplevel. It should return an empty string.Petr4.P4info.to_string Petr4.P4info.dummy;;
Currently petr4
is merely a P4 front-end. By default, it will parse
a source program to an abstract syntax tree and print it out, either
as P4 or encoded into JSON.
Run petr4 -help
to see the list of currently-supported options.
Petr4 is an open-source project. We encourage contributions! Please file issues on Github.
See the list of contributors.
Petr4 is released under the Apache2 License.