HOTFIX Make some informative warning logs optional, comment about imp…

…lies (#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.
runtimeverification · Nov 17, 2024 · 044df58 · 044df58
1 parent e2cb204
commit 044df58
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 15 deletions.
diff --git 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
@@ -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,17 +223,20 @@ 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 ->
                 pure . Left $ ErrorObj "Wrong result type" (-32002) $ toJSON _wrong
 
     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