`ModuleToKORE` silently absorbs `format` attribute

[tothtamas28]

Consider the following definition:

module FORMAT
    syntax Foo ::= r"foo" Bar [symbol(foo), format("%2")]
    syntax Bar ::= "bar"
endmodule

The generated KORE symbol for foo is then the following:

symbol Lblfoo{}(SortBar{}) : SortFoo{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2,20,2,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/ttoth/git/pyk/format.k)"), symbol'Kywd'{}("foo")]

Notice how format is present in the input but not the output. This is because ModuleToKORE does not generate format for productions that have items other than terminals and non-terminals:

https://github.com/runtimeverification/k/blob/61bd7894317815333c55964afc514c86efa1522f/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java#L1726

Does it make sense to have format only in KAST and not in KORE? If not, we should add a validation pass that emits an error if format is put on such a production.

[Baltoli]

The KAST and KORE format attributes are different; the LLVM backend can't handle regex terminals in the same way as the frontend. The underlying issue is turning a regex expression into a string, but maybe we should allow the user to pass the attribute through so long as they don't mention the regex terminal.

[tothtamas28]

Possibly related: there's already an error that enforces format on productions with regex terminals:

[Error] Compiler: Expected format attribute on production with regular
expression terminal.
        Source(/home/ttoth/git/pyk/format.k)
        Location(2,20,2,44)
        2 |         syntax Foo ::= r"foo" Bar [symbol(foo)]
          .                        ^~~~~~~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 structural errors.

[Baltoli]

This implies that if the regex terminal is mentioned, we should emit an error.