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-folder with the -O parameter. But this folder 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 probably the easiest option, as it does not require any arcane docker-commandline options.

However, it assumes that the output can be written into a single file, and you cannot use the -O option of phasar-cli . Also, may need to docker cp the IR files to analyze into the docker container first.

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 multiple result files or large/many project files to analyze, you may want to mount a "shared folder" where the project-files live that should be analyzed. The result files will be written back into the same "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