[K-Bug] `kompile --backend haskell` generates invalid textual KORE for some attributes

[tothtamas28]

What component is the issue in?

Front-End

Which command

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

What K Version?

K version: v5.5.80-0-g59eb5a8cbd

Operating System

Linux

K Definitions (If Possible)

// empty.k

module EMPTY-SYNTAX
endmodule

module EMPTY
    imports INT
endmodule

Steps to Reproduce

kompile --backend haskell empty.k

Expected Results

The resulting definition.kore file contains axioms like

axiom{R} \implies{R} (
  \top{R}(),
  \equals{SortInt{},R} (
    Lbl'UndsAnd-'Int'Unds'{}(VarI1:SortInt{},Lbl'UndsAnd-'Int'Unds'{}(VarI2:SortInt{},VarC:SortInt{})),
   \and{SortInt{}} (
     Lbl'UndsAnd-'Int'Unds'{}(Lbl'UndsAnd-'Int'Unds'{}(VarI1:SortInt{},VarI2:SortInt{}),VarC:SortInt{}),
      \top{SortInt{}}())))
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/ttoth/git/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), concrete{}(VarI1:SortInt{},VarI2:SortInt{}), symbolic{}(VarC:SortInt{}), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1198,8,1198,50)"), simplification{}(""), UNIQUE'Unds'ID{}("1b7de709091a3290862d7a9ca2625659b666b89c5a3b27bdfee178b1628fd179")]

Here, attributes concrete{}(VarI1:SortInt{},VarI2:SortInt{}) and symbolic{}(VarC:SortInt{}) are not valid textual KORE according to design decision Attributes as Patterns.

[radumereuta]

@tothtamas28 I did a short investigation and I found the place where these are printed: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java#L1838 But to me this looks good. If the backends are accepting this format and rely on it, we just need to update the documentation.

I'm curious about what @ana-pantilie has to say about the format.

[ana-pantilie]

@tothtamas28 so is the expected outcome concrete{}("VarI1:SortInt{}","VarI2:SortInt{}"), symbolic{}("VarC:SortInt{}") (so with string literals instead of actual variables as arguments)?

Is this a blocker or making things awkward on the pyk side, or do you think it will sometime in the future? If not, then I think we can make an exception to the design decision above.

[tothtamas28]

is the expected outcome concrete{}("VarI1:SortInt{}","VarI2:SortInt{}")

Yes, that would be valid textual KORE according to the documentation. I'd probably go with concrete{}("VarI1","VarI2") though as 1) then parsing the strings would be unnecessary 2) type information can be easily inferred in the first place.

Is this a blocker or making things awkward on the pyk side

It's a blocker in the sense that pyk intends to implement a parser for textual KORE as it is documented.

If not, then I think we can make an exception to the design decision above.

I don't think making an exception is a good idea. We should either discard the design decision altogether (after due consideration), or commit to it.

[ana-pantilie]

It's a blocker in the sense that pyk intends to implement a parser for textual KORE as it is documented.

If that's the case then we can always extend the Kore language, and say we allow variables as well in that context (unless there's a good reason we shouldn't). That design document was written well before we had the concrete and symbolic attributes.

[tothtamas28]

Sure, but is having an element-variable as argument really necessary for these attributes? You can just store the variable name and resolve it in its respective scope.

[ana-pantilie]

That means that the concrete and symbolic attribute parsers will need to be made contextual, and they currently aren't. Is it really worth changing 2 backends (maybe 3 if the llvm backend doesn't ignore this) and the frontend for this? Again, is this making something in pyk more complicated than it should be?

[tothtamas28]

is this making something in pyk more complicated than it should be?

This is not a pyk issue, I can implement this design or an alternative without a problem. But there is a discrepancy between implementation and documentation that needs to be resolved one way or the other.

Is it really worth changing 2 backends (maybe 3 if the llvm backend doesn't ignore this) and the frontend for this?

I mean, there is a whole design document that deals with this exact question, which means it was important enough for someone to spend time elaborating on it and documenting it. No design is set in stone of course, but let's try to understand the tradeoffs before discarding it.

Answering your question, it is a trivial change in the frontend and probably not an issue in the LLVM backend (at least I had no issues parsing LLVM KORE definitions so far).

That means that the concrete and symbolic attribute parsers will need to be made contextual

Would it be difficult to do so? Is parsing and processing attributes not done in separate passes?

2 backends (maybe 3

What's the third backend?

[ana-pantilie]

What's the third backend?

There are two Haskell backends.

No design is set in stone of course, but let's try to understand the tradeoffs before discarding it.

That;s what I'm asking, what are the real tradeoffs?

[ana-pantilie]

Also, even if the change seems minimal, it's actually not. First of all it requires the integration of 3 separate projects and second of all it becomes a breaking change, so every Kore regression test we have in the backends need to be regenerated, and that means that the ones which can't be regenerated are lost and the ones which can be will have to be regenerated manually by one of our developers. So, again, if this is a non-issue in pyk then my answer is that we do not have the required resources to take care of this now, so I would suggest modifying the design document to reflect the current implementation.

[radumereuta]

I tend to agree with Ana. Let's just update the documentation file (last update Jan 30, 2019 from a discussion between grosu, bmmoore, dwightguth, u--, njohnwalker, traiansf, hreada.) The piece of code that generates this was written by traiansf on March 23, 2020.

The most up to date documentation is the code. That's why I always advocate for code comments. @tothtamas28 would that work for you? Let me know if there are other inconsistencies in the document before I close this issue.

[tothtamas28]

would that work for you?

For now let's just create a PR that documents the exception in attribute syntax, and then reference that PR in this issue.

Let's also bring the issue up for discussion during the next K planning meeting. Then it can be either A) closed as completed (after perhaps further adjustments to the documentation), or B) scheduled for later when the Haskell team has bandwidth to deal with it.

[Baltoli]

Consensus agrees with above comments that the correct thing to do here is to update the design document to reflect what the backends do (i.e. allow attributes to be arbitrary patterns).

@dwightguth notes that as far as he knows, nothing in the code assumes the structure in the design decision. We should avoid changing the structure of existing attributes. Passing complex structure to the backends could be harder.

@ehildenb has a use case:

• c.f. Maude's log attribute for logging subterms