[K-Bug] Unexpected name collisions of tokens with rules in `domains.md`

[jberthold]

What component is the issue in?

Front-End

Which command

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

What K Version?

v7.0.116

Operating System

Linux

K Definitions (If Possible)

module TEST-SYNTAX
  imports INT

  syntax Thing ::= A ( Int ) [symbol(A)]
                 | B ( Int ) [symbol(B)]
                 | C ( Int ) [symbol(C)]
endmodule

module TEST
  imports TEST-SYNTAX

endmodule

Steps to Reproduce

Trying to compile this file (with defaults: `kompile test.k`) yields a number of errors about tokens `B` and `C`

``` $ kompile test.k [Error] Inner Parser: Parse error: unexpected token 'B' following token 'andBool'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1130,21,1130,22) 1130 | rule true andBool B:Bool => B:Bool . ^ [Error] Inner Parser: Parse error: unexpected token 'B'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1131,8,1131,9) 1131 | rule B:Bool andBool true => B:Bool [simplification] . ^ [Error] Inner Parser: Parse error: unexpected token 'B' following token 'xorBool'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1140,22,1140,23) 1140 | rule false xorBool B:Bool => B:Bool . ^ [Error] Inner Parser: Parse error: unexpected token 'B'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1141,8,1141,9) 1141 | rule B:Bool xorBool false => B:Bool [simplification] . ^ [Error] Inner Parser: Parse error: unexpected token 'B'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1142,8,1142,9) 1142 | rule B:Bool xorBool B:Bool => false . ^ [Error] Inner Parser: Parse error: unexpected token 'B' following token 'orBool'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1146,21,1146,22) 1146 | rule false orBool B:Bool => B . ^ [Error] Inner Parser: Parse error: unexpected token 'B'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1147,8,1147,9) 1147 | rule B:Bool orBool false => B [simplification] . ^ [Error] Inner Parser: Parse error: unexpected token 'B' following token 'impliesBool'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1154,25,1154,26) 1154 | rule true impliesBool B:Bool => B . ^ [Error] Inner Parser: Parse error: unexpected token 'B'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(1157,8,1157,9) 1157 | rule B:Bool impliesBool false => notBool B [simplification] . ^ [Error] Inner Parser: Parse error: unexpected token 'C' following token '#if'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(2318,12,2318,13) 2318 | rule #if C:Bool #then B1::K #else _ #fi => B1 requires C . ^ [Error] Inner Parser: Parse error: unexpected token 'C' following token '#if'. Source(/nix/store/5jg4sp6ih9r5mb6a0cpg67lri592kpgp-k-7.0.116-57dd5ccd463ba891310a1d3a7d71f4e620476863/include/kframework/builtin/domains.md) Location(2319,12,2319,13) 2319 | rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C . ^ [Error] Compiler: Had 11 parsing errors. ```

When renaming B to BB and C to CC, the compilation succeeds.

In addition (as a separate issue maybe), after renaming and running kompile test.k, when I revert the test.k file to use the previous names B and C and re-run kompile test.k, the compilation also allegedly succeeds , unless the test-kompiled directory is deleted.

Expected Results

Successful compilation independent of the chosen constructor names.

[Baltoli]

What if we wrote:

"A" "(" Int ")"

instead? Do we still get the issue?

[Baltoli]

@dwightguth suggests we could precompile the prelude and avoid this kind of issue - separate scanner for the standard library and user code. Bit of an architectural change to do this sensibly.

[Baltoli]

This is not unique to the standard library. It can crop up in KEVM et. al. when smart contract code uses identifiers that collide with variables (solution there is munging / renaming).

[pxhdev]

This is not unique to the standard library. It can crop up in KEVM et. al. when smart contract code uses identifiers that collide with variables (solution there is munging / renaming).

I also encountered this issue. My situation is that the target ASM uses A-E to represent registers. However, if I code like syntax Reg ::= "B", it will corrupt the standard library. Unfortunately, renaming "A" to "RegA" or something similar is not an option, as it does not conform to the syntax. I think the ultimate solution would be to implement namespaces, but a temporary workaround might be to add a prefix or postfix to the standard library variables.