[Bug] [kast] - Cannot parse json configurations with #And at top.

[nishantjr]

K Version

$ kompile --version
RV-K version 1.0-SNAPSHOT
Git revision: 9b8639c
Git branch: UNKNOWN
Build date: Tue Aug 11 17:28:02 CDT 2020

Description

kast crashes when parsing an input file with #And at the top.

Input Files

file: Test.k

module TEST
    imports INT

    configuration <k> fresh </k>
    syntax KItem ::= "fresh"
    rule fresh => ?_:Int 
    
    syntax KItem ::= "odd"
    rule I => odd requires I %Int 2 ==Int 1
endmodule

Reproduction Steps

$ kompile --backend haskell test.k && krun --output json > out.json &&  kast --input json --output kore --debug out.json 
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.
kore-exec: [284153] Warning (WarnIfLowProductivity):
    Warning! Poor performance: productivity dropped to aprox. 69%
java.lang.ArrayIndexOutOfBoundsException: 0
	at scala.collection.mutable.WrappedArray$ofRef.apply(WrappedArray.scala:130)
	at org.kframework.unparser.KPrint.filterConjunction(KPrint.java:290)
	at org.kframework.unparser.KPrint.filterSubst(KPrint.java:267)
	at org.kframework.unparser.KPrint.abstractTerm(KPrint.java:235)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:160)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:152)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:140)
	at org.kframework.kast.KastFrontEnd.run(KastFrontEnd.java:147)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
	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: 0)

Expected Behavior

kast should have returned a configuration formatted in kore.

[dwightguth]

I would rather we went back to the drawing board and figured out if there's a way to support Nishant's use case that doesn't involve passing the result of krun --output json to kast. This feels like something I don't want us to have to support long term.

[ehildenb]

@nishantjr can you fill in more details about how this issue came up in your high-level workflow?

We think that relying on the frontend to do Kore -> Kast -> external tool -> Kast -> Kore should not be what's done. Maybe there is another way to accomplish the same thing?

[nishantjr]

@ehildenb I had needed the following pipeline to implement Boogie.

PGM -> kore-exec  -> kast-to-json -> [Use pyk to transform kore] -> kast-to-kore -> kore-exec -> ...

The first kore-exec produced a constrained term with a \and. After transforming this kore and trying to feed it back to kore-exec, I encountered this error.

I am no longer using pyk because of this bug, so I'm not stuck on this any more. (I've written a K definition for manipulating kore instead.)

[radumereuta]

@ehildenb @dwightguth there are multiple problems here

1. we already discussed the problem of kast, json being lossy transformations and that's one of the problems
   https://github.com/kframework/k/blob/issue1509/kernel/src/main/java/org/kframework/unparser/KPrint.java#L300
   JSON returns a label here without parameters, and then we try to apply on a list of 0 params => K crashes with IndexOutOfBounds

• I don't have a fix for this. Probably we need to bump the JSON version and include parameters. It's likely to break external tools.

2. Another problem is related to KPrint not being flexible enough to handle every single input:
   https://github.com/kframework/k/blob/issue1509/kernel/src/main/java/org/kframework/unparser/KPrint.java#L181
   It used the default semantics module and fail because it couldn't find generated labels (casts, inj, etc)
   I've updated it so it uses the module with all the labels it would encounter.