Master #510

sanidhya00081 · 2025-01-09T16:14:15Z

Integrated a mechanism to detect and prevent invalid INVOKESTATIC calls by validating method properties during runtime in JPF (line 274).
Optimized the test pipeline by using Gradle-native methods to manage input-output dependencies, ensuring task portability and proper execution order.

cyrille-artho

I think there is a typo, please fix it so we can try the CI build/test again.

build.gradle

sanidhya00081 · 2025-01-10T17:24:27Z

yeah sure @cyrille-artho

sanidhya00081 · 2025-01-11T15:28:41Z

Could you suggest me any changes, according to the errors the code encountered. @cyrille-artho

cyrille-artho · 2025-01-11T15:31:53Z

Thanks! The build file works now, but one of the paths seems to be wrong, and D.java is missing in your PR, so it can't be found:

 - Property '$1' specifies file '/home/runner/work/jpf-core/jpf-core/src/main/java/D.java' which doesn't exist.

See the full log here: https://github.com/javapathfinder/jpf-core/actions/runs/12714274234/job/35472592178?pr=510

sanidhya00081 · 2025-01-11T15:37:20Z

Thanks for quoting the issue @cyrille-artho . I would be working on the on some amendments and would come up with a new PR.

…mpileD

sanidhya00081 · 2025-01-12T10:10:05Z

Hey! @cyrille-artho could this issue be assigned to me?

cyrille-artho · 2025-01-12T14:17:53Z

Hey! @cyrille-artho could this issue be assigned to me?

This is a PR, not an issue. I can assign an issue to you once you have made a successful PR.

This version works better than the previous one, but it still results in build failures:

  - Property '$1' specifies file '/home/runner/work/jpf-core/jpf-core/src/main/java/D.java' which doesn't exist.
    
    Reason: An input file was expected to be present but it doesn't exist.
    
    Possible solutions:
      1. Make sure the file exists before the task is called.
      2. Make sure that the task which produces the file is declared as an input.
    
    For more information, please refer to https://docs.gradle.org/8.4/userguide/validation_problems.html#input_file_does_not_exist in the Gradle documentation.
  - Gradle detected a problem with the following location: '/home/runner/work/jpf-core/jpf-core/build/classes/java/main'.
    
    Reason: Task ':createJpfClassesJar' uses this output of task ':modifyAndCompileD' without declaring an explicit or implicit dependency. This can lead to incorrect results being produced, depending on what order the tasks are executed.
    
    Possible solutions:
      1. Declare task ':modifyAndCompileD' as an input of ':createJpfClassesJar'.
      2. Declare an explicit dependency on ':modifyAndCompileD' from ':createJpfClassesJar' using Task#dependsOn.
      3. Declare an explicit dependency on ':modifyAndCompileD' from ':createJpfClassesJar' using Task#mustRunAfter.

I can see that jpf-core appears twice in a row in the path above (jpf-core/jpf-core), which is probably the reason the file is not found.
Gradle build dependency rules have changed a bit recently, so try to see if explicit dependency declarations fix the build.
Make sure that the Gradle build is successful on your system, as this will accelerate the CI/review cycle.

corrected the paths of C.java and D.java Added explicit dependencies in compileTestJava, compileModules, createJpfClassesJar

sanidhya00081 · 2025-01-12T19:17:26Z

The build was successful on my system @cyrille-artho

cyrille-artho · 2025-01-13T08:17:09Z

Great! I can confirm that the new build now works. This resolves the most difficult step.
To completen the work on issue #250, we need two more things:

A test case that demonstrates that JPF incorrectly allows a static call to a non-static method to be executed, even though the "static" keyword had been removed and the file recompiled. You can find out how to write tests to run inside JPF on the wiki: https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests
A fix that adds an additional check for the "static" flag in the method and correctly rejects such a call.

sanidhya00081 · 2025-01-13T09:55:30Z

@cyrille-artho Thanks!! I would surely be working on these two points and will revert back in a day.

checks whether JPF incorrectly allows a static call to a non-static method. The test has passed and the build was successful.

sanidhya00081 · 2025-01-14T16:19:27Z

I have created the test file and have successfully checked whether JPF incorrectly allows a static call to a non-static method. The build was successful. @cyrille-artho

cyrille-artho · 2025-01-14T18:24:26Z

Hi,
Thank you for your first attempt at a test. Note that just because an instance is null, the call is still a dynamic call. Your test therefore does not test the right thing.
A call to a static method is generated by using the class name instead of an instance. Your example C.java does this. If you run C.main against a re-compiled D.java (where the keyword static has been removed), you get a very different exception:

