Welcome
Welcome to the homepage of the demonstration package for the paper:
P. Braione, G. Denaro and M. Pezzè. JBSE: A Symbolic Executor for Java Programs with Complex Heap Inputs. In Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2015), pp 602-613.
The package provides an environment that allows to demonstrate JBSE with a (hopingly) small setup effort. It contains binary and source code distributions of the experimental subjects and the tools used to produce the experimental data. The supported platforms are Mac OS X (64-bits only), Linux (32- and 64-bits) and Windows (32-bits only).
Contacts
For any issue or suggestion please contact Pietro Braione.
Downloading
You can download the package here. It is a not-so-small (~340 MBytes) .zip file.
Setting up
The demonstration package comes with "batteries included": It contains all the dependencies necessary to execute the experiments and gather the results. The package itself is in the form of an Eclipse workspace, so you will need a working setup of Java 8 and Eclipse (we used the Eclipse Mars distribution, but any more recent Eclipse distribution will suit). As you can see this distribution just contains this instructions file and a folder named FSE2016. Run Eclipse, then select File > Switch workspace... and point to the FSE2016 folder, wherever you want to put it. After bootstrap you will see an Eclipse workspace with five projects:
dataStructures: the project containing the subject programs for the P1-P4 experiment series;
tsafe: same for the P5 experiment series;
closure-37b: same for the P6 experiment series;
closure-72b: same for the P7 experiment series;
FSE2016: this project contains all the code necessary to start the experiments and gather the results.
At this point you will need to set some variables and project dependencies to make everything work. This because there are some tools (Z3, SAT solvers, PALE and MONA) that are binary and come in different versions according to the platform. Therefore you must set some configuration strings so that the right binaries for your platform are used. The only project in the workspace that depends on the binaries is the FSE2016 project, and by default it is configured to work with Mac OS X 64-bits. In the case your operating system is different you must do these two steps:
The Alloy Analyzer needs a reference to a native SAT solver library. Open the Libraries tab of the Configure Build Path settings of the FSE2016 Eclipse project. Then, select alloy-dev.jar and open its drop-down list (click the small triangular arrow on the left of the jar icon). Then, click the Native Library Location row and the Edit... button. The native libraries are in the FSE2016/lib folder, and are contained in folders named after the platform: amd64-mac for Mac OS X 64-bits, x86-linux for Linux 32-bits, amd64-linux for Linux 64-bits, and x86-windows for Windows 32-bits. On Windows native SAT solvers are not used, so you can omit this step.
There is a Java variable in the FSE2016 project that should be set to the operating system. Open the FSE2016 project, then the source folder named runner, and then edit the file runner/Settings.java. On the top of the Settings class you will find the declaration of a static final variable named ARCHITECTURE. You will notice that it is set to the value "amd64-osx". Set it to the same name of the subfolder of FSE2016/lib that contains the binaries for your architecture.
For example, if your platform is Linux 32-bits you must set the native library location of alloy-dev.jar to FSE2016/lib/x86-linux, and set ARCHITECTURE = "x86-linux".
A note on Windows
Alloy on Windows does not use the native SAT solvers, and defaults to the pure Java (and slower) SAT4J solver. This is a limitation of Alloy, not of the demonstration package.
Running the experiments
To run the experiments the FSE2016 project offers a convenient runner that makes the process automatic. It can be invoked from the command line or from Eclipse. The most convenient way to launch the experiments is from Eclipse, by using the (only) launch configuration available in the Eclipse workspace: Under Eclipse click the main menu Run > Run Configurations..., then select Java Application > FSE2016 on the left, click the Arguments tab on the right and under the Program arguments text box insert your favorite command line args as reported below. These are:
[-f <fileName>] [-t <nThreads>] [<nExperiment>]
where:
<fileName> is the name of some experiments file; you will find them under the experiments folder of the FSE2016 project; by default FSE2016/experiments/examples.txt will be used;
<nThreads> is the number of threads in the thread pool; to maximize throughput the FSE2016 experiment runner can use a thread pool and launch many experiments in parallel; by default the number of threads is 1;
<nExperiment> is a line number in the experiments file; if specified, the runner will execute only the experiment at that line number, if not specified all the lines in the experiments file will be processed.
Note that symbolic execution is resource-hungry, both in terms of CPU cycles and in terms of memory consumption. The JVM (Hotspot) setting is -Xms512m -Xmx1024m, but your mileage may vary. If you want to change these setting in the Eclipse launch configuration click the main menu Run > Run Configurations..., select Java Application > FSE2016 on the left, click the Arguments tab on the right and under the VM arguments text box change the amount of memory specified for the -Xms and/or -Xmx options.
If you are more adventurous and want to launch the experiments from the command line, open a shell and change the current directory to the home of the FSE2016 project. Then launch using the following command:
java -Xms512m -Xmx1024m -Djava.library.path=<pathToNativeBinaries> -cp <classPath> runner.FSE2016 [-f <fileName>] [-t <nThreads>] [<nExperiment>]
where:
<pathToNativeBinaries> must be the path to the FSE2016/lib subfolder where the native binaries for your platform are, as discussed in the "Setting up" section;
<classPath> must contain the FSE2016/bin folder and all the jars in the FSE2016/lib folder;
<fileName>, <nThreads> and <nExperiment> are discussed above.
The experiments file format
In the experiments folder of the FSE2016 project you will find some pre-canned experiments files. The files can be used to reproduce the results of the experiments series doubly_linked_list (p1.txt), tree_map (p2.txt), avl_tree (p3.txt), node_caching_linked_list (p4.txt), tsafe, closure37b, and closure72b (p5-7.txt). Beware! The time necessary for reproducing a series of experiments is usually very long. To maximize throughput we sorted the experiments in the files roughly from the fastest to the slowest. You can also find an examples.txt file with a selection of interesting experiments with execution times ranging from few milliseconds to some minutes. If you really want to run all the experiments be ready to wait a lot (in our setting it takes about three-four days to complete everything).
Should you ever mangle with the experiments files, e.g. to finely control which experiments you want to launch, you must be aware of the experiments file format. Every row can be either a comment, when the row is started by a double dash (--), or an experiment in the form:
<subjectName>:<entryPoint>:<solver>
where:
<subjectName> can be one of: doubly_linked_list, tree_map, avl_tree, node_caching_linked_list, tsafe, closure37b, closure72b;
<entryPoint> is the name of the method that must be executed symbolically. For tsafe this is always TS_R_1, for closure37b is always traverse, for closure72b is always process. For the data structures subjects they have form test_<num>, where <num> is a suitable number - they are too many to be listed here, please refer to the settings files P1.txt to P4.txt for a complete list.
<solver> is the name of a solver configuration. It can be one of plainInit (for JBSEZ3), hex (for JBSEHEX), preconditioned (for JBSERepOk), consRepOk (for JBSEConsRepOk), alloy (for JBSEAlloy), or pale (for JBSEPALE).
By using the provided experiments files as templates you can build your own files with the experiments you prefer. For convenience you can also comment out whole regions of an experiments file by putting a /* mark at the beginning of a row, and a */ mark at the end of a row (only beginning and end - no sophisticated parsing, sorry).
Interpreting the output
Every experiment will symbolically execute a method in one of the subject programs, gather the results, and produce them in a single output text file. All the text files are located in the out/ directory of the FSE2016 project, and they are named after their corresponding line in the experiments file, <subjectName>.<entryPoint>.<solver>.txt. The typical content of one of these files will be something like:
This is the Java Bytecode Symbolic Executor's Run Tool (JBSE v.0.7).
Connecting to Z3 at /XXX/YYY/z3.
Starting symbolic execution of method doubly_linked_list/TestDoublyLinkedList:()V:test_X at Mon Jun 08 14:50:57 CEST 2015.
Symbolic execution finished at Mon Jun 08 14:50:58 CEST 2015.
Analyzed states: 5640, Analyzed traces: 25, Safe: 19 (11 concretizable), Unsafe: 4 (2 concretizable), Out of scope: 1 (0 concretizable), Violating assumptions: 1.
Elapsed time: 887 msec, Average speed: 635 states/sec, Elapsed concretization time: 713 msec, (80,38% of total), Elapsed time in decision procedure: 42 msec (4,74% of total).
Let us concentrate on the numbers, and explain how they are related to the numbers reported in the paper's figures.
The traces are either valid or invalid. Valid traces are marked as safe (no assertion violated) or unsafe (some assertion violated). Invalid traces are marked either out of scope (not enough computing resources to analyze them) or violating assumptions (an assumption violation detection can be injected at any point of a symbolic execution by means of instrumentation code).
Traces are either concretizable or not. Concretizable traces are all the traces whose initial symbolic state does not contradict any of the preconditions and data structure invariants. Otherwise the trace is said to be not concretizable.
The measure reported as "# Infeasible execution traces with JBSEsolver" in Figure 3 is the number of valid, not concretizable traces. In the previous example it is (19 - 11) + (4 - 2) = 10. Note that for the subjects TSAFE, Closure37 and Closure72 Figure 3 reports the result of the only symbolic execution, for the Classic Data Structures subjects it reports the quantiles for the population of all the executions.
The measure reported as "Execution time for JBSEsolver wrt JBSEHEX" in Figure 3 is obtained from the elapsed time minus the time of the concretization check, divided by the average time of the HEX technique. In the above example, if the HEX technique would take on average 100 msec to complete, it would be (887 - 713)/100 = 1,74.
What is replicable and what isn't?
If we optimistically assume that this demonstration package has no bugs, then only one of all the previously introduced measures will not be exactly replicable: the execution time.
A small caveat. For maximum replicability we packed the projects with the precompiled binaries for the subject programs. If you want to recompile the subject programs take into account that there is a noticeable difference in the binaries produced by different Java compilers. If you recompile anything with a compiler different from the one we used (the Eclipse Java Compiler 4.4.1) the results may differ. For convenience we included a copy of the Eclipse Java Compiler 4.4.1 under the tools/ folder of the FSE2016 project.