Audit the anywhere attribute

[tothtamas28]

Related:

• Make KAST preprocessing pipeline explicit in _module_to_kore pyk#1022 (comment)

In ModuleToKORE, the anywhere attribute is added to a symbol in two cases.

1. If the symbol is overloaded.
   

   k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

   Line 1647 in 57001ad

   boolean isAnywhere = overloads.contains(prod);

2. If the symbol is rewritten by a rule that is anywhere.
   

   k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

   Line 1651 in 57001ad

   isAnywhere |= r.att().contains(Att.ANYWHERE());

We should consider the possibility of the following simplifications.

1. Split the two uses.
   • For case (1), introduce overloaded.
   • For case (2), require anywhere on productions instead of rules, similarly to how macro is used (first deprecate and emit a warning, then make it an error, etc).
2. Try to eliminate case (1).
   • The overload poset is reproducible in the backends based the symbol-overload attribute on overload axioms.
   • Alternatively, we can emit the overload poset directly using a symbol attribute, similarly to how e.g. priorities works.

[Baltoli]

The reasoning here is that it allows the LLVM backend to resolve overloading by actually just treating these axioms as anywhere rules and performing the associated rewrite.

[Baltoli]

We want to document these cases rather than modify them, I think:

• The first case that we use anywhere to rewrite overloaded symbols to their least form
• The second is caching the information "this symbol has an anywhere rule associated with it" so that the backend doesn't have to recompute

What does the legacy Haskell backend do here?

[ehildenb]

Are there any direct uses of eth anywhere attribute in semantics themselves? I don't think KEVM, KMIR, or KWasm has them, what about KCC?

If those places are minimal, maybe we can require that the user puts the anywhere attribute directly on the symbol, instead of on the rule, nad that would make it so that the pass maybe doesn't need to be a Definition-wide pass, but a Module-level pass.

[Baltoli]

The C semantics uses it pretty pervasively in the translation semantics. Maybe those usages would be translatable? I'd need to check to see

[ehildenb]

Are there any symbols that have some anywhere rules but not all of them? Or is it the case that every anywhere rule, has as its top symbol foo(..), that foo(...) only ever shows up at the top of an anywhere rule? If it's the case, we can move the attribute to the symbol, and then add a check instead of a pass which moves the attribute for teh user.

[tothtamas28]

Are there any symbols that have some anywhere rules but not all of them?

Yes, as pointed out by @dwightguth during today's K Compiler meeting, there might be rules for an anywhere symbol which we only want to apply on top.

So the only way to get rid of that pass is to do it in llvm-kompile (assuming the Haskell backend does not require it), if the additional execution time of this preprocessing step is acceptable there.

[ehildenb]

I don't understand, what is the example of a rule where there is an anywhere symbol where we only want to apply on top? Are they easily rewritten to not use that feature? I guess the goal here is t orestrict the allowed behavior in order to make our compiler more modular. If there are a few simple modifications we can make to the semantics to achieve that goal, then we should go for it. So we need the specific examples lined up and triaged

[tothtamas28]

I don't understand, what is the example of a rule where there is an anywhere symbol where we only want to apply on top?

As opposed to e.g. macro, currently the granularity of anywhere is per rule, so there might exist a symbol x that

• has a rewrite rule x => f [anywhere]
• has a rewrite rule x => f that's not anywhere

If we want to admit such symbols, then we cannot replace anywhere on rules by anywhere on symbols.

[ehildenb]

Yeah, I'm wondering what the use cases of such rules are. Are there any that are not re-writable to something else? What does it mean to have a non-anywhere rule where the LHS is a constructor in K? Does that mean it must be a topmost rule? If it's a function, why does it need to be anywhere?

[tothtamas28]

Another confusing thing regarding the two uses of anywhere on symbols.

Attribute constructor is only put on a symbol if it is not anywhere:

k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

Line 1668 in c4988e9

isConstructor &= !isAnywhere;

There's also method isConstructor that does not consider overloads:

k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

Line 1627 in c4988e9

private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {

And this function is used to filter productions for generating no-confusion axioms:

k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

Line 753 in c4988e9

|| !isConstructor(prod2, functionRulesMap)

Btw, for no-junk axioms, a third logic is used:

k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

Line 805 in c4988e9

if (isFunction(prod) || prod.isSubsort() || isBuiltinProduction(prod)) {