From 044df58b3c8852a12ca92388cea1970d0d2ad3c5 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Nov 2024 02:42:13 +1100 Subject: [PATCH] HOTFIX Make some informative warning logs optional, comment about implies (#4072) The `logMessage'` function, which emits log messages _unconditionally_, was used for logging some exception conditions in booster. However, these warnings should not appear by default in user-facing output when booster is called through the proxy and just falls back to using kore-rpc. The changes do not remove the log messages, they are now emitted at context `[proxy]`, which is a common and recommended log setting to see what the server is up to. Besides changing the `logMessage'` calls, a comment is added to point out where the incompleteness of the `implies` endpoint is rooted in the code. --- booster/library/Booster/Pattern/Implies.hs | 9 ++++---- booster/tools/booster/Proxy.hs | 25 +++++++++++++--------- 2 files changed, 19 insertions(+), 15 deletions(-) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 92ec8d9cfb..5b884377b4 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -92,7 +92,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = map (pack . renderDefault . pretty' @mods) $ Set.toList freeVarsRminusL | not (null unsupportedL) || not (null unsupportedR) -> do - Booster.Log.logMessage' + Booster.Log.logMessage ("aborting due to unsupported predicate parts" :: Text) unless (null unsupportedL) $ Booster.Log.withContext Booster.Log.CtxDetail $ @@ -154,7 +154,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (externaliseExistTerm existsL patL.term) (externaliseExistTerm existsR patR.term) subst - else + else -- FIXME This is incomplete because patL.constraints are not assumed in the check. + ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case (Right newPreds, _) -> if all (== Predicate TrueBool) newPreds @@ -164,9 +165,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (externaliseExistTerm existsL patL.term) (externaliseExistTerm existsR patR.term) subst - else -- here we conservatively abort - -- an anlternative would be to return valid, putting the unknown constraints into the - -- condition. i.e. the implication holds conditionally, if we can prove that the unknwon constraints are true + else -- here we conservatively abort (incomplete) pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints" (Left other, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index deeb8282ef..25155aee02 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -110,9 +110,10 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of pure res Left err -> do Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' $ - Text.pack $ - "implies error in booster: " <> fromError err + Booster.Log.logMessage . Text.pack $ + "Implies abort in booster: " + <> fromError err + <> ". Falling back to kore." (koreRes, koreTime) <- Stats.timed $ kore req logStats ImpliesM (boosterTime + koreTime, koreTime) pure koreRes @@ -139,7 +140,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of case bResult of Left err -> do Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' $ + Booster.Log.logMessage $ Text.pack $ "get-model error in booster: " <> fromError err Stats.timed $ kore req @@ -222,9 +223,12 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of fromString other = Text.pack (show other) Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' $ - Text.unwords - ["Problem with simplify request: ", Text.pack getErrMsg, "-", boosterError] + Booster.Log.logMessage $ + "Problem with booster simplify request: " + <> Text.pack getErrMsg + <> " - " + <> boosterError + <> ". Falling back to kore." -- NB the timing information for booster execution is lost here. loggedKore SimplifyM req _wrong -> @@ -232,7 +236,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of loggedKore method r = do Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' $ + Booster.Log.logMessage $ Text.pack $ show method <> " (using kore)" (result, time) <- Stats.timed $ kore r @@ -584,7 +588,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of when (length filteredNexts < maybe 0 length nextStates) $ Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' + Booster.Log.logMessage (Text.pack ("Pruned #Bottom states: " <> show (length nextStates))) case reason of @@ -617,7 +621,8 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of } | otherwise = Nothing Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' ("Continuing after rewriting with rule " <> rewriteRuleId) + Booster.Log.logMessage + ("Continuing after rewriting with rule " <> rewriteRuleId) pure $ Left ( execStateToKoreJson onlyNext