How to point to a SMT solver on Windows?

Question

How to point to a SMT solver on Windows?

Closed this issue 4 years ago · 10 comments

Hello, I am writing an academic paper on NOPOL and I am trying to setup the project on Windows 10. I followed all steps up to step 4, but now I seem to be unable to point to a SMT solver and I would greatly appreciate some help.

I decided to go with the SMT solver Z3 and downloaded the pre-built binary z3-4.8.8-x64-win.zip from their releases.

Then, I used the following command lines to execute NOPOL, with my correct username:

java -jar "C:\Users\<user>\nopol\nopol\target/nopol-0.2-SNAPSHOT-jar-with-dependencies.jar" 
-s src/main/java/ 
-c C:\Users\<user>\.m2\repository\junit\junit\4.11\junit-4.11.jar;C:\Users\<user>\.m2\repository\org\hamcrest\hamcrest-core\1.3\hamcrest-core-1.3.jar 
-t symbolic_examples.symbolic_example_1.NopolExampleTest 
-p C:\Users\<user>\Documents\z3-4.8.8-x64-win\bin

However, I am getting an exception and executing NOPOL fails:

java.lang.NullPointerException
at xxl.java.compiler.DynamicClassCompiler.(DynamicClassCompiler.java:45)
at xxl.java.compiler.DynamicClassCompiler.(DynamicClassCompiler.java:30)
at fr.inria.lille.commons.spoon.SpoonedFile.(SpoonedFile.java:62)
at fr.inria.lille.commons.spoon.SpoonedProject.(SpoonedProject.java:17)
at fr.inria.lille.repair.nopol.NoPol.(NoPol.java:112)
at fr.inria.lille.repair.Main.main(Main.java:95)

Testing revealed that leaving the parameter -p empty causes the same exception as the current path that is provided for the SMT solver. At the path C:\Users<user>\Documents\z3-4.8.8-x64-win\bin, there is the extracted content of the z3-4.8.8-x64-win.zip file. Since the instructions mention that -p should point to a binary path, I chose this path, however, in the example that is provided, a single file is referenced. Yet, in the content of z3-4.8.8-x64-win.zip, there is no binary file, if I see it correctly. There is a z3.exe, a com.microsoft.z3.jar and a z3.py, but no file that resembles the example "z3_for_linux" in NOPOL.

Which file do I have to reference there? I would greatly appreciate some assistance.

monperrus commented 4 years ago

perfect

Answer 1 · 2020-08-14T08:12:05.000Z

-p C:\Users\<user>\Documents\z3-4.8.8-x64-win\bin This is folder, it should point to an executable, eg -p C:\Users\<user>\Documents\z3-4.8.8-x64-win\bin\z3.exe

Answer 2 · 2020-08-14T15:24:55.000Z

Thank you for your response, monperrus!

Unfortunately, the issue persists even when pointing to the executable, throwing the previously posted error message. Could the Java version be the problem? In the output before the exception occurs, it displays:

17:16:54.085 [main] INFO fr.inria.lille.repair.nopol.NoPol - Java version: 1.8.0_261
17:16:54.085 [main] INFO fr.inria.lille.repair.nopol.NoPol - JAVA_HOME: C:\Program Files\Java\jdk1.8.0_251

Then it displays PATH and all paths in there, followed by the exception. Lastly, it displays the usage with all parameters.

Answer 3 · 2020-08-14T15:26:19.000Z

Sorry for closing the issue, I am used to have an upload button next to the comment button.

I have attached the full log of NOPOL as a text file to this comment.

nopol_output.txt

EDIT: In the text file, the path is C:\Users<user>\nopol\nopol>, but the issue also happens from the C:\Users<user>\nopol\test-projects path from the instructions.

Answer 4 · 2020-08-17T07:30:10.000Z

What happens if you debug the problem and add a breakpoint just before the exception?

Answer 5 · 2020-08-17T16:09:13.000Z

Thanks again for your response!

If I try to setup the project in my IDE, Eclipse, to be able to set break points, I get a different error when running the project with the following configuration:

