Skip to content

Commit

Permalink
Use typed log context in kore, add optional timestamp (with flexible …
Browse files Browse the repository at this point in the history 
…parsing) (#3967)
  • Loading branch information
@jberthold
jberthold authored Jul 2, 2024
1 parent 144d223 commit e7409dc
Show file tree
Hide file tree
Showing 60 changed files with 262 additions and 198 deletions.
4 changes: 2 additions & 2 deletions booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,8 @@
{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
{"context":[{"request":"4"},"booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
Expand Down
5 changes: 3 additions & 2 deletions booster/tools/booster/Server.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ import Control.Monad.Logger (
import Control.Monad.Trans.Reader (runReaderT)
import Data.Aeson qualified as JSON
import Data.Bifunctor (bimap)
import Data.ByteString.Char8 qualified as BS
import Data.Coerce (coerce)
import Data.Conduit.Network (serverSettings)
import Data.IORef (writeIORef)
Expand Down Expand Up @@ -176,7 +177,7 @@ main = do
not contextLoggingEnabled
|| ( let contextStrs =
concatMap
( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
)
ctxt
in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts
Expand Down Expand Up @@ -508,7 +509,7 @@ translateSMTOpts = \case
mkKoreServer ::
Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext "kore") $ do
flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext $ Log.CLNullary CtxKore) $ do
sd@GlobalMain.SerializedDefinition{internedTextCache} <-
GlobalMain.deserializeDefinition
koreSolverOptions
Expand Down
3 changes: 2 additions & 1 deletion dev-tools/kore-rpc-dev/Server.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import Control.Monad.Logger (
)
import Control.Monad.Trans.Reader (runReaderT)
import Data.Aeson.Types (Value (..))
import Data.ByteString.Char8 qualified as BS
import Data.Conduit.Network (serverSettings)
import Data.IORef (writeIORef)
import Data.InternedText (globalInternedTextCache)
Expand Down Expand Up @@ -187,7 +188,7 @@ main = do
null logContextsWithcustomLevelContexts
|| ( let contextStrs =
concatMap
( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
)
ctxt
in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts
Expand Down
52 changes: 50 additions & 2 deletions kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,18 @@ module Kore.JsonRpc.Types.ContextLog (
module Kore.JsonRpc.Types.ContextLog,
) where

import Control.Applicative ((<|>))
import Data.Aeson ((.:), (.:?), (.=))
import Data.Aeson.TH (deriveJSON)
import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
import Data.Aeson.Types qualified as JSON
import Data.Data (Data, toConstr)
import Data.Sequence (Seq)
import Data.Text (Text, unpack)
import Data.Text qualified as Text
import Data.Time.Clock.System (SystemTime (..), systemToUTCTime, utcToSystemTime)
import Data.Time.Format (defaultTimeLocale, formatTime, parseTimeM)
import Text.Read (readMaybe)

data SimpleContext
= -- component
Expand All @@ -30,6 +35,7 @@ data SimpleContext
| -- mode/phase
CtxInternalise
| CtxMatch
| CtxUnify
| CtxDefinedness
| CtxConstraint
| CtxSMT
Expand All @@ -45,6 +51,7 @@ data SimpleContext
CtxKoreTerm
| CtxDetail
| CtxSubstitution
| CtxRemainder
| CtxDepth
| CtxTiming
| -- standard log levels
Expand Down Expand Up @@ -183,9 +190,50 @@ instance ToJSON CLMessage where
toJSON (CLValue value) = value

data LogLine = LogLine
{ context :: Seq CLContext
{ timestamp :: Maybe SystemTime
, context :: Seq CLContext
, message :: CLMessage
}
deriving stock (Show, Eq)

$(deriveJSON defaultOptions ''LogLine)
instance FromJSON LogLine where
parseJSON = JSON.withObject "LogLine" $ \l ->
LogLine
<$> (l .:? "timestamp" >>= parseTimestamp)
<*> l .: "context"
<*> l .: "message"

parseTimestamp :: Maybe JSON.Value -> JSON.Parser (Maybe SystemTime)
parseTimestamp Nothing = pure Nothing
parseTimestamp (Just x) =
JSON.withScientific "numeric timestamp" (pure . Just . fromNumeric) x
<|> JSON.withText "human-readable timestamp" fromString x
<|> JSON.withText "nanosecond timestamp" fromNanos x
where
-- fromNumeric :: Scientific -> SystemTime
fromNumeric n =
let seconds = truncate n
nanos = truncate $ 1e9 * (n - fromIntegral seconds) -- no leap seconds
in MkSystemTime seconds nanos
fromString s = do
utc <- parseTimeM False defaultTimeLocale timestampFormat (Text.unpack s)
pure . Just $ utcToSystemTime utc
fromNanos s =
case readMaybe (Text.unpack s) of
Nothing -> fail $ "bad number " <> show s
Just (n :: Integer) -> pure . Just $ fromNumeric (fromIntegral n :: Double)

instance ToJSON LogLine where
toJSON LogLine{timestamp, context, message} =
JSON.object $
maybe
[]
(\t -> ["timestamp" .= formatted t])
timestamp
<> ["context" .= context, "message" .= message]
where
formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime

-- same format as the one used in Booster.Util
timestampFormat :: String
timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q"
4 changes: 2 additions & 2 deletions kore/src/Kore/Equation/Application.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ import Kore.Internal.TermLike (
TermLike,
)
import Kore.Internal.TermLike qualified as TermLike
import Kore.Log.DebugContext (inContext)
import Kore.Log.DebugContext (SimpleContext (CtxConstraint), inContext)
import Kore.Log.DecidePredicateUnknown (
OnDecidePredicateUnknown (..),
srcLoc,
Expand Down Expand Up @@ -362,7 +362,7 @@ checkRequires ::
Predicate RewritingVariableName ->
ExceptT (CheckRequiresError RewritingVariableName) Simplifier ()
checkRequires onUnknown sideCondition predicate requires =
inContext "constraint" $
inContext CtxConstraint $
do
let requires' = makeAndPredicate predicate requires
-- The condition to refute:
Expand Down
69 changes: 23 additions & 46 deletions kore/src/Kore/Equation/DebugEquation.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ import Data.Text (
Text,
)
import Data.Text qualified as Text
import Data.Vector qualified as Vec
import Debug
import GHC.Generics qualified as GHC
import Generics.SOP qualified as SOP
Expand All @@ -48,7 +47,7 @@ import Kore.Attribute.SourceLocation (
)
import Kore.Equation.Equation (Equation (..))
import Kore.Internal.OrCondition (OrCondition)
import Kore.Internal.Pattern (Conditional (..), Pattern)
import Kore.Internal.Pattern (Conditional (..), Pattern, toTermLike)
import Kore.Internal.Predicate (Predicate)
import Kore.Internal.SideCondition (SideCondition)
import Kore.Internal.TermLike (
Expand Down Expand Up @@ -294,10 +293,14 @@ instance Entry DebugAttemptEquation where
helpDoc _ = "log equation application attempts"

oneLineContextDoc = \case
_entry@DebugAttemptEquation{} -> ["detail"]
_entry@DebugAttemptEquation{} -> single CtxDetail
(DebugAttemptEquationResult _ result) -> case result of
Right Conditional{term} -> ["success", "term " <> (showHashHex $ hash term), "kore-term"]
Left{} -> ["failure"]
Right Conditional{term} ->
[ CLNullary CtxSuccess
, CtxTerm `withShortId` showHashHex (hash term)
, CLNullary CtxKoreTerm
]
Left{} -> single CtxFailure

oneLineDoc (DebugAttemptEquation equation _term) =
maybe
Expand All @@ -310,21 +313,6 @@ instance Entry DebugAttemptEquation where
Right Conditional{term} -> " " <> unparse term
Left failure -> " " <> Pretty.pretty (failureDescription failure)

oneLineContextJson = \case
_entry@DebugAttemptEquation{} -> JSON.String "detail"
_entry@(DebugAttemptEquationResult _equation result) ->
case result of
Right Conditional{term} ->
JSON.Array $
Vec.fromList
[ JSON.String "success"
, JSON.object
[ "term" JSON..= showHashHex (hash term)
]
, JSON.String "kore-term"
]
Left _failure -> JSON.String "failure"

oneLineJson = \case
_entry@(DebugAttemptEquation equation _term) ->
JSON.toJSON $ renderDefault (maybe "UNKNOWN" pretty (srcLoc equation))
Expand All @@ -350,12 +338,7 @@ instance Entry DebugTermContext where
oneLineDoc DebugTermContext{} = mempty

oneLineContextDoc (DebugTermContext term) =
["term " <> (showHashHex $ hash term)]

oneLineContextJson (DebugTermContext term) =
JSON.object
[ "term" JSON..= showHashHex (hash term)
]
[CtxTerm `withShortId` showHashHex (hash term)]

oneLineJson :: DebugTermContext -> JSON.Value
oneLineJson DebugTermContext{} =
Expand All @@ -366,13 +349,7 @@ instance Entry DebugTerm where

oneLineDoc (DebugTerm term) = unparse term

oneLineContextDoc DebugTerm{} =
["kore-term"]

oneLineContextJson DebugTerm{} =
JSON.toJSON
[ "kore-term" :: Text
]
oneLineContextDoc DebugTerm{} = single CtxKoreTerm

oneLineJson (DebugTerm term) =
JSON.toJSON $ Kore.Syntax.Json.fromTermLike (getRewritingTerm term)
Expand All @@ -383,18 +360,9 @@ instance Entry DebugEquation where
oneLineDoc _ = mempty

oneLineContextDoc (DebugEquation equation) =
let equationKindTxt = if isSimplification equation then "simplification" else "function"
in [ equationKindTxt <> " " <> shortRuleIdText equation
]
oneLineContextJson (DebugEquation equation) =
let equationKindTxt = if isSimplification equation then "simplification" else "function"
in JSON.Array $
Vec.fromList
[ JSON.object
[ equationKindTxt
JSON..= ruleIdText equation
]
]
let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
in [equationKind `withId` ruleIdText equation]

oneLineJson _ = JSON.Null

whileDebugTerm ::
Expand Down Expand Up @@ -485,7 +453,16 @@ instance Entry DebugApplyEquation where
]
helpDoc _ = "log equation application successes"

oneLineJson _ = JSON.Null
oneLineContextDoc (DebugApplyEquation equation result) =
let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
in [ equationKind `withId` ruleIdText equation
, CLNullary CtxSuccess
, CtxTerm `withShortId` showHashHex (hash result)
, CLNullary CtxKoreTerm
]

oneLineJson (DebugApplyEquation _ result) =
JSON.toJSON $ Kore.Syntax.Json.fromTermLike . getRewritingTerm $ toTermLike result

{- | Log when an 'Equation' is actually applied.
Expand Down
56 changes: 26 additions & 30 deletions kore/src/Kore/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,24 +162,22 @@ respond reqId serverState moduleName runSMT =
traversalResult <-
liftIO
( runSMT (Exec.metadataTools serializedModule) lemmas $
Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) $
Log.logWhile (Log.DebugContext "kore") $
Log.logWhile (Log.DebugContext "execute") $
Exec.rpcExec
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
(coerce stepTimeout)
( if fromMaybe False movingAverageStepTimeout
then EnableMovingAverage
else DisableMovingAverage
)
( if fromMaybe False assumeStateDefined
then EnableAssumeInitialDefined
else DisableAssumeInitialDefined
)
tracingEnabled
serializedModule
(toStopLabels cutPointRules terminalRules)
verifiedPattern
withContextLog Log.CtxExecute $
Exec.rpcExec
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
(coerce stepTimeout)
( if fromMaybe False movingAverageStepTimeout
then EnableMovingAverage
else DisableMovingAverage
)
( if fromMaybe False assumeStateDefined
then EnableAssumeInitialDefined
else DisableAssumeInitialDefined
)
tracingEnabled
serializedModule
(toStopLabels cutPointRules terminalRules)
verifiedPattern
)

stop <- liftIO $ getTime Monotonic
Expand Down Expand Up @@ -433,9 +431,7 @@ respond reqId serverState moduleName runSMT =
result <-
liftIO
. runSMT (Exec.metadataTools serializedModule) lemmas
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
. Log.logWhile (Log.DebugContext "kore")
. Log.logWhile (Log.DebugContext "implies")
. withContextLog Log.CtxImplies
. evalInSimplifierContext serializedModule
. runExceptT
$ Claim.checkSimpleImplication
Expand Down Expand Up @@ -518,9 +514,7 @@ respond reqId serverState moduleName runSMT =
result <-
liftIO
. runSMT (Exec.metadataTools serializedModule) lemmas
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
. Log.logWhile (Log.DebugContext "kore")
. Log.logWhile (Log.DebugContext "simplify")
. withContextLog Log.CtxSimplify
. evalInSimplifierContext serializedModule
$ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt

Expand Down Expand Up @@ -616,9 +610,7 @@ respond reqId serverState moduleName runSMT =
serializedModule <-
liftIO
. runSMT metadataTools lemmas
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
. Log.logWhile (Log.DebugContext "kore")
. Log.logWhile (Log.DebugContext "add-module")
. withContextLog Log.CtxAddModule
$ Exec.makeSerializedModule newModule
internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache

Expand Down Expand Up @@ -677,9 +669,7 @@ respond reqId serverState moduleName runSMT =
else
liftIO
. runSMT tools lemmas
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
. Log.logWhile (Log.DebugContext "kore")
. Log.logWhile (Log.DebugContext "get-model")
. withContextLog Log.CtxGetModel
. SMT.Evaluator.getModelFor tools
$ NonEmpty.fromList preds

Expand All @@ -706,6 +696,12 @@ respond reqId serverState moduleName runSMT =
-- this case is only reachable if the cancel appeared as part of a batch request
Cancel -> pure $ Left cancelUnsupportedInBatchMode
where
withContextLog :: Log.SimpleContext -> SMT.SMT a -> SMT.SMT a
withContextLog method =
Log.logWhile (Log.DebugContext $ Log.CLWithId $ Log.CtxRequest $ Text.pack reqId)
. Log.inContext Log.CtxKore
. Log.inContext method

withMainModule module' act = do
let mainModule = fromMaybe moduleName module'
ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState
Expand Down
Loading

0 comments on commit e7409dc

Please sign in to comment.