`String.equals(Object)` makes JPF on Java 11 crash

Question

`String.equals(Object)` makes JPF on Java 11 crash

quadhier opened this issue 6 months ago · 16 comments

Hi @cyrille-artho , I found a bug in implementation of String.equals(Object) in JPF and it only exists on master branch (for Java 11). A simple program like the following one would reveal this issue.

public class StringCmp {
  public static void main (String[] args) {
    System.out.println("a".equals(new Object()));
  }
}

The fix is straightforward, yet it requires some knowledge of native peers. I think it would be a good candidate for "good first issue". If you agree, perhaps you could tag this issue with the label, allowing new contributors the opportunity to resolve the bug.

Answer 1 · 2024-03-21T07:52:12.000Z

To fix the bug that only exists on the master branch when using String.equals(Object), alter the code in the StringCmp class to correctly compare a String with an Object.

Answer 2 · 2024-03-21T08:06:57.000Z

Hi,
Thank you for finding the bug. In this case, adding a test and fix is indeed easy (as you have already provided the test and adding a test merely involves using the skeleton from https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests).
This fix involves a small change in the native peer.
I'll mark it as a good issue for beginners.

Answer 3 · 2024-03-21T09:31:43.000Z

Hi , @quadhier
I known how to solve this type of problem but unable to get the file which you are talking about .

Answer 4 · 2024-03-21T10:41:42.000Z

Hi , @quadhier I known how to solve this type of problem but unable to get the file which you are talking about .

Which file? If you mean StringCmp.java, I have shown its source code above. Run it with JPF and you could reproduce the crash.

Answer 5 · 2024-03-25T01:21:43.000Z

Hi @cyrille-artho ,
i know the problem's solution but unable to get file which of file contain this bug(#439) , please help me..

Answer 6 · 2024-03-25T07:40:08.000Z

In this case, String needs a new equals method. You can find the model class for String in src/classes.

Answer 7 · 2024-03-25T14:46:47.000Z

Thanks @cyrille-artho...

Answer 8 · 2024-05-20T22:53:11.000Z

@cyrille-artho If you would like, you can assign this issue to me!

Answer 9 · 2024-05-21T06:27:11.000Z

Please go ahead and try to add a test and fix.

Answer 10 · 2024-08-13T03:11:04.000Z

Hey @cyrille-artho I have written a test to check for errors


    @Test
    public void testStringEquals_differentObj(){
        if(verifyNoPropertyViolation()){
            String word="a";
            boolean actual=word.equals(new Object());
            boolean expected =false;
            assertEquals(expected,actual);
        }
    }

Answer 11 · 2024-08-13T06:49:37.000Z

Yes, this test works (in the sense that it fails in the current version of JPF). Please update PR #465 or make a new one, and I will merge it.

Answer 12 · 2024-08-13T07:15:31.000Z

the test has failed and here is the stack trace

---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.equals
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:186)
	at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
	at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1910)
	at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1861)
	at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
	at gov.nasa.jpf.vm.VM.forward(VM.java:1721)
	at gov.nasa.jpf.search.Search.forward(Search.java:937)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
	at gov.nasa.jpf.JPF.run(JPF.java:613)
	at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:675)
	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:806)
	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
	at java11.StringEqualsTest.testStringEqual_differentObj(StringEqualsTest.java:8)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at org.junit.runners.BlockJUnit4ClassRunner$1.evaluate(BlockJUnit4ClassRunner.java:100)
	at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:366)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:103)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:63)
	at org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
	at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
	at org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
	at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
	at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:413)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.runTestClass(JUnitTestClassExecutor.java:112)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:58)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:40)
	at org.gradle.api.internal.tasks.testing.junit.AbstractJUnitTestClassProcessor.processTestClass(AbstractJUnitTestClassProcessor.java:60)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:52)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at com.sun.proxy.$Proxy2.processTestClass(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$2.run(TestWorker.java:176)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
	at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Caused by: gov.nasa.jpf.JPFException: object is not of type java.lang.String
	at gov.nasa.jpf.vm.DynamicElementInfo.getStringBytes(DynamicElementInfo.java:134)
	at gov.nasa.jpf.vm.DynamicElementInfo.asString(DynamicElementInfo.java:99)
	at gov.nasa.jpf.vm.MJIEnv.getStringObject(MJIEnv.java:771)
	at gov.nasa.jpf.vm.JPF_java_lang_String.equals__Ljava_lang_Object_2__Z(JPF_java_lang_String.java:178)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
	... 55 more

JPF internal exception executing: :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.equals
java.lang.AssertionError: JPF internal exception executing: :gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.equals
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:156)
	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:810)
	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
	at java11.StringEqualsTest.testStringEqual_differentObj(StringEqualsTest.java:8)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at org.junit.runners.BlockJUnit4ClassRunner$1.evaluate(BlockJUnit4ClassRunner.java:100)
	at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:366)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:103)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:63)
	at org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
	at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
	at org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
	at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
	at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:413)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.runTestClass(JUnitTestClassExecutor.java:112)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:58)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:40)
	at org.gradle.api.internal.tasks.testing.junit.AbstractJUnitTestClassProcessor.processTestClass(AbstractJUnitTestClassProcessor.java:60)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:52)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at com.sun.proxy.$Proxy2.processTestClass(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$2.run(TestWorker.java:176)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
	at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)

Answer 13 · 2024-08-13T09:51:15.000Z

I assume your fix resolves this? If so, please make a new PR or update the existing one with your new test case.

Answer 14 · 2024-08-13T11:34:42.000Z

the tests have passed for the fixed implementation of the equals method and created a pull request

> Task :compileAnnotationsJava UP-TO-DATE
> Task :processAnnotationsResources NO-SOURCE
> Task :annotationsClasses UP-TO-DATE
> Task :copyLibs UP-TO-DATE
> Task :compileJava UP-TO-DATE
> Task :processResources NO-SOURCE
> Task :classes UP-TO-DATE
> Task :generateBuildInfo
> Task :generateVersion
> Task :copyResources
> Task :compileExamplesJava UP-TO-DATE
> Task :compileClassesJava UP-TO-DATE
> Task :processClassesResources NO-SOURCE
> Task :classesClasses UP-TO-DATE
> Task :compilePeersJava UP-TO-DATE
> Task :processPeersResources NO-SOURCE
> Task :peersClasses UP-TO-DATE
> Task :compileTestJava UP-TO-DATE
> Task :compileModules UP-TO-DATE
> Task :compile UP-TO-DATE
> Task :createAnnotationsJar UP-TO-DATE
> Task :createClassloaderSpecificTestsJar UP-TO-DATE
> Task :createJpfClassesJar UP-TO-DATE
> Task :createJpfJar
> Task :createRunJpfJar UP-TO-DATE
> Task :createRunTestJar UP-TO-DATE
> Task :buildJars
> Task :processTestResources NO-SOURCE
> Task :testClasses UP-TO-DATE
  running jpf with args:
JavaPathfinder core system v8.0 (rev 92265f85d9f5d68adf6604692b5016a518735440) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
java11.StringEqualsTest.runTestMethod()

====================================================== search started: 8/13/24, 5:00 PM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;

====================================================== results
no errors detected

====================================================== search finished: 8/13/24, 5:00 PM
> Task :test
java11.StringEqualsTest > testStringEqual_differentObj PASSED
Test Execution: SUCCESS
Summary: 1 tests, 1 passed, 0 failed, 0 skipped
BUILD SUCCESSFUL in 15s
18 actionable tasks: 5 executed, 13 up-to-date
5:00:53 PM: Execution finished ':test --tests "java11.StringEqualsTest.testStringEqual_differentObj"'.

Answer 15 · 2024-08-13T12:23:44.000Z

Thanks, PR #491 fixes the bug and tests the fix.

Answer 16 · 2024-09-03T03:07:45.000Z

hi @cyrille-artho how can i start contributing in the community