Disallow sorts with case-insensitive equal names

Open
#4,508 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
Tech stack
macos, python
Domain
compilers, operating-systems

Research direction

Reproduce the issue with the shown kompile and krun commands on macOS, then inspect the generated LblisFoo.yaml and LblisFOO.yaml files and the decision-tree compilation path. Done means sorts equal up to casing are rejected before their generated files can collide, with coverage for the reported example.

Written by the indexing model from the issue text.

Description

Consider the following definition:

module TEST
  imports BOOL

  syntax Foo ::= "Foo"
  syntax FOO ::= "FOO"

  syntax KItem ::= result(KItem, Bool, Bool)
  rule F:Foo => result(F, isFoo(F), isFOO(F))
  rule F:FOO => result(F, isFoo(F), isFOO(F))
endmodule

We can see by inspection that there is no term X for which isFoo(X) and isFOO(X) are both true. However, on macOS, we can observe the following executions:

$ kompile test.k
$ krun -cPGM='Foo'
<k>
  result ( Foo , false , false ) ~> .K
</k>
$ krun -cPGM='FOO'
<k>
  result ( FOO , true , true ) ~> .K
</k>

That is, isFoo(Foo) => false, and isFOO(Foo) => true! Both of these rewrites are incorrect.

Some digging reveals that the reason for this is the case-insensitive filesystem on macOS; when decision trees are compiled, files LblisFoo.yaml and LblisFOO.yaml are both generated. However, one of them overwrites the other because of case-insensitivity. This means that the logic for all case-insensitive-equal sorts gets collapsed into one.

The solution (I think) is to disallow sorts that are equal up to casing.

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.