search

javapathfinder / jpf-core

JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.
533 stars 337 forks source link

Missing check for STATIC method when executing #250

Open ilovejpf opened 4 years ago

ilovejpf commented 4 years ago

Hi! I find that jpf is missing check static method, which can be severe! Let me show you an example. First, you write a class C, which will later be compiled to a method call to use INVOKESTATIC.

cat > C.java <<EOF
class C {
   public static void main(String[] a) {
     int i = 123;
     D.m("foobar");
     System.out.println(i);
   }
}
EOF

Then you write the static method m in class D.

cat > D.java <<EOF
class D {
   public static String m(String s) { return s; }
}
EOF

Then you can run javac C.java D.java to compile, and both java C and java -jar build/RunJPF.jar +classpath=. C should work fine.

Then you remove that static in class D by running sed -i s/static// D.java; javac D.java, then java C will throw IncompatibleClassChangeError as expected.

java.lang.IncompatibleClassChangeError: Expected static method D.m(Ljava/lang/String;)Ljava/lang/String;
    at C.main(C.java:4)

However, java -jar build/RunJPF.jar +classpath=. C will print out 248 (please note that this number should be 123! ) and end up with no errors detected. Missing the check can lead to executing something unexpected and destroy certain variables in the program. The fix may be adding a check for whether the method to be invoked is actually static or not when executing INVOKESTATIC. Thanks!

cyrille-artho commented 4 years ago

Hi, Thank you very much for noticing this. This is an issue that we hope won't be too hard to fix, but it may be difficult to test. We would need the following:

  1. C.java and D.java, which are both compiled as usual during gradle's testCompile phase.
  2. Before the tests run, we'd need a task that (a) creates a modified version of D.java in a temporary directory, (b) compiles it, and (c) moves D.class (the compiled file) to the location of the other compiled files.
  3. Now the tests can run.

This special task in (2) can be implemented using doFirst: https://docs.gradle.org/current/userguide/build_lifecycle.html

The actions inside that task could be implemented as shell tasks, as in: https://discuss.gradle.org/t/run-a-process-before-tests/25690/2

However, this would make this particular gradle task less portable and more failure-prone; it should at the very least not prevent the other tests from running if it cannot execute. Perhaps it's also possible to use a gradle-native task to compile the modified D.java.

What do you think?

alokprince commented 3 years ago

can I try to solve this issue? I am a beginner and I am willing to learn and work on this issue as my first issue.

cyrille-artho commented 3 years ago

You are welcome to work on this, as I'm not aware of anyone else doing so. As I've written earlier, testing this issue is non-trivial.

alokprince commented 3 years ago

I will try my best for this issue.

Venkatesh-24 commented 2 years ago

Hi I am a beginner. Can I try to solve this issue??

cyrille-artho commented 2 years ago

Yes, it seems alokprince is not working on this issue right now, so please give it a try.

Venkatesh-24 commented 2 years ago

@cyrille-artho can you please point me to related documentation and entry point of the codebase.I am new to this repository.

cyrille-artho commented 2 years ago

See the history of this issue and the JPF wiki to get started. A good way to resolve this issue would be to have a test for it first, which (as described above) is not so simple because code has to be compiled twice.

Venkatesh-24 commented 2 years ago

Okay I will try my best to solve it.

shoyebmd424 commented 1 year ago

I can try solve this issue please assign me for this issue

CrypticMessenger commented 7 months ago

Hi @cyrille-artho , can I work on this issue? I have identified the changes and tested locally, it resolves the problem, I am currently working on writing Unit test (the way you suggested in this thread).

cyrille-artho commented 7 months ago

Yes, there is no recent comment from anyone working on this, so feel free to go ahead.

sshaikshoaib commented 4 months ago

Hi I am a beginner. can I work for this issue

cyrille-artho commented 4 months ago

Yes, please give it a try. Manually reproducing the existing incorrect behavior is not very hard, but automating this with a special build target is a bit more work. Try one step first and let us know how far you get.

siddhesh0705 commented 2 weeks ago

Hi, I’m Siddhesh Sangale, and I’m new to open-source contributions. I’m eager to get started by tackling some beginner-friendly tasks that can help me build confidence and gain experience. While I’m just beginning my open-source journey, I’m excited to grow my skills and contribute to impactful projects.

I’m looking forward to working on something meaningful and gradually taking on bigger challenges as I learn. I would appreciate any guidance or suggestions for good starting points.

can you appoint me with this issue ?

cyrille-artho commented 2 weeks ago

Yes, a fix for this is fairly easy, and as long as the issue remains open and there has not been any activity for a while, it's safe to assume that it has not been resolved yet. Feel free to try to fix this in the code, and I can change the issue later to ask for an automated test for this.

siddhesh0705 commented 2 weeks ago

@cyrille-artho can you provide me with the inital steps that how can start with this issue and on which branch I can find this issue ?

siddhesh0705 commented 2 weeks ago

@cyrille-artho I have submitted a Pull Request to address this issue. Could you please review it and provide feedback or suggest any changes needed to meet your requirements?