NumericValueChecker incorrectly reports out-of-range error

[ChangWan723]

I encountered an issue with NumericValueChecker in JDK 11, where it incorrectly reports a variable as out of range, even though the variable's value is clearly within the specified range. This behavior seems like a bug, but I'm not quite sure.

Could you please clarify if this is a bug? Or is there something wrong with my usage?

---

Test Code Example:

public class NumericTest extends TestJPF {
    static class C2 {
        void doSomething() {
            double x = 0.5;
        }
    }

    @org.junit.Test
    public void testVars() {
        if (verifyNoPropertyViolation("+listener=.listener.NumericValueChecker",
                "+range.vars=x",
                "+range.x.var=*$C2.doSomething():x",
                "+range.x.max=0.9")) {
            C2 c2 = new C2();
            c2.doSomething();
        }
    }
}

The NumericValueChecker should verify that the local variable x in method doSomething is within the specified range (i.e., x <= 0.9). Since the value of x is 0.5 , no error is expected to be reported. But it reported an error (0.500000 > 0.900000):

Error Message:

====================================================== error 1
gov.nasa.jpf.listener.NumericValueChecker
local variable x out of range: 0.500000 > 0.900000
	 at project.jpf.NumericTest$C2.doSomething(NumericTest.java:9)

[shreyasCs012]

I think the problem is in the check() method of the listener NumericValueChecker Here is an isolated test to see the error is present in the check() method :

 @Test
    public void test_check() {
        if (verifyNoPropertyViolation()) {
            NumericValueChecker.FieldCheck obj = new NumericValueChecker.FieldCheck(null, 4.9e-324, 0.9);
            String actual = obj.check(0.5);
            assertEquals(null, actual);
        }
    }

Error :

JPF found unexpected errors: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.AssertionError: JPF found unexpected errors: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:816)
	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
	at gov.nasa.jpf.listener.VerTrackerTest.test_check(VerTrackerTest.java:19)
	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)


> Task :test
gov.nasa.jpf.listener.VerTrackerTest > test_check FAILED
    java.lang.AssertionError at VerTrackerTest.java:19
Test Execution: FAILURE
Summary: 1 tests, 0 passed, 1 failed, 0 skipped
1 test completed, 1 failed
> Task :test FAILED
FAILURE: Build failed with an exception.
* What went wrong:
Execution failed for task ':test'.
> There were failing tests. See the report at: file:///C:/Users/shrey/jpf-core/build/reports/tests/test/index.html
BUILD FAILED in 11s

[cyrille-artho]

Hi,
I cannot reproduce the bug. On what system are you running the example?
Perhaps on an M-series chip with Mac OS X? In that case, we have to fix the compilation settings, as Mac OS X does not use strict_fp by default in some Java versions. OpenJDK may be affected.
As a result of this, the presentation of floating point numbers in memory may not be standard-conformant, which explains the wrong behavior.

[shreyasCs012]

I am running this on a Windows 11 and OpenJDK version "11.0.24"

[cyrille-artho]

Can you please make a branch with your changes on a forked repo and provide me with the exact command to reproduce the bug? Perhaps it's floating-point (and hardware) dependent, perhaps not.

[shreyasCs012]

I am running this test using Intellij but if you run the command ./gradlew.bat test I think you should see the error :

PS C:\Users\shrey\jpf-core> ./gradlew.bat test

> Task:test

gov.nasa.jpf.listener.NumericValueCheckerTest > test_check FAILED
    java.lang.AssertionError at NumericValueCheckerTest.java:11

By the way when I am using the if (verifyNoPropertyViolation()) it does not recognize the class NumericValueChecker but without that I am getting the expected error

[cyrille-artho]

Without verifyNoPropertyViolation, the code runs as a normal JUnit test on the host JVM, so JPF will not be tested. Such tests tend to pass but test nothing.

I could reproduce the result now, so it is not a floating point issue. I copy the full unit test code for reference below, as the code above lacked the package and import declarations.

package gov.nasa.jpf.test.mc.data;

import gov.nasa.jpf.util.TypeRef;
import gov.nasa.jpf.util.test.TestJPF;

import org.junit.Test;

public class NumericTest extends TestJPF {
    static class C2 {
        void doSomething() {
            double x = 0.5;
        }
    }

    @org.junit.Test
    public void testVars() {
        if (verifyNoPropertyViolation("+listener=.listener.NumericValueChecker",
                "+range.vars=x",
                "+range.x.var=*$C2.doSomething():x",
                "+range.x.max=0.9")) {
            C2 c2 = new C2();
            c2.doSomething();
        }
    }
}

[shreyasCs012]

The problem lies in line 72 :

 } else if (v > (long)max){ //line 72
        return String.format("%f > %f", v, max);
      }

the max value ( 0.9 ) is not used to check the condition rather the value (0.0) is used so the condition ( 0.5 > 0.0) becomes true if the type conversion is not used then the test is passing.

[cyrille-artho]

Yes, I have just adapted the test and found the reason, too. I've pushed a fix to a branch and will merge it once CI has completed.
Thank you very much for helping track this down!

[shreyasCs012]

So is the type conversion a mistake there or was there a purpose doing it ?

[cyrille-artho]

It was a copy/paste mistake (at least that's what it looks like). I've indicated as much in my commit message.

[cyrille-artho]

#496