`UNIQUE_ID`s are not unique

[tothtamas28]

This has multiple causes, including

• https://github.com/runtimeverification/k/issues/3906
• The user defines the same rule in two different modules, which then only differ in Source / Location.

A pyk script to list duplicate IDs:

from pyk.kast.outer import read_kast_definition

DEFINITION_DIR = 'kompiled/compiled.json'  # set accordingly

defn = read_kast_definition(DEFINITION_DIR)

rules_by_id = {}
for rule in defn.rules:
    unique_id = rule.att['UNIQUE_ID']
    rules_by_id.setdefault(unique_id, set()).add(rule)

for unique_id, rules in rules_by_id.items():
    if len(rules) > 1:
        print(unique_id)

The rules can then be looked up in compiled.txt by ID.

[Baltoli]

We should codify precisely the semantics of the UNIQUE_ID attribute and make sure that we understand it properly.

[gtrepta]

My understanding is that UNIQUE_ID is meant to be a hash of the rule body/requires and any semantics changing attributes it has. So any two rules that are semantically the same, despite being in different source locations, are supposed to have the same id.