kast: NoSuchElementException: key not found: bl_Map_

[virgil-serbanuta]

This was originally produced by a kore-print command, which said

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

so here it goes:

Versions:

$ kast --version
K version:    v6.0.87-0-g3997d65c22-dirty
Build date:   Lu sep 11 21:21:03 EEST 2023

To reproduce: llvm.zip

kast --input kore --definition /mnt/data/runtime-verification/elrond-wasm-real-elrond/.kbuild/kmxwasm-semantics/0a9b8db/target/v6.0.87-0-g3997d65c22-dirty/llvm --output json output.kore --debug

Stack trace:

java.util.NoSuchElementException: key not found: bl_Map_
        at scala.collection.MapLike.default(MapLike.scala:236)
        at scala.collection.MapLike.default$(MapLike.scala:235)
        at scala.collection.AbstractMap.default(Map.scala:65)
        at scala.collection.MapLike.apply(MapLike.scala:144)
        at scala.collection.MapLike.apply$(MapLike.scala:143)
        at scala.collection.AbstractMap.apply(Map.scala:65)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:308)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:320)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:320)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:320)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:320)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.unparser.KPrint.sortCollections(KPrint.java:322)
        at org.kframework.unparser.KPrint.abstractTerm(KPrint.java:205)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:132)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:124)
        at org.kframework.kast.KastFrontEnd.run(KastFrontEnd.java:223)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:57)
        at org.kframework.main.Main.runApplication(Main.java:126)
        at org.kframework.main.Main.runApplication(Main.java:116)
        at org.kframework.main.Main.main(Main.java:53)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException
(NoSuchElementException: key not found: bl_Map_)

[virgil-serbanuta]

I forgot this: output.zip

FWIW, this output file was produced by krun, with the llvm backend (I didn't include the interpreter in the archive above to keep the archive size under the github limit; also, the interpreter was less likely to be interesting).

[radumereuta]

By default, kast tries to pretty print using the syntax module.
If you give it a configuration term, then you need to specify the main module which contains all the labels.

[virgil-serbanuta]

FWIW:

• kast was being called by krun here, and I don't remember seeing krun passing the main module to kast, but I may be wrong.
• I think that bl_Map_ is not an actual label. The most similar thing I found was Lbl_Map_. I'm not sure whether it matters, but Lbl_Map_ was used in some of those \right-assoc or \left-asssoc things that seem to be kind of recent. If they are, indeed, new, then maybe there is some parsing issue related to them.