Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

HOTFIX Make some informative warning logs optional, comment about implies #4072

Merged
merged 1 commit into from
Nov 17, 2024
Merged

HOTFIX Make some informative warning logs optional, comment about implies #4072

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions booster/library/Booster/Pattern/Implies.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 $
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down
25 changes: 15 additions & 10 deletions booster/tools/booster/Proxy.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading