[K-Bug] ConcurrentModificationException while running kompile

[adharshkamath]

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.