Add option to turn an arbitrary log entry into an error (#2298)

Author: andreiburdusa

kore/src/Kore/Log.hs

@@ -119,18 +119,19 @@ koreLogTransformer
     -> LogAction m ActualEntry
 koreLogTransformer koreLogOptions baseLogger =
     Colog.cmap
-        ( warningsToErrors warningSwitch
-        )
+        ( toErrors warningSwitch )
         baseLogger
   where
-    KoreLogOptions { warningSwitch } = koreLogOptions
+    KoreLogOptions { turnedIntoErrors, warningSwitch } = koreLogOptions
 
-    warningsToErrors :: WarningSwitch -> ActualEntry -> ActualEntry
-    warningsToErrors AsError entry@ActualEntry { actualEntry }
+    toErrors :: WarningSwitch -> ActualEntry -> ActualEntry
+    toErrors AsError ActualEntry { actualEntry }
         | entrySeverity actualEntry == Warning =
             error . show . longDoc $ actualEntry
+    toErrors _ entry@ActualEntry { actualEntry }
+        | typeOfSomeEntry actualEntry `elem` turnedIntoErrors =
+            error . show . longDoc $ actualEntry
         | otherwise = entry
-    warningsToErrors AsWarning entry = entry
 
 koreLogFilters
     :: Applicative m

kore/src/Kore/Log/KoreLogOptions.hs

@@ -68,6 +68,7 @@ import Kore.Log.DebugSolver
     )
 import Kore.Log.Registry
     ( getEntryTypesAsText
+    , getNoErrEntryTypesAsText
     , parseEntryType
     )
 import Kore.Log.SQLite
@@ -96,6 +97,7 @@ data KoreLogOptions = KoreLogOptions
     , startTime :: !TimeSpec
     , logSQLiteOptions :: !LogSQLiteOptions
     , warningSwitch :: !WarningSwitch
+    , turnedIntoErrors :: !EntryTypes
     , debugApplyEquationOptions :: !DebugApplyEquationOptions
     , debugAttemptEquationOptions :: !DebugAttemptEquationOptions
     , debugEquationOptions :: !DebugEquationOptions
@@ -117,6 +119,7 @@ defaultKoreLogOptions exeName startTime =
         , startTime
         , logSQLiteOptions = def @LogSQLiteOptions
         , warningSwitch = def @WarningSwitch
+        , turnedIntoErrors = mempty
         , debugApplyEquationOptions = def @DebugApplyEquationOptions
         , debugAttemptEquationOptions = def @DebugAttemptEquationOptions
         , debugEquationOptions = def @DebugEquationOptions
@@ -182,6 +185,7 @@ parseKoreLogOptions exeName startTime =
     <*> pure startTime
     <*> parseLogSQLiteOptions
     <*> parseWarningSwitch
+    <*> (mconcat <$> many parseErrorEntries)
     <*> parseDebugApplyEquationOptions
     <*> parseDebugAttemptEquationOptions
     <*> parseDebugEquationOptions
@@ -201,12 +205,13 @@ parseEntryTypes =
             [ "Log entries: logs entries of supplied types"
             , "Available entry types:"
             , (OptPretty.indent 4 . OptPretty.vsep)
-                (OptPretty.text <$> getEntryTypesAsText)
+                ( OptPretty.text <$> getEntryTypesAsText )
             ]
 
-    parseCommaSeparatedEntries =
-        Options.maybeReader $ Parser.parseMaybe parseEntryTypes'
-
+parseCommaSeparatedEntries :: Options.ReadM EntryTypes
+parseCommaSeparatedEntries =
+    Options.maybeReader $ Parser.parseMaybe parseEntryTypes'
+  where
     parseEntryTypes' :: Parser.Parsec String String EntryTypes
     parseEntryTypes' = Set.fromList <$> Parser.sepEndBy parseSomeTypeRep comma
 
