PolDet@JPF
PolDet (Pollution Detection) implementation using Java PathFinder. This tool detects JUnit tests that pollute the shared program state. For more information, read our paper accepted by JPF workshop 2021: https://y553546436.github.io/files/jpf_sen.pdf .
PolDet implementation
PolDet implementation is in the following three files:
- src/tests/PolDet/PolDetMain.java
- src/peers/JPF_PolDetListener.java
- src/main/gov/nasa/jpf/vm/serialize/PolDetSerializer.java
File PolDetMain.java contains class PolDetMain, the entry class to run PolDet. It also contains PolDetListener class, a specialized JUnit listener to call our code before and after the test. File JPF_PolDetListener.java contains the peer class for PolDetListener class. File PolDetSerializer.java contains a specialized JPF state serializer which ignores certain irrelevant parts of the state when serializing.
7 example JUnit test methods are in src/tests/PolDet/PolDetExamples.java, which can be used to check the functionality of PolDet.
Note that no existing code is changed in jpf-core, so it is unlikely that some existing functionality breaks with the changes.
Usage
To run PolDet@JPF:
./gradlew runPolDet -PtestClasspath=$CLASSPATH -PtestClass=$CLASSNAME
where $CLASSPATH
is the classpath to the test class, and $CLASSNAME
is the fully qualified test class name.
To test PolDet@JPF on the 7 example tests in src/tests/PolDet/PolDetExamples.java, run
./gradlew testPolDet
Get the classpath for a Maven project
If you want to run a test class in a Maven project, you can get the classpath containing the class and its dependencies with the following command:
cd $MODULE
CP=$(pwd)/target/classes:$(pwd)/target/test-classes:$(mvn dependency:build-classpath | grep -A1 "\[INFO\] Dependencies classpath:" | tail -1)
For a single-module maven project, MODULE
is the project directory. For a multi-project maven directory, MODULE
is the specific module directory containing the test class. For example, project httpcomponents-client (https://github.com/apache/httpcomponents-client) contains sub-modules like httpclient5 and httpclient5-cache. If your test class is inside httpclient5 module, you should run the CP=...
command in directory httpcomponents-client/httpclient5
to get the correct classpath. To test your classpath, you can run PolDet@JPF on test class org.apache.hc.client5.http.async.methods.SimpleBasicHttpRequests
with the script above. There should be one test method named testCreateMethodUriString
detected as a polluter test.