add PolDet (Pollution Detection) implementation

[y553546436]

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:

1. src/tests/PolDet/PolDetMain.java
2. src/peers/JPF_PolDetListener.java
3. 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.

[cyrille-artho]

Thank you for this contribution. Unfortunately, the build fails. Can you please investigate?
You can click on "Details" next to the Travis CI build info to see the full information.

/home/travis/build/javapathfinder/jpf-core/src/classes/sun/misc/SharedSecrets.java:175: error: cannot find symbol
  public void setJavaObjectInputStreamReadString(sun.misc.JavaObjectInputStreamReadString ignored) {
                                                         ^
  symbol:   class JavaObjectInputStreamReadString
  location: package sun.misc

[y553546436]

Thank you for this contribution. Unfortunately, the build fails. Can you please investigate?
You can click on "Details" next to the Travis CI build info to see the full information.

/home/travis/build/javapathfinder/jpf-core/src/classes/sun/misc/SharedSecrets.java:175: error: cannot find symbol
  public void setJavaObjectInputStreamReadString(sun.misc.JavaObjectInputStreamReadString ignored) {
                                                         ^
  symbol:   class JavaObjectInputStreamReadString
  location: package sun.misc

The build failure is not due to my code. The JPF builds in Travis CI have been failing due to the same reason since this commit : 1f9c880
You can see the Travis CI build logs: https://travis-ci.org/github/javapathfinder/jpf-core/builds
However, in my local machine, the build passes. I guess it is because a different version of Java is used on Travis CI. I use java version 1.8.0_271 in my local machine. Maybe you can try to configure Travis CI to use a newer java version.

[mmuesly]

I can confirm that the mentioned test case is an issue with the build system. #286 should bring in a more recent java version to ci and in the best case this is sufficient to fix the build.

[mmuesly]

@y553546436 could you rebase this PR against the current master? I merged the new build system. After a rebase, this PR should pick up the new CI system and we could easily check whether everything is working nicely now.

[y553546436]

@y553546436 could you rebase this PR against the current master? I merged the new build system. After a rebase, this PR should pick up the new CI system and we could easily check whether everything is working nicely now.

Thanks! I have rebased my commit and it indeed passes all checks now.

[cyrille-artho]

Looks good, thanks a lot! Do you have a test (even a simple one) that confirms that the feature is working as intended? Maybe you can write a JPF unit test that calls your main method with a very simple example, and either test that something expected happens, or at the very least, that the test runs without crashing.

[y553546436]

Looks good, thanks a lot! Do you have a test (even a simple one) that confirms that the feature is working as intended? Maybe you can write a JPF unit test that calls your main method with a very simple example, and either test that something expected happens, or at the very least, that the test runs without crashing.

Can you give me some guideline on how to write a JPF unit test? For example, is there an easy way of writing a test that runs something in the JPF level (instead of the native JVM level) and checks whether the JPF crashes? Besides, after running something in the JPF level, is there some way to check the JPF's output? I didn't find guidelines for this in the wiki and the comment in file TestJPF.java is a bit hard to understand. Thanks a lot!

[cyrille-artho]

Hi Luke, You are right, the wiki page is just an overview; we are always grateful for additional documentation: https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests Perhaps this test can give you some hints: src/tests/gov/nasa/jpf/test/java/io/FileIOTest.java It is in general not so easy to capture JPF's output. You could, for example, work with a listener or write a customer reporter (to report the final result). However, it may be easier to check some key data that your extension detects/reports, and check with one or two assertions if that corresponds to your expectations. Perhaps this can be done? Have two tests that execute one unit test each with your extension, one of them with test pollution and the other one without? Luke Yi wrote:

…

Looks good, thanks a lot! Do you have a test (even a simple one) that confirms that the feature is working as intended? Maybe you can write a JPF unit test that calls your |main| method with a very simple example, and either test that something expected happens, or at the very least, that the test runs without crashing. Can you give me some guideline on how to write a JPF unit test? For example, is there an easy way of writing a test that runs something in the JPF level (instead of the native JVM level) and checks whether the JPF crashes? Besides, after running something in the JPF level, is there some way to check the JPF's output? I didn't find guidelines for this in the wiki and the comment in file TestJPF.java is a bit hard to understand. Thanks a lot! — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#285 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABXV4R3FECME277CFABQKMDTILY5PANCNFSM42IDKU7A>.

-- Regards, Cyrille Artho - http://artho.com/ There is no comfort without pain; thus we define salvation through suffering. -- Cato

[y553546436]

Hi Luke, You are right, the wiki page is just an overview; we are always grateful for additional documentation: https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests Perhaps this test can give you some hints: src/tests/gov/nasa/jpf/test/java/io/FileIOTest.java It is in general not so easy to capture JPF's output. You could, for example, work with a listener or write a customer reporter (to report the final result). However, it may be easier to check some key data that your extension detects/reports, and check with one or two assertions if that corresponds to your expectations. Perhaps this can be done? Have two tests that execute one unit test each with your extension, one of them with test pollution and the other one without? Luke Yi wrote:
…
Looks good, thanks a lot! Do you have a test (even a simple one) that confirms that the feature is working as intended? Maybe you can write a JPF unit test that calls your |main| method with a very simple example, and either test that something expected happens, or at the very least, that the test runs without crashing. Can you give me some guideline on how to write a JPF unit test? For example, is there an easy way of writing a test that runs something in the JPF level (instead of the native JVM level) and checks whether the JPF crashes? Besides, after running something in the JPF level, is there some way to check the JPF's output? I didn't find guidelines for this in the wiki and the comment in file TestJPF.java is a bit hard to understand. Thanks a lot! — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#285 (comment)>, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABXV4R3FECME277CFABQKMDTILY5PANCNFSM42IDKU7A.
-- Regards, Cyrille Artho - http://artho.com/ There is no comfort without pain; thus we define salvation through suffering. -- Cato

Hi Cyrille, thanks to your detailed guideline, I managed to write a JPF test (src/tests/PolDet/PolDetTest.java) that runs PolDet@JPF on the 7 example JUnit tests created by me (src/tests/PolDet/PolDetExamples.java). The 7 example tests contain 3 polluter tests (t2, t5, t6), and PolDet@JPF expectedly reports 2 polluter tests (t2, t5), with t6 being a false negative due to common-root isomorphism (described in my paper). t7 modifies the cache in JPF using reflection, and is correctly classified as not a polluter test.
I have checked this JPF test by running command
./gradlew test --tests PolDetTest
Gradle shows the test passes, and the system output is as expected.

Explanation on the two jars added

Because the PolDet@JPF is dependent on JUnit, I have to provide the JPF test with classpath that contains JUnit dependency (see line 38 in src/tests/PolDet/PolDetTest.java), for which I added two jars (hamcrest-core-1.3.jar and junit-4.12.jar) in src/tests/PolDet .

[cyrille-artho]

Thank you for adding a unit test, this will ensure that the extension's basic functionality still runs when other changes are made to jpf-core.
Your PR includes JAR files for JUnit and its dependency. Could you please try to remove those? These JAR files are supposed to be included automatically by Gradle, so I assume that the build/test still runs without your extra copy.

[y553546436]

Thank you for adding a unit test, this will ensure that the extension's basic functionality still runs when other changes are made to jpf-core.
Your PR includes JAR files for JUnit and its dependency. Could you please try to remove those? These JAR files are supposed to be included automatically by Gradle, so I assume that the build/test still runs without your extra copy.

Thanks for your quick reply. I understand that the copy of these two JAR files are not desirable, but the problem is that Gradle supports these two JAR files automatically in JVM level, but not in JPF level. Because the PolDet@JPF runs JUnit in the JPF level, I have to provide it with JUnit dependency in the JPF test. If I remove the JAR files, the following error occurs:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
 java.lang.ClassNotFoundException: class not found: org.junit.runner.JUnitCore
     at PolDetMain.main(PolDetMain.java:39)
     at PolDetTest.testPolDet(PolDetTest.java:39)
     at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
     at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

My workaround is adding these two JAR files and adding them in the JPF classpath (line 38 in src/tests/PolDet/PolDetTest.java). I didn't find other ways to circumvent the issue without adding the JAR files.

[cyrille-artho]

I see. Gradle produces the right JAR files in ~/.gradle, but of course we cannot use that path directly.
Perhaps it's possible to get this from Gradle?
This should produce the two file names:

configurations.runtimeClasspath.findAll { it.name.endsWith('jar'} && (it.name.contains('junit') || it.name.contains('hamcrest')) }

Is it perhaps possible to produce a gradle app task to run the test, instead of a unit test (where I think we are too limited and cannot pass command line arguments)?
Something like gradle run --args='foo --bar'; probably just using the full runtimeClasspath could work here.
I'm not a Gradle expert, unfortunately, so these are all the pointers I can give you right now.
Please see if you can get it to work.
If not, I can accept this PR under a new branch, and we can create a new ticket for this classpath issue.

[y553546436]

I see. Gradle produces the right JAR files in ~/.gradle, but of course we cannot use that path directly.
Perhaps it's possible to get this from Gradle?
This should produce the two file names:

configurations.runtimeClasspath.findAll { it.name.endsWith('jar'} && (it.name.contains('junit') || it.name.contains('hamcrest')) }

Is it perhaps possible to produce a gradle app task to run the test, instead of a unit test (where I think we are too limited and cannot pass command line arguments)?
Something like gradle run --args='foo --bar'; probably just using the full runtimeClasspath could work here.
I'm not a Gradle expert, unfortunately, so these are all the pointers I can give you right now.
Please see if you can get it to work.
If not, I can accept this PR under a new branch, and we can create a new ticket for this classpath issue.

Thanks for your advice. I have successfully removed the two JARs from the commit. After consideration, I agree with you that it makes more sense to produce a gradle app to run the test. To run PolDet@JPF on the example tests now, we can simply run

./gradlew testPolDet

It also occurred to me that to help people use the tool, we can produce another gradle app that executes PolDet@JPF on a given test class (with given classpath to it). With this gradle app, we can run PolDet@JPF more easily by:

./gradlew runPolDet -PtestClasspath=$CLASSPATH -PtestClass=$CLASSNAME

where $CLASSPATH is the classpath to the test class, and $CLASSNAME is the fully qualified test class name.
In summery, I removed the two JARs and add two gradle apps: 'runPolDet' which executes PolDet on the given test class, and 'testPolDet' which executes PolDet on the example tests in PolDetExamples.java.

[cyrille-artho]

Very nice, thanks! I have just started the CI builds and will get back to it later and merge your PR if the builds pass.

[varad64]

Hello @y553546436, the jpf-core project is currently covered under the Apache License v2.0. And 4 files added as part of your contribution towards support for pollution detection make use of the General Public License (GPL) v3.0. Both of these licenses are not compatible and one cannot contain the other.

Would you please be open to distribute your code under the Apache License as it would help greatly in ensuring license compatibility across the project?

The 4 files currently covered under GPL v3.0 are PolDetSerializer, JPF_PolDetListener, PolDetMain and PolDetExamples.

Thanks in advance!

cc @cyrille-artho @pparizek