17:57:36.066` [main] INFO fr.inria.lille.repair.nopol.NoPol - Source files: [src\main\java]
17:57:36.066 [main] INFO fr.inria.lille.repair.nopol.NoPol - Classpath: [file:/C:/Users//.m2/repository/junit/junit/4.11/junit-4.11.jar, file:/C:/Users//.m2/repository/org/hamcrest/hamcrest-core/1.3/hamcrest-core-1.3.jar]
17:57:36.066 [main] INFO fr.inria.lille.repair.nopol.NoPol - Statement type: CONDITIONAL
17:57:36.066 [main] INFO fr.inria.lille.repair.nopol.NoPol - Args: [symbolic_examples.symbolic_example_1.NopolExampleTest]
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Config: Config{synthesisDepth=3, collectStaticMethods=true, collectStaticFields=false, collectLiterals=false, onlyOneSynthesisResult=true, sortExpressions=true, maxLineInvocationPerTest=250, timeoutMethodInvocation=2000, dataCollectionTimeoutInSecondForSynthesis=900, addWeight=0.19478, subWeight=0.04554, mulWeight=0.0102, divWeight=0.00613, andWeight=0.10597, orWeight=0.05708, eqWeight=0.22798, nEqWeight=0.0, lessEqWeight=0.0255, lessWeight=0.0947, methodCallWeight=0.1, fieldAccessWeight=0.08099, constantWeight=0.14232, variableWeight=0.05195, mode=REPAIR, type=CONDITIONAL, synthesis=SMT, oracle=ANGELIC, solver=Z3, solverPath='C:\Users<user>\Documents\z3-4.8.8-x64-win\bin\z3.exe', projectSources=[src\main\java], projectClasspath='[Ljava.net.URL;@16c0663d', projectTests=[symbolic_examples.symbolic_example_1.NopolExampleTest], complianceLevel=7, outputFolder=., json=false}
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Available processors (cores): 4
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Free memory: 236 MB
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Maximum memory: 3 GB
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Total memory available to JVM: 245 MB
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - Java version: 1.8.0_251
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - JAVA_HOME: C:\Program Files\Java\jdk1.8.0_251
17:57:36.076 [main] INFO fr.inria.lille.repair.nopol.NoPol - PATH: /.../
java.util.concurrent.ExecutionException: java.lang.NullPointerException
at java.util.concurrent.FutureTask.report(FutureTask.java:122)
at java.util.concurrent.FutureTask.get(FutureTask.java:206)
at fr.inria.lille.repair.Main.main(Main.java:106)
Caused by: java.lang.NullPointerException
at com.gzoltar.core.GZoltar.run(GZoltar.java:51)
at fr.inria.lille.localization.GZoltarFaultLocalizer.run(GZoltarFaultLocalizer.java:163)
at fr.inria.lille.localization.GZoltarFaultLocalizer.(GZoltarFaultLocalizer.java:94)
at fr.inria.lille.localization.GZoltarFaultLocalizer.(GZoltarFaultLocalizer.java:68)
at fr.inria.lille.localization.GZoltarFaultLocalizer.createInstance(GZoltarFaultLocalizer.java:60)
at fr.inria.lille.repair.nopol.NoPol.createLocalizer(NoPol.java:178)
at fr.inria.lille.repair.nopol.NoPol.build(NoPol.java:130)
at fr.inria.lille.repair.Main$1.call(Main.java:101)
at java.util.concurrent.FutureTask.run(FutureTask.java:266)
at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
at java.lang.Thread.run(Thread.java:748)

Usage: java -jar nopol.jar
[(-m|--mode) <repair|ranking>] (-e|--type) <condition|precondition|pre_then_cond|loop|arithmetic> [(-o|--oracle) <angelic|symbolic>] [(-y|--synthesis) <smt|dynamoth>] [(-l|--solver) <z3|cvc4>] [(-p|--solver-path) ] (-s|--source) source1;source2;...;sourceN (-c|--classpath) [(-t|--test) test1;test2;...;testN ] [--complianceLevel ] [--maxTime ] [--maxTimeType ] [(-z|--flocal) < cocospoon|dumb|gzoltar>] [--output ] [--json[:]]

[(-m|--mode) <repair|ranking>]
Define the mode of execution. (default: repair)

(-e|--type) <condition|precondition|pre_then_cond|loop|arithmetic>
The repair type (example fixing only conditions, or adding
precondition). REQUIRED OPTION (default: condition)

[(-o|--oracle) <angelic|symbolic>]
Define the oracle (only used with repair mode). (default: angelic)

[(-y|--synthesis) <smt|dynamoth>]
Define the patch synthesis. (default: smt)

[(-l|--solver) <z3|cvc4>]
Define the solver (only used with smt synthesis). (default: z3)

[(-p|--solver-path) ]
Define the solver binary path (only used with smt synthesis).

(-s|--source) source1;source2;...;sourceN
Define the path to the source code of the project.

(-c|--classpath)
Define the classpath of the project.

[(-t|--test) test1;test2;...;testN ]
Define the test classes of the project (both failing and passing),
fully-qualified, separated with ':' (even if the classpath contains
other tests, only those are considered.

[--complianceLevel ]
The compliance level of the project. (default: 7)

[--maxTime ]
The maximum time execution in minute for the whole execution of
Nopol.(default: 10)

[--maxTimeType ]
The maximum time execution in minute for one type of patch. (default: 5)

[(-z|--flocal) < cocospoon|dumb|gzoltar>]
Define the fault localizer to be used. (default: gzoltar)

[--output ]
Define the location where the patches will be saved. (default: .)

[--json[:]]
Output a json file in the current working `directory.

