Harsh4902 / modbat-JPF

repo for docker image of Modbat-JPF integration
0 stars 0 forks source link

jpf-nhandler needs to be setup to handle file reads #1

Open cyrille-artho opened 2 months ago

cyrille-artho commented 2 months ago

With the current setup, we can run Modbat on small examples. Two features don't work at the moment:

  1. Obtaining the version number of Modbat; this happens when you use -h or -v. The version number is obtained from the metadata of modbat.jar. Therefore, options like -v read that metadata and display it.

In JPF, Modbat is /not/ run from its JAR file, but instead directly via its main entry point in modbat.mbt.Main. The JAR file is therefore not available.

To fix problems with -v or -h, we might need a small modification of Modbat, to print some default value if the data from the JAR file cannot read.

Fix: Try to see if you can get a valid package handle if the current way does not work in config/src/main/scala/modbat/config/Version.scala. If that's not possible, provide a default string.

To work on this, it's best to create a new, small, isolated test case first that calls these API methods on ClassLoader. We want to test if the information in the ClassLoader instance in JPF is incomplete, or if some information is really not available when loading a class directly instead of from a JAR file.

There may already be similar tests for JPF's classloader that you can build on.

  1. The heuristic to print more readable transition names fails, because the bytecode cannot be read. Class modbat.util.SourceInfo uses the Java library class JarFile to read contents from a JAR file. It seems like methods such as jar.getInputStream fail.

A correct configuration of jpf-nhandler might be able to fix this.

cyrille-artho commented 2 months ago

If you put code inside a call to verifyNoPropertyViolation, you run it as part of a unit test that uses JPF:

https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests

Code outside that statement runs as a unit test on the JVM. If you comment out if (verifyNoPropertyViolation()) { and the closing curly brace, then you run the test on the JVM, where it should pass (and show you the "normal" behavior). If you use JPF, then we can see if something behaves differently and needs to be fixed.

A fix can be a better jpf-nhandler configuration or an enhancement of a model class.

Harsh4902 commented 2 months ago

@cyrille-artho I have delegated getDefinedPackage method to host jvm using nhandler.spec.delegate = java.lang.ClassLoader.getDefinedPackage. Now I am getting some error while running -v stack trace of error is given below. I am not able to find where should I look to resolve this error, please suggest a way to tackle this.

[SEVERE] JPF exception, terminating: exception in native method java.lang.ClassLoader.getDefinedPackage
java.lang.ArrayIndexOutOfBoundsException: Index 7 out of bounds for length 2
    at gov.nasa.jpf.vm.NamedFields.getReferenceValue(NamedFields.java:85)
    at gov.nasa.jpf.vm.ElementInfo.getReferenceField(ElementInfo.java:1156)
    at nhandler.conversion.jvm2jpf.JVM2JPFGenericConverter.setInstanceFields(JVM2JPFGenericConverter.java:132)
    at nhandler.conversion.jvm2jpf.JVM2JPFConverter.updateJPFNonArrObj(JVM2JPFConverter.java:267)
    at nhandler.conversion.jvm2jpf.JVM2JPFConverter.getUpdatedJPFObj(JVM2JPFConverter.java:189)
    at nhandler.conversion.jvm2jpf.JVM2JPFConverter.updateJPFObj(JVM2JPFConverter.java:66)
    at OTF_JPF_java_lang_ClassLoader.getDefinedPackage__Ljava_lang_String_2__Ljava_lang_Package_2(OTF_JPF_java_lang_ClassLoader.class)
    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)
    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.JPF.start(JPF.java:189)
    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.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
pparizek commented 2 months ago

I am not sure it is a good idea to delegate specific method from ClassLoader, because it's model class and native peer is quite inherent to how JPF works internally. But still I can look for the root cause of this error. Can you post what commands have you run to get this error?

Harsh4902 commented 2 months ago

