Petr4

The Petr4 project is developing the formal semantics of the P4 Language backed by an independent reference implementation.

POPL'21 artifact

See https://verified-network-toolchain.github.io/petr4/ or check out the gh-pages branch for information on the Petr4 artifact.

Getting Started

Installing Petr4

1. Install OPAM 2 following the official OPAM installation instructions. Make sure opam --version reports version 2 or later.

2. Install external dependencies:

   sudo apt-get install m4 libgmp-dev
   

Installing from OPAM

1. Install petr4 from the opam repository. This will take a while the first time because it installs OPAM dependencies.

   opam install petr4
   

Installing from source

You can use the scripts to install Petr4. Alternatively, follow theses steps:

1. Check the installed version of OCaml:

   ocamlc -v
   

   If the version is less than 4.09.1, upgrade:

   opam switch 4.09.1
   

2. Install p4pp from source.

3. Use OPAM to install dependencies.

   opam install . --deps-only
   

   If this doesn't work, install the dependencies manually.

   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
   

4. Build binaries using the supplied Makefile

   make
   

5. Install binaries in local OPAM directory

   make install
   

6. [Optional] Run tests

   make test
   

Running Petr4

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.

Web user interface

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.

Contributing

Petr4 is an open-source project. We encourage contributions! Please file issues on Github.

Credits

See the list of contributors.

License

Petr4 is released under the Apache2 License.