Even if I was able to set a breakpoint, Java is not one of my main programming languages and I don't know how much I could contribute to solving the issue. Since it is not a requirement for my paper to actually run NOPOL, I might give up on trying to set it up, even if it would be a great enhancement to use it to create my own examples to show how the tool solves different issues giving reality to the theory behind it.

Answer 6 · 2020-08-17T16:26:53.000Z

this is a gzoltar bug, probably due to an incorrect classpath. to make progress, you can try with "--flocal cocospoon" to disable gzoltar

Answer 7 · 2020-08-18T17:57:34.000Z

After adding "--flocal cocospoon", I get this error

java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.ClassNotFoundException: symbolic_examples.symbolic_example_1.NopolExampleTest
at java.util.concurrent.FutureTask.report(FutureTask.java:122)
at java.util.concurrent.FutureTask.get(FutureTask.java:206)
at fr.inria.lille.repair.Main.main(Main.java:106)
Caused by: java.lang.RuntimeException: java.lang.ClassNotFoundException: symbolic_examples.symbolic_example_1.NopolExampleTest
at fr.inria.lille.localization.CocoSpoonBasedSpectrumBasedFaultLocalizer.runTests(CocoSpoonBasedSpectrumBasedFaultLocalizer.java:104)
at fr.inria.lille.localization.CocoSpoonBasedSpectrumBasedFaultLocalizer.(CocoSpoonBasedSpectrumBasedFaultLocalizer.java:34)
at fr.inria.lille.repair.nopol.NoPol.createLocalizer(NoPol.java:182)
at fr.inria.lille.repair.nopol.NoPol.build(NoPol.java:130)
at fr.inria.lille.repair.Main$1.call(Main.java:101)
at java.util.concurrent.FutureTask.run(FutureTask.java:266)
at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
at java.lang.Thread.run(Thread.java:748)
Caused by: java.lang.ClassNotFoundException: symbolic_examples.symbolic_example_1.NopolExampleTest
at java.net.URLClassLoader.findClass(URLClassLoader.java:382)
at java.lang.ClassLoader.loadClass(ClassLoader.java:418)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:355)
at java.lang.ClassLoader.loadClass(ClassLoader.java:351)
at fr.inria.lille.repair.common.BottomTopURLClassLoader.loadClass(BottomTopURLClassLoader.java:43)
at fr.inria.lille.localization.CocoSpoonBasedSpectrumBasedFaultLocalizer.runTests(CocoSpoonBasedSpectrumBasedFaultLocalizer.java:89)
... 8 more

As told in the instructions after I downloaded your project examples and did not change any directories, I added for the source code of the project the path "src/main/java" and the tests for that source code is in "src/test/java". Maybe this is the problem because the tests are in a different directory?

Out of curiosity, I changed the test class for the parameter -t to "symbolic_examples.symbolic_example_1.NopolExample", which is the source code file and there it runs fine, although it obviously doesn't find statements since it is not include tests:

19:48:29.161 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - OOPS, no statement at all, no test results
19:48:29.161 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - ----INFORMATION----
19:48:29.167 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb classes : 32
19:48:29.167 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb methods : 54
19:48:29.169 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements Analyzed : 0
19:48:29.169 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements with Angelic Value Found : 0
19:48:29.169 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb inputs in SMT : 0
19:48:29.173 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb SMT level: 0
19:48:29.173 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb variables in SMT : 0
19:48:29.173 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - NoPol Execution time : 2329ms
19:48:29.173 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol -
NO_ANGELIC_VALUE

So the issue seems to be that it isn't able to find the class containing the test cases. Even when I give -t the absolute path to the file I still get the same error. I also tried moving the class file to the same directory of the source code and renaming it, but nonetheless it still yields the same error.

Although interestingly, if I move the test file itself to the location of the source code, not renaming it and updating references, I get these messages instead:

19:54:34.628 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #1
19:54:34.629 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExampleTest:44 which is executed by 1 tests
452601009
19:54:34.713 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #2
19:54:34.713 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExampleTest:45 which is executed by 1 tests
452601009
19:54:34.786 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #3
19:54:34.786 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExampleTest:37 which is executed by 1 tests
452601009
19:54:34.849 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #4
19:54:34.849 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExampleTest:38 which is executed by 1 tests
452601009
19:54:34.918 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #5
19:54:34.919 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:16 which is executed by 7 tests
-126608641
19:54:34.964 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #6
19:54:34.964 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:15 which is executed by 8 tests
-126608641
19:54:35.013 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - looking with class fr.inria.lille.repair.nopol.spoon.smt.ConditionalReplacer
19:54:35.018 [pool-1-thread-1] ERROR fr.inria.lille.repair.nopol.NoPol - Error ExecutionException java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.ClassNotFoundException: symbolic_examples.symbolic_example_1.NopolExampleTest
19:54:35.018 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #7
19:54:35.019 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:22 which is executed by 9 tests
-126608641
19:54:35.063 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #8
19:54:35.063 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:24 which is executed by 9 tests
-126608641
19:54:35.107 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #9
19:54:35.108 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:23 which is executed by 9 tests
-126608641
19:54:35.155 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - statement #10
19:54:35.155 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - Analysing SourceLocation symbolic_examples.symbolic_example_1.NopolExample:12 which is executed by 9 tests
-126608641
19:54:35.210 [pool-1-thread-1] DEBUG fr.inria.lille.repair.nopol.NoPol - looking with class fr.inria.lille.repair.nopol.spoon.smt.ConditionalReplacer
19:54:35.213 [pool-1-thread-1] ERROR fr.inria.lille.repair.nopol.NoPol - Error ExecutionException java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.ClassNotFoundException: symbolic_examples.symbolic_example_1.NopolExampleTest
19:54:35.214 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - ----INFORMATION----
19:54:35.218 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb classes : 33
19:54:35.219 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb methods : 63
19:54:35.220 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements Analyzed : 0
19:54:35.220 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements with Angelic Value Found : 0
19:54:35.220 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb inputs in SMT : 0
19:54:35.222 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb SMT level: 0
19:54:35.222 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb variables in SMT : 0
19:54:35.222 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - NoPol Execution time : 3075ms
19:54:35.222 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol -
NO_ANGELIC_VALUE

So still, it doesn't find the class. What could be the issue here?

Answer 8 · 2020-08-19T05:25:03.000Z

This is most likely a classpath problem: * make sure you have recompiled the project under repair, both the app and the tests * make sure to give the right folders as classpath (-c|--classpath) <classpath> Define the classpath of the project separated by a path separator (`:` on Linux). Must contain the application binary classes (`target/classes`) Must contain the application test classes (`target/test-classes`) Must contain the library classes (`lib/junit.jar` for instance)

Answer 9 · 2020-08-19T15:32:00.000Z

Thank you very much for your assistance and bearing with my questions, monperrus! I managed to execute NOPOL for the example test class by fixing the classpath problem with your explanation and solution.

Please feel free to close this issue now.