@pparizek I used java --add-opens java.base/jdk.internal.loader=ALL-UNNAMED -jar /root/jpf/jpf-core/build/RunJPF.jar ModbatTest4.jpf and then I got this error.

cyrille-artho commented 2 months ago

Pavel is right, JPF has its own class loader and class metadata. You therefore want to use that, as you might otherwise run into discrepancies. For example, JPF uses model classes to replace existing library classes, but the native JVM would not know about that and return metadata about the wrong class.

Harsh4902 commented 2 months ago

Okay, so we have to make changes in ClassLoader class. getDefinedPackage is a native method in this class, can we modify it?

pparizek commented 2 months ago

You can define the method in the model class as normal (Java-only) or native, and in the case of native method you need to create a native peer method too. If the method is native in the standard JDK (host JVM), then it does not have to be native in the JPF model class.

Harsh4902 commented 2 months ago

@pparizek thank you. I am starting with inspecting the ClassLoader of standard JDK.

pparizek commented 2 months ago

Besides that, I tried to run setup.sh on my Ubuntu computer with fresh installation of OpenJDK 11 and Scala 2.11.12, and got an error in build file '/tmp/m-jpf/jpf-nhandler/build.gradle' line: 12.

Details: A problem occurred evaluating root project 'jpf-nhandler'. .jpf directory cannot be found

It is probably related to this line: implementation files(jpf.Jar.getFullPath())

Harsh4902 commented 2 months ago

@pparizek I have made one change in setup.sh. Can you please try it again?

pparizek commented 2 months ago

It still does not work and fails with the same error message. I believe there is a problem with "jpf.Jar.getFullPath()" in implementation files(jpf.Jar.getFullPath()) at line 12 of jpf-nhandler/build.gradle. Maybe some dependency has to be downloaded or specified manually? Do you have locally some environment variables or other settings that I may not have defined?

Harsh4902 commented 2 months ago

@pparizek Okay, let me check again.

pparizek commented 2 months ago

My guess is that it does not see the directory /tmp/.jpf/, and has no way of getting to it. Maybe it assumes that .jpf is located in $HOME. I tried to copy /tmp/.jpf to my $HOME and it helped somehow.

cyrille-artho commented 2 months ago

Are you referring to a location for site.properties? You can try passing an argument called site or jpf.site to JPF, which can override the location of site.properties. I think this still works: site=/tmp/m-jpf/site.properties If you add this to your .jpf configuration file (or the command line options, with +site=...), then you can supply your own site.properties that configurations nhandler in the right way.

pparizek commented 2 months ago

The script build.gradle in jpf-handler expects to find site.properties in $HOME/.jpf apparently. It was the build process of jpf-nhandler that was failing. So when I put a copy of site.properties into $HOME/.jpf, everything started to work.

cyrille-artho commented 2 months ago

I see. I think we can still use a different site.properties at run-time for testing. I would prefer that, as I modify my own (large) site.properties file often for different use cases, so tests would be brittle if they relied on the user's settings rather than having their own.

Harsh4902 commented 2 months ago

@cyrille-artho @pparizek I have found one interesting thing. Package modbat.mbt can be loaded by the JPF, but there is one variable versionInfo of Package class which is null every time and that's why toString or any other methods which are using this variable is not working, and it's throwing NullPointerException.

I have created a test case in this PR which can demonstrate this failure.

cyrille-artho commented 2 months ago

Thanks! I think this is not so easy to fix. If I remember correctly, much of the metadata and version number are obtained through loading the code from its JAR file. When running Modbat through a unit test, that file is not directly accessible (not in the same way as usual), and some of the metadata might not be correctly visible. This will at least affect the version number and commit hash metadata, which are in META-INF in the JAR file. Perhaps we can fix the package metadata (package name etc.), which will likely work by hooking into JPF's own metadata for this.

cyrille-artho commented 2 months ago