@@ -244,6 +249,27 @@ parseWarningSwitch =
         <> Options.help "Turn warnings into errors"
         )
 
+parseErrorEntries :: Parser EntryTypes
+parseErrorEntries =
+    option parseCommaSeparatedEntries info
+  where
+    info =
+        mempty
+        <> Options.long "error-entries"
+        <> Options.helpDoc ( Just nonErrorEntryTypes )
+
+    nonErrorEntryTypes :: OptPretty.Doc
+    nonErrorEntryTypes =
+        OptPretty.vsep
+            [ "Turn arbitrary log entries into errors"
+            , "Available entry types:"
+            , (OptPretty.indent 4 . OptPretty.vsep)
+                (OptPretty.text <$> getNoErrEntryTypesAsText)
+            {- The user can still give error entries as arguments, but it's
+                useless, so we don't list them here
+            -}
+            ]
+
 -- | Caller of the logging function
 newtype ExeName = ExeName { getExeName :: String }
     deriving (Eq, Show)
@@ -396,6 +422,7 @@ unparseKoreLogOptions
         _
         logSQLiteOptions
         warningSwitch
+        toError
         debugApplyEquationOptions
         debugAttemptEquationOptions
         debugEquationOptions
@@ -409,6 +436,7 @@ unparseKoreLogOptions
         , debugSolverOptionsFlag debugSolverOptions
         , logSQLiteOptionsFlag logSQLiteOptions
         , ["--warnings-to-errors" | AsError <- [warningSwitch] ]
+        , logEntriesFlag toError
         , debugApplyEquationOptionsFlag debugApplyEquationOptions
         , debugAttemptEquationOptionsFlag debugAttemptEquationOptions
         , debugEquationOptionsFlag debugEquationOptions

kore/src/Kore/Log/Registry.hs

@@ -11,12 +11,20 @@ module Kore.Log.Registry
     , typeToText
     , textToType
     , getEntryTypesAsText
+    , getErrEntryTypesAsText
+    , getNoErrEntryTypesAsText
     , typeOfSomeEntry
+    , entryTypeRepsErr
+    , entryTypeRepsNoErr
     , entryTypeReps
     ) where
 
 import Prelude.Kore
 
+import Control.Lens
+    ( (%~)
+    )
+import qualified Control.Lens as Lens
 import Data.Functor.Classes
     ( eq2
     )
@@ -139,7 +147,8 @@ data Registry =
 -- When adding a new entry type you should register it here.
 registry :: Registry
 registry =
-    let textToType = (Map.fromList . map register) entryTypeReps
+    let textToType =
+            (Map.fromList . map register) entryTypeReps
         typeToText = makeInverse textToType
     in if textToType `eq2` makeInverse typeToText
           then Registry { textToType, typeToText }
@@ -154,41 +163,49 @@ registry =
         (asText type', type')
 
 entryTypeReps :: [SomeTypeRep]
-entryHelpDocs :: [Pretty.Doc ()]
-(entryTypeReps, entryHelpDocs) =
-    unzip
-    [ mk $ Proxy @DebugSolverSend
-    , mk $ Proxy @DebugSolverRecv
-    , mk $ Proxy @DebugClaimState
-    , mk $ Proxy @DebugAppliedRewriteRules
-    , mk $ Proxy @DebugSubstitutionSimplifier
-    , mk $ Proxy @ErrorBottomTotalFunction
-    , mk $ Proxy @ErrorDecidePredicateUnknown
-    , mk $ Proxy @ErrorParse
-    , mk $ Proxy @ErrorVerify
-    , mk $ Proxy @ErrorRuleMergeDuplicateIds
-    , mk $ Proxy @ErrorRuleMergeDuplicateLabels
-    , mk $ Proxy @WarnFunctionWithoutEvaluators
-    , mk $ Proxy @WarnSymbolSMTRepresentation
-    , mk $ Proxy @WarnStuckClaimState
-    , mk $ Proxy @WarnIfLowProductivity
-    , mk $ Proxy @WarnTrivialClaim
-    , mk $ Proxy @WarnRetrySolverQuery
-    , mk $ Proxy @DebugEvaluateCondition
-    , mk $ Proxy @ErrorException
-    , mk $ Proxy @ErrorRewriteLoop
-    , mk $ Proxy @LogMessage
-    , mk $ Proxy @InfoAttemptUnification
-    , mk $ Proxy @InfoReachability
-    , mk $ Proxy @InfoExecBreadth
-    , mk $ Proxy @ErrorRewritesInstantiation
-    , mk $ Proxy @DebugAttemptEquation
-    , mk $ Proxy @DebugApplyEquation
-    , mk $ Proxy @DebugUnification
-    , mk $ Proxy @InfoProofDepth
-    , mk $ Proxy @InfoExecDepth
-    , mk $ Proxy @DebugProven
-    ]
+entryTypeReps = entryTypeRepsErr <> entryTypeRepsNoErr
+
+entryTypeRepsErr, entryTypeRepsNoErr :: [SomeTypeRep]
+entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
+( (entryTypeRepsNoErr, entryHelpDocsNoErr)
+    , (entryTypeRepsErr, entryHelpDocsErr) )
+  =
+    (   [ mk $ Proxy @DebugSolverSend
+        , mk $ Proxy @DebugSolverRecv
+        , mk $ Proxy @DebugClaimState
+        , mk $ Proxy @DebugAppliedRewriteRules
+        , mk $ Proxy @DebugSubstitutionSimplifier
+        , mk $ Proxy @WarnFunctionWithoutEvaluators
+        , mk $ Proxy @WarnSymbolSMTRepresentation
+        , mk $ Proxy @WarnStuckClaimState
+        , mk $ Proxy @WarnIfLowProductivity
+        , mk $ Proxy @WarnTrivialClaim
+        , mk $ Proxy @WarnRetrySolverQuery
+        , mk $ Proxy @DebugEvaluateCondition
+        , mk $ Proxy @LogMessage
+        , mk $ Proxy @InfoAttemptUnification
+        , mk $ Proxy @InfoReachability
+        , mk $ Proxy @InfoExecBreadth
+        , mk $ Proxy @DebugAttemptEquation
+        , mk $ Proxy @DebugApplyEquation
+        , mk $ Proxy @DebugUnification
+        , mk $ Proxy @InfoProofDepth
+        , mk $ Proxy @InfoExecDepth
+        , mk $ Proxy @DebugProven
+        ]
+
+    ,   [ mk $ Proxy @ErrorBottomTotalFunction
+        , mk $ Proxy @ErrorDecidePredicateUnknown
+        , mk $ Proxy @ErrorParse
+        , mk $ Proxy @ErrorVerify
+        , mk $ Proxy @ErrorRuleMergeDuplicateIds
+        , mk $ Proxy @ErrorRuleMergeDuplicateLabels
+        , mk $ Proxy @ErrorException
+        , mk $ Proxy @ErrorRewriteLoop
+        , mk $ Proxy @ErrorRewritesInstantiation
+        ]
+    )
+    & Lens.each %~ unzip
   where
     mk proxy =
         let tRep = someTypeRep proxy
@@ -233,4 +250,10 @@ typeOfSomeEntry :: SomeEntry -> SomeTypeRep
 typeOfSomeEntry (SomeEntry entry) = SomeTypeRep (typeOf entry)
 
 getEntryTypesAsText :: [String]
-getEntryTypesAsText = show <$> entryHelpDocs
+getEntryTypesAsText = getNoErrEntryTypesAsText <> getErrEntryTypesAsText
+
+getErrEntryTypesAsText :: [String]
+getErrEntryTypesAsText = show <$> entryHelpDocsErr
+
+getNoErrEntryTypesAsText :: [String]
+getNoErrEntryTypesAsText = show <$> entryHelpDocsNoErr