Skip to content

Commit ec980ea

Browse files
geo2ageo2a
committed
Merge remote-tracking branch 'origin/master' into georgy/kore-log-filtering
2 parents 990dce3 + c42b8f0 commit ec980ea

File tree

29 files changed

+1215
-732
lines changed

29 files changed

+1215
-732
lines changed

‎booster/library/Booster/CLOptions.hs

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,9 @@ data CLOptions = CLOptions
3030
, llvmLibraryFile :: Maybe FilePath
3131
, port :: Int
3232
, logLevels :: [LogLevel]
33+
, logTimeStamps :: Bool
34+
, logContexts :: [String]
35+
, notLogContexts :: [String]
3336
, simplificationLogFile :: Maybe FilePath
3437
, smtOptions :: Maybe SMTOptions
3538
, equationOptions :: EquationOptions
@@ -78,6 +81,26 @@ clOptionsParser =
7881
)
7982
)
8083
)
84+
<*> switch (long "log-timestamps" <> help "Add timestamps to logs")
85+
<*> many
86+
( option
87+
str
88+
( metavar "CONTEXT"
89+
<> long "log-context"
90+
<> short 'c'
91+
<> help
92+
"Log context"
93+
)
94+
)
95+
<*> many
96+
( option
97+
str
98+
( metavar "CONTEXT"
99+
<> long "not-log-context"
100+
<> help
101+
"Not in log context"
102+
)
103+
)
81104
<*> optional
82105
( strOption
83106
( metavar "JSON_LOG_FILE"

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import Booster.Pattern.ApplyEquations
1414
import Booster.Pattern.Base
1515

1616
import Booster.LLVM as LLVM (API, simplifyBool)
17+
import Booster.Log
1718
import Booster.Pattern.Bool
1819
import Booster.Pattern.Util (isConcrete, sortOfTerm)
1920
import Booster.Util (Flag (..))
@@ -73,7 +74,7 @@ instance Pretty ComputeCeilSummary where
7374
]
7475

7576
computeCeilsDefinition ::
76-
MonadLoggerIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary])
77+
LoggerMIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary])
7778
computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
7879
(rewriteTheory', ceilSummaries) <-
7980
runWriterT $
@@ -87,7 +88,7 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
8788
pure (def{rewriteTheory = rewriteTheory'}, toList ceilSummaries)
8889

8990
computeCeilRule ::
90-
MonadLoggerIO io =>
91+
LoggerMIO io =>
9192
Maybe LLVM.API ->
9293
KoreDefinition ->
9394
RewriteRule.RewriteRule "Rewrite" ->

‎booster/library/Booster/JsonRpc.hs

Lines changed: 46 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
2020
import Control.Monad
2121
import Control.Monad.Extra (whenJust)
2222
import Control.Monad.IO.Class
23-
import Control.Monad.Logger.CallStack (MonadLoggerIO)
2423
import Control.Monad.Logger.CallStack qualified as Log
2524
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
2625
import Crypto.Hash (SHA256 (..), hashWith)
@@ -45,12 +44,9 @@ import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
4544
import Booster.Definition.Base (KoreDefinition (..))
4645
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
4746
import Booster.LLVM as LLVM (API)
47+
import Booster.Log
4848
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
49-
import Booster.Pattern.Base (
50-
Pattern (..),
51-
Term,
52-
Variable,
53-
)
49+
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
5450
import Booster.Pattern.Base qualified as Pattern
5551
import Booster.Pattern.Rewrite (
5652
RewriteFailed (..),
@@ -69,6 +65,7 @@ import Booster.Syntax.Json.Internalise (
6965
TermOrPredicates (..),
7066
internalisePattern,
7167
internaliseTermOrPredicate,
68+
logPatternError,
7269
patternErrorToRpcError,
7370
pattern CheckSubsorts,
7471
pattern DisallowAlias,
@@ -88,7 +85,7 @@ import Kore.Syntax.Json.Types qualified as Syntax
8885

8986
respond ::
9087
forall m.
91-
MonadLoggerIO m =>
88+
LoggerMIO m =>
9289
MVar ServerState ->
9390
Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res)
9491
respond stateVar =
@@ -97,14 +94,14 @@ respond stateVar =
9794
| isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String)
9895
| isJust req.movingAverageStepTimeout ->
9996
pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
100-
RpcTypes.Execute req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
97+
RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "execute" $ do
10198
start <- liftIO $ getTime Monotonic
10299
-- internalise given constrained term
103100
let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term
104101

105102
case internalised of
106103
Left patternError -> do
107-
Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
104+
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
108105
pure $
109106
Left $
110107
RpcError.backendError $
@@ -113,13 +110,12 @@ respond stateVar =
113110
]
114111
Right (pat, substitution, unsupported) -> do
115112
unless (null unsupported) $ do
113+
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
114+
logMessage ("ignoring unsupported predicate parts" :: Text)
116115
Log.logWarnNS
117116
"booster"
118117
"Execute: ignoring unsupported predicate parts"
119-
Log.logOtherNS
120-
"booster"
121-
(Log.LevelOther "ErrorDetails")
122-
(Text.unlines $ map prettyPattern unsupported)
118+
123119
let cutPoints = fromMaybe [] req.cutPointRules
124120
terminals = fromMaybe [] req.terminalRules
125121
mbDepth = fmap RpcTypes.getNat req.maxDepth
@@ -153,7 +149,7 @@ respond stateVar =
153149
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
154150
else Nothing
155151
pure $ execResponse duration req result substitution unsupported
156-
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
152+
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext "add-module" $ runExceptT $ do
157153
-- block other request executions while modifying the server state
158154
state <- liftIO $ takeMVar stateVar
159155
let nameAsId = fromMaybe False nameAsId'
@@ -211,10 +207,10 @@ respond stateVar =
211207
(if nameAsId then Map.insert (getId newModule.name) _module else id) $
212208
Map.insert moduleHash _module state.addedModules
213209
}
214-
Log.logInfo $
210+
Booster.Log.logMessage $
215211
"Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
216212
pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
217-
RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
213+
RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "simplify" $ do
218214
start <- liftIO $ getTime Monotonic
219215
let internalised =
220216
runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -249,8 +245,7 @@ respond stateVar =
249245
result <- case internalised of
250246
Left patternErrors -> do
251247
forM_ patternErrors $ \patternError ->
252-
Log.logErrorNS "booster" $
253-
"Error internalising cterm: " <> pack (show patternError)
248+
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
254249
Log.logOtherNS
255250
"booster"
256251
(Log.LevelOther "ErrorDetails")
@@ -262,15 +257,12 @@ respond stateVar =
262257
map patternErrorToRpcError patternErrors
263258
-- term and predicate (pattern)
264259
Right (TermAndPredicates pat substitution unsupported) -> do
265-
Log.logInfoNS "booster" "Simplifying a pattern"
266260
unless (null unsupported) $ do
261+
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
262+
logMessage ("ignoring unsupported predicate parts" :: Text)
267263
Log.logWarnNS
268264
"booster"
269-
"Simplify: ignoring unsupported predicates in input"
270-
Log.logOtherNS
271-
"booster"
272-
(Log.LevelOther "ErrorDetails")
273-
(Text.unlines $ map prettyPattern unsupported)
265+
"Simplify: ignoring unsupported predicate parts"
274266
-- apply the given substitution before doing anything else
275267
let substPat =
276268
Pattern
@@ -302,36 +294,35 @@ respond stateVar =
302294
| otherwise -> do
303295
Log.logInfoNS "booster" "Simplifying predicates"
304296
unless (null ps.unsupported) $ do
305-
Log.logWarnNS
306-
"booster"
307-
"Simplify: ignoring unsupported predicates in input"
308-
Log.logOtherNS
309-
"booster"
310-
(Log.LevelOther "ErrorDetails")
311-
(Text.unlines $ map prettyPattern ps.unsupported)
312-
Log.logOtherNS "booster" (Log.LevelOther "Simplify") $ renderText (pretty ps)
297+
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
298+
logMessage ("ignoring unsupported predicate parts" :: Text)
299+
Log.logWarnNS
300+
"booster"
301+
"Simplify: ignoring unsupported predicate parts"
302+
-- apply the given substitution before doing anything else
313303
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
314-
ApplyEquations.simplifyConstraints
315-
doTracing
316-
def
317-
mLlvmLibrary
318-
solver
319-
mempty
320-
predicates
321-
>>= \case
322-
(Right newPreds, _) -> do
323-
let predicateSort =
324-
fromMaybe (error "not a predicate") $
325-
sortOfJson req.state.term
326-
result =
327-
map (externalisePredicate predicateSort) newPreds
328-
<> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
329-
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
330-
<> ps.unsupported
304+
withContext "constraint" $
305+
ApplyEquations.simplifyConstraints
306+
doTracing
307+
def
308+
mLlvmLibrary
309+
solver
310+
mempty
311+
predicates
312+
>>= \case
313+
(Right newPreds, _) -> do
314+
let predicateSort =
315+
fromMaybe (error "not a predicate") $
316+
sortOfJson req.state.term
317+
result =
318+
map (externalisePredicate predicateSort) newPreds
319+
<> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
320+
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
321+
<> ps.unsupported
331322

332-
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
333-
(Left something, _) ->
334-
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
323+
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
324+
(Left something, _) ->
325+
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
335326
whenJust solver SMT.closeSolver
336327
stop <- liftIO $ getTime Monotonic
337328

@@ -341,7 +332,7 @@ respond stateVar =
341332
RpcTypes.Simplify
342333
RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData}
343334
pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result)
344-
RpcTypes.GetModel req -> withContext req._module $ \case
335+
RpcTypes.GetModel req -> withModule req._module $ \case
345336
(_, _, Nothing) -> do
346337
Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
347338
pure $ Left RpcError.notImplemented
@@ -470,13 +461,13 @@ respond stateVar =
470461
-- using "Method does not exist" error code
471462
_ -> pure $ Left RpcError.notImplemented
472463
where
473-
withContext ::
464+
withModule ::
474465
Maybe Text ->
475466
( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions) ->
476467
m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
477468
) ->
478469
m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
479-
withContext mbMainModule action = do
470+
withModule mbMainModule action = do
480471
state <- liftIO $ readMVar stateVar
481472
let mainName = fromMaybe state.defaultMain mbMainModule
482473
case Map.lookup mainName state.definitions of
@@ -806,11 +797,6 @@ mkLogRewriteTrace
806797
{ reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)
807798
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
808799
}
809-
IsNotMatch r _ _ ->
810-
Failure
811-
{ reason = "Produced a non-match"
812-
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
813-
}
814800
RewriteSortError r _ _ ->
815801
Failure
816802
{ reason = "Sort error while unifying"

0 commit comments

Comments
 (0)