For our purposes, it is not important that versionInfo is accurate for testing, as long as it returns a value that is safe to use. As we cannot retrieve the information when the code is executed differently than normal, returning an empty string might be a good fallback option. However, we don't want to hard-code an empty string in JPF's model classes if we can avoid that. Perhaps jpf-nhandler can be configured to return certain constants for certain methods? The other package metadata (such as the name) can probably be retrieved somehow.

Harsh4902 commented 1 month ago

@pparizek @cyrille-artho I added a new file temp.sh to this repo in which I have changed origin of modbat and jpf-core. In jpf-core I have added implementation of some methods in java.lang.Class and java.lang.ClassLoader by which now we can use Class.getPackage() method to get package of current class. Same way in modbat I have changed constructor of modbat.config.Version class which now can accept both object of String and Package class. By this way we can run -v and -h in modbat on JPF. Still there are exception which is thrown by JPF but still we get ouput of -v and -h.

Harsh4902 commented 1 month ago

Here is the full output of runnig modbat with -h argument on JPF:

JavaPathfinder core system v8.0 (rev 0916082fac91405e11ec7ce55f9068ce84d61aaa) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
modbat.mbt.Main.main("-h")

====================================================== search started: 6/28/24, 9:50 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
scala modbat.jar vnull rev null
Usage: scala modbat.jar [--OPTION=value] ... CLASSNAME
  -h, --help                    show this help and exit
  -s, --show                    show current configuration
  -v, --version                 show version number and exit
      --[no-]redirect-out       redirect output to log file
      --[no-]init               run initialization code
      --[no-]shutdown           run shutdown code
      --[no-]setup              execute setup methods before each test
      --[no-]cleanup            execute cleanup methods after each test
      --[no-]delete-empty-log   remove empty log files after test
      --[no-]remove-log-on-success remove non-empty log files on success
      --[no-]dotify-coverage    show coverage in dot file format
      --[no-]dotify-path-coverage show path coverage in dot file format
      --path-coverage-graph-mode path coverage graph mode: abstracted or full graph
      --[no-]path-label-detail  show detailed label in path coverage graphs
      --[no-]bfsearch-fun       use user-defined search function of path coverage graphs
      --dot-dir                 output directory for dot files
      --[no-]stop-on-failure    stop model exploration after a test failed
      --[no-]precond-as-failure test fails if scala.Predef.requires fails
      --[no-]print-stack-trace  print stack trace of uncaught exception
      --[no-]show-choices       show choices inside transitions [1]
      --classpath               overrides environment variable CLASSPATH if set
      --log-path                output path for traces
      --log-level               level at which messages are logged
  -s, --random-seed             random seed for initial test
      --abort-probability       probability of aborting test sequence
      --maybe-probability       probability of executing "maybe" statement
  -n, --n-runs                  number of test runs
      --mode                    usage mode (execute tests or generate dot file)
      --search                  search mode (for usage mode=exec)
      --bandit-tradeoff         bandit trade off value (for usage search=heur)
      --backtrack-t-reward      backtrack transition reward (for usage search=heur)
      --self-t-reward           self-loop transition reward (for usage search=heur)
      --good-t-reward           good and successful transition reward (for usage search=heur)
      --fail-t-reward           failed transition reward (for usage search=heur)
      --precond-pass-reward     passed precondition reward (for usage search=heur)
      --precond-fail-reward     failed precondition reward (for usage search=heur)
      --assert-pass-reward      passed assertion reward (for usage search=heur)
      --assert-fail-reward      failed assertion reward (for usage search=heur)
      --loop-limit              limit times same state is visited; 0 = no limit
      --[no-]auto-labels        use auto-generated labels if no label given
[1] Error trace shows internal choices; dot output shows choices and launches.
    Note: Nested choices and coverage of choices currently not supported.
