Runtime LTL

This is an undergraduate research project aiming towards creating a runtime verification process for C++ code that will check the function call graph against an LTL formula.

Process

This is done by creating an LLVM IR pass that inserts calls to a verification system at the beginning and end of annotated functions.

Functions are annotated like so:

__attribute__((annotate("ltl_verify"))) void annotate_this() {
  printf("Hello world!\n");
}

Calls are made to a separately loaded shared object containing the runtime library for the verification system.

Requirements

• CMake >= 3.11
• SPOT 2.7.1 (https://spot.lrde.epita.fr/install.html)
• ninja 1.8.2
• LLVM 7 (llvm-config should be in your PATH)
• Clang 7

Building

To build, please run configure, which will setup a build directory to use CMake with Ninja as the target build system. If you are familiar with CMake, feel free to set this up to use other build systems. The configure script will perform an initial build of the shared object; afterwards, to re-build upon changes to the source, run cmake --build $PROJECT_ROOT/build.

Using Nix

If you use Nix you can simply run nix-shell to install the required dependencies. Further, you can build the shared object with nix-build. Make sure that the build directory does not exist, as it will be copied by nix-build and conflict with the new build directory the nix build process will try to generate.

During development it is recommended to use the process described in Building to avoid rebuilding the shared object from scratch after every change.

Using run-pass.sh

run-pass.sh is a script for quickly testing the runtime ltl plugin on C and C++ files (example files can be found in the tests folder). It is designed to deal with both nix and non-nix environments. The script is commented, but rough, as I am not very familiar with bash scripting.

The script will compile the input file to IR and then print out the IR. It will also compile the file to a binary that it will then execute. I would prefer to use the lli interpreter, but unfortunately that requires manually setting up the linking to the standard library, which is a complex task better tackled later on in the project.

Syntax:

[PASS_SO=<plugin shared object>] [CLANG=<clang binary>]
./run-pass.sh <source input>
    [<binary output file>] [<IR output file>]

Environment variables can be defined that affect the behavior of the program. PASS_SO will provide a path for the shared object that should be loaded. CLANG will provide a path to a clang executable that should be used.

The first argument is the source file, the second argument is an optional file to output the binary to, and the third argument is an optional file to output the generated IR to.