Docker Image

Get the Image

We enclose the PASTA tool and all experimental subjects in the research paper into a docker image (OSF). The container (pasta-icse21.tar.gz) is ~900 MB and includes all pre-compiled experimental subjects. Researchers can use this package to reproduce our experimental results.

Load the Image

Use the docker load in the command line. Loading the container image may take a few minutes.

$ docker load --input pasta-icse21.tar.gz
114ca5b7280f: Loading ...
...
Loaded image: pasta-icse21:latest

Upon a successful load, you may see the PASTA image in the docker’s image list:

$ docker image ls
REPOSITORY     TAG       IMAGE ID       CREATED          SIZE
pasta-icse21   latest    b06f063db252   xxx              2.44GB

Start a Container

After loading the image, you can start a container to run the experiment, logged in as root. All experimental subjects are located in the /home/dsu/ directory.

$ docker run -it pasta-icse21:latest bash
root@fbd4c1397dae#:/ ls /home/dsu
icse21  pasta-tool

The icse21 directory contains subjects and scripts to run the experiment, and pasta-tool contains a copy of the PASTA tool and necessary libraries. You can run this PASTA exactly like the tutorial:

root@fbd4c1397dae:/home/dsu# java -jar pasta-tool/pasta/pasta-1.0-full.jar
Usage pasta:
  pasta distiller <args>                Distill gadgets from programs.
  pasta synthesizer <args>              Synthesize transformers.
  pasta verifier <args>                 Verify a transformer against test cases.

Run the Experiments

Get into icse21 directory. The ftpserver directory contains 4 changed classes and tomcat80 directory contains 22 changed classes. Details can be found in our research paper.

For all experiments, we assume you’re at the /home/dsu/icse21 directory.

Run Experiment for One Subject

runOne.sh accepts an example as input. You can also specify the timeout value (in minutes) for the synthesizer to run. Preprocessing time is not accounted for the timeout. Preprocessing large projects may take a few minutes.

To try the motivating example in the research paper (SocketProcessor), you may set a 2-minute timeout:

# bash runOne.sh tomcat80/f4451c 2
Run example f4451c from tomcat80
Run dpg
Run distiller
Distill gadgets for tomcat80/f4451c
Distilling   2%  
...
Run synthesizer in verifier mode

After 2 minutes, two log files are generated inside tomcat80/f4451c:

# ls tomcat80/f4451c
summary.log  verifier.log ... ...

The verifier.log contains the generated transformers and their testing results, like:

# cat tomcat80/f4451c/verifier.log
/* -------- Transformer #1 (cost = 2.3684) -------- */
 ... transformer code ...

------------------
Test transformer:
[SuccessRate]   0.6667
[CompareTimes]  3       [IdenticalTimes]        2       [NotIdenticalTimes]     1
[NotIdenticalStates]    TransformerTest.TestSocketNull+socketNull
[IdenticalStates]       TransformerTest.TestSocketNotNull2+socketNotNull
[IdenticalStates]       TransformerTest.TestSocketNotNull1+socketNotNull

This transformer did not pass all test cases (success rate 0.6667). [CompareTimes] means how many tests are executed, [IdenticalTimes] and [NotIdenticalTimes] mean how many tests this transformer passes or fails.

Finally, the summary.log contains a summary of all generated transformers:

# cat tomcat80/f4451c/summary.log
For tomcat80/f4451c:
Number of all tested transformers: 21
Number of all test-passing transformers: 2
Id of the first test-passing transformer: 4

In our 2-minute run, PASTA generated and tested 21 candidate transformers. 2 transformers pass all tests. The first test-passing transformer is the Transformer #4. The algorithm should be deterministic.

Run Batched Experiments for All Subjects

runAll.sh only accepts a timeout value (in minutes, default is 30, for each subject) as its parameter. Synthesizer will execute for that amount of time for each subject. PASTA also generates the verifier.log and summary.log in each subject’s root directory.

Below is an independent full run of PASTA (docker image) with a 15-minute timeout on an Intel i5 machine. For the third column (n/m): n means the n-th test passing transformer is the semantics-correct one; m means how many transformers have been tested when finding the semantics-correct one. All major results in the paper are reproduced (all cases succeeded with a correct transformer also succeeded). There may be slight performance variance due to hardware/software configurations and our minor changes to the implementation.