Skip to content

Commit 4366fbf

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 50c3359 + e7409dc commit 4366fbf

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+262
-198
lines changed

‎booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,8 @@
5757
{"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"}}}
5858
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
5959
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
60-
{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
61-
{"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"}}}
60+
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
61+
{"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"}}}
6262
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
6363
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
6464
{"context":[{"request":"4"},"booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}

‎booster/tools/booster/Server.hs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ import Control.Monad.Logger (
2222
import Control.Monad.Trans.Reader (runReaderT)
2323
import Data.Aeson qualified as JSON
2424
import Data.Bifunctor (bimap)
25+
import Data.ByteString.Char8 qualified as BS
2526
import Data.Coerce (coerce)
2627
import Data.Conduit.Network (serverSettings)
2728
import Data.IORef (writeIORef)
@@ -176,7 +177,7 @@ main = do
176177
not contextLoggingEnabled
177178
|| ( let contextStrs =
178179
concatMap
179-
( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
180+
( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
180181
)
181182
ctxt
182183
in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts
@@ -508,7 +509,7 @@ translateSMTOpts = \case
508509
mkKoreServer ::
509510
Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
510511
mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
511-
flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext "kore") $ do
512+
flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext $ Log.CLNullary CtxKore) $ do
512513
sd@GlobalMain.SerializedDefinition{internedTextCache} <-
513514
GlobalMain.deserializeDefinition
514515
koreSolverOptions

‎dev-tools/kore-rpc-dev/Server.hs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ import Control.Monad.Logger (
1919
)
2020
import Control.Monad.Trans.Reader (runReaderT)
2121
import Data.Aeson.Types (Value (..))
22+
import Data.ByteString.Char8 qualified as BS
2223
import Data.Conduit.Network (serverSettings)
2324
import Data.IORef (writeIORef)
2425
import Data.InternedText (globalInternedTextCache)
@@ -187,7 +188,7 @@ main = do
187188
null logContextsWithcustomLevelContexts
188189
|| ( let contextStrs =
189190
concatMap
190-
( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c
191+
( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c
191192
)
192193
ctxt
193194
in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts

‎kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs

Lines changed: 50 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,18 @@ module Kore.JsonRpc.Types.ContextLog (
88
module Kore.JsonRpc.Types.ContextLog,
99
) where
1010

11+
import Control.Applicative ((<|>))
12+
import Data.Aeson ((.:), (.:?), (.=))
1113
import Data.Aeson.TH (deriveJSON)
1214
import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
1315
import Data.Aeson.Types qualified as JSON
1416
import Data.Data (Data, toConstr)
1517
import Data.Sequence (Seq)
1618
import Data.Text (Text, unpack)
1719
import Data.Text qualified as Text
20+
import Data.Time.Clock.System (SystemTime (..), systemToUTCTime, utcToSystemTime)
21+
import Data.Time.Format (defaultTimeLocale, formatTime, parseTimeM)
22+
import Text.Read (readMaybe)
1823

1924
data SimpleContext
2025
= -- component
@@ -30,6 +35,7 @@ data SimpleContext
3035
| -- mode/phase
3136
CtxInternalise
3237
| CtxMatch
38+
| CtxUnify
3339
| CtxDefinedness
3440
| CtxConstraint
3541
| CtxSMT
@@ -45,6 +51,7 @@ data SimpleContext
4551
CtxKoreTerm
4652
| CtxDetail
4753
| CtxSubstitution
54+
| CtxRemainder
4855
| CtxDepth
4956
| CtxTiming
5057
| -- standard log levels
@@ -183,9 +190,50 @@ instance ToJSON CLMessage where
183190
toJSON (CLValue value) = value
184191

185192
data LogLine = LogLine
186-
{ context :: Seq CLContext
193+
{ timestamp :: Maybe SystemTime
194+
, context :: Seq CLContext
187195
, message :: CLMessage
188196
}
189197
deriving stock (Show, Eq)
190198

191-
$(deriveJSON defaultOptions ''LogLine)
199+
instance FromJSON LogLine where
200+
parseJSON = JSON.withObject "LogLine" $ \l ->
201+
LogLine
202+
<$> (l .:? "timestamp" >>= parseTimestamp)
203+
<*> l .: "context"
204+
<*> l .: "message"
205+
206+
parseTimestamp :: Maybe JSON.Value -> JSON.Parser (Maybe SystemTime)
207+
parseTimestamp Nothing = pure Nothing
208+
parseTimestamp (Just x) =
209+
JSON.withScientific "numeric timestamp" (pure . Just . fromNumeric) x
210+
<|> JSON.withText "human-readable timestamp" fromString x
211+
<|> JSON.withText "nanosecond timestamp" fromNanos x
212+
where
213+
-- fromNumeric :: Scientific -> SystemTime
214+
fromNumeric n =
215+
let seconds = truncate n
216+
nanos = truncate $ 1e9 * (n - fromIntegral seconds) -- no leap seconds
217+
in MkSystemTime seconds nanos
218+
fromString s = do
219+
utc <- parseTimeM False defaultTimeLocale timestampFormat (Text.unpack s)
220+
pure . Just $ utcToSystemTime utc
221+
fromNanos s =
222+
case readMaybe (Text.unpack s) of
223+
Nothing -> fail $ "bad number " <> show s
224+
Just (n :: Integer) -> pure . Just $ fromNumeric (fromIntegral n :: Double)
225+
226+
instance ToJSON LogLine where
227+
toJSON LogLine{timestamp, context, message} =
228+
JSON.object $
229+
maybe
230+
[]
231+
(\t -> ["timestamp" .= formatted t])
232+
timestamp
233+
<> ["context" .= context, "message" .= message]
234+
where
235+
formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime
236+
237+
-- same format as the one used in Booster.Util
238+
timestampFormat :: String
239+
timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q"

‎kore/src/Kore/Equation/Application.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ import Kore.Internal.TermLike (
8989
TermLike,
9090
)
9191
import Kore.Internal.TermLike qualified as TermLike
92-
import Kore.Log.DebugContext (inContext)
92+
import Kore.Log.DebugContext (SimpleContext (CtxConstraint), inContext)
9393
import Kore.Log.DecidePredicateUnknown (
9494
OnDecidePredicateUnknown (..),
9595
srcLoc,
@@ -362,7 +362,7 @@ checkRequires ::
362362
Predicate RewritingVariableName ->
363363
ExceptT (CheckRequiresError RewritingVariableName) Simplifier ()
364364
checkRequires onUnknown sideCondition predicate requires =
365-
inContext "constraint" $
365+
inContext CtxConstraint $
366366
do
367367
let requires' = makeAndPredicate predicate requires
368368
-- The condition to refute:

‎kore/src/Kore/Equation/DebugEquation.hs

Lines changed: 23 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ import Data.Text (
3636
Text,
3737
)
3838
import Data.Text qualified as Text
39-
import Data.Vector qualified as Vec
4039
import Debug
4140
import GHC.Generics qualified as GHC
4241
import Generics.SOP qualified as SOP
@@ -48,7 +47,7 @@ import Kore.Attribute.SourceLocation (
4847
)
4948
import Kore.Equation.Equation (Equation (..))
5049
import Kore.Internal.OrCondition (OrCondition)
51-
import Kore.Internal.Pattern (Conditional (..), Pattern)
50+
import Kore.Internal.Pattern (Conditional (..), Pattern, toTermLike)
5251
import Kore.Internal.Predicate (Predicate)
5352
import Kore.Internal.SideCondition (SideCondition)
5453
import Kore.Internal.TermLike (
@@ -294,10 +293,14 @@ instance Entry DebugAttemptEquation where
294293
helpDoc _ = "log equation application attempts"
295294

296295
oneLineContextDoc = \case
297-
_entry@DebugAttemptEquation{} -> ["detail"]
296+
_entry@DebugAttemptEquation{} -> single CtxDetail
298297
(DebugAttemptEquationResult _ result) -> case result of
299-
Right Conditional{term} -> ["success", "term " <> (showHashHex $ hash term), "kore-term"]
300-
Left{} -> ["failure"]
298+
Right Conditional{term} ->
299+
[ CLNullary CtxSuccess
300+
, CtxTerm `withShortId` showHashHex (hash term)
301+
, CLNullary CtxKoreTerm
302+
]
303+
Left{} -> single CtxFailure
301304

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

313-
oneLineContextJson = \case
314-
_entry@DebugAttemptEquation{} -> JSON.String "detail"
315-
_entry@(DebugAttemptEquationResult _equation result) ->
316-
case result of
317-
Right Conditional{term} ->
318-
JSON.Array $
319-
Vec.fromList
320-
[ JSON.String "success"
321-
, JSON.object
322-
[ "term" JSON..= showHashHex (hash term)
323-
]
324-
, JSON.String "kore-term"
325-
]
326-
Left _failure -> JSON.String "failure"
327-
328316
oneLineJson = \case
329317
_entry@(DebugAttemptEquation equation _term) ->
330318
JSON.toJSON $ renderDefault (maybe "UNKNOWN" pretty (srcLoc equation))
@@ -350,12 +338,7 @@ instance Entry DebugTermContext where
350338
oneLineDoc DebugTermContext{} = mempty
351339

352340
oneLineContextDoc (DebugTermContext term) =
353-
["term " <> (showHashHex $ hash term)]
354-
355-
oneLineContextJson (DebugTermContext term) =
356-
JSON.object
357-
[ "term" JSON..= showHashHex (hash term)
358-
]
341+
[CtxTerm `withShortId` showHashHex (hash term)]
359342

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

367350
oneLineDoc (DebugTerm term) = unparse term
368351

369-
oneLineContextDoc DebugTerm{} =
370-
["kore-term"]
371-
372-
oneLineContextJson DebugTerm{} =
373-
JSON.toJSON
374-
[ "kore-term" :: Text
375-
]
352+
oneLineContextDoc DebugTerm{} = single CtxKoreTerm
376353

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

385362
oneLineContextDoc (DebugEquation equation) =
386-
let equationKindTxt = if isSimplification equation then "simplification" else "function"
387-
in [ equationKindTxt <> " " <> shortRuleIdText equation
388-
]
389-
oneLineContextJson (DebugEquation equation) =
390-
let equationKindTxt = if isSimplification equation then "simplification" else "function"
391-
in JSON.Array $
392-
Vec.fromList
393-
[ JSON.object
394-
[ equationKindTxt
395-
JSON..= ruleIdText equation
396-
]
397-
]
363+
let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
364+
in [equationKind `withId` ruleIdText equation]
365+
398366
oneLineJson _ = JSON.Null
399367

400368
whileDebugTerm ::
@@ -485,7 +453,16 @@ instance Entry DebugApplyEquation where
485453
]
486454
helpDoc _ = "log equation application successes"
487455

488-
oneLineJson _ = JSON.Null
456+
oneLineContextDoc (DebugApplyEquation equation result) =
457+
let equationKind = if isSimplification equation then CtxSimplification else CtxFunction
458+
in [ equationKind `withId` ruleIdText equation
459+
, CLNullary CtxSuccess
460+
, CtxTerm `withShortId` showHashHex (hash result)
461+
, CLNullary CtxKoreTerm
462+
]
463+
464+
oneLineJson (DebugApplyEquation _ result) =
465+
JSON.toJSON $ Kore.Syntax.Json.fromTermLike . getRewritingTerm $ toTermLike result
489466

490467
{- | Log when an 'Equation' is actually applied.
491468

‎kore/src/Kore/JsonRpc.hs

Lines changed: 26 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -162,24 +162,22 @@ respond reqId serverState moduleName runSMT =
162162
traversalResult <-
163163
liftIO
164164
( runSMT (Exec.metadataTools serializedModule) lemmas $
165-
Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) $
166-
Log.logWhile (Log.DebugContext "kore") $
167-
Log.logWhile (Log.DebugContext "execute") $
168-
Exec.rpcExec
169-
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
170-
(coerce stepTimeout)
171-
( if fromMaybe False movingAverageStepTimeout
172-
then EnableMovingAverage
173-
else DisableMovingAverage
174-
)
175-
( if fromMaybe False assumeStateDefined
176-
then EnableAssumeInitialDefined
177-
else DisableAssumeInitialDefined
178-
)
179-
tracingEnabled
180-
serializedModule
181-
(toStopLabels cutPointRules terminalRules)
182-
verifiedPattern
165+
withContextLog Log.CtxExecute $
166+
Exec.rpcExec
167+
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
168+
(coerce stepTimeout)
169+
( if fromMaybe False movingAverageStepTimeout
170+
then EnableMovingAverage
171+
else DisableMovingAverage
172+
)
173+
( if fromMaybe False assumeStateDefined
174+
then EnableAssumeInitialDefined
175+
else DisableAssumeInitialDefined
176+
)
177+
tracingEnabled
178+
serializedModule
179+
(toStopLabels cutPointRules terminalRules)
180+
verifiedPattern
183181
)
184182

185183
stop <- liftIO $ getTime Monotonic
@@ -433,9 +431,7 @@ respond reqId serverState moduleName runSMT =
433431
result <-
434432
liftIO
435433
. runSMT (Exec.metadataTools serializedModule) lemmas
436-
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
437-
. Log.logWhile (Log.DebugContext "kore")
438-
. Log.logWhile (Log.DebugContext "implies")
434+
. withContextLog Log.CtxImplies
439435
. evalInSimplifierContext serializedModule
440436
. runExceptT
441437
$ Claim.checkSimpleImplication
@@ -518,9 +514,7 @@ respond reqId serverState moduleName runSMT =
518514
result <-
519515
liftIO
520516
. runSMT (Exec.metadataTools serializedModule) lemmas
521-
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
522-
. Log.logWhile (Log.DebugContext "kore")
523-
. Log.logWhile (Log.DebugContext "simplify")
517+
. withContextLog Log.CtxSimplify
524518
. evalInSimplifierContext serializedModule
525519
$ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt
526520

@@ -616,9 +610,7 @@ respond reqId serverState moduleName runSMT =
616610
serializedModule <-
617611
liftIO
618612
. runSMT metadataTools lemmas
619-
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
620-
. Log.logWhile (Log.DebugContext "kore")
621-
. Log.logWhile (Log.DebugContext "add-module")
613+
. withContextLog Log.CtxAddModule
622614
$ Exec.makeSerializedModule newModule
623615
internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache
624616

@@ -677,9 +669,7 @@ respond reqId serverState moduleName runSMT =
677669
else
678670
liftIO
679671
. runSMT tools lemmas
680-
. Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId)
681-
. Log.logWhile (Log.DebugContext "kore")
682-
. Log.logWhile (Log.DebugContext "get-model")
672+
. withContextLog Log.CtxGetModel
683673
. SMT.Evaluator.getModelFor tools
684674
$ NonEmpty.fromList preds
685675

@@ -706,6 +696,12 @@ respond reqId serverState moduleName runSMT =
706696
-- this case is only reachable if the cancel appeared as part of a batch request
707697
Cancel -> pure $ Left cancelUnsupportedInBatchMode
708698
where
699+
withContextLog :: Log.SimpleContext -> SMT.SMT a -> SMT.SMT a
700+
withContextLog method =
701+
Log.logWhile (Log.DebugContext $ Log.CLWithId $ Log.CtxRequest $ Text.pack reqId)
702+
. Log.inContext Log.CtxKore
703+
. Log.inContext method
704+
709705
withMainModule module' act = do
710706
let mainModule = fromMaybe moduleName module'
711707
ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState

0 commit comments

Comments
 (0)