[K-Bug] Kompile crash instead of error for [left] attribute

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

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

What K Version?

K version: v7.1.30-0-g0cfdcda602-dirty Build date: Jo iun 27 11:21:15 EEST 2024

Operating System

Linux

K Definitions (If Possible)

a.k:

module A
    imports A-SYNTAX
endmodule

module A-SYNTAX
    syntax A ::= B  [left]

    syntax B ::= "b"
endmodule

Steps to Reproduce

kompile a.k --debug

produces

java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because the return value of "org.kframework.definition.Tag.name()" is null
        at org.kframework.backend.kore.ModuleToKORE.lambda$getAssoc$18(ModuleToKORE.java:1820)
        at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:178)
        at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
        at scala.collection.convert.JavaCollectionWrappers$IteratorWrapper.forEachRemaining(JavaCollectionWrappers.scala:31)
        at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1845)
        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.backend.kore.ModuleToKORE.getAssoc(ModuleToKORE.java:1823)
        at org.kframework.backend.kore.ModuleToKORE.syntaxAttributes(ModuleToKORE.java:1788)
        at org.kframework.backend.kore.ModuleToKORE.koreAttributes(ModuleToKORE.java:1674)
        at org.kframework.backend.kore.ModuleToKORE.translateSymbol(ModuleToKORE.java:483)
        at org.kframework.backend.kore.ModuleToKORE.translateSymbols(ModuleToKORE.java:452)
        at org.kframework.backend.kore.ModuleToKORE.convert(ModuleToKORE.java:244)
        at org.kframework.backend.kore.KoreBackend.getKompiledStringAndWriteSyntaxMacros(KoreBackend.java:96)
        at org.kframework.backend.kore.KoreBackend.getKompiledString(KoreBackend.java:86)
        at org.kframework.backend.kore.KoreBackend.getKompiledString(KoreBackend.java:79)
        at org.kframework.backend.llvm.LLVMBackend.accept(LLVMBackend.java:59)
        at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:114)
        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 NullPointerException
(NullPointerException: Cannot invoke "String.equals(Object)" because the return
value of "org.kframework.definition.Tag.name()" is null)

Expected Results

Error that left associativity is not applicable or successful compilation