Exception in thread "main" java.lang.IncompatibleClassChangeError: Expected static method

So your test can try that and call C.main instead; C.main then calls D.m, and we get the exception. (You can also call D.m directly from your test, as your regular unit tests will be compiled against the original static version of D.m. So we don't need to keep C.java anymore.)

If you adapt the test, it should first fail, because JPF does not check the static flag properly at run time, so the call to D.m succeeds even if D has been recompiled with a dynamic method.

cyrille-artho · 2025-01-14T18:25:53Z

I think it's a good idea to first try to get a "properly failing" test, so we are sure that the expected exception is checked against in the right way. After that, the one-line change in JPF to fix the test can easily be confirmed as valid by rerunning the test against the fix.

sanidhya00081 · 2025-01-14T18:34:59Z

@cyrille-artho Sure!! I would that and will revert back asap. I have understood the issue. Thank you @cyrille-artho for the clear guidance. It really makes easy for me to proceed towards next steps.

When I am rebuilding, the exception is caught and the test fails with the message.

sanidhya00081 · 2025-01-15T18:37:13Z

I have tested the failure case successfully and have made a PR to show it. But I am not able to get what can I do next. @cyrille-artho can you give me some suggestions.

cyrille-artho

Please remove temp. files and move the test files to the right place. You might not need C.java anymore. Furthermore, the tests no longer compile, so please check your build.

cyrille-artho · 2025-01-16T08:02:08Z

__test__

@@ -0,0 +1 @@
+***


Please remove any temporary files in the PR. Change the test so any such files are removed at the end of the test.

cyrille-artho · 2025-01-16T08:03:06Z

src/main/gov/nasa/jpf/D.java

@@ -0,0 +1,8 @@
+package gov.nasa.jpf;


These files should be in src/test.

Please remove this file (as it is no longer needed, we have src/test/.../D.java now.

cyrille-artho · 2025-01-16T08:03:14Z

src/main/java/C.java

@@ -0,0 +1,7 @@
+class C {


Move to src/test.

cyrille-artho · 2025-01-16T08:03:24Z

src/main/java/D.java

@@ -0,0 +1,3 @@
+class D {


Move to src/test.

cyrille-artho · 2025-01-16T08:06:38Z

As of now, some test files need to be moved to src/test. D.java is not found in one case during compilation, causing it to fail. Please check:

/home/runner/work/jpf-core/jpf-core/src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java:13: error: cannot find symbol
                D.m(); // This should throw IncompatibleClassChangeError after D.java is recompiled without static
                ^
  symbol:   variable D
  location: class StaticCallToNonStaticTest

…emporary files. Stored D.java in src/test. Updated dependencies for JUNIT5. The build was successful.

sanidhya00081 · 2025-01-16T19:19:56Z

@cyrille-artho I have made the suggested changes for cleaning up files and removing them at the end. Made some dependency changes in build.gradle. Updated StaticCallToNonStaticTest.java.

cyrille-artho

Great, you have almost all the points resolved. There are a few changes remaining, but I hope they will be easy to do. Please see my comments.

cyrille-artho · 2025-01-16T19:21:28Z

src/main/gov/nasa/jpf/D.java

@@ -0,0 +1,8 @@
+package gov.nasa.jpf;


Please remove this file (as it is no longer needed, we have src/test/.../D.java now.

cyrille-artho · 2025-01-16T19:22:57Z

src/test/C.java

@@ -0,0 +1,7 @@
+class C {


I think this file can be deleted, as testStaticCallToNonStatic does not use it, and we don't need a standalone example; once testStaticCallToNonStatic works as intended, it is simple enough to copy this to main in an empty class if one wants a standalone program to run the test.

cyrille-artho · 2025-01-16T19:23:07Z

src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java

+    @Test
+    public void testStaticCallToNonStatic() {
+        // Create an instance of D
+        D instance = new D();


Please remove.

cyrille-artho · 2025-01-16T19:23:56Z

src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java

+        // Expect IncompatibleClassChangeError when calling instance.m()
+        try {
+            System.out.println("Calling m() method");
+            instance.m();  // This should throw IncompatibleClassChangeError


This has to be D.m(); (like in C.java).

cyrille-artho · 2025-01-16T19:24:30Z

src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java

+
+        // Expect IncompatibleClassChangeError when calling instance.m()
+        try {
+            System.out.println("Calling m() method");


The println statement here can be deleted, as it is not desirable in a unit test to print to the console.

cyrille-artho · 2025-01-16T19:27:14Z

Thank you very much! The process is mostly working now, but you accidentally changed the static to a dynamic call in the test; please see my comments.

Another thing I have not commented on, for some reason, this time, only one test (for your new feature) was run, rather than over 1000 tests. I don't know if this is due to change in the build/test process in build.gradle or due to caching by GitHub.

cyrille-artho · 2025-01-16T19:34:31Z

Having now tried a clean clone with the test, I see that there is a problem with the new build dependencies.
I also think that the extra dependency is in the wrong order (it should be reversed):

tasks.named('compileTestJava') {
    dependsOn(copyLibs)
    dependsOn(copyResources)
    mustRunAfter(modifyAndCompileD)
}

We want compileTestJava to run before modifyAndCompileD, such that the code of the new test correctly compiles against the static method in D. Only after that, we recompile D.java, which will cause the test against D to fail.
Perhaps the dependency fix will again ensure that over 1000 unit tests (the entire test suite) is used.

cyrille-artho

Regarding build dependencies.

cyrille-artho · 2025-01-16T19:37:59Z

build.gradle

@@ -76,16 +114,20 @@ tasks.named('compilePeersJava') {
 tasks.named('compileTestJava') {
    dependsOn(copyLibs)
    dependsOn(copyResources)
+    mustRunAfter(modifyAndCompileD)


I think this is reversed. I am not very familiar with the Gradle DSL, and the documentation is not 100 % clear, but this dependency and others (even some that have been declared previously) might be redundant or reversed. Please look at the dependencies and ensure that the original unit tests are preserved, so we have again over 1000 tests in the CI build/test.
You can check this by running ./gradlew clean test.

cyrille-artho

The original 1010 now run again, but the new test does not run yet.
I think I've found the incorrect (reverse) dependency in build.gradle; please try to change that and run the tests again.

cyrille-artho · 2025-01-24T08:33:56Z

build.gradle

@@ -76,16 +112,25 @@ tasks.named('compilePeersJava') {
 tasks.named('compileTestJava') {
    dependsOn(copyLibs)
    dependsOn(copyResources)
+    shouldRunAfter(modifyAndCompileD)


This dependency should be the other way around: in the declaration of modifyAndCompileD, that task should run after compileTestJava, so we first compile the tests normally and then modify D.java and re-compile it.

cyrille-artho · 2025-01-24T18:07:22Z

Thanks for tidying up the PR. The 1010 basic tests now run and pass, but the new test does not run for some reason.
One thing you could try is to add a new Gradle target specifically for your new test and run this as a third test-related task in .github/workflows/simple_build.yml:

    - name: Run test on modified class file
      run: ./gradlew xy

(where xy is substituted with the new target).

…ets StaticCallToNonStaticTest. And the build was fine.

sanidhya00081 · 2025-01-27T07:09:27Z

Hey @cyrille-artho I have added a new test to specifically target the StaticCallToNonStaticTest.java. The final build was also successful. So, could you please check it and provide me with needful suggestions.

cyrille-artho

Please also add the new test target to the GitHub action, so the additional test is executed after the regular unit tests have passed.
Please remove lib, as the library dependencies are specified in build.gradle and downloaded automatically.

Removed lib.

sanidhya00081 · 2025-01-27T15:24:24Z

Hey @cyrille-artho I have made the changes assuring the successful build of new test and the old tests.

cyrille-artho · 2025-01-27T15:32:52Z

Thanks! I can see that the new Gradle target runModifiedTest with the test gets started, but for some reason, it does not find the test. There is no JUnit output in that target (and that new test suite should fail until we have a fix). Can you please take a look?

sanidhya00081 · 2025-01-27T17:21:26Z

@cyrille-artho Now my new test is targeting StaticCallToNonStaticTest(). And the output says

StaticCallToNonStaticTest > testStaticCallToNonStatic() STANDARD_OUT
    Static method m() is called!

The build was also successful with successful running of other 1010 tests.

sanidhya00081 · 2025-01-27T17:22:27Z

I checked it with method m() in D.java as first non-static than static @cyrille-artho .

sanidhya00081 · 2025-01-29T10:30:53Z

Hey @cyrille-artho could you please check the changes.

cyrille-artho

Thanks, I can see that the test is now executed.
Please make sure the test expects an exception of the right type, as it currently passes due to JPF not throwing the required exception.
Also, try to remove settings.json and the "cleanup" function unless the latter is really needed.

cyrille-artho · 2025-01-29T14:03:02Z

src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java

+}
+
+    // Cleanup method to delete the temporary file after tests
+    @AfterClass


Is this cleanup function needed? Your new test does not create a temp. file directly. If this happens due to some side effect somewhere, we can ignore it (and add that file to .gitignore).

cyrille-artho · 2025-01-29T14:04:28Z

src/tests/gov/nasa/jpf/StaticCallToNonStaticTest.java

+
+    @Test
+    public void testStaticCallToNonStatic() {
+  D.m();


This test should expect an exception: Try
Assertions.assertThrows(java.lang.IncompatibleClassChangeError, D.m());
This should make the test fail, so we can ensure that the fix that we need is tested against.
After the fix is in place, the test will succeed.

cyrille-artho · 2025-01-29T14:06:46Z

Hi, I've now run the tests and checked the output. Please make the new test *fail* for now, as the required check and exceptions are not there yet. A fix later on will make the test pass.

…

On Wed, Jan 29, 2025 at 11:31 AM sanidhya00081 ***@***.***> wrote: Hey @cyrille-artho <https://github.com/cyrille-artho> could you please check the changes. — Reply to this email directly, view it on GitHub <#510 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABXV4R5MRSBXWUB5UAYGSIT2NCUXJAVCNFSM6AAAAABU4QQC6GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMMRRGI2TCOBUGA> . You are receiving this because you were mentioned.Message ID: ***@***.***>

-- Regards, Cyrille Artho

Now the test first fails with an error and after the correction all the test pass.

Now, first the test fails with an error and later it passes with successful build.

Updated .gitignore by placing seetings.jason into it. The build was successful.

sanidhya00081 · 2025-01-30T15:45:21Z

Hey @cyrille-artho please check my last commits. All the things work as intended. The test first fails and after the correction it passes. I have updated the clean-up thing as well as settings.json.

sanidhya00081 · 2025-01-31T14:33:33Z

@cyrille-artho The failed build has occurred as to show that the test runs against incorrect function.

sanidhya00081 · 2025-01-31T14:34:10Z

Should I now proceed with the correction after that the build will be successful @cyrille-artho

cyrille-artho · 2025-01-31T14:37:19Z

Great job, we now have a test that reproduces the problem. Next, we want to fix the issue.
Most likely, the fix is to be made in src/main/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java, in method execute.
This code handles method calls to static methods. It currently lacks a check to ensure that the invoked method is actually static.
The callee is a JPF-internal data structure of type MethodInfo. Its method isStatic should be an easy way to check whether the invoked method is indeed static when expected to be. In that case, JPF should throw an exception at the level of the application under test (and not within itself).
You can see that you do not want to throw an exception in the usual way, but luckily, the code in execute already has a similar example:

    if (callee == null) {
      return ti.createAndThrowException("java.lang.NoSuchMethodException", cname + '.' + mname);
    }

Helper method createAndThrowException can build the right type of object and return its descriptor in a way that the application will then see a newly constructed exception.
You can add a check on whether the callee instance is static and then throw an exception, very similar to the code above. Of course, the type should be "java.lang.IncompatibleClassChangeError".
We are just a few lines away from resolving this issue now!

cyrille-artho · 2025-01-31T14:41:10Z

Yes, please try the fix I outlined; if it works, all old and new tests will pass.

sanidhya00081 · 2025-02-06T18:26:20Z

Hey @cyrille-artho , I am stuck solving the issue from last 5 days but the concept I am implementing in INVOKESTATIC.java is not wrking properly I think or I can say that it is not throwing exception properly. Here is the code I am implementing in INVOKESTATIC.java inside execute method:

if(!callee.isStatic()) {
      return ti.createAndThrowException("java.lang.IncompatibleClassChangeError", callee.getFullName());
    }

Could you provide me with any suggestions that what could I be doing wrong or any tips or ideas.

cyrille-artho · 2025-02-07T07:19:01Z

Your suggested change looks good. Where in the code did you put the check? What is the result?
You can update your PR with the latest change, which is the easiest way for me to see and test your exact change.

included StaticCallToNonStaticTest.class in test in build.gradle

sanidhya00081 · 2025-02-07T18:18:47Z

@cyrille-artho In my PR you could see that I added the check in INVOKESTATIC.java as suggested. But else everything works fine when I make static in D.java. But when I remove it I think compiler only is rejecting the method saying static reference to non-static function and INVOKESTATIC.java is not working in this case.

cyrille-artho

Method D.m needs to be static when the main source tree is compiled, otherwise, compilation fails.

cyrille-artho · 2025-02-10T08:03:01Z

src/tests/gov/nasa/jpf/test/D.java

+
+public class D {
+    // Non-static method
+    public void m() {


This method should be static but then be compiled separately as a non-static method after an edit (which is made by build.gradle).

sanidhya00081 · 2025-02-10T09:55:50Z

After making D.java static the build runs fine @cyrille-artho . But I am not able to understand that why INVOKESTAITC.java is not throwing exception. Or how the static check in INVOKESTATIC.java helps in our build process.

Added missing static check before execution

c4367a1

cyrille-artho requested changes Jan 10, 2025

View reviewed changes

build.gradle Outdated Show resolved Hide resolved

Corrected the typo (task-> tasks) line 274

3b0d4d5

sanidhya00081 requested a review from cyrille-artho January 11, 2025 14:37

Added the missing file, now the path is correct, in task: modifyAndCo…

fc442af

…mpileD

imported java.nio.file.Files and java.nio.file.Paths

95fde67

corrected the paths of C.java and D.java Added explicit dependencies in compileTestJava, compileModules, createJpfClassesJar

Created the test file StaticCallToNonStaticTest.java

d5a7bf8

checks whether JPF incorrectly allows a static call to a non-static method. The test has passed and the build was successful.

I have made the suggested changes.

04b5b9d

When I am rebuilding, the exception is caught and the test fails with the message.

cyrille-artho requested changes Jan 16, 2025

View reviewed changes

Added a clean up method in StaticCallToNonStaticTest.java to handle t…

23459e9

…emporary files. Stored D.java in src/test. Updated dependencies for JUNIT5. The build was successful.

cyrille-artho requested changes Jan 16, 2025

View reviewed changes

cyrille-artho reviewed Jan 24, 2025

View reviewed changes

Corrected te dependency issue I think this works as intended.

c06462f

I have tried adding a new target task named runModifiedTest that targ…

1decb36

…ets StaticCallToNonStaticTest. And the build was fine.

cyrille-artho requested changes Jan 27, 2025

View reviewed changes

sanidhya00081 added 2 commits January 27, 2025 20:26

Merge branch 'javapathfinder:master' into master

ab1b945

Added new test target to Github action.

892a4c7

Removed lib.

New test is targetting the StaticCallToNonStaticTest()

b758439

cyrille-artho requested changes Jan 29, 2025

View reviewed changes

sanidhya00081 added 3 commits January 30, 2025 15:22

Removed the clean up method and moved settings.jason to .gitignore.

3f8c0ff

Now the test first fails with an error and after the correction all the test pass.

Removed the clean up method and moved settings.jason to .gitignore.

ab0e4b7

Now, first the test fails with an error and later it passes with successful build.

Removed the clean up method.

6685800

Updated .gitignore by placing seetings.jason into it. The build was successful.

Added static check condition in INVOKESTATIC.java.

00a6308

included StaticCallToNonStaticTest.class in test in build.gradle

cyrille-artho reviewed Feb 10, 2025

View reviewed changes

		@@ -0,0 +1 @@
		***

Master #510

Are you sure you want to change the base?

Master #510

Conversation

sanidhya00081 commented Jan 9, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

sanidhya00081 commented Jan 10, 2025

sanidhya00081 commented Jan 11, 2025

cyrille-artho commented Jan 11, 2025

sanidhya00081 commented Jan 11, 2025

sanidhya00081 commented Jan 12, 2025

cyrille-artho commented Jan 12, 2025

sanidhya00081 commented Jan 12, 2025

cyrille-artho commented Jan 13, 2025

sanidhya00081 commented Jan 13, 2025

sanidhya00081 commented Jan 14, 2025

cyrille-artho commented Jan 14, 2025

cyrille-artho commented Jan 14, 2025

sanidhya00081 commented Jan 14, 2025

sanidhya00081 commented Jan 15, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrille-artho commented Jan 16, 2025

sanidhya00081 commented Jan 16, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrille-artho commented Jan 16, 2025

cyrille-artho commented Jan 16, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrille-artho commented Jan 24, 2025

sanidhya00081 commented Jan 27, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

sanidhya00081 commented Jan 27, 2025

cyrille-artho commented Jan 27, 2025

sanidhya00081 commented Jan 27, 2025 • edited Loading

sanidhya00081 commented Jan 27, 2025

sanidhya00081 commented Jan 29, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cyrille-artho commented Jan 29, 2025 via email

sanidhya00081 commented Jan 30, 2025

sanidhya00081 commented Jan 31, 2025

sanidhya00081 commented Jan 31, 2025

cyrille-artho commented Jan 31, 2025

cyrille-artho commented Jan 31, 2025

sanidhya00081 commented Feb 6, 2025

cyrille-artho commented Feb 7, 2025

sanidhya00081 commented Feb 7, 2025

cyrille-artho left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sanidhya00081 commented Feb 10, 2025

sanidhya00081 commented Jan 27, 2025 •

edited

Loading