search

collins-research / FuzzM

Other
14 stars 5 forks source link

FSM example does not work with Z3 solver #1

Open mister-walter opened 4 years ago

mister-walter commented 4 years ago

I have a feeling this is due to using a newer version of Z3. Pretty sure this is actually a JKind problem but FuzzM will have to update its vendored version of JKind to track any potential fixes on the JKind side.

# from inside FuzzM/examples/fsm-model
$ java -jar ../../fuzzm/fuzzm/bin/fuzzm.jar -fuzzm fsm.lus -solver z3  
==========================================
  FuzzM 0.2
==========================================
fuzzm.engines.OutputEngine:164        | OutputEngine is starting ..
fuzzm.engines.GeneratorEngine:109     | GeneratorEngine is starting ..
fuzzm.engines.TestHeuristicEngine:133 | TestHeuristicEngine is starting ..
fuzzm.engines.SolverEngine:80         | SolverEngine is starting ..
uzzm.engines.GeneralizationEngine:204 | GeneralizationEngine is starting ..
fuzzm.engines.TestHeuristicEngine:140 | Sending input bound constraint: Message: [Constraint] 0:id:+-1 : false
fuzzm.engines.Director:157            | Message: [Constraint] 0:id:+-1 : false
fuzzm.solver.Solver:236               | Writing file : /home/drew/tmp/fuzzmlocal/examples/fsm-model/fuzzm_fsm_16533819781863925089/fuzz.lus
fuzzm.solver.Solver:216               | Command([/usr/lib/jvm/java-14-openjdk/bin/java, -jar, /home/drew/tmp/fuzzmlocal/fuzzm/fuzzm/mvn-repo/jkind/jkind/uf/jkind-uf.jar, -jkind, -xml, -solver, z3, --no_slicing, /home/drew/tmp/fuzzmlocal/examples/fsm-model/fuzzm_fsm_16533819781863925089/fuzz.lus]) exited with code: 248
fuzzm.solver.Solver:216               | STDERR : bmc process failed
fuzzm.solver.Solver:216               | STDERR : jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:135)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:83)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:208)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:198)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:63)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.BmcEngine.checkProperties(BmcEngine.java:49)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.BmcEngine.main(BmcEngine.java:40)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.Engine.run(Engine.java:35)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
fuzzm.solver.Solver:216               | STDERR :    at java.base/java.lang.Thread.run(Thread.java:832)
fuzzm.solver.Solver:216               | STDERR : k-induction process failed
fuzzm.solver.Solver:216               | STDERR : jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:135)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:83)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:208)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:198)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:63)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.Engine.run(Engine.java:35)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
fuzzm.solver.Solver:216               | STDERR :    at java.base/java.lang.Thread.run(Thread.java:832)
fuzzm.solver.Solver:216               | STDERR : invariant-generation process failed
fuzzm.solver.Solver:216               | STDERR : jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
fuzzm.solver.Solver:216               | STDERR :    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:135)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:83)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:208)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:198)
fuzzm.solver.Solver:216               | STDERR :    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:63)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.invariant.AbstractInvariantGenerationEngine.refineBaseStep(AbstractInvariantGenerationEngine.java:74)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.invariant.AbstractInvariantGenerationEngine.main(AbstractInvariantGenerationEngine.java:49)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.Engine.run(Engine.java:35)
fuzzm.solver.Solver:216               | STDERR :    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
fuzzm.solver.Solver:216               | STDERR :    at java.base/java.lang.Thread.run(Thread.java:832)
fuzzm.engines.Director:157            | Message: [UNSAT] 0:id:+-1 Time = 0.581 s
^C    -------------------------------------
    --^^--        SUMMARY          --^^--
    -------------------------------------

System info:

$ z3 --version
Z3 version 4.8.9 - 64 bit
$ java -jar fuzzm/fuzzm/bin/fuzzm.jar -fuzzm -version    
FuzzM 0.2
$ git rev-parse HEAD # from inside the FuzzM repo
5a7ad514a8f5292a2f933a2a6008b709677eb458
mister-walter commented 4 years ago

I opened an issue over on the JKind repo - see loonwerks/jkind#59