Installing and Running SPF from the command line?

[Luke Yi]

I found few documents for installing SPF. The README.md file in the repo https://github.com/SymbolicPathFinder/jpf-symbc has instructions for installing in Eclipse. I wonder if I can install and run SPF from the command line. I found this relevant discussion: https://groups.google.com/g/java-pathfinder/c/fvYID669dII , but I didn't find much useful information there. The official website (http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc/doc) mentioned in the discussion cannot be opened now. Are there any documents/materials/instructions for installing and running SPF from the command line? Thanks!

[Yannic Noller]

Hi Luke! 

For a stable version I can recommend to take the latest SPF version from its master branch: https://github.com/SymbolicPathFinder/jpf-symbc and I usually use the jpf-core version for Java 8 from its specific branch: https://github.com/javapathfinder/jpf-core/tree/java-8. I have not tried it with later version from jpf-core. But I am happy to assist if there are any issues.

For its installation you would need to correctly set up the site.properties file in your home directory and build jpf-core and jpf-symbc accordingly.

To configure SPF you need to have a proper .jpf configuration. You can find the some SPF specific elements and sample configuration here: https://github.com/SymbolicPathFinder/jpf-symbc/wiki/Documentation

Running SPF from the command line is then not very different from JPF. For example:

DYLD_LIBRARY_PATH=/Users/yannic/repositories/jpf-symbc/lib \

  java -Xmx1024m -ea \

  -cp "/Users/yannic/repositories/jpf-symbc/build/*:/Users/yannic/repositories/jpf-core/build/*" \

  gov.nasa.jpf.tool.RunJPF \

  /Users/yannic/repositories/jpf-symbc/src/examples/TestZ3.jpf

• The DYLD_LIBRARY_PATH is for MacOS. You may need to change this to match your platform. It sets the java library path that should include SPF's lib folder to use the available solvers.
  
• Carefully set the correct paths to the class files (i.e., the build folders).
• You can use the gov.nasa.jpf.tool.RunJPF class to start the process and pass the .jpf file as parameter.

Just in case if it matters: Additionally, you could also call SPF directly in a Java program by creating a JPF object. Let me know if you need more information on that. 

I hope this helps! Let me know if there are more questions.

-- Yannic

[Luke Yi]

Hi Yannic,

Thanks for your help! I have run some examples in src/examples and it seems the SPF is running correctly on my Mac now. The SIP in Mac stuck me for a while, as it made the DYLD_LIBRARY_PATH not working, and I had to disable it following https://developer.apple.com/documentation/security/disabling_and_enabling_system_integrity_protection . I have some questions about how I run it though:

1. I tried to run your command on src/examples/ByteTest.jpf, and I got "java.lang.NoClassDefFoundError: com/microsoft/z3/Expr". Then after I added "jpf-symbc/lib/*" or just "jpf-symbc/lib/com.microsoft.z3.jar" to the Java classpath, it runs fine. Is this expected? If yes, should I add "jpf-symbc/lib/*", or only "jpf-symbc/lib/com.microsoft.z3.jar" suffices?

2. I see that TestZ3.jpf specifies that the two parameters of testMod should be symbolic, so there should be more than one branch to explore. However, when I run src/examples/TestZ3.jpf, I only got "java.lang.ArithmeticException: div by 0" for the "testMod" method, which seemed like the two parameters are not made symbolic. Is this expected?

Thanks again for your help. I will prepare a reproducible script for installing the SPF and share it here.

Best,

Luke

[Luke Yi]

Thanks to Yannic's help, I have successfully installed and run the SPF from the command line. Here is the bash script to set up the SPF in unix-based systems, following our discussion here. I hope others can benefit from the script.

Best Wishes,

Luke