Skip to content

Static analysis tool which checks P4 code for bugs

Notifications You must be signed in to change notification settings

AzureMarker/p4-analyzer

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

p4-analyzer

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.

Build

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.

About

Static analysis tool which checks P4 code for bugs

Topics

Resources

Stars

Watchers

Forks

Languages