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 or tutorial.

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: Copy the files

You can copy the results-file <results-file-in-container> to a file <results-file-on-host> on the host-system using

docker cp <container-id>:/usr/src/phasar/<results-file-in-container> <results-file-on-host>

and copy the source-file to using

docker cp <llvm-ir-file> <container-id>:<llvm-ir-file-in-container>

where you have to fill in <container-id> with the name or id of the container in which you have run the analysis. You can lookup the container-id using docker ps -a or directly specify a name for the container using --name on docker run or docker create.

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_LinearConstantAnalysis --output results.json
docker ps -a
docker cp 0b9d6e6a283a:/usr/src/phasar/results.json results.json

Then you can inspect the results.json file, which is now copied to the host system.

Note: The container-id 0b9d6e6a283a is specific for this run and will very likely differ on your machine or with different containers.

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. Assume for now, that the source-file simple.ll is located on the host system in the current folder ./. Then you can use the following command to run the analysis on this file and write back the results to ./results.json on the host system:

docker run --mount type=bind,source=$(pwd)/,target=/usr/src/example/ phasar -m /usr/src/example/simple.ll -O /usr/src/example/results.json -D IDELinearConstantAnalysis