[WARNING] orphan NativePeer method: java.net.URLClassLoader.<init>()V
[WARNING] orphan NativePeer method: java.net.URLClassLoader.<init>(Ljava/lang/ClassLoader;)V
[SEVERE] JPF exception, terminating: exception in native method java.lang.ClassLoader.findSystemClass
java.lang.NullPointerException
    at gov.nasa.jpf.vm.Types.getClassNameFromTypeName(Types.java:751)
    at gov.nasa.jpf.vm.JPF_java_lang_ClassLoader.findSystemClass__Ljava_lang_String_2__Ljava_lang_Class_2(JPF_java_lang_ClassLoader.java:117)
    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)
    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.JPF.start(JPF.java:189)
    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.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
cyrille-artho commented 1 month ago

Great, it's nice to see this work. The version number/string is not available except via the JAR file, so they can be null, as Modbat does not crash with them being null. The new problem is now due to URLClassLoader not being fully supported. I suggest you make a small test case to reproduce this issue in isolation.

Harsh4902 commented 1 month ago

@cyrille-artho @pparizek There is loadModelClass method in modbat.mbt.MBT class which tries to load model class while running modbat. when we are using -v or -h then there variable modelClass is null in modbat.mbt.Main. this is the reason we are getting NullPointerException. That's why I have add some extra check in loadModelclass method. new implementation is here:

def loadModelClass(className: String): Unit = {
    /* load model class */

    if (className == null)
      return

    try {   
      val classloader =
        new URLClassLoader(classLoaderURLs,
                           Thread.currentThread().getContextClassLoader())
      modelClass = classloader.loadClass(className)
    } catch {
      case e: ClassNotFoundException => {
        log.error("Class \"" + className + "\" not found.")
        throw e
      }
    }
  }

Now we can safely run modbat on JPF. Result after this change:

JavaPathfinder core system v8.0 (rev 0916082fac91405e11ec7ce55f9068ce84d61aaa) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
modbat.mbt.Main.main("-h")

====================================================== search started: 7/1/24, 4:37 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
scala modbat.jar vnull rev null
Usage: scala modbat.jar [--OPTION=value] ... CLASSNAME
  -h, --help                    show this help and exit
  -s, --show                    show current configuration
  -v, --version                 show version number and exit
      --[no-]redirect-out       redirect output to log file
      --[no-]init               run initialization code
      --[no-]shutdown           run shutdown code
      --[no-]setup              execute setup methods before each test
      --[no-]cleanup            execute cleanup methods after each test
      --[no-]delete-empty-log   remove empty log files after test
      --[no-]remove-log-on-success remove non-empty log files on success
      --[no-]dotify-coverage    show coverage in dot file format
      --[no-]dotify-path-coverage show path coverage in dot file format
      --path-coverage-graph-mode path coverage graph mode: abstracted or full graph
      --[no-]path-label-detail  show detailed label in path coverage graphs
      --[no-]bfsearch-fun       use user-defined search function of path coverage graphs
      --dot-dir                 output directory for dot files
      --[no-]stop-on-failure    stop model exploration after a test failed
      --[no-]precond-as-failure test fails if scala.Predef.requires fails
      --[no-]print-stack-trace  print stack trace of uncaught exception
      --[no-]show-choices       show choices inside transitions [1]
      --classpath               overrides environment variable CLASSPATH if set
      --log-path                output path for traces
      --log-level               level at which messages are logged
  -s, --random-seed             random seed for initial test
      --abort-probability       probability of aborting test sequence
      --maybe-probability       probability of executing "maybe" statement
  -n, --n-runs                  number of test runs
      --mode                    usage mode (execute tests or generate dot file)
      --search                  search mode (for usage mode=exec)
      --bandit-tradeoff         bandit trade off value (for usage search=heur)
      --backtrack-t-reward      backtrack transition reward (for usage search=heur)
      --self-t-reward           self-loop transition reward (for usage search=heur)
      --good-t-reward           good and successful transition reward (for usage search=heur)
      --fail-t-reward           failed transition reward (for usage search=heur)
      --precond-pass-reward     passed precondition reward (for usage search=heur)
      --precond-fail-reward     failed precondition reward (for usage search=heur)
      --assert-pass-reward      passed assertion reward (for usage search=heur)
      --assert-fail-reward      failed assertion reward (for usage search=heur)
      --loop-limit              limit times same state is visited; 0 = no limit
      --[no-]auto-labels        use auto-generated labels if no label given
