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

Reproduce the crash with the provided a.k definition using kompile a.k --debug. Start in org.kframework.backend.kore.ModuleToKORE.java around getAssoc line 1820, then verify compilation no longer throws the reported NullPointerException and instead reports that left associativity is invalid or compiles successfully.

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