Fix "Hooked sorts may not have subsorts" error (#2177)

Author: andreiburdusa

kore/app/share/GlobalMain.hs

@@ -118,6 +118,9 @@ import Kore.IndexedModule.IndexedModule
     ( VerifiedModule
     )
 import Kore.Log as Log
+import Kore.Log.ErrorParse
+    ( errorParse
+    )
 import Kore.Parser
     ( ParsedPattern
     , parseKoreDefinition
@@ -506,7 +509,7 @@ mainParse parser fileName = do
     parseResult <-
         clockSomething "Parsing the file" (parser fileName contents)
     case parseResult of
-        Left err         -> error err
+        Left err         -> errorParse err
         Right definition -> return definition
 
 type LoadedModule = VerifiedModule Attribute.Symbol

kore/src/Kore/ASTVerifier/AttributesVerifier.hs

@@ -19,6 +19,10 @@ module Kore.ASTVerifier.AttributesVerifier
     ) where
 
 import qualified Control.Lens as Lens
+import Data.Foldable
+    ( find
+    , for_
+    )
 import Data.Generics.Product
 import Prelude.Kore
 
@@ -28,6 +32,7 @@ import qualified Data.Functor.Foldable as Recursive
 import Kore.ASTVerifier.Error
 import qualified Kore.Attribute.Axiom as Attribute
     ( Axiom
+    , sourceLocation
     )
 import Kore.Attribute.Hook
 import Kore.Attribute.Overload
@@ -37,6 +42,9 @@ import Kore.Attribute.Sort
 import Kore.Attribute.Sort.HasDomainValues
 import Kore.Attribute.Subsort as Subsort
 
+import Kore.AST.AstWithLocation
+    ( locationFromAst
+    )
 import qualified Kore.Attribute.Parser as Attribute.Parser
 import qualified Kore.Attribute.Symbol as Attribute
 import Kore.Error
@@ -50,11 +58,18 @@ import Kore.Syntax.Application
     ( SymbolOrAlias (..)
     )
 import Kore.Syntax.Definition
+import Kore.Syntax.Id
+    ( prettyPrintAstLocation
+    )
 import Kore.Syntax.Pattern
 import Kore.Syntax.Variable
     ( VariableName (..)
     )
+import Kore.Unparser
+    ( unparse
+    )
 import qualified Kore.Verified as Verified
+import Pretty
 
 parseAttributes :: MonadError (Error VerifyError) m => Attributes -> m Hook
 parseAttributes = Attribute.Parser.liftParser . Attribute.Parser.parseAttributes
@@ -138,11 +153,29 @@ verifyNoHookAttribute attributes = do
 
 verifyNoHookedSupersort
     :: MonadError (Error VerifyError) error
-    => [Kore.Attribute.Sort.Sort]
+    => IndexedModule Verified.Pattern Attribute.Symbol attrs
+    -> Attribute.Axiom SymbolOrAlias VariableName
+    -> [Subsort.Subsort]
     -> error ()
-verifyNoHookedSupersort supersortsAtts = do
-    let isHooked = getHasDomainValues . hasDomainValues <$> supersortsAtts
-    when (or isHooked) $ koreFail "Hooked sorts may not have subsorts."
+verifyNoHookedSupersort indexedModule axiom subsorts = do
+    let isHooked =
+            getHasDomainValues . hasDomainValues
+            . getSortAttributes indexedModule
+            . Subsort.supersort
+        hookedSubsort = find isHooked subsorts
+    for_ hookedSubsort $ \sort ->
+        koreFail . unlines $
+            [ "Hooked sorts may not have subsorts."
+            , "Hooked sort:"
+            , show . unparse $ Subsort.supersort sort
+            , "Its subsort:"
+            , show . unparse $ Subsort.subsort sort
+            , "Location in the Kore file:"
+            , show . prettyPrintAstLocation
+                $ locationFromAst (Subsort.supersort sort)
+            , "Location in the original K file: "
+            , show . pretty $ Attribute.sourceLocation axiom
+            ]
 
 verifyAxiomAttributes
     :: forall error attrs
@@ -152,9 +185,8 @@ verifyAxiomAttributes
     -> error (Attribute.Axiom Internal.Symbol.Symbol VariableName)
 verifyAxiomAttributes indexedModule axiom = do
     let overload = axiom Lens.^. field @"overload"
-        supersorts = Subsort.supersort <$> getSubsorts (axiom Lens.^. field @"subsorts")
-        supersortsAtts = getSortAttributes indexedModule <$> supersorts
-    verifyNoHookedSupersort supersortsAtts
+        subsorts = getSubsorts (axiom Lens.^. field @"subsorts")
+    verifyNoHookedSupersort indexedModule axiom subsorts
     case getOverload overload of
             Nothing -> do
                 let newOverload = Overload Nothing

kore/src/Kore/Log/ErrorParse.hs

@@ -0,0 +1,40 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.ErrorParse
+    ( ErrorParse (..)
+    , errorParse
+    ) where
+
+import Prelude.Kore
+
+import Control.Monad.Catch
+    ( Exception (..)
+    , MonadThrow
+    , throwM
+    )
+import Pretty
+
+import Log
+
+newtype ErrorParse = ErrorParse { message :: String }
+    deriving Show
+
+instance Exception ErrorParse where
+    toException = toException . SomeEntry
+    fromException exn =
+        fromException exn >>= fromEntry
+
+instance Pretty ErrorParse where
+    pretty ErrorParse { message } =
+        Pretty.pretty message
+
+instance Entry ErrorParse where
+    entrySeverity _ = Error
+
+errorParse :: MonadThrow log => String -> log a
+errorParse message =
+    throwM ErrorParse { message }

kore/src/Kore/Log/Registry.hs

@@ -71,6 +71,9 @@ import Kore.Log.ErrorDecidePredicateUnknown
 import Kore.Log.ErrorException
     ( ErrorException
     )
+import Kore.Log.ErrorParse
+    ( ErrorParse
+    )
 import Kore.Log.ErrorRewriteLoop
     ( ErrorRewriteLoop
     )
@@ -151,6 +154,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @DebugSubstitutionSimplifier
     , mk $ Proxy @ErrorBottomTotalFunction
     , mk $ Proxy @ErrorDecidePredicateUnknown
+    , mk $ Proxy @ErrorParse
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckClaimState

test/no-injection-into-hooked/test.k.verify.out.golden

@@ -2,3 +2,12 @@ Error:
   module 'TEST':
   axiom declaration:
     Hooked sorts may not have subsorts.
+    Hooked sort:
+    SortInt{}
+    Its subsort:
+    SortS{}
+    Location in the Kore file:
+    "./test-kompiled/definition.kore 209:136"
+    Location in the original K file: 
+    
+