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

Open
#4,437 4 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
35/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Stale
Domain
compilers

Research direction

Start by reproducing the failure with the provided test.k definition using kompile, then inspect the Boolean and conditional rules in builtin/domains.md referenced by the errors. Done means compilation succeeds with constructor names B and C, including after deleting the generated test-kompiled directory and rerunning kompile.

Written by the indexing model from the issue text.

Description

What component is the issue in?

Front-End

Which command
  • 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.

Dominant language
Python
Stars
591
Forks
163
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.