Usages of klabel{}(_) attribute remain

[Baltoli]

When working on runtimeverification/k#4035, I noticed that one test exercising the legacy Haskell backend failed after making the mechanical klabel(_), symbol refactorings implied in that issue: https://github.com/runtimeverification/k/tree/master/k-distribution/tests/regression-new/issue-1676-koreBytes

The error from the backend was:

$ make issue-1676-koreBytes
set -o pipefail; (cat 1.test.in 2>/dev/null || true) | /Users/brucecollie/code/k/k-distribution/bin/krun 1.test --output kore --no-exc-wrap  --definition ./test-kompiled | diff - 1.test.out
kore-exec: [147057] Error (ErrorException):
    Expecting hook 'BYTES.int2bytes' to reduce concrete pattern:
        /* T Fn D Spa */
        LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness{}(
            /* T Fn D Sfa Cl */ \dv{SortInt{}}("0"),
            /* T Fn D Sfa Cl */ \dv{SortInt{}}("0"),
            /* T Fn D Sfa Cl */ LbllittleEndianBytes{}()
        )
    CallStack (from HasCallStack):
      error, called at src/Kore/Rewrite/Axiom/EvaluationStrategy.hs:193:26 in kore-0.60.0.0-DddjtXjEFiY3CtblfXDv9H:Kore.Rewrite.Axiom.EvaluationStrategy
Expecting hook 'BYTES.int2bytes' to reduce concrete pattern:
    /* T Fn D Spa */
    LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness{}(
        /* T Fn D Sfa Cl */ \dv{SortInt{}}("0"),
        /* T Fn D Sfa Cl */ \dv{SortInt{}}("0"),
        /* T Fn D Sfa Cl */ LbllittleEndianBytes{}()
    )
CallStack (from HasCallStack):
  error, called at src/Kore/Rewrite/Axiom/EvaluationStrategy.hs:193:26 in kore-0.60.0.0-DddjtXjEFiY3CtblfXDv9H:Kore.Rewrite.Axiom.EvaluationStrategy
Created bug report: kore-exec.tar.gz
[Error] krun: kore-exec ./test-kompiled/definition.kore --module TEST --pattern /var/folders/8r/bzvz46gd0r5_fr11jt23fzyw0000gn/T/.krun-2024-03-15-12-34-50-bXtH0QYDVx/tmp.in.2uQgOtQkNg --output /var/folders/8r/bzvz46gd0r5_fr11jt23fzyw0000gn/T/.krun-2024-03-15-12-34-50-bXtH0QYDVx/result.kore
[Error] krun: Backend crashed during rewriting with exit code 1
0a1,16
> /* T Fn D Sfa Cl */
> Lbl'-LT-'generatedTop'-GT-'{}(
>     /* T Fn D Sfa Cl */
>     Lbl'-LT-'k'-GT-'{}(
>         /* T Fn D Sfa Cl */
>         kseq{}(
>             /* T Fn D Sfa Cli */
>             /* Inj: */ inj{SortBytes{}, SortKItem{}}(
>                 /* T Fn D Sfa Cl */ \dv{SortBytes{}}("")
>             ),
>             /* T Fn D Sfa Cl */ dotk{}()
>         )
>     ),
>     /* T Fn D Sfa Cl */
>     Lbl'-LT-'generatedCounter'-GT-'{}(/* T Fn D Sfa Cl */ \dv{SortInt{}}("0"))
> )
make: *** [1.test] Error 1

Some digging into the code reveals that this is because the backend treats Endianness and Signedness terms as special-cased builtins, but because these are not K hooked symbols, the backend needs to inspect the klabel{}(_) attribute to check for special-casing.

I have opened a draft fix in #3741 that simply looks for symbol'Kywd' instead of klabel in these cases (the only such places klabel is used). With this fix applied, I can pass the K regression test suite. However, there is now a dependency loop between the frontend and backend that we need to resolve to merge the fix. If there's a way to first look at klabel, then symbol'Kywd' if there's no klabel, then I think that would address the issue. We would then be able to update the K dependency for the integration tests and immediately remove the backwards compatibility.

[Baltoli]

As an update, I opened this Frankenstein PR: #3744

It demonstrates that if runtimeverification/k#4045 is merged along with #3741, that the integration test suite here is all successful. We still need to figure out exactly how to close this loop though.