[K-Bug] ConcurrentModificationException while running kompile

Start by reproducing the failure with kompile on the simple-untyped.md definition after adding the empty Stmt production. Read DefinitionParsing.java around resolveConfigBubbles and parseBubble, then inspect EarleyParser.java around complete, as indicated by the stack trace. Done means the input no longer crashes with ConcurrentModificationException and reports the problematic empty production clearly.

What component is the issue in?

Front-End

Which command

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

What K Version?

K version: v7.1.170; Build date: Thu Oct 31 22:28:38 CDT 2024

Operating System

Linux

K Definitions (If Possible)

https://github.com/runtimeverification/pl-tutorial/blob/master/2_languages/1_simple/1_untyped/simple-untyped.md

Steps to Reproduce

Add a production rule for Stmt

syntax Stmt := ...
               ...
               ...
              | ""
              ...

This causes kompile simple-untyped.md to crash.

Observed Results

The output of kompile simple-untyped.md is the following:

java.util.ConcurrentModificationException: java.util.ConcurrentModificationException
        at java.base/jdk.internal.reflect.DirectConstructorHandleAccessor.newInstance(DirectConstructorHandleAccessor.java:62)
        at java.base/java.lang.reflect.Constructor.newInstanceWithCaller(Constructor.java:502)
        at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:486)
        at java.base/java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:540)
        at java.base/java.util.concurrent.ForkJoinTask.reportException(ForkJoinTask.java:567)
        at java.base/java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:670)
        at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateParallel(ReduceOps.java:927)
        at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:233)
        at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
        at org.kframework.kompile.DefinitionParsing.lambda$resolveConfigBubbles$20(DefinitionParsing.java:476)
        at scala.collection.parallel.AugmentedIterableIterator.map2combiner(RemainsIterator.scala:107)
        at scala.collection.parallel.AugmentedIterableIterator.map2combiner$(RemainsIterator.scala:104)
        at scala.collection.parallel.immutable.ParHashSet$ParHashSetIterator.map2combiner(ParHashSet.scala:77)
        at scala.collection.parallel.ParIterableLike$Map.leaf(ParIterableLike.scala:1020)
        at scala.collection.parallel.Task.$anonfun$tryLeaf$1(Tasks.scala:52)
        at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
        at scala.util.control.Breaks$$anon$1.catchBreak(Breaks.scala:97)
        at scala.collection.parallel.Task.tryLeaf(Tasks.scala:55)
        at scala.collection.parallel.Task.tryLeaf$(Tasks.scala:49)
        at scala.collection.parallel.ParIterableLike$Map.tryLeaf(ParIterableLike.scala:1017)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal(Tasks.scala:159)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal$(Tasks.scala:156)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.internal(Tasks.scala:304)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute(Tasks.scala:149)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute$(Tasks.scala:148)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.compute(Tasks.scala:304)
        at java.base/java.util.concurrent.RecursiveAction.exec(RecursiveAction.java:194)
        at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:387)
        at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1312)
        at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1843)
        at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1808)
        at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:188)
Caused by: java.util.ConcurrentModificationException
        at java.base/java.util.ArrayList$Itr.checkForComodification(ArrayList.java:1095)
        at java.base/java.util.ArrayList$Itr.next(ArrayList.java:1049)
        at org.kframework.parser.inner.kernel.EarleyParser.complete(EarleyParser.java:1107)
        at org.kframework.parser.inner.kernel.EarleyParser.parse(EarleyParser.java:862)
        at org.kframework.parser.inner.ParseInModule.parseStringTerm(ParseInModule.java:396)
        at org.kframework.parser.inner.ParseInModule.parseString(ParseInModule.java:340)
        at org.kframework.kompile.DefinitionParsing.parseBubble(DefinitionParsing.java:955)
        at org.kframework.kompile.DefinitionParsing.lambda$resolveConfigBubbles$18(DefinitionParsing.java:474)
        at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:273)
        at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
        at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
        at java.base/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:1024)
        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$ReduceTask.doLeaf(ReduceOps.java:960)
        at java.base/java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:934)
        at java.base/java.util.stream.AbstractTask.compute(AbstractTask.java:327)
        at java.base/java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:754)
        ... 5 more
[Error] Internal: Uncaught exception thrown of type
ConcurrentModificationException (ConcurrentModificationException:
java.util.ConcurrentModificationException)

Expected Results

While adding an empty string as a production rule is not a "good" input to begin with, the tool would be more usable, if I was pointed to the empty string right away instead of a crash deeper in the library. I'm not completely sure if the crash is due to the empty string even. It is only my guess, since removing it no longer causes the crash.