search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

--symbolic-execution interacts badly with strictness #1554

Open grosu opened 9 years ago

grosu commented 9 years ago

Same context as explained in #1553. Everything works fine if I do not add the strictness attribute to line 23, but as soon as I do it the --symbolic-execution option of krun throws the exception below. The version of the same exception with the --debug option is shown in #1553.

krun ../lesson_7/tests/exponential-type.lambda --symbolic-execution
java.lang.UnsupportedOperationException: missing SMTLib translation for '_->_
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:409)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:702)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:367)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.accept(ConjunctiveFormula.java:663)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.translateConstraint(KILtoSMTLib.java:142)
    at org.kframework.backend.java.symbolic.SMTOperations.checkUnsat(SMTOperations.java:40)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.checkUnsat(ConjunctiveFormula.java:468)
    at org.kframework.backend.java.kil.ConstrainedTerm.unify(ConstrainedTerm.java:202)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:166)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:75)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.conventionalRewriteRun(JavaSymbolicExecutor.java:114)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.javaRewriteEngineRun(JavaSymbolicExecutor.java:137)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.run(JavaSymbolicExecutor.java:73)
    at org.kframework.krun.tools.Executor$Tool.execute(Executor.java:168)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:124)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:88)
    at org.kframework.transformation.TransformationCompositionProvider$2.run(TransformationCompositionProvider.java:120)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:83)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:51)
    at org.kframework.main.Main.runApplication(Main.java:110)
    at org.kframework.main.Main.runApplication(Main.java:100)
    at org.kframework.main.Main.main(Main.java:52)
java.lang.UnsupportedOperationException: missing SMTLib translation for isKResult
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:409)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:702)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:444)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:702)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:444)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:702)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:366)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.accept(ConjunctiveFormula.java:663)
    at org.kframework.backend.java.symbolic.KILtoSMTLib.translateConstraint(KILtoSMTLib.java:142)
    at org.kframework.backend.java.symbolic.SMTOperations.checkUnsat(SMTOperations.java:40)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.checkUnsat(ConjunctiveFormula.java:468)
    at org.kframework.backend.java.kil.ConstrainedTerm.unify(ConstrainedTerm.java:202)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:166)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:75)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.conventionalRewriteRun(JavaSymbolicExecutor.java:114)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.javaRewriteEngineRun(JavaSymbolicExecutor.java:137)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.run(JavaSymbolicExecutor.java:73)
    at org.kframework.krun.tools.Executor$Tool.execute(Executor.java:168)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:124)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:88)
    at org.kframework.transformation.TransformationCompositionProvider$2.run(TransformationCompositionProvider.java:120)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:83)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:51)
    at org.kframework.main.Main.runApplication(Main.java:110)
    at org.kframework.main.Main.runApplication(Main.java:100)
    at org.kframework.main.Main.main(Main.java:52)
:/k/lib/native/linux64:/usr/java/packages/lib/amd64:/usr/lib64:/lib64:/lib:/usr/lib
[Error] Internal: Uncaught exception thrown of type UnsatisfiedLinkError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
dwightguth commented 9 years ago

I remember this issue. This is the reason why I wrote those examples the way they are with explicit heating/cooling instead of strictness. The problem is the heating rule:

rule T1:Type -> T2:Type => T2 ~> T1 -> HOLE requires notBool isKResult(T2)

If a type variable _0 is on the top of the K cell, then it is logically valid to unify that type variable with this rule. That triggers the following equality being added to the constraint:

_0 = _1 -> _2

The SMT solver does not have an axiomatization of this construct and so it does not know how to solve this equality, leading to the errors you see.

I am pretty sure what you actually need to resolve this issue is a strategy saying "only apply heating rules if a cooling rule cannot apply".