[1] Error trace shows internal choices; dot output shows choices and launches.
    Note: Nested choices and coverage of choices currently not supported.

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

====================================================== statistics
elapsed time:       00:00:00
states:             new=13,visited=0,backtracked=13,end=1
search:             maxDepth=13,constraints=0
choice generators:  thread=13 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=12), data=0
heap:               new=6836,released=2978,maxLive=3729,gcCycles=13
instructions:       645313
max memory:         90MB
loaded code:        classes=597,methods=12045

====================================================== search finished: 7/1/24, 4:37 AM
Harsh4902 commented 1 month ago

@pparizek @cyrille-artho You can use temp.sh file to verify results on you system.

cyrille-artho commented 1 month ago

Hi, Thank you for noticing. I think the idea of your fix works, but loadModelClass should never be called in such situations. Instead, a fix in Main.run seems better:

There is already a line that response to modbat.config.ConfigMgr.parseArgs returning None:

        case None => // nothing

For some reason, that case block is empty. It should return instead (and the comment should read "exit" or similar).

Can you please try that change? If the tests then pass (including the tests in bin/test.sh), please make a PR for Modbat.

(I don't know why this does not result in a NPE when running Modbat normally; otherwise, I would have caught this long ago.)

Harsh4902 commented 1 month ago

@cyrille-artho I have raised PR for the same on gitlab. I am raising one more PR in which I have added a constructor in Version.scala class which now can accept object of Package class as well and made some changed accordingly. Please check that also.

Harsh4902 commented 1 month ago

@pparizek @cyrille-artho I have created a Dockerfile, so now we can run this in a separate environment for testing purposes. One missing thing in the Dockerfile is the JAVA_HOME variable, but we cannot set it in the Dockerfile because we cannot determine whether the image is ARM-based or AMD-based. Therefore, we have to configure it manually before running the scripts.

cyrille-artho commented 1 month ago

Great, this also works on another computer I am using that has docker. However, I get failures for all unit tests of jpf-nhandler. Perhaps this was a minor configuration issue on my side. The tests for Modbat with JPF still pass.

As the next steps, please:

  1. Document how to use the Dockerfile by updating README.md of this repo.
  2. Try the minor update that sets JAVA_HOME with a wildcard so it works for both ARM and AMD.
  3. See if you can reproduce the failing jpf-nhandler unit tests on AMD.
  4. Write scripts to automate the testing of common usages of Modbat: -v and -h, and running Modbat on a model.

At some point, we'll run into Modbat not being able to read class files, so we'll have to look into how to support this with JPF and jpf-nhandler then. It is possible that jpf-nhandler still works correctly even if the unit tests failed, because the configuration will be different when it's used together with the application.

Harsh4902 commented 1 month ago

@cyrille-artho @pparizek I have added test.sh which will run common usages of modbat. Also updated README file for the same.

cyrille-artho commented 1 month ago

Thanks, it looks like this mostly works.

Please double-check what the working directory for your scripts (setup.sh and test.sh) should be. The README also uses /utils as the path for these scripts, but it should be /root/utils.

Finally, all the tests work as expected, except that I get one indication of problems in /root/utils/190abff3778.err:

[ERROR] Class file modbat/examples/SimpleModel$$anonfun$1.class cannot be loaded.
[ERROR] modbat/examples/SimpleModel$$anonfun$1.class: file not found

(same for other files named $2, $3, etc.)

So the script test.sh shows that everything works except loading content from a JAR file. As we discussed earlier, a small test case for JPF is best to narrow down what needs to be changed (in JPF's model classes or native peers or the jpf-nhandler setup) to make that work. Once you have that working as a small-ish JPF unit test, we can transfer the setup to Modbat.