search

kframework / k-legacy

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

krun uncaught exception #2116

Open grosu opened 8 years ago

grosu commented 8 years ago
  1. kompile this version of KOOL typed static: https://github.com/grosu/k/tree/krun-exception/k-distribution/tutorial/2_languages/2_kool/2_typed/2_static
  2. krun as follows and see the exception:
file a bug report at https://github.com/kframework/k/issues
D:\github\grosu\k\k-distribution\tutorial\2_languages\2_kool\2_typed\2_static>krun ..\programs\field.kool --debug
java.lang.AssertionError
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:293)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:253)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:169)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:174)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:174)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:87)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:244)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:108)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:88)
        at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
        at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
        at org.kframework.krun.KRun.run(KRun.java:86)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
        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.AssertionError
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:293)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:253)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:169)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:174)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:278)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:174)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:193)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:243)
        at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:87)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:244)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:108)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:88)
        at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
        at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
        at org.kframework.krun.KRun.run(KRun.java:86)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
        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)
[Error] Internal: Uncaught exception thrown of type AssertionError.
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
grosu commented 8 years ago

I think I found the culprit. It is this rule:

https://github.com/grosu/k/blob/krun-exception/k-distribution/tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.k#L547-L557

Here it is, again:

  rule <task> <k> class C:Id extends C':Id { S:Stmts } => stmt ...</k> </task>
       (.Bag => <class>...
               <className> C </className>
               <extends> C' </extends>
             ...</class>)
//       <br/>
       (.Bag => <task>
                <k> checkType(class(C')) ~> S </k>
                <inClass> C </inClass>
                <ctenvT> .Map </ctenvT>
             </task>)  [structural]

If you comment it out, you get a stuck configuration as you expect. If you modify it minimally to apply and then stuck the computation, for example by adding a new type stmtStuck and replacing stmt with stmtStuck in the first line, then you get the exception again. So it really has a problem applying such a rule, probably because of the configuration abstraction.

I'll debug some more and try to find an alternative rule, but I wanted you to know the above so that you can fix the bugs.

grosu commented 8 years ago

I tried lots of different ways to fix this: reordering the cells, using parentheses for grouping, even adding one more layer of cells, <tasks/> and <classes>, and everything failed with the same exception thrown because of the same rule.

I don't know how to continue, so I need help here asap, otherwise we are not going to make it with KOOL.

@daejunpark , since you spent a lot of time with KOOL and with configuration abstraction, can you please step in and help here? Maybe we have the same problem reported in this commit?

https://github.com/kframework/k/commit/2230bb3947c34b34b09e44eaa2ea2dfbd46b31cf

andreistefanescu commented 8 years ago

This is a bug probably due to associative matching. I think I am the best person to look into it.

daejunpark commented 8 years ago

@andreistefanescu thanks. Let me know if you need my help. I can work again after classes, around 2pm.