Add attribute whitelist and group(_) attribute

[Scott-Guest]

First step of #2625

• Update Att.scala to include all attributes used in the frontend code or documented in the K User Manual
• Add a group(name1,...,nameN) attribute for user-defined groups
• Add a --pedantic-attributes flag to enforce that all attributes are either provided through group(_) or defined in Att

In the process, I also changed the type of attribute keys from String to a case class Att.Key with a String field. This is useful because

• keeping the Att.Key constructor private forces every new attribute to define its key in Att, thereby maintaining the whitelist
• IDE navigation can now point you to every usage of an attribute

The diff is quite large, but almost all changes just replace string literals "my-att" with Att.MY_ATT().

[Scott-Guest]

@radumereuta I know you mentioned expanding the group(_) attributes in KILtoKORE. I ended up having to place it a little earlier because KILtoKORE expects an already-constructed Context which will only be correctly built once group(_) is already expanded.

[radumereuta]

Looks very good.
See my inline comments. I think you're missing a few location info for some error messages.
This is very large, and I would like it if someone else at least skims over it.

[Scott-Guest]

After my latest changes, a KeyType member was added to Att.Key which can be one of the following:

• BuiltIn, for user-facing attributes
• Internal, for compiler-internal attributes
• UserGroup, for user-defined groups provided via group(_)
• Raw, for yet-to-be-processed or unrecognized attributes

The pipeline now works as follows:

• The parser inserts a BuiltIn if the key is recognized, or else inserts a Raw key.
• Immediately after every call to the parser, a pass ProcessGroupAttributes is run which:
  • Replaces [group(g1,...,gN)] with [g1,...,gN]
  • If --pedantic-attributes is disabled, replaces every Raw key with a UserGroup (or errors if it conflicts with an Internal)
• In KILtoKORE, ProcessGroupAttributes is run again. Two passes are necessary because
  • the first pass ensures the Context passed to KILtoKORE is constructed correctly
  • the second pass ensures that rule attributes are expanded, which would be missed in the first pass
    as rules are still unparsed
• In CheckAtt, errors are emitted for any unhandled Raw keys
• In GenerateSentencesFromConfigDecl, the same process is applied to cell-attributes <cell foo="bar">

A few things worth mentioning:

• transition was made a built-in rather than an internal (differing from the list @dwightguth provided) because of its use here: https://github.com/runtimeverification/k/blob/master/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
• index was added to the whitelist. I can't for the life of me seem to find where this gets used, but removing it from syntax Map ::= Map Map in domains.md breaks the test map-symbolic-tests-haskell/assignment-11-spec.k
• smt-prelude was removed from a few tests (it appears to be dead-code anyways)
• lookup and choice attributes were removed (also dead code, and conflicted with user groups in the PL tutorials)

Additionally, we now report errors if user groups conflict with internal attributes, regardless of the --pedantic-attributes flag. In a follow-up submit, I'll address this and make it so that internal and group attributes are namespaced separately.

[dwightguth]

I'm aware that transition is still existing in some places. I didn't put it on the whitelist because it is a dead attribute that no longer does anything and needs to eventually be deleted everywhere.

[dwightguth]

I'd guess that the map test in question is probably just fragile. It's not a big deal to leave it there so that we don't have to try to fix the test now, but it's probably worth having someone investigate the test and try and see why changing one attribute of one production leads to a different test output

[Scott-Guest]

Blocked until runtimeverification/k-exercises/pull/36 is merged

[Baltoli]

Dwight will need to hit the final approval as there are unresolved change requests but this looks good to me; I note that the blocking PR to k-exercises is merged as well.

Stale