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.
Install external dependencies:
sudo apt-get install m4 libgmp-dev
opam install petr4
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.09.1, upgrade:
opam switch 4.09.1
Install p4pp from source.
Install Coq and Bignum.
opam install coq
opam install bignum
If this doesn't work, install the dependencies manually.
opam install ANSITerminal alcotest bignum cstruct-sexp pp ppx_deriving ppx_import 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
Use dune to build and install petr4.
opam install . --deps-only
opam exec -- dune build
dune install
[Optional] Run tests
make test
To run the CI tests locally:
opam exec -- make ci-test
To run STF tests:
opam exec -- make test-stf
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
uses js_of_ocaml
to provide a web interface. To compile to javascript,
run make web
. Then open index.html
in html_build
in a browser.
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.