[Bug] Parsing empty programs throws ArrayIndexOutOfBoundsException

[david-k]

K Version

K version:    v5.1.250-0-g07918e142
Build date:   Sat Nov 06 22:18:15 CET 2021

Description

Consider the following definition:

module EMPTY-INPUT
  syntax Prog ::= ""
endmodule

Then kast empty --debug (where empty is an empty file) produces the following output:

java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 0
	at org.kframework.parser.inner.kernel.Parser.finishStateReturn(Parser.java:699)
	at org.kframework.parser.inner.kernel.Parser.workListStep(Parser.java:669)
	at org.kframework.parser.inner.kernel.Parser.parse(Parser.java:574)
	at org.kframework.parser.inner.ParseInModule.parseStringTerm(ParseInModule.java:239)
	at org.kframework.parser.inner.ParseInModule.parseString(ParseInModule.java:197)
	at org.kframework.parser.inner.ParseInModule.parseString(ParseInModule.java:164)
	at org.kframework.kompile.CompiledDefinition.parseSingleTerm(CompiledDefinition.java:204)
	at org.kframework.parser.KRead.prettyRead(KRead.java:66)
	at org.kframework.parser.KRead.prettyRead(KRead.java:54)
	at org.kframework.kast.KastFrontEnd.run(KastFrontEnd.java:137)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:57)
	at org.kframework.main.Main.runApplication(Main.java:118)
	at org.kframework.main.Main.runApplication(Main.java:108)
	at org.kframework.main.Main.main(Main.java:56)
[Error] Internal: Uncaught exception thrown of type
ArrayIndexOutOfBoundsException (ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 0)

Note that ArrayIndexOutOfBoundsException is only thrown if the grammar actually accepts an empty program. I.e., if we have

module EMPTY-INPUT
  syntax Prog ::= "hi"
endmodule

then kast empty correctly complains about an unexpected end of file.

Expected Behavior

If a grammar accepts empty programs, then parsing empty programs should succeed.

[radumereuta]

Should be able to add a special case for this situation.