This tool aims to validate various safety properties of P4 programs. It does this by first converting P4 code to a CFG (Control Flow Graph) inspired by GCL, then generating logical predicates which are used to check the reachability of bugs.

This project is written in Rust, so first install Rust: https://www.rust-lang.org/tools/install

There is also a dependency on the Z3 theorem prover, so install the library (including header files) either from source or your distribution's package manager (z3-devel for Fedora, libz3-dev for Debian systems).

Now that Rust and Z3 are installed, use cargo to build the project (with optimizations):

cargo build --release

The compiled binary is located at target/release/p4-analyzer.