[K-Bug] ArrayIndexOutOfBoundsException in KPrint.filterSubst

dwightguth commented 1 year ago

What component is the issue in?

Front-End

Which command

[ ] kompile
[X] kast
[ ] krun
[ ] kprove
[ ] kprovex
[ ] ksearch

What K Version?

v5.5.147

Operating System

Linux

K Definitions (If Possible)

module EQ-SYNTAX
  imports INT-SYNTAX
  imports ML-SYNTAX

  syntax Pgm ::= init ( Int ) [macro]
  rule init(0) => { 3 #Equals 4 }
  rule init(1) => { 3 #Equals 3 }
endmodule

module EQ
  imports EQ-SYNTAX
  configuration <k color="green"> $PGM:Pgm </k>
endmodule

Steps to Reproduce

kompile eq.k
kast --output pretty -e 'init(1)' --expand-macros

Expected Results

We would expect to see:

{
  3
#Equals
  3
}

Instead we get the following exception and stack trace:

java.lang.ArrayIndexOutOfBoundsException: Index 0 out of bounds for length 0
        at scala.collection.mutable.WrappedArray$ofRef.apply(WrappedArray.scala:193)
        at org.kframework.unparser.KPrint.filterSubst(KPrint.java:249)
        at org.kframework.unparser.KPrint.abstractTerm(KPrint.java:207)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:132)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:124)
        at org.kframework.kast.KastFrontEnd.run(KastFrontEnd.java:225)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:57)
        at org.kframework.main.Main.runApplication(Main.java:119)
        at org.kframework.main.Main.runApplication(Main.java:109)
        at org.kframework.main.Main.main(Main.java:57)
[Error] Internal: Uncaught exception thrown of type
ArrayIndexOutOfBoundsException (ArrayIndexOutOfBoundsException: Index 0 out of
bounds for length 0)

https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/unparser/KPrint.java#L249 is the offending line. It's looking to find the first sort parameter of the ML equals and can't find it because sort parameters haven't been added to the rule.

Not entirely sure what the appropriate fix ought to be. I believe we should discuss.

Baltoli commented 1 year ago

Same underlying issue as https://github.com/runtimeverification/k/issues/3436 - we need to add sort parameter inference in both cases. Has been implemented in Pyk with not a hugely complex implementation - we could backport that into the frontend, perhaps as a new pass or as part of AddSortInjections

Care should be taken to handle the full generality of sorts, parametric symbols etc. that the frontend needs to - Pyk implementation isn't fully general yet.

Baltoli commented 1 year ago

Workaround is also to disable substitution filtering if necessary

runtimeverification / k