Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Dec 4, 2020
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
041b547
Add option to turn an arbitrary log entry into an error
andreiburdusa Dec 3, 2020
15f2c85
Rebuild
andreiburdusa Dec 3, 2020
e0322b5
Split entries between errors and non-errors
andreiburdusa Dec 4, 2020
4b19c46
Addressed comments
andreiburdusa Dec 4, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions kore/src/Kore/Log.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
36 changes: 32 additions & 4 deletions kore/src/Kore/Log/KoreLogOptions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ import Kore.Log.DebugSolver
)
import Kore.Log.Registry
( getEntryTypesAsText
, getNoErrEntryTypesAsText
, parseEntryType
)
import Kore.Log.SQLite
Expand Down Expand Up @@ -96,6 +97,7 @@ data KoreLogOptions = KoreLogOptions
, startTime :: !TimeSpec
, logSQLiteOptions :: !LogSQLiteOptions
, warningSwitch :: !WarningSwitch
, turnedIntoErrors :: !EntryTypes
, debugApplyEquationOptions :: !DebugApplyEquationOptions
, debugAttemptEquationOptions :: !DebugAttemptEquationOptions
, debugEquationOptions :: !DebugEquationOptions
Expand All @@ -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
Expand Down Expand Up @@ -182,6 +185,7 @@ parseKoreLogOptions exeName startTime =
<*> pure startTime
<*> parseLogSQLiteOptions
<*> parseWarningSwitch
<*> (mconcat <$> many parseErrorEntries)
<*> parseDebugApplyEquationOptions
<*> parseDebugAttemptEquationOptions
<*> parseDebugEquationOptions
Expand All @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -396,6 +422,7 @@ unparseKoreLogOptions
_
logSQLiteOptions
warningSwitch
toError
debugApplyEquationOptions
debugAttemptEquationOptions
debugEquationOptions
Expand All @@ -409,6 +436,7 @@ unparseKoreLogOptions
, debugSolverOptionsFlag debugSolverOptions
, logSQLiteOptionsFlag logSQLiteOptions
, ["--warnings-to-errors" | AsError <- [warningSwitch] ]
, logEntriesFlag toError
, debugApplyEquationOptionsFlag debugApplyEquationOptions
, debugAttemptEquationOptionsFlag debugAttemptEquationOptions
, debugEquationOptionsFlag debugEquationOptions
Expand Down
97 changes: 60 additions & 37 deletions kore/src/Kore/Log/Registry.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
Expand Down Expand Up @@ -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 }
Expand All @@ -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) )
Comment on lines +170 to +171
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
( (entryTypeRepsNoErr, entryHelpDocsNoErr)
, (entryTypeRepsErr, entryHelpDocsErr) )
( (entryTypeRepsNoErr, entryHelpDocsNoErr)
, (entryTypeRepsErr, entryHelpDocsErr)
)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't compile

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I was just thinking this would look nicer, but it's fine either way imo. Everything else looks ok to me.

=
( [ 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
Expand Down Expand Up @@ -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