search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Output parse error when using Z3 #59

Closed mister-walter closed 3 years ago

mister-walter commented 4 years ago

Ran into a problem when using Z3 with FuzzM, I think it is a problem with JKind's output parsing for newer versions of Z3. I was able to reproduce on JKind 4.4.0 (FuzzM uses a vendored copy of JKind 4.0.0).

Here's the file that FuzzM ends up calling JKind on (note that I had to upload it as a .txt file because GitHub didn't like the .lus extension). fuzz.txt

Here's the command I called and the output:

$ java -jar jkind/build/libs/jkind.jar -jkind -xml -solver z3 --no_slicing fuzz.txt
==========================================
  JKind 4.4.0
==========================================

There are 1 properties to be checked.
PROPERTIES TO BE CHECKED: [___fuzzProperty]

    -------------------------------------
    --^^--        SUMMARY          --^^--
    -------------------------------------

UNKNOWN PROPERTIES: [___fuzzProperty]

bmc process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
    at jkind.engines.BmcEngine.checkProperties(BmcEngine.java:48)
    at jkind.engines.BmcEngine.main(BmcEngine.java:39)
    at jkind.engines.Engine.run(Engine.java:36)
    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
    at java.base/java.lang.Thread.run(Thread.java:832)
k-induction process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
    at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
    at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
    at jkind.engines.Engine.run(Engine.java:36)
    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
    at java.base/java.lang.Thread.run(Thread.java:832)
invariant-generation process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
    at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
    at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
    at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
    at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
    at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
    at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
    at org.antlr.v4.runtime.Parser.match(Parser.java:223)
    at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
    at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
    at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
    at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
    at jkind.engines.invariant.AbstractInvariantGenerationEngine.refineBaseStep(AbstractInvariantGenerationEngine.java:74)
    at jkind.engines.invariant.AbstractInvariantGenerationEngine.main(AbstractInvariantGenerationEngine.java:49)
    at jkind.engines.Engine.run(Engine.java:36)
    at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
    at java.base/java.lang.Thread.run(Thread.java:832)

System info:

$ z3 --version
Z3 version 4.8.9 - 64 bit
$ git rev-parse HEAD # from inside the jkind repo
1f836bb08bc66256233fef4ee1a92e8c6a04592d
$ java --version
openjdk 14.0.2 2020-07-14
OpenJDK Runtime Environment (build 14.0.2+12)
OpenJDK 64-Bit Server VM (build 14.0.2+12, mixed mode)
lgwagner commented 3 years ago

Hi. This will take some time to diagnose and fix. In the meantime, this particular benchmark seems to work correctly with Z3 4.8.8. That might help you get around this problem until a proper fix is made and released.