For information about the software related to "Model checking-based performance prediction for P4 by D. Lukács, G. Pongrácz, M. Tejfel", please see this page.
For information about the software related to "Component-based error detection of P4 programs by G. Tóth, M. Tejfel", please see this page.
For information about the software related to "P4Query: Static Analyser Framework by D. Lukács, G. Tóth, M. Tejfel", please see the following sections.
This is a pre-alpha proof-of-concept tool without extensive testing: expect bugs and incomplete coverage.
P4Query is a static code analysis framework for the P4 language. We intend P4Query to be a knowledge base or infrastructure that can host various coding-related applications, such as compilers, code comprehension tools, IDEs, and formal verification tools.
Implemented features (applications):
- Visualization
- Verification of various safety-properties
- A proof-of-concept P4 compiler
Implemented features (infrastructure):
- Syntax tree (based on P4 specs)
- Symbol table
- Call analysis
- Control flow analysis
- All information is stored in a knowledge graph (a graph database with Gremlin API).
- Several other features (such as program dependency and data flow analysis) are planned.
You need Java 8 or higher to execute the tool.
We use Graphviz to visualize the graphs, so we recommend to install it.
For trying the tool, download the release, unpack the ZIP and launch it using the following command:
$ ./p4query.cmd draw -A ControlFlowThis will create an SVG of the control flow graph in your temp directory for the built-in basic.p4 file. For more information on parameters (including supplying your own P4 file), please see User Guide.
Note: if the command doesn't work for you, you can also try launching the JAR in the ZIP file directly ($ java -jar pquery.jar draw -A ControlFlow).
This research project is mainly developed in an internal repository.
If you would like to cooperate with us in the project, please contact the authors. If you already know what you're doing, the contribution guide can be useful.
P4Query is licensed under the Apache License, Version 2.0.
Authors:
Acknowledgements:
- Thanks for Ali Fattaholmanan for publishing his ANTLR implementation of the P4 grammar.
- Thanks for all the developers for working on the dependencies in the
pom.xmls.