Remove assert in verify class

[mmuesly]

The failing test case in #294 seems related to this assert statement. If I remove it, the test passes. But I have no clue how this effects in a side effect the ExchangerTest. If we remove it, everything work on my system.

Any ideas why this is the case?

[mmuesly]

Anyhow, removing this assert statement makes CI pass and jitpack.io will work as requested in #290.
Check the jitpack.io build of this commit: https://jitpack.io/com/github/mmuesly/jpf-core/cfee1f0/build.log

[cyrille-artho]

Thanks for identifying the root cause of the problem. I'll get in touch with Luke, who wrote the assertion.

[y553546436]

Sorry for the trouble caused.

I found that the method not actually run when executing the ExchangerTest because even if I replace the assertion line with if (true) throw new AssertionError();, ExchangerTest still passes. Actually, as mentioned in the code comment, this method is not expected to be executed in any way in JPF, but its peer method is expected to run.

I found assertTrue method in Verify.java, which seems to serve the same functionality with assert. After I replace the assert with assertTrue the ExchangerTest passes as well. However, the assertTrue was marked deprecated. Was there any reason why assertTrue method existed (e.g., somehow directly assert in Verify.java would break something)?

I propose to replace assert with assertTrue for now, because they should serve the same functionality. It is even fine to remove it because this method is not expected to run anyhow. It needs further investigation though to figure out the exact reason why the assertion breaks the test.

[cyrille-artho]

@mmuesly : Can you please try this? Perhaps changing assert to assertTrue will resolve this issue as well.
On my local machine, I now get a strange assertion error that hints at a problem with the build; it's the same with assert or assertTrue:

java.lang.AssertionError: JPF internal exception executing: :gov.nasa.jpf.JPF$ExitException: JPF configuration error: class not found gov.nasa.jpf.vm.JVMForwarder
	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 gov.nasa.jpf.test.java.concurrent.ExchangerTest.testTimeoutExchange(ExchangerTest.java:59)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:50)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:47)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:325)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:78)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:57)
	at org.junit.runners.ParentRunner$3.run(ParentRunner.java:290)
	at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:71)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:288)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:58)
	at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:268)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:363)
	at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.runTestClass(JUnitTestClassExecutor.java:110)
	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:38)
	at org.gradle.api.internal.tasks.testing.junit.AbstractJUnitTestClassProcessor.processTestClass(AbstractJUnitTestClassProcessor.java:62)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:51)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:32)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:93)
	at com.sun.proxy.$Proxy2.processTestClass(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.processTestClass(TestWorker.java:118)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.remote.internal.hub.MessageHubBackedObjectConnection$DispatchWrapper.dispatch(MessageHubBackedObjectConnection.java:175)
	at org.gradle.internal.remote.internal.hub.MessageHubBackedObjectConnection$DispatchWrapper.dispatch(MessageHubBackedObjectConnection.java:157)
	at org.gradle.internal.remote.internal.hub.MessageHub$Handler.run(MessageHub.java:404)
	at org.gradle.internal.concurrent.ExecutorPolicy$CatchAndRecordFailures.onExecute(ExecutorPolicy.java:63)
	at org.gradle.internal.concurrent.ManagedExecutorImpl$1.run(ManagedExecutorImpl.java:46)
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
	at org.gradle.internal.concurrent.ThreadFactoryImpl$ManagedThreadRunnable.run(ThreadFactoryImpl.java:55)
	at java.lang.Thread.run(Thread.java:748)

[y553546436]

assertTrue works in my local Mac and a Linux server. If not worked in all platforms, removing the assert is probably also fine.

[cyrille-artho]

assertTrue works on my other computer. It uses the same Java version so it may be some very obscure issue that prevents the build from working properly on the former one.
So let's change the assertion to assertTrue rather than removing it.

[mmuesly]

I found that the method not actually run when executing the ExchangerTest because even if I replace the assertion line with if (true) throw new AssertionError();, ExchangerTest still passes. Actually, as mentioned in the code comment, this method is not expected to be executed in any way in JPF, but its peer method is expected to run.

If this code is not supposed to run, as the peer method takes over all the times, I vote for removing the method body, leaving an empty method with return 0l. This is sufficient for the Peer to get integrated into the execution.

Anyhow, it remains strange that his change has an effect at all.

[y553546436]

It's fine for me to remove the method body as well. If we do that, we might as well remove the method body for the other getBitFlip methods that are below this one.

[cyrille-artho]

Luke Yi wrote:

It's fine for me to remove the method body as well. If we do that, we might as well remove the method body for the other |getBitFlip| methods that are below this one. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#297 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABXV4R4DYXMALXX6DZI4WWTUCCIFZANCNFSM5DVNCNUA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

If both methods are dead (unused) code, then please remove them. Perhaps something strange happens with JPF's class loading in case they cause problems even when not executed. -- Regards, Cyrille Artho - http://artho.com/ Murder is always a mistake -- one should never do anything one cannot talk about after dinner. -- Oscar Wilde, "The Picture of Dorian Gray"

[y553546436]

I checked that after replacing the bodies of all getBitFlip methods in Verify.java with return 0 (or return false for the one that returns boolean), the ExchangerTest passes, and the BitFlipTest also passes, indicating that the change does not affect the bit-flip extension.

[mmuesly]

I did what you said.

[y553546436]

I did what you said.

Thanks a lot! Looks like the checks passed with the new changes.

[cyrille-artho]

OK, I think I see now what happens. The "real" bitFlip is in the native peer src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java. For some reason, the model-class bit flip in Verify caused problems.
If my assumption is correct, it would be better to declare all of these methods native rather than having an empty body. Empty methods will just be confusing for people who come later.
Can you please try to convert them? For example, the first one would become:

 public native static long getBitFlip (long v, int nBit, int len);

(Just put native after the visibility qualifier in each method and remove the body.)
This would also be much cleaner than having minimal method bodies that are never executed.

[y553546436]

That's a good idea. I tried and with the changes you mentioned, the ExchangerTest and BitFlipTest both pass. It may be a nicer way to fix the issue.
I saw many other methods in Verify.java have empty bodies (e.g., setShared), any reason why they were left like that? Should we also try to clean them? I can look into them and make a new PR after this PR is accepted.

[cyrille-artho]

I see. This code is probably really old, because it is from when Nastaran created this git repository in 2017. We don't have the history anymore of these changes, it is quite likely that the methods were written before the Model Java Interface and @MJI annotation features were added to JPF.
I will accept this PR now as is. Please look for methods with empty bodies and convert them to native methods where appropriate. We can then accept those changes as a separate PR.