[Bug] [kompile] - Uncaught exception thrown of type AssertionError

[yanliu18]

K Version

K version:    v5.2.95-0-gaa5eee670-dirty
Build date:   Tue Mar 01 00:15:37 AEDT 2022

Description

Internal: Uncaught exception thrown of type AssertionError
(AssertionError: null)

Input Files

File name:
stmt.k

module LESSON-16-A-SYNTAX
  imports INT-SYNTAX
  imports ID-SYNTAX

  syntax Exp ::= Id | Int
  syntax Decl ::= "int" Id "=" Exp ";" [strict(2)] 
  syntax Pgm ::= List{Decl,""}
endmodule

module STMT
    imports LESSON-16-A-SYNTAX
    imports BOOL

    syntax Stmt ::= Id "=" Exp ";" [strict(2)]
    syntax Pgm ::= List{Stmt, ""} 

    configuration <T>
                  <k> $PGM:Pgm </k>
                  <state> .Map </state>
                </T>

  // declaration sequence
  rule <k> S:Stmt; P:Pgm => S ~> P ...</k>
  rule <k> .Pgm => . ...</k>

  // variable declaration
  rule <k> X:Id = I:Int ; => . ...</k>
       <state> STATE => STATE [ X <- I ] </state>

  // variable lookup
  rule <k> X:Id => I ...</k>
       <state>... X |-> I ...</state>

  syntax Bool ::= isKResult(K) [symbol, function]
  rule isKResult(_:Int) => true
  rule isKResult(_) => false [owise]
endmodule

Reproduction Steps

kompile --debug stmt.k

bug report:

java.lang.AssertionError
	at org.kframework.definition.UserList.getLists(UserList.java:48)
	at org.kframework.parser.inner.generator.RuleGrammarGenerator.getCombinedGrammarImpl(RuleGrammarGenerator.java:473)
	at org.kframework.parser.inner.ParseInModule.getParsingModule(ParseInModule.java:122)
	at org.kframework.parser.inner.kernel.Scanner.<init>(Scanner.java:56)
	at org.kframework.parser.inner.ParseInModule.getScanner(ParseInModule.java:183)
	at org.kframework.kompile.DefinitionParsing.lambda$resolveConfigBubbles$17(DefinitionParsing.java:323)
	at scala.collection.parallel.AugmentedIterableIterator.map2combiner(RemainsIterator.scala:116)
	at scala.collection.parallel.AugmentedIterableIterator.map2combiner$(RemainsIterator.scala:113)
	at scala.collection.parallel.immutable.ParHashSet$ParHashSetIterator.map2combiner(ParHashSet.scala:81)
	at scala.collection.parallel.ParIterableLike$Map.leaf(ParIterableLike.scala:1064)
	at scala.collection.parallel.Task.$anonfun$tryLeaf$1(Tasks.scala:53)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
	at scala.util.control.Breaks$$anon$1.catchBreak(Breaks.scala:67)
	at scala.collection.parallel.Task.tryLeaf(Tasks.scala:56)
	at scala.collection.parallel.Task.tryLeaf$(Tasks.scala:50)
	at scala.collection.parallel.ParIterableLike$Map.tryLeaf(ParIterableLike.scala:1061)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask.compute(Tasks.scala:153)
	at scala.collection.parallel.AdaptiveWorkStealingTasks$WrappedTask.compute$(Tasks.scala:149)
	at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$WrappedTask.compute(Tasks.scala:440)
	at java.base/java.util.concurrent.RecursiveAction.exec(RecursiveAction.java:194)
	at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:373)
	at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1182)
	at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1655)
	at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1622)
	at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:165)
[Error] Internal: Uncaught exception thrown of type AssertionError
(AssertionError: null)

[Baltoli]

The problem here is that you're trying to declare the Pgm sort as two different syntactic lists. Internally, we desugar Lists like this (taken from the K source code):

    // find all productions annotated with 'userList'
    // expecting to always find 2 of them of the form:
    // Es ::= E "," Es  [right, userList, klabel(...)]
    // Es ::= ".Es"     [userList, klabel(...)]

which will only work for a single list production per sort.

I agree that this could do with a nicer error message than the assertion failure you're seeing.

[ehildenb]

kompile should print out a nice structured error that points out both locations.