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.
517 stars 326 forks source link

StringIndexOutOfBoundsException #456

Open eklaDFF opened 1 month ago

eklaDFF commented 1 month ago

@cyrille-artho

Our next error is

---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.lang.String.getBytes
    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 gov.nasa.jpf.test.java.nio.BufferTest.testCharBufferConstructor(BufferTest.java:51)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
    at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.base/java.lang.reflect.Method.invoke(Method.java:568)
    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:77)
    at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.base/java.lang.reflect.Method.invoke(Method.java:568)
    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 jdk.proxy1/jdk.proxy1.$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: java.lang.StringIndexOutOfBoundsException: begin 0, end 3, length 1
    at java.base/java.lang.String.checkBoundsBeginEnd(String.java:4606)
    at java.base/java.lang.String.getBytes(String.java:1732)
    at gov.nasa.jpf.vm.JPF_java_lang_String.getBytes__II_3BI__V(JPF_java_lang_String.java:111)
    at jdk.internal.reflect.GeneratedMethodAccessor11.invoke(Unknown Source)
    at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.base/java.lang.reflect.Method.invoke(Method.java:568)
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
    ... 55 more

It seems like we have problem with java.base/java.lang.String.getBytes() implementation.

This problem is with only one of the failed tests [1/8].

cyrille-artho commented 1 month ago

This one may be a bit more difficult to debug. The problem is a logical problem: The native peer requests four bytes (from 0 to 3), but the string is of length 1. Several possibilities:

Can you create a standalone example from test, with a .jpf file that executes the problematic test through JPF's command line interface? Then, we can try to use the MethodTracker to see what methods are called on the target String.

eklaDFF commented 1 month ago

What will the content of example ? I mean what example will test this ?

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// I tried to find the inner implementation of getBytes(...). And then applied there.

Screenshot 2024-05-30 at 11 41 04 PM

Now our failed tests reduced.

Test Execution: FAILURE
Summary: 1002 tests, 995 passed, 7 failed, 0 skipped

1002 tests completed, 7 failed

> Task :test FAILED

FAILURE: Build failed with an exception.

* What went wrong:
Execution failed for task ':test'.

But why our own logic failed here ?

cyrille-artho commented 1 month ago

What I meant was the following:

  1. Check which class implements the unit test that fails.
  2. Check if the source of that unit test also has a main method. Many JPF tests have that, to facilitate running them as a small stand-alone program. If you can't find a main, add one taking a different JPF test class as an example.
  3. If you run the test from the command line through its main, you get more information about why it fails. There is an internal assumption in the code that no longer holds under Java 11; we first have to find out why the test fails before we can fix it.
eklaDFF commented 1 month ago

running jpf with args: JavaPathfinder core system v8.0 (rev 9e0c5277807c44519d9503f948e92bed91da202a) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test gov.nasa.jpf.test.java.nio.BufferTest.runTestMethod()

====================================================== search started: 03/06/24, 12:14 pm [WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe; [WARNING] orphan NativePeer method: java.util.ResourceBundle.getClassContext()[Ljava/lang/Class; running jpf with args: JavaPathfinder core system v8.0 (rev 9e0c5277807c44519d9503f948e92bed91da202a) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test gov.nasa.jpf.test.java.nio.BufferTest.runTestMethod()

====================================================== search started: 03/06/24, 12:14 pm [WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe; [WARNING] orphan NativePeer method: java.lang.StringCoding.decode([BII)[C [WARNING] orphan NativePeer method: java.lang.StringCoding.encode([CII)[B

====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.misc.ScopedMemoryAccess.registerNatives at jdk.internal.misc.ScopedMemoryAccess.registerNatives(no peer) at jdk.internal.misc.ScopedMemoryAccess.(ScopedMemoryAccess.java:83) at java.nio.BufferMismatch.(BufferMismatch.java:35) at java.nio.ByteBuffer.equals(ByteBuffer.java:311) at gov.nasa.jpf.test.java.nio.BufferTest.testByteBufferConstructor(BufferTest.java:45) 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)

====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} owned locks:java.lang.Class@2d0,java.lang.Class@2d3 call stack: at jdk.internal.misc.ScopedMemoryAccess.(ScopedMemoryAccess.java:83) at java.nio.BufferMismatch.(BufferMismatch.java:35) at java.nio.ByteBuffer.equals(ByteBuffer.java:311) at gov.nasa.jpf.test.java.nio.BufferTest.testByteBufferConstructor(BufferTest.java:45) at java.lang.reflect.Method.invoke(Method.java) at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 03/06/24, 12:14 pm

cyrille-artho commented 1 month ago

I see. We first want to understand what has changed in the string contents for the strings created by BufferTest.testCharBufferConstructor. Please use a debugger or add some logging code to see this. (You may have to log the content in hexadecimal to see exactly what the contents are.)