Remove uses of klabel{}(_) attribute for special-casing symbols (#3741

)

See #3742 for full context; this PR adds a backwards-compatible check
for `symbol'Kywd` as well as `klabel` for the pseudo-builtin sorts
`Endianness` and `Signedness`. When this is merged, I'll be able to
finish working on runtimeverification/k#4045.
Then, when that PR lands, the frontend will no longer emit `klabel(_)`
to KORE, and we can safely remove the backwards-compatible part of this
PR.

The integration test suite's checked-in KORE files are all updated to
use the new attribute rather than the old one, but the tests that use K
to compile fresh KORE will still be using `klabel(_)` until the
dependency update job induced by the changes above goes through.

I have verified manually that building K with this HB commit allows the
failing integration test in #3742 to pass.

Thanks @jberthold for the suggestions!

~~The implementation here would ideally be made backwards-compatible; my
version induces a dependency loop (hence failing tests, it would need an
update to the K dependency to go through first for the integration test
suite to pass).~~

kore/src/Kore/Attribute/Symbol/SymbolKywd.hs

@@ -20,7 +20,7 @@ import Prelude.Kore
   Hold an optional Text, which is an empty string if the attribute had
   no argument. Use sites can check emptiness to achieve old behaviour.
 -}
-newtype SymbolKywd = SymbolKywd {getSymbol :: Maybe Text}
+newtype SymbolKywd = SymbolKywd {getSymbolKywd :: Maybe Text}
     deriving stock (Eq, Ord, Show)
     deriving stock (GHC.Generic)
     deriving anyclass (Hashable, NFData)
@@ -50,13 +50,13 @@ instance ParseAttributes SymbolKywd where
     -- if an argument is present, use it for the contents, otherwise
     -- leave it empty (but present) to signal presence of the attribute.
     parseAttribute =
-        withApplication symbolKywdId $ \params args SymbolKywd{getSymbol} -> do
+        withApplication symbolKywdId $ \params args SymbolKywd{getSymbolKywd} -> do
             Parser.getZeroParams params
             mbArg <- Parser.getZeroOrOneArguments args
-            unless (isNothing getSymbol) $ failDuplicate symbolKywdId
+            unless (isNothing getSymbolKywd) $ failDuplicate symbolKywdId
             StringLiteral arg <- maybe (pure $ StringLiteral "") getStringLiteral mbArg
             pure $ SymbolKywd (Just arg)
 
 instance From SymbolKywd Attributes where
     from =
-        maybe def (from @AttributePattern . symbolKywdAttribute) . getSymbol
+        maybe def (from @AttributePattern . symbolKywdAttribute) . getSymbolKywd

kore/src/Kore/Builtin/Endianness.hs

@@ -62,9 +62,9 @@ endiannessVerifier ctor =
     worker application = do
         -- TODO (thomas.tuegel): Move the checks into the symbol verifiers.
         unless (null arguments) (koreFail "expected zero arguments")
-        let Attribute.Symbol.SymbolKywd{getSymbol} =
+        let Attribute.Symbol.SymbolKywd{getSymbolKywd} =
                 Attribute.Symbol.symbolKywd $ symbolAttributes symbol
-        unless (isJust getSymbol) (koreFail "expected symbol'Kywd'{}() attribute")
+        unless (isJust getSymbolKywd) (koreFail "expected symbol'Kywd'{}() attribute")
         return (EndiannessF . Const $ ctor symbol)
       where
         arguments = applicationChildren application

kore/src/Kore/Builtin/Signedness.hs

@@ -62,9 +62,9 @@ signednessVerifier ctor =
     worker application = do
         -- TODO (thomas.tuegel): Move the checks into the symbol verifiers.
         unless (null arguments) (koreFail "expected zero arguments")
-        let Attribute.Symbol.SymbolKywd{getSymbol} =
+        let Attribute.Symbol.SymbolKywd{getSymbolKywd} =
                 Attribute.Symbol.symbolKywd $ symbolAttributes symbol
-        unless (isJust getSymbol) (koreFail "expected symbol'Kywd'{}() attribute")
+        unless (isJust getSymbolKywd) (koreFail "expected symbol'Kywd'{}() attribute")
         return (SignednessF . Const $ ctor symbol)
       where
         arguments = applicationChildren application

kore/src/Kore/Builtin/Verifiers.hs

@@ -171,7 +171,7 @@ lookupApplicationVerifier ::
     ApplicationVerifiers patternType ->
     Maybe (ApplicationVerifier patternType)
 lookupApplicationVerifier symbol verifiers = do
-    key <- getHook symbol <|> getKlabel symbol
+    key <- getHook symbol <|> getKlabel symbol <|> getSymbolKywd symbol
     HashMap.lookup key verifiers
   where
     getHook =
@@ -184,6 +184,11 @@ lookupApplicationVerifier symbol verifiers = do
             . Attribute.Symbol.getKlabel
             . Attribute.Symbol.klabel
             . symbolAttributes
+    getSymbolKywd =
+        fmap KlabelSymbolKey
+            . Attribute.Symbol.getSymbolKywd
+            . Attribute.Symbol.symbolKywd
+            . symbolAttributes
 
 applicationPatternVerifierHooks ::
     ApplicationVerifiers patternType ->

kore/src/Kore/Internal/Symbol.hs

@@ -229,11 +229,11 @@ klabel name =
         (typed @Attribute.Symbol . typed @Attribute.Klabel)
         Attribute.Klabel{getKlabel = Just name}
 
-symbolKywd :: Symbol -> Symbol
-symbolKywd =
+symbolKywd :: Text -> Symbol -> Symbol
+symbolKywd name =
     Lens.set
         (typed @Attribute.Symbol . typed @Attribute.SymbolKywd)
-        Attribute.SymbolKywd{getSymbol = Just ""}
+        Attribute.SymbolKywd{getSymbolKywd = Just name}
 
 {- | Coerce a sort injection symbol's source and target sorts.
 

kore/test/Test/Kore/Attribute/Symbol.hs

@@ -187,7 +187,7 @@ test_SymbolKywd =
     [ testCase "parseAttribute" $
         assertEqual
             "[symbolKywd{}()]"
-            (Right SymbolKywd{getSymbol = Just ""})
+            (Right SymbolKywd{getSymbolKywd = Just ""})
             (symbolKywd <$> parse [symbolKywdAttribute ""])
     , testCase "defaultSymbolAttributes" $
         assertEqual

kore/test/Test/Kore/Attribute/Symbol/SymbolKywd.hs

@@ -20,7 +20,7 @@ parseSymbolKywd = parseAttributes
 test_symbolKywd :: TestTree
 test_symbolKywd =
     testCase "[symbolKywd{}()] :: SymbolKywd" $
-        expectSuccess SymbolKywd{getSymbol = Just ""} $
+        expectSuccess SymbolKywd{getSymbolKywd = Just ""} $
             parseSymbolKywd $
                 Attributes [symbolKywdAttribute ""]
 
@@ -42,7 +42,7 @@ test_duplicate =
 test_argument :: TestTree
 test_argument =
     testCase "[symbolKywd{}(\"legal\")]" $
-        expectSuccess SymbolKywd{getSymbol = Just "legal"} $
+        expectSuccess SymbolKywd{getSymbolKywd = Just "legal"} $
             parseSymbolKywd $
                 Attributes [legalAttribute]
   where

kore/test/Test/Kore/Builtin/Definition.hs

@@ -54,7 +54,6 @@ import Kore.Internal.Symbol (
     function,
     hook,
     injective,
-    klabel,
     smthook,
     sortInjection,
     symbolKywd,
@@ -732,32 +731,28 @@ concatString x y = mkApplySymbol concatStringSymbol [x, y]
 littleEndianBytesSymbol :: Internal.Symbol
 littleEndianBytesSymbol =
     builtinSymbol "littleEndianBytes" endiannessSort []
-        & klabel "littleEndianBytes"
-        & symbolKywd
+        & symbolKywd "littleEndianBytes"
 littleEndianBytes :: InternalVariable variable => TermLike variable
 littleEndianBytes =
     mkEndianness (Endianness.LittleEndian littleEndianBytesSymbol)
 bigEndianBytesSymbol :: Internal.Symbol
 bigEndianBytesSymbol =
     builtinSymbol "bigEndianBytes" endiannessSort []
-        & klabel "bigEndianBytes"
-        & symbolKywd
+        & symbolKywd "bigEndianBytes"
 bigEndianBytes :: InternalVariable variable => TermLike variable
 bigEndianBytes =
     mkEndianness (Endianness.BigEndian bigEndianBytesSymbol)
 signedBytesSymbol :: Internal.Symbol
 signedBytesSymbol =
     builtinSymbol "signedBytes" signednessSort []
-        & klabel "signedBytes"
-        & symbolKywd
+        & symbolKywd "signedBytes"
 signedBytes :: InternalVariable variable => TermLike variable
 signedBytes =
     mkSignedness (Signedness.Signed signedBytesSymbol)
 unsignedBytesSymbol :: Internal.Symbol
 unsignedBytesSymbol =
     builtinSymbol "unsignedBytes" signednessSort []
-        & klabel "unsignedBytes"
-        & symbolKywd
+        & symbolKywd "unsignedBytes"
 unsignedBytes :: InternalVariable variable => TermLike variable
 unsignedBytes =
     mkSignedness (Signedness.Unsigned unsignedBytesSymbol)