LLVM backend failing to evaluate function

[virgil-serbanuta]

For the example below, the LLVM backend ends execution with an error, outputting an unevaluated function, without any obvious reason for not evaluating it.

[Error] krun: ./a-kompiled/interpreter 
/tmp/.krun-2023-06-26-17-49-17-Oq7lqoxprx/tmp.in.zDrsIYS8SO -1 
/tmp/.krun-2023-06-26-17-49-17-Oq7lqoxprx/result.kore
g ( ListItem ( wrap ( b"a" ) ) )

All or most of the elements in the semantics below seem to be needed for reproducing the issue (e.g. using a normal Map, or passing a list directly to g, without producing it with Set2List(keys(...)) do not generate the error above).

To reproduce:
a.k

module A
    imports BYTES
    imports COLLECTIONS
    imports K-EQUAL-SYNTAX
    imports LIST

    syntax List ::= f ( MapBytesToBytes ) [function, symbol, klabel(myF)]
                  | g ( List )            [function, symbol, klabel(myG)]
    rule f(M) => g(Set2List(keys(M)))

    rule g(.List) => .List
    rule g(ListItem(_:WrappedBytes) L:List) => g(L:List)

    syntax KItem  ::= a(MapBytesToBytes)
                    | b(List)

    rule a(M) => b(f(M))

    syntax WrappedBytes ::= wrap(Bytes)  [symbol, klabel(wrapBytes)]

    syntax MapBytesToBytes  [hook(MAP.Map)]
    syntax MapBytesToBytes ::= MapBytesToBytes MapBytesToBytes
          [ left, function, hook(MAP.concat), klabel(_MapBytesToBytes_),
            symbol, assoc, comm, unit(.MapBytesToBytes), element(_Bytes2Bytes|->_),
            index(0), format(%1%n%2)
          ]
    syntax MapBytesToBytes ::= ".MapBytesToBytes"
          [ function, total, hook(MAP.unit),
            klabel(.MapBytesToBytes), symbol, latex(\dotCt{MapBytesToBytes})
          ]
    syntax MapBytesToBytes ::= WrappedBytes "Bytes2Bytes|->" WrappedBytes
          [ function, total, hook(MAP.element),
            klabel(_Bytes2Bytes|->_), symbol,
            latex({#1}\mapsto{#2}), injective
          ]

    syntax Set ::= keys(MapBytesToBytes)  [function, total, hook(MAP.keys)]
endmodule

start:

a(wrap(b"a") Bytes2Bytes|-> wrap(b"b"))

command line:

kompile a.k --backend llvm && krun start

[Baltoli]

The problem here is that the wrap(_) terms are missing an injection into KItem because the element constructor is defined in terms of the WrappedBytes sort. I'm not sure yet what the best solution is, but I think I can probably minimise the example a bit.

[Baltoli]

We discussed this in the K meeting, and the conclusion was that there are two main solutions to deal with this problem:

1. workaround for now, make the arguments to your map element constructor of sort KItem. This obviously sidesteps the entire point of your type-safe collection, but will make your example work as presented.
2. Modify your definition to hook every collection function and type that you need to use to operate over the WrappedBytes sort. This requires a lot of changes to your code, and isn't our preferred solution.
3. We will look to modify the LLVM backend to implement versions of the required hooks that add an injection into KItem when called. This will require only a very small modification to your code as presented, but needs a bit of backend support.

[Baltoli]

Steps to implement the backend support in (3) above:

• Emit a table mapping tags to a sort string; this will only work for regular symbols and should be carefully documented as such.
• Add dual versions of the collection hooks (MAP.element etc.) that use that table to construct injected terms when called.

[virgil-serbanuta]

The solution should allow the semantics to also work in the Haskell backend.