Bugs needed to be addressed in the sv-comp branch

[sohah]

There are some bugs encountered in the sv-comp branch that we need to fix. This google sheet details the current state. The log files for the run of the sv-comp versus the master branch can also be find here.

[saifk16]

There are some bugs encountered in the sv-comp branch that we need to fix. This google sheet details the current state. The log files for the run of the sv-comp versus the master branch can also be find here.

Will have a look.

[Sameersawant77]

hello @sohah to look into this issue, do we need to change jpf-core to java-8 branch or peterschrammel-sv-comp-run-script branch ? as the current master branch is built using java-11

[sohah]

hello @sohah to look into this issue, do we need to change jpf-core to java-8 branch or peterschrammel-sv-comp-run-script branch ? as the current master branch is built using java-11

@Sameersawant77
No do not use the master branch, please use the sv-comp branch when working on this issue. It requires java 8. The jpf-core is a submodule, so just make sure to update the submodule so it can use the one specified on this branch.

[Sameersawant77]

@sohah I have set up the project using java-8 branch of jpf-core, while trying to run the NumericExample.jpf. I get no libz3java in java.library.path. But i do have it and made an alias in ~/.zshrc. Is it a compatibility issue of libz3java library with intel chip macs and apple silicon chip mac? should i create a Dockerfile for easier and consistent setups? Attaching the steps that i used

sameersawant@Sameers-MacBook-Air jpf-symbc % cat ~/.zshrc
export JAVA_HOME=$(/usr/libexec/java_home -v 1.8)
alias jpf-run='export DYLD_LIBRARY_PATH=/Users/sameersawant/dev/jpf/jpf-symbc/jpf-symbc/lib; java -Djava.library.path=/Users/sameersawant/dev/jpf/jpf-symbc/jpf-symbc/lib'
export NVM_DIR="$HOME/.nvm"
[ -s "$NVM_DIR/nvm.sh" ] && \. "$NVM_DIR/nvm.sh"  # This loads nvm
[ -s "$NVM_DIR/bash_completion" ] && \. "$NVM_DIR/bash_completion"  # This loads nvm bash_completion
sameersawant@Sameers-MacBook-Air jpf-symbc % ls lib                                                                                                                
64bit						libcvc3-2-3.dll					libcvc3jni-2.dll				libz3.dylib
automaton.jar					libcvc3-2.dll					libcvc3jni.2.3.0.dylib				libz3java.dylib
backup_intel					libcvc3-5.0.0.jar				libcvc3jni.2.3.dylib				opt4j-2.4.jar
choco-1_2_04.jar				libcvc3.2.3.0.dylib				libcvc3jni.2.dylib				org.hamcrest.core_1.3.0.v20180420-1519.jar
choco-solver-2.1.1-20100709.142532-2.jar	libcvc3.2.3.dylib				libcvc3jni.dll					org.sat4j.pb.jar
com.microsoft.z3.jar				libcvc3.2.dylib					libcvc3jni.dylib				parser.jar
coral.jar					libcvc3.dll					libcvc3jni.so					proteus.jar
grappa.jar					libcvc3.dylib					libcvc3jni.so.2					scale.jar
green.jar					libcvc3.jar					libcvc3jni.so.2.3				solver.jar
hamcrest-core-1.3.jar				libcvc3.so					libcvc3jni.so.2.3.0				Statemachines.jar
hampi.jar					libcvc3.so.2					libgmp.10.dylib					STPJNI.jar
iasolver.jar					libcvc3.so.2.3					libSTPJNI.so					string.jar
inv-solver.jar					libcvc3.so.2.3.0				libyices.so					yicesapijava.jar
junit-4.13.2.jar				libcvc3jni-2-3-0.dll				libYicesLite.so
libcvc3-2-3-0.dll				libcvc3jni-2-3.dll				libz3.a
sameersawant@Sameers-MacBook-Air jpf-symbc % cat src/examples/demo/NumericExample.jpf 
target=demo.NumericExample
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples
symbolic.method = demo.NumericExample.test(sym#sym)

symbolic.dp=z3
listener = .symbc.SymbolicListener

search.multiple_errors=true
sameersawant@Sameers-MacBook-Air jpf-symbc % jpf-run -Xmx1024m -ea -jar ../../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf
symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=-1.7976931348623157E308
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 25906f2bfd0e72f4c79617ddb7c47be0c11f9d9c) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
demo.NumericExample.main()

====================================================== search started: 1/1/26 10:55 PM
java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
	at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1875)
	at java.lang.Runtime.loadLibrary0(Runtime.java:844)
	at java.lang.System.loadLibrary(System.java:1136)
	at com.microsoft.z3.Native.<clinit>(Native.java:17)
	at com.microsoft.z3.Context.<init>(Context.java:74)
	at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3$Z3Wrapper.<init>(ProblemZ3.java:76)
	at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3$Z3Wrapper.getInstance(ProblemZ3.java:70)
	at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.<init>(ProblemZ3.java:96)
	at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:98)
	at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:395)
	at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:339)
	at gov.nasa.jpf.symbc.bytecode.IDIV.execute(IDIV.java:121)
	at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
	at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
	at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
	at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
	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 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 gov.nasa.jpf.tool.Run.call(Run.java:80)
	at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
sameersawant@Sameers-MacBook-Air jpf-symbc % 

[sohah]

@Sameersawant77 , Are you setting the library path correctly? if you are using a mac, then I think you should set "DYLD_LIBRARY_PATH".

[Sameersawant77]

@sohah I have added a Dockerfile for easier setup and alias, not worrying about OS and dependencies and reducing complexity from so many steps. Let me know if i should change something in this or continue setting manually in macbook to look into the sv-comp branch issues.

[sohah]

Thank you @Sameersawant77 . Your PR looks good to me, just need a small usability change. Have you started looking at any of the bugs listed? You might want to start looking at cast1.yml at line 139 in the sheet. This is a regression bug, that is if you run the master branch, that bug is gone. You can probably see what is done wrong there. I am doubting that the construction of the z3 constraint is wrong.

To reproduce you can use the .jpf configuration that is produced by the sv-comp script.