Skip to content

verified-network-toolchain/petr4

main
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
bin
 
 
 
 
 
 
 
 
 
 
lib
 
 
 
 
 
 
 
 
 
 
 
 
web
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Build Status

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.