kore-parser: Print human-readable parse errors (#2243)

Author: ttuegel

kore/app/parser/Main.hs

@@ -2,6 +2,11 @@ module Main (main) where
 
 import Prelude.Kore
 
+import Control.Monad.Catch
+    ( Exception (..)
+    , SomeException
+    , handle
+    )
 import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
@@ -30,9 +35,6 @@ import Kore.Attribute.Symbol
     )
 import qualified Kore.Builtin as Builtin
 import Kore.Debug
-import Kore.Error
-    ( printError
-    )
 import Kore.IndexedModule.IndexedModule
     ( VerifiedModule
     , toVerifiedDefinition
@@ -41,6 +43,9 @@ import Kore.Log
     ( runLoggerT
     )
 import qualified Kore.Log as Log
+import Kore.Log.ErrorVerify
+    ( errorVerify
+    )
 import Kore.Parser
     ( parseKoreDefinition
     , parseKorePattern
@@ -119,53 +124,61 @@ parserInfoModifiers =
                 \Verifies well-formedness"
     <> header "kore-parser - a parser for Kore definitions"
 
+{- | Top-level exception handler.
+
+Renders exceptions for the user with 'displayException' and exits
+unsuccessfully.
+
+ -}
+handleTop :: IO () -> IO ()
+handleTop =
+    handle handler
+  where
+    handler = die . displayException @SomeException
 
 -- TODO(virgil): Maybe add a regression test for main.
 -- | Parses a kore file and Check wellformedness
 main :: IO ()
-main = do
+main = handleTop $ do
     options <-
         mainGlobal
             (ExeName "kore-parser")
             Nothing  -- environment variable name for extra arguments
             commandLineParser
             parserInfoModifiers
-    case localOptions options of
-        Nothing ->  -- global options parsed, but local failed; exit gracefully
-            return ()
-        Just KoreParserOptions
-            { fileName
-            , patternFileName
-            , mainModuleName
-            , willPrintDefinition
-            , willPrintPattern
-            , willVerify
-            , appKore
-            }
-            -> flip runLoggerT Log.emptyLogger $ do
-                parsedDefinition <- mainDefinitionParse fileName
-                indexedModules <- if willVerify
-                    then lift $ mainVerify parsedDefinition
-                    else return Map.empty
-                lift $ when willPrintDefinition
-                    $ if appKore
-                        then putStrLn
-                            $ unparseToString2
-                            $ completeDefinition
-                            $ toVerifiedDefinition indexedModules
-                    else putDoc (debug parsedDefinition)
-
-                when (patternFileName /= "") $ do
-                    parsedPattern <- mainPatternParse patternFileName
-                    when willVerify $ do
-                        indexedModule <-
-                            lift $ lookupMainModule
-                                (ModuleName mainModuleName)
-                                indexedModules
-                        _ <- mainPatternVerify indexedModule parsedPattern
-                        return ()
-                    when willPrintPattern $
-                        lift $ putDoc (debug parsedPattern)
+    for_ (localOptions options) $ \koreParserOptions ->
+        flip runLoggerT Log.emptyLogger $ do
+            let KoreParserOptions { fileName } = koreParserOptions
+            parsedDefinition <- mainDefinitionParse fileName
+            let KoreParserOptions { willVerify } = koreParserOptions
+            indexedModules <- if willVerify
+                then lift $ mainVerify parsedDefinition
+                else return Map.empty
+            let KoreParserOptions { willPrintDefinition } = koreParserOptions
+            let KoreParserOptions { appKore } = koreParserOptions
+            lift $ when willPrintDefinition
+                $ if appKore
+                    then putStrLn
+                        $ unparseToString2
+                        $ completeDefinition
+                        $ toVerifiedDefinition indexedModules
+                else putDoc (debug parsedDefinition)
+
+            let KoreParserOptions { patternFileName } = koreParserOptions
+            unless (null patternFileName) $ do
+                parsedPattern <- mainPatternParse patternFileName
+                when willVerify $ do
+                    let KoreParserOptions { mainModuleName } = koreParserOptions
+                    indexedModule <-
+                        lookupMainModule
+                            (ModuleName mainModuleName)
+                            indexedModules
+                        & lift
+                    _ <- mainPatternVerify indexedModule parsedPattern
+                    return ()
+                let KoreParserOptions { willPrintPattern } = koreParserOptions
+                when willPrintPattern $
+                    lift $ putDoc (debug parsedPattern)
 
 -- | IO action that parses a kore definition from a filename and prints timing
 -- information.
@@ -182,18 +195,12 @@ mainPatternParse = mainParse parseKorePattern
 mainVerify
     :: ParsedDefinition
     -- ^ Parsed definition to check well-formedness
-    -> IO
-        (Map.Map
-            ModuleName
-            (VerifiedModule StepperAttributes)
-        )
+    -> IO (Map.Map ModuleName (VerifiedModule StepperAttributes))
 mainVerify definition = flip runLoggerT Log.emptyLogger $ do
     verifyResult <-
         clockSomething "Verifying the definition"
             (verifyAndIndexDefinition
                 Builtin.koreVerifiers
                 definition
             )
-    case verifyResult of
-        Left err1            -> liftIO $ die $ printError err1
-        Right indexedModules -> return indexedModules
+    either errorVerify return verifyResult

kore/app/share/GlobalMain.hs

@@ -118,14 +118,16 @@ import qualified Kore.Attribute.Symbol as Attribute
     ( Symbol
     )
 import qualified Kore.Builtin as Builtin
-import Kore.Error
 import Kore.IndexedModule.IndexedModule
     ( VerifiedModule
     )
 import Kore.Log as Log
 import Kore.Log.ErrorParse
     ( errorParse
     )
+import Kore.Log.ErrorVerify
+    ( errorVerify
+    )
 import Kore.Parser
     ( ParsedPattern
     , parseKoreDefinition
@@ -451,7 +453,7 @@ mainPatternVerify verifiedModule patt = do
     verifyResult <-
         clockSomething "Verifying the pattern"
             (runPatternVerifier context $ verifyStandalonePattern Nothing patt)
-    either (error . printError) return verifyResult
+    either errorVerify return verifyResult
   where
     context =
         PatternVerifier.verifiedModuleContext verifiedModule
@@ -500,9 +502,7 @@ verifyDefinitionWithBase
             Builtin.koreVerifiers
             definition
         )
-    case verifyResult of
-        Left err1               -> error (printError err1)
-        Right indexedDefinition -> return indexedDefinition
+    either errorVerify return verifyResult
 
 {- | Parse a Kore definition from a filename.
 

kore/src/Kore/Log/ErrorParse.hs

@@ -25,8 +25,8 @@ newtype ErrorParse = ErrorParse { message :: String }
 
 instance Exception ErrorParse where
     toException = toException . SomeEntry
-    fromException exn =
-        fromException exn >>= fromEntry
+    fromException exn = fromException exn >>= fromEntry
+    displayException = message
 
 instance Pretty ErrorParse where
     pretty ErrorParse { message } =

kore/src/Kore/Log/ErrorVerify.hs

@@ -0,0 +1,44 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.ErrorVerify
+    ( ErrorVerify (..)
+    , errorVerify
+    ) where
+
+import Prelude.Kore
+
+import Control.Monad.Catch
+    ( Exception (..)
+    , MonadThrow
+    , throwM
+    )
+import Pretty
+
+import Kore.ASTVerifier.Error
+    ( VerifyError
+    )
+import qualified Kore.Error as Kore
+import Log
+
+newtype ErrorVerify = ErrorVerify { koreError :: Kore.Error VerifyError }
+    deriving Show
+
+instance Exception ErrorVerify where
+    toException = toException . SomeEntry
+    fromException exn = fromException exn >>= fromEntry
+    displayException = Kore.printError . koreError
+
+instance Pretty ErrorVerify where
+    pretty ErrorVerify { koreError } =
+        Pretty.pretty (Kore.printError koreError)
+
+instance Entry ErrorVerify where
+    entrySeverity _ = Error
+
+errorVerify :: MonadThrow log => Kore.Error VerifyError -> log a
+errorVerify koreError =
+    throwM ErrorVerify { koreError }

kore/src/Kore/Log/Registry.hs

@@ -84,6 +84,9 @@ import Kore.Log.ErrorRuleMergeDuplicate
     ( ErrorRuleMergeDuplicateIds
     , ErrorRuleMergeDuplicateLabels
     )
+import Kore.Log.ErrorVerify
+    ( ErrorVerify
+    )
 import Kore.Log.InfoAttemptUnification
     ( InfoAttemptUnification
     )
@@ -162,6 +165,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @ErrorBottomTotalFunction
     , mk $ Proxy @ErrorDecidePredicateUnknown
     , mk $ Proxy @ErrorParse
+    , mk $ Proxy @ErrorVerify
     , mk $ Proxy @ErrorRuleMergeDuplicateIds
     , mk $ Proxy @ErrorRuleMergeDuplicateLabels
     , mk $ Proxy @WarnFunctionWithoutEvaluators

kore/src/Log/Entry.hs

@@ -69,7 +69,9 @@ data SomeEntry where
 
 instance Show SomeEntry where
     show (SomeEntry entry) = show entry
-instance Exception SomeEntry
+
+instance Exception SomeEntry where
+    displayException = show . longDoc
 
 instance Entry SomeEntry where
     toEntry = id

kore/test/resources/test-bool-2.kore.golden

@@ -0,0 +1,34 @@
+ifeq ($(origin TOP), undefined)
+	TOP = $(shell git rev-parse --show-toplevel)
+endif
+
+include $(TOP)/include.mk
+
+DIFF = diff -u
+%.golden: DIFF = true
+
+FAILED = ( mv $@ $@.fail && false )
+
+TESTS = $(wildcard *.kore)
+OUTS += $(foreach TEST, $(TESTS), $(TEST).out)
+GOLDEN += $(foreach TEST, $(TESTS), $(TEST).golden)
+
+%.kore.out : %.kore $(KORE_PARSER)
+	$(KORE_PARSER) --no-print-definition $< 2>$@ || true
+	$(DIFF) $*.kore.golden $@ || $(FAILED)
+
+%.golden: %.out
+	cp $< $@
+
+### TARGETS
+
+test: test-k
+
+test-k: $(OUTS)
+
+golden: $(GOLDEN)
+
+clean:
+	rm -fr *.out *.fail
+
+.PHONY: test-k test golden clean