[K-Bug] ClassCastException for #as and cells

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.121-0-g894298664c

Operating System

Linux

K Definitions (If Possible)

module A
imports INT

configuration

.K
0

rule
1 => A ...
( 0 #as A:ThingCell => 1 )
endmodule

Steps to Reproduce

$ kompile a.k 
[Error] Internal: Uncaught exception thrown of type ClassCastException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(ClassCastException: class org.kframework.kore.ADT$KAs cannot be cast to class
org.kframework.kore.KRewrite (org.kframework.kore.ADT$KAs and
org.kframework.kore.KRewrite are in unnamed module of loader 'app'))
[Warning] Compiler: Could not find main syntax module with name A-SYNTAX in
definition.  Use --syntax-module to specify one. Using A as default.

Here's the full stack trace:

$ kompile a.k --debug
java.lang.ClassCastException: class org.kframework.kore.ADT$KAs cannot be cast to class org.kframework.kore.KRewrite (org.kframework.kore.ADT$KAs and org.kframework.kore.KRewrite are in unnamed module of loader 'app')
        at org.kframework.compile.AddParentCells.getParent(AddParentCells.java:246)
        at org.kframework.compile.AddParentCells.getParent(AddParentCells.java:246)
        at org.kframework.compile.AddParentCells.lambda$concretizeCell$10(AddParentCells.java:297)
        at java.base/java.util.stream.Collectors.lambda$groupingBy$53(Collectors.java:1142)
        at java.base/java.util.stream.ReduceOps$3ReducingSink.accept(ReduceOps.java:169)
        at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
        at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
        at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
        at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
        at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
        at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
        at org.kframework.compile.AddParentCells.concretizeCell(AddParentCells.java:297)
        at org.kframework.compile.AddParentCells.concretize(AddParentCells.java:316)
        at org.kframework.compile.AddParentCells.concretize(AddParentCells.java:334)
        at org.kframework.compile.ConcretizeCells.concretize(ConcretizeCells.java:61)
        at org.kframework.definition.ModuleTransformer$.$anonfun$fromSentenceTransformer$3(transformers.scala:31)
        at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
        at scala.collection.StrictOptimizedIterableOps.map$(StrictOptimizedIterableOps.scala:87)
        at scala.collection.immutable.HashSet.map(HashSet.scala:34)
        at org.kframework.definition.ModuleTransformer$.$anonfun$fromSentenceTransformer$2(transformers.scala:29)
        at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:109)
        at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:960)
        at org.kframework.definition.ModuleTransformer.apply(transformers.scala:104)
        at org.kframework.definition.ModuleTransformer.apply(transformers.scala:99)
        at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:156)
        at org.kframework.compile.ConcretizeCells.transformDefinition(ConcretizeCells.java:41)
        at org.kframework.backend.kore.KoreBackend.lambda$steps$21(KoreBackend.java:260)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at scala.Function1.$anonfun$andThen$1(Function1.scala:87)
        at org.kframework.backend.kore.KoreBackend.lambda$steps$26(KoreBackend.java:320)
        at org.kframework.kompile.Kompile.run(Kompile.java:218)
        at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:91)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:60)
        at org.kframework.main.Main.runApplication(Main.java:127)
        at org.kframework.main.Main.runApplication(Main.java:117)
        at org.kframework.main.Main.main(Main.java:58)
[Error] Internal: Uncaught exception thrown of type ClassCastException
(ClassCastException: class org.kframework.kore.ADT$KAs cannot be cast to class
org.kframework.kore.KRewrite (org.kframework.kore.ADT$KAs and
org.kframework.kore.KRewrite are in unnamed module of loader 'app'))
[Warning] Compiler: Could not find main syntax module with name A-SYNTAX in
definition.  Use --syntax-module to specify one. Using A as default.

Expected Results

It would be nice if the #as construct above would just work #as expected.

If that's not possible, it would be nice to at least have some information about what the problem is, preferably file+line+column information. Now that I know what the issue is, I can see that there is a KAs involved, which might (or might not) mean that it's related to #as. Honestly, the stack trace and the default error message is probably readable only by K developers.

Now, since I spent a lot of time commenting out code in a non-trivial semantics until the error disappeared, then did some additional binary search on the last block of code that I commented out, I would like to suggest something that would make K less painful to use:

Why not have a global stack-like object containing context information for the thing that K is doing (e.g. it's trying to process the rule found at this location, or it's looking at this specific part of the rule, or something), and then the various parts that process stuff could push and pop their context info, then, when there is an unexpected error, the main function (or some other function close to the top level) could catch this and print the context stack before rethrowing.