Using PhASAR with Docker

Abstract

Recently we have prepared PhASAR for being able to run in a docker container. This makes it a lot easier to use PhASAR, since it is no longer required for each user to build it manually. Additionally PhASAR is now platform independent - as far as docker is, which increases the usability.

For more information about docker see the documentation.

In the following you can find guides on how to use PhASAR from a container and how to build it.

Fetch a prebuilt Docker image

A prebuilt docker image can be found at https://hub.docker.com/r/pdschbrt/phasar.

Pull the docker image using:

docker pull pdschbrt/phasar

We are currently setting up an automated pipeline such that a new docker image is build for each push made to PhASAR's repository.

Build a Docker Image

When you don't want to use a prebuilt docker image, you can also build it yourself.

First, open the terminal and navigate to the top level PhASAR directory. This folder should contain a Dockerfile file. If not, please check your current branch. To build the image, type

docker build -t phasar:latest .

This can take some time and will utilize as many cores of your machine as you have assigned to the docker engine. Note: This build-process requires an internet connection as it needs to install all PhASAR-dependencies.

Run PhASAR from a Container

Once you have installed docker and have a PhASAR-image available on your computer, running it is easy:

docker run phasar

Appending any command-line parameters will pass them directly to PhASAR. For example docker run phasar --help will display the help-screen of PhASAR.

Accessing files from container

There are several analyses, which (can) write their analysis-results into a file. As without docker, you can specify the results-file with the -O parameter. But this file will now be created and written to only in the container. Additionally you may want to copy LLVM-IR to the container in order to analyze it.

There are two ways to do this:

Option 1: Redirect phasar's stdout into a file

This is probbaly the easiest option, as it does not require any docker cp or binding volumes. However, it assumes that the output can be written into a single file.

Example

Consider the example file simple.ll. It contains the constant variables %2,%3 and %4 (alias the variables i, j and k from the .cpp file). We now run a linear constant propagation to check this property:

docker run phasar -m ./examples/llvm-hello-world/target/simple.ll -D ide-lca > lca-report.txt

Option 2: Bind a volume

When you have large/many source files, it may be very cumbersome to copy each file to the container. Instead you can mount the directory, where the source files live, directly to the container and write back the results in this "shared folder".

docker run --mount type=bind,source=<your-source-folder-on-host>,target=<mount-point-in-container> phasar <args>

Example

Consider now the example of a linear constant analysis from above. Then you can use the following command to run the analysis on this file and write back the results to ./lca-results/ on the host system:

mkdir -p lca-results # Create results-folder
docker run --mount type=bind,source=$(pwd)/,target=/usr/src/example/ phasar -m ./examples/llvm-hello-world/target/simple.ll -O /usr/src/example/lca-results -D ide-lca