Check consistency of constraints before evaluating a pattern #4013
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
cf8aa7c to
f0ce5de
Compare
|
KEMV performance at 5cb20aa and |
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
5cb20aa to
1a34695
Compare
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
22162c0 to
2483a57
Compare
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
8c9f9d9 to
985fcbc
Compare
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
985fcbc to
7f7d667
Compare
Comment on lines
+195
to
+211
| failBecauseUnknown :: | ||
| forall io. | ||
| Log.LoggerMIO io => | ||
| Set Predicate -> | ||
| ExceptT SMTError (SMT io) Bool | ||
| failBecauseUnknown psToCheck = | ||
| smtRun GetReasonUnknown >>= \case | ||
| Unknown reason -> do | ||
| Log.withContext Log.CtxAbort $ | ||
| Log.logMessage $ | ||
| "Returned Unknown. Reason: " <> fromMaybe "UNKNOWN" reason | ||
| throwE $ SMTSolverUnknown reason mempty psToCheck | ||
| other -> do | ||
| let msg = "Unexpected result while calling ':reason-unknown': " <> show other | ||
| Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg | ||
| throwSMT' msg | ||
|
|
There was a problem hiding this comment.
I previously made it so that we call GetReasonUnknown whenever we get an Unknown result from the solver. Hence we should never need to call GetReasonUnknown explicitly.
There was a problem hiding this comment.
Sorry should have made this explicit in the type... I think we should change Response to:
data Response' reason
= Success -- for command_
| Sat
| Unsat
| Unknown reason
| Values [(SExpr, Value)]
| Error BS.ByteString
deriving stock (Eq, Ord, Show)
type Response = Response' Text
type ResponseMay = Response' (Maybe Text)s.t.
runCmd :: forall cmd io. (SMTEncode cmd, LoggerMIO io) => cmd -> SMT io Response
runCmd c = runCmdMaybe c >>= \case
Unknown Nothing -> pure $ Unknown"Could not determine reason when running GetReasonUnknown"
Unknown (Just reason) -> pure $ Unknown reason
Success -> pure Success
Sat -> pure Sat
Unsat -> pure Unsat
Values vs -> pure $ Values vs
Error e -> pure $ Error e
where
runCmdMaybe :: forall cmd'. SMTEncode cmd' => cmd' -> SMT io ResponseMay
runCmdMaybe cmd = do
let cmdBS = encode cmd
ctxt <- SMT get
case ctxt.mbSolver of
Nothing -> pure $ Unknown (Just "server started without SMT solver")
Just solverRef -> do
whenJust ctxt.mbTranscriptHandle $ \h -> do
whenJust (comment cmd) $ \c ->
liftIO (BS.hPutBuilder h c)
liftIO (BS.hPutBuilder h $ cmdBS <> "\n")
output <- (liftIO $ readIORef solverRef) >>= \solver -> run_ cmd solver cmdBS
let result = readResponse output
whenJust ctxt.mbTranscriptHandle $
liftIO . flip BS.hPutStrLn (BS.pack $ "; " <> show output <> ", parsed as " <> show result <> "\n")
case result of
Error{} -> do
logMessage $
"SMT solver reports: " <> pack (show result)
pure result
Unknown Nothing ->
runCmdMaybe GetReasonUnknown >>= \case
unknownWithReason@(Unknown (Just _)) -> pure unknownWithReason
_ -> pure result
_ -> pure result
There was a problem hiding this comment.
Agree we should resolve this. The underlying ambiguity is that we use Response at low level as well as high level.
We could maybe even have ResponseSolver = Response' () instead of the optionality in ResponseMay, and make the GetReasonUnknown call in runCmd instead of runCmdMay.
jberthold
reviewed
Aug 6, 2024
Comment on lines
-250
to
+270
| let mkTraces duration | ||
| let mkTraces durationLog | ||
| | Just True <- req.logTiming = | ||
| Just [ProcessingTime (Just Booster) duration] | ||
| Just [ProcessingTime (Just Booster) durationLog] |
There was a problem hiding this comment.
o/t ...maybe we should just remove all code for log-timing...
What I am using is the proxy-level timing log, not this level underneath.
There was a problem hiding this comment.
I've prepared a separate PR that removes "log-timing" and "log-fallbacks": #4015
Comment on lines
467
to
501
| withContext CtxConstraint | ||
| . withContext CtxDetail | ||
| . withTermContext (coerce $ collapseAndBools pat.constraints) | ||
| $ pure () | ||
| consistent <- withContext CtxConstraint $ SMT.isSat solver pat.constraints | ||
| withContext CtxConstraint $ do | ||
| logMessage $ | ||
| "Constraints consistency check returns: " <> show consistent | ||
|
|
||
| case consistent of | ||
| Right False -> do | ||
| -- the constraints are unsatisfiable, which means that the patten is Bottom | ||
| throw . SideConditionFalse . collapseAndBools $ pat.constraints | ||
| Left SMT.SMTSolverUnknown{} -> do | ||
| -- unlikely case of an Unknown response to a consistency check. | ||
| -- continue to preserver the old behaviour. | ||
| withContext CtxConstraint . logWarn . Text.pack $ | ||
| "Constraints consistency UNKNOWN: " <> show consistent | ||
| continue | ||
| Left other -> | ||
| -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ | ||
| liftIO $ Exception.throw other | ||
| Right True -> do | ||
| -- constraints are consistent, continue | ||
| continue | ||
| where | ||
| continue = do | ||
| newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults | ||
| -- after evaluating the term, evaluate all (existing and | ||
| -- newly-acquired) constraints, once | ||
| traverse_ simplifyAssumedPredicate . predicates =<< getState | ||
| -- this may yield additional new constraints, left unevaluated | ||
| evaluatedConstraints <- predicates <$> getState | ||
| pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions} | ||
|
|
There was a problem hiding this comment.
It is debatable whether we should give the SMT solver the original (unevaluated) pat.constraints here.
As discussed, we should (eventually) keep the originals around but they might contain unevaluated function calls that the solver would abstract over. AFAICT it is still a sound approximation, though, the solver might just not recognise existing contradictions because it abstracts them away.
And a few stylistic things to note:
- (minor) code mixes record-dot (
pat.constraints) and field pun match (pat{term, ceilConditions}access - the
continueconstruction is unnecessary if we anyway throw exceptions or just go on with a warning - Repeated
withContext CtxConstraintcould be gathered
Suggested change
| withContext CtxConstraint | |
| . withContext CtxDetail | |
| . withTermContext (coerce $ collapseAndBools pat.constraints) | |
| $ pure () | |
| consistent <- withContext CtxConstraint $ SMT.isSat solver pat.constraints | |
| withContext CtxConstraint $ do | |
| logMessage $ | |
| "Constraints consistency check returns: " <> show consistent | |
| case consistent of | |
| Right False -> do | |
| -- the constraints are unsatisfiable, which means that the patten is Bottom | |
| throw . SideConditionFalse . collapseAndBools $ pat.constraints | |
| Left SMT.SMTSolverUnknown{} -> do | |
| -- unlikely case of an Unknown response to a consistency check. | |
| -- continue to preserver the old behaviour. | |
| withContext CtxConstraint . logWarn . Text.pack $ | |
| "Constraints consistency UNKNOWN: " <> show consistent | |
| continue | |
| Left other -> | |
| -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ | |
| liftIO $ Exception.throw other | |
| Right True -> do | |
| -- constraints are consistent, continue | |
| continue | |
| where | |
| continue = do | |
| newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults | |
| -- after evaluating the term, evaluate all (existing and | |
| -- newly-acquired) constraints, once | |
| traverse_ simplifyAssumedPredicate . predicates =<< getState | |
| -- this may yield additional new constraints, left unevaluated | |
| evaluatedConstraints <- predicates <$> getState | |
| pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions} | |
| withContext CtxConstraint $ do | |
| consistent <- | |
| withContext CtxDetail . withTermContext (coerce $ collapseAndBools pat.constraints) $ | |
| SMT.isSat solver pat.constraints | |
| logMessage $ "Constraints consistency check returns: " <> show consistent | |
| case consistent of | |
| Right False -> do | |
| -- the constraints are unsatisfiable, which means that the patten is Bottom | |
| throw . SideConditionFalse . collapseAndBools $ pat.constraints | |
| Left SMT.SMTSolverUnknown{} -> do | |
| -- unlikely case of an Unknown response to a consistency check. | |
| -- continue to preserver the old behaviour. | |
| logWarn . Text.pack $ "Constraints consistency UNKNOWN: " <> show consistent | |
| Left other -> | |
| -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ | |
| liftIO $ Exception.throw other | |
| Right True -> -- constraints are consistent, continue | |
| pure () | |
| newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults | |
| -- after evaluating the term, evaluate all (existing and | |
| -- newly-acquired) constraints, once | |
| traverse_ simplifyAssumedPredicate . predicates =<< getState | |
| -- this may yield additional new constraints, left unevaluated | |
| evaluatedConstraints <- predicates <$> getState | |
| pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions} |
There was a problem hiding this comment.
- after discussing in the daily meeting, we have decided to proceed with checking the constrains as is
- I've introduced some stylistic corrections --- thanks!
Comment on lines
+137
to
+139
| -- | This function defines the strategy to increment the timeout when retrying a solver query | ||
| updateOptionsOnRetry :: SMTOptions -> SMTOptions | ||
| updateOptionsOnRetry opts = opts{timeout = 2 * opts.timeout, retryLimit = ((-) 1) <$> opts.retryLimit} |
There was a problem hiding this comment.
Good idea to locate the option change for retries in a separate function.
Maybe we can make this monadic so that we can log the change (see other comment below).
Also, I just recognise that opts.retryLimit is optional, maybe it should always have a non-negative value?
Comment on lines
+195
to
+211
| failBecauseUnknown :: | ||
| forall io. | ||
| Log.LoggerMIO io => | ||
| Set Predicate -> | ||
| ExceptT SMTError (SMT io) Bool | ||
| failBecauseUnknown psToCheck = | ||
| smtRun GetReasonUnknown >>= \case | ||
| Unknown reason -> do | ||
| Log.withContext Log.CtxAbort $ | ||
| Log.logMessage $ | ||
| "Returned Unknown. Reason: " <> fromMaybe "UNKNOWN" reason | ||
| throwE $ SMTSolverUnknown reason mempty psToCheck | ||
| other -> do | ||
| let msg = "Unexpected result while calling ':reason-unknown': " <> show other | ||
| Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg | ||
| throwSMT' msg | ||
|
|
There was a problem hiding this comment.
Agree we should resolve this. The underlying ambiguity is that we use Response at low level as well as high level.
We could maybe even have ResponseSolver = Response' () instead of the optionality in ResponseMay, and make the GetReasonUnknown call in runCmd instead of runCmdMay.
| solve smtGiven sexprsToCheck transState | ||
| _ -> failBecauseUnknown reasonUnknown | ||
|
|
||
| _ -> failBecauseUnknown psToCheck >> pure Nothing -- Nothing is unreachable and is here to make the type checker happy |
There was a problem hiding this comment.
Nothing is unreachable
Instead, failBecauseUnknown could have a flexible return type ExceptT SMTError (SMT io) a because it will anyway never return any a thing. If we keep failBecauseUnknown, that is...
Comment on lines
+564
to
+565
| lift $ hardResetSolver (updateOptionsOnRetry opts) | ||
| Log.logMessage ("Retrying with higher timeout" :: Text) |
There was a problem hiding this comment.
We should maybe add the same logMessage to the checkPredicates retry code path. Or rather make updateOptionsOnRetry emit the log message?
| @@ -1,6 +1,7 @@ | |||
| {"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""} | |||
| {"context":["proxy"],"message":"Starting RPC server"} | |||
| {"context":["proxy"],"message":"Processing request 4"} | |||
| {"context":[{"request":"4"},"booster","execute",{"term":"bd7c50d"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} | |||
There was a problem hiding this comment.
There is a second log change (removal of a similar line, same inner-most term but different outer ones) that CI is currently failing on.
| "depth": 1, | ||
| "depth": 0, |
There was a problem hiding this comment.
The test name is not quite right any more (the state is not rewritten).
The difference to the other test is that a rewrite b -> d would be possible, so maybe vacuous-not-rewritten ?
| @@ -107,6 +107,7 @@ feature_shell "cd kevm-pyk && poetry run pytest src/tests/integration/test_prove | |||
| mkdir -p $SCRIPT_DIR/logs | |||
|
|
|||
| # use special options if given, but restore KORE_RPC_OPTS afterwards | |||
| FEATURE_SERVER_OPTS=${FEATURE_SERVER_OPTS:-''} | |||
geo2a
force-pushed
the
georgy/evaluate-pattern-pruning
branch
from
b0276d4 to
575428c
Compare
|
Closed in favor of #4020 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #4012