From 99988c1418780c0150d9134e469028364b04b3d1 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Thu, 27 Jun 2024 16:46:33 +0100 Subject: [PATCH 01/25] implment isSat --- booster/library/Booster/SMT/Interface.hs | 63 ++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index d88a8b06f5..9dee83e79c 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -15,6 +15,7 @@ module Booster.SMT.Interface ( finaliseSolver, getModelFor, checkPredicates, + isSat, hardResetSolver, ) where @@ -493,3 +494,65 @@ checkPredicates ctxt givenPs givenSubst psToCheck "Given ∧ P and Given ∧ !P interpreted as " <> pack (show (positive', negative')) pure (positive', negative') + +isSat :: + forall io. + Log.LoggerMIO io => + SMT.SMTContext -> + Set Predicate -> + io (Either SMTError Bool) +isSat ctxt psToCheck + | null psToCheck = pure . Right $ True + | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do + Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg + pure . Left . SMTTranslationError $ errMsg + | Right (smtToCheck, transState) <- translated = Log.withContext Log.CtxSMT $ do + evalSMT ctxt . runExceptT $ solve smtToCheck transState + where + translated :: Either Text ([DeclareCommand], TranslationState) + translated = + SMT.runTranslator $ + mapM (\(Predicate p) -> Assert (mkComment p) <$> SMT.translateTerm p) $ + Set.toList psToCheck + + solve smtToCheck transState = solve' + where + solve' = do + lift $ hardResetSolver ctxt.options + Log.getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + Log.logMessage . Pretty.renderOneLineText $ + hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck)) + lift $ declareVariables transState + mapM_ smtRun smtToCheck + smtRun CheckSat >>= \case + Sat -> pure True + Unsat -> pure False + Unknown _ -> retry + other -> do + let msg = "Unexpected result while calling 'check-sat': " <> show other + Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg + throwSMT' msg + + retry = do + opts <- lift . SMT $ gets (.options) + case opts.retryLimit of + Just x | x > 0 -> do + let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1} + lift $ hardResetSolver newOpts + Log.logMessage ("Retrying with higher timeout" :: Text) + solve' + _ -> failBecauseUnknown + + failBecauseUnknown :: ExceptT SMTError (SMT io) Bool + failBecauseUnknown = + 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 From f368038f95b7bdf63070977d914875323aefe43b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 15:09:49 +0200 Subject: [PATCH 02/25] Check constraints for consistency in evaluatePattern' --- .../library/Booster/Pattern/ApplyEquations.hs | 35 ++++++++++++++----- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index ca5fee67b1..06bee3b752 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -439,7 +439,11 @@ evaluateTerm' :: evaluateTerm' direction = iterateEquations direction PreferFunctions {- | Simplify a Pattern, processing its constraints independently. - Returns either the first failure or the new pattern if no failure was encountered + + Before evaluating the term of the pattern, + the constraints of the pattern are checked for consistency with an SMT solver. + + Returns either the first failure or the new pattern if no failure was encountered. -} evaluatePattern :: LoggerMIO io => @@ -458,13 +462,28 @@ evaluatePattern' :: Pattern -> EquationT io Pattern evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ 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} + solver <- (.smtSolver) <$> getConfig + -- check initial constraints for consistency, reporting an error if they are Bottom + SMT.isSat solver pat.constraints >>= \case + Right False -> do + let collapseAndBools :: Set Predicate -> Predicate + collapseAndBools = undefined + -- the constraints are unsatisfiable, which means that the patten is Bottom + throw . SideConditionFalse . collapseAndBools $ pat.constraints + Left unknwon@SMT.SMTSolverUnknown{} -> do + -- unlikely case of an Unknown response to a consistency check. + -- What to do here? fail hard for now. + liftIO $ Exception.throw unknwon + Left other -> liftIO $ Exception.throw other -- fail hard on other SMT errors + Right True -> do + -- constrains are consistent, continue + 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} where -- when TooManyIterations exception occurred while evaluating the top-level term, -- i.e. not in a recursive evaluation of a side-condition, From 32b08b7b6550a0ffe62598eb2489e7514c9be4e1 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 15:17:51 +0200 Subject: [PATCH 03/25] Do not fail on Unknown pattern constraints --- .../library/Booster/Pattern/ApplyEquations.hs | 27 ++++++++++++------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 06bee3b752..feab1ae6ee 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -472,19 +472,26 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do throw . SideConditionFalse . collapseAndBools $ pat.constraints Left unknwon@SMT.SMTSolverUnknown{} -> do -- unlikely case of an Unknown response to a consistency check. - -- What to do here? fail hard for now. - liftIO $ Exception.throw unknwon - Left other -> liftIO $ Exception.throw other -- fail hard on other SMT errors + -- What to do here? continue for now to preserver the old behaviour. + withPatternContext pat . logWarn . Text.pack $ + "Constraints consistency check returns: " <> show unknwon + continue + Left other -> + -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ + liftIO $ Exception.throw other Right True -> do -- constrains are consistent, continue - 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} + 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} + -- when TooManyIterations exception occurred while evaluating the top-level term, -- i.e. not in a recursive evaluation of a side-condition, -- it is safe to keep the partial result and ignore the exception. From 59bd44babaf6e736e93e12c163e4606b07e09a98 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 16:46:50 +0200 Subject: [PATCH 04/25] Ignore prelude check result when running with noSolver --- booster/library/Booster/SMT/Interface.hs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 9dee83e79c..7ccdd68623 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -12,6 +12,7 @@ module Booster.SMT.Interface ( SMTError (..), initSolver, noSolver, + isNoSolver, finaliseSolver, getModelFor, checkPredicates, @@ -34,7 +35,7 @@ import Data.Either.Extra (fromLeft', fromRight') import Data.IORef import Data.Map (Map) import Data.Map qualified as Map -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, isNothing) import Data.Set (Set) import Data.Set qualified as Set import Data.Text as Text (Text, pack, unlines, unwords) @@ -121,6 +122,10 @@ noSolver = do , options = defaultSMTOptions{retryLimit = Just 0} } +-- | Detect of the @SMTContext@ does not have a solver +isNoSolver :: SMT.SMTContext -> Bool +isNoSolver SMTContext{mbSolver} = isNothing mbSolver + -- | Hot-swap @SMTOptions@ in the active @SMTContext@, update the query timeout swapSmtOptions :: forall io. Log.LoggerMIO io => SMTOptions -> SMT io () swapSmtOptions smtOptions = do @@ -163,10 +168,14 @@ checkPrelude = do case check of Sat -> pure () other -> do - Log.logMessage $ "Initial SMT definition check returned " <> pack (show other) - SMT get >>= closeContext - throwSMT' $ - "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other + ctxt <- SMT get + if isNoSolver ctxt + then -- when running with a dummy solver, ignore the Unknown prelude check + pure () + else do + Log.logMessage $ "Initial SMT definition check returned " <> pack (show other) + throwSMT' $ + "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other -- | Send the commands from the definition's SMT prelude runPrelude :: Log.LoggerMIO io => SMT io () From fd3ea50456b584c5b53531494e6f21f662e2b48c Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 17:32:00 +0200 Subject: [PATCH 05/25] Set FEATURE_SERVER_OPTS to '' if it's unbound --- scripts/performance-tests-kevm.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/performance-tests-kevm.sh b/scripts/performance-tests-kevm.sh index 2ca4ec2df3..e0f2c27563 100755 --- a/scripts/performance-tests-kevm.sh +++ b/scripts/performance-tests-kevm.sh @@ -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:-''} if [ ! -z "${FEATURE_SERVER_OPTS}" ]; then echo "Using special options '${FEATURE_SERVER_OPTS}' via KORE_RPC_OPTS" if [ ! -z "${KORE_RPC_OPTS:-}" ]; then From bb6a765294ad121b1d00eb2d97a00c5e6702c3df Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 18:16:47 +0200 Subject: [PATCH 06/25] Emit more logs from evaluatePattern' --- .../library/Booster/Pattern/ApplyEquations.hs | 22 ++++++++++++++----- 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index feab1ae6ee..4a66fc3bcf 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -464,17 +464,24 @@ evaluatePattern' :: evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do solver <- (.smtSolver) <$> getConfig -- check initial constraints for consistency, reporting an error if they are Bottom - SMT.isSat solver pat.constraints >>= \case + 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 - let collapseAndBools :: Set Predicate -> Predicate - collapseAndBools = undefined -- the constraints are unsatisfiable, which means that the patten is Bottom throw . SideConditionFalse . collapseAndBools $ pat.constraints - Left unknwon@SMT.SMTSolverUnknown{} -> do + Left SMT.SMTSolverUnknown{} -> do -- unlikely case of an Unknown response to a consistency check. -- What to do here? continue for now to preserver the old behaviour. - withPatternContext pat . logWarn . Text.pack $ - "Constraints consistency check returns: " <> show unknwon + withContext CtxConstraint . logWarn . Text.pack $ + "Constraints consistency UNKNOWN: " <> show consistent continue Left other -> -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ @@ -503,6 +510,9 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do pure partialResult err -> throw err + collapseAndBools :: Set Predicate -> Predicate + collapseAndBools = coerce . foldAndBool . map coerce . Set.toList + -- evaluate the given predicate assuming all others simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io () simplifyAssumedPredicate p = do From 29524b86583acf214ad16eaf695759e2cdd7ee45 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 1 Aug 2024 18:17:23 +0200 Subject: [PATCH 07/25] Check consistency of the pattern before rewriting --- booster/library/Booster/JsonRpc.hs | 78 +++++++++++++++++++----------- 1 file changed, 51 insertions(+), 27 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 11a0399f2c..5245022fa2 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -155,33 +155,57 @@ respond stateVar request = solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions - logger <- getLogger - prettyModifiers <- getPrettyModifiers - let rewriteConfig = - RewriteConfig - { definition = def - , llvmApi = mLlvmLibrary - , smtSolver = solver - , varsToAvoid = substVars - , doTracing - , logger - , prettyModifiers - , mbMaxDepth = mbDepth - , mbSimplify = rewriteOpts.interimSimplification - , cutLabels = cutPoints - , terminalLabels = terminals - } - result <- - performRewrite rewriteConfig substPat - SMT.finaliseSolver solver - stop <- liftIO $ getTime Monotonic - let duration = - if fromMaybe False req.logTiming - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ execResponse duration req result substitution unsupported + -- check input pattern's consistency before starting rewriting + evaluatedInitialPattern <- + ApplyEquations.evaluatePattern + def + mLlvmLibrary + solver + mempty + substPat + + case evaluatedInitialPattern of + (Left ApplyEquations.SideConditionFalse{}, _) -> do + stop <- liftIO $ getTime Monotonic + let duration = + if fromMaybe False req.logTiming + then + Just $ + fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 + else Nothing + pure $ execResponse duration req (0, mempty, RewriteTrivial substPat) substitution unsupported + (Left other, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + (Right newPattern, _simplifierCache) -> do + -- FIXME do not throw away @simplifierCache@, pass it to performRewrite somehow + logger <- getLogger + prettyModifiers <- getPrettyModifiers + let rewriteConfig = + RewriteConfig + { definition = def + , llvmApi = mLlvmLibrary + , smtSolver = solver + , varsToAvoid = substVars + , doTracing + , logger + , prettyModifiers + , mbMaxDepth = mbDepth + , mbSimplify = rewriteOpts.interimSimplification + , cutLabels = cutPoints + , terminalLabels = terminals + } + + result <- + performRewrite rewriteConfig newPattern + SMT.finaliseSolver solver + stop <- liftIO $ getTime Monotonic + let duration = + if fromMaybe False req.logTiming + then + Just $ + fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 + else Nothing + pure $ execResponse duration req result substitution unsupported RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar From 88522821780849aeb1121cc21a0e8fbbf0746625 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 2 Aug 2024 09:44:41 +0200 Subject: [PATCH 08/25] Move log message out --- booster/library/Booster/SMT/Interface.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 7ccdd68623..50f7931195 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -168,12 +168,12 @@ checkPrelude = do case check of Sat -> pure () other -> do + Log.logMessage $ "Initial SMT definition check returned " <> pack (show other) ctxt <- SMT get if isNoSolver ctxt then -- when running with a dummy solver, ignore the Unknown prelude check pure () - else do - Log.logMessage $ "Initial SMT definition check returned " <> pack (show other) + else throwSMT' $ "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other From 8f13183cd09fbfd8cae9a3648f5b0c6d3475897a Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 2 Aug 2024 09:51:11 +0200 Subject: [PATCH 09/25] Remove bad hardResetSolver --- booster/library/Booster/SMT/Interface.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 50f7931195..bc08d0417c 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -527,7 +527,6 @@ isSat ctxt psToCheck solve smtToCheck transState = solve' where solve' = do - lift $ hardResetSolver ctxt.options Log.getPrettyModifiers >>= \case ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> Log.logMessage . Pretty.renderOneLineText $ From 1948b1521e990d89b9d89962a5a0e020610708fb Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 2 Aug 2024 10:04:05 +0200 Subject: [PATCH 10/25] Hard reset in the beginning of isSat --- booster/library/Booster/SMT/Interface.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index bc08d0417c..04021d050d 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -516,7 +516,9 @@ isSat ctxt psToCheck Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg pure . Left . SMTTranslationError $ errMsg | Right (smtToCheck, transState) <- translated = Log.withContext Log.CtxSMT $ do - evalSMT ctxt . runExceptT $ solve smtToCheck transState + evalSMT ctxt . runExceptT $ do + lift $ hardResetSolver ctxt.options + solve smtToCheck transState where translated :: Either Text ([DeclareCommand], TranslationState) translated = From 8bef12a6713bab924cfe1e4b59ebda6716ea3e58 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 2 Aug 2024 15:55:46 +0200 Subject: [PATCH 11/25] Update integration test output --- .../test-log-simplify-json/simplify-log.txt.golden | 1 + 1 file changed, 1 insertion(+) diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index e7d03842a4..dc3c511503 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -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"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} From 432ff02751da22a446713afa8825e52ac0dccc87 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 11:12:23 +0200 Subject: [PATCH 12/25] pretty: print substitution as bindings, separate imports --- dev-tools/package.yaml | 1 + dev-tools/pretty/Pretty.hs | 24 ++++++++++++++++-------- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index 3ab1e66bc3..cf002942bd 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -157,6 +157,7 @@ executables: - base - aeson - bytestring + - containers - hs-backend-booster - prettyprinter - text diff --git a/dev-tools/pretty/Pretty.hs b/dev-tools/pretty/Pretty.hs index e7a2400bc9..0dafebdf71 100644 --- a/dev-tools/pretty/Pretty.hs +++ b/dev-tools/pretty/Pretty.hs @@ -9,6 +9,15 @@ module Main ( main, ) where +import Control.Monad.Trans.Except +import Data.Aeson (eitherDecode) +import Data.ByteString.Lazy qualified as BS +import Data.Map qualified as Map +import Data.Text.IO qualified as Text +import Prettyprinter +import System.Environment (getArgs) + +import Booster.Pattern.Base (Term, Variable (..)) import Booster.Pattern.Pretty import Booster.Prettyprinter (renderDefault) import Booster.Syntax.Json (KoreJson (..)) @@ -21,12 +30,6 @@ import Booster.Syntax.Json.Internalise ( pattern DisallowAlias, ) import Booster.Syntax.ParsedKore (internalise, parseKoreDefinition) -import Control.Monad.Trans.Except -import Data.Aeson (eitherDecode) -import Data.ByteString.Lazy qualified as BS -import Data.Text.IO qualified as Text -import Prettyprinter -import System.Environment (getArgs) main :: IO () main = do @@ -40,9 +43,11 @@ main = do Left err -> putStrLn $ "Error: " ++ err Right KoreJson{term} -> do case runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term of - Right (trm, _subst, _unsupported) -> do + Right (trm, subst, _unsupported) -> do putStrLn "Pretty-printing pattern: " putStrLn $ renderDefault $ pretty' @'[Decoded] trm + putStrLn "Substitution: " + mapM_ (putStrLn . prettyPrintSubstItem) (Map.toList subst) Left (NoTermFound _) -> case runExcept $ internalisePredicates DisallowAlias CheckSubsorts Nothing internalDef [term] of Left es -> error (show es) @@ -53,7 +58,10 @@ main = do putStrLn "Ceil predicates: " mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.ceilPredicates putStrLn "Substitution: " - mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.substitution + mapM_ (putStrLn . prettyPrintSubstItem) (Map.toList ts.substitution) putStrLn "Unsupported predicates: " mapM_ print ts.unsupported Left err -> error (show err) + +prettyPrintSubstItem :: (Variable, Term) -> String +prettyPrintSubstItem (v, t) = show v.variableName <> " |-> " <> (renderDefault . pretty' @'[Decoded] $ t) From 7fe9293a7660d72bf79a190c6e3e33c81eb6f286 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 12:42:39 +0200 Subject: [PATCH 13/25] Update outputs of booster/test/rpc-integration/test-substitution --- .../test-substitutions/README.md | 9 +- .../response-circular-equations.booster-dev | 62 +---- ...onse-symbolic-bottom-predicate.booster-dev | 240 ------------------ .../response-symbolic-bottom-predicate.json | 125 +++------ ...nse-symbolic-two-substitutions.booster-dev | 12 +- .../response-vacuous-but-rewritten.json | 47 ++-- .../response-vacuous-without-rewrite.json | 43 ++-- 7 files changed, 89 insertions(+), 449 deletions(-) delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md index 1c7a208f58..2311202566 100644 --- a/booster/test/rpc-integration/test-substitutions/README.md +++ b/booster/test/rpc-integration/test-substitutions/README.md @@ -31,10 +31,9 @@ NB: Booster applies the given substitution before performing any action. - with an additional constraint `Y = 1 +Int X` (internalised as a substitution) - leading to a contradictory constraint `X = 1 +Int X` after rewriting and adding `Y =Int X` from the `ensures`-clause - - `kore-rpc-booster` returns `vacuous` after 1 step - - `kore-rpc-dev` returns `vacuous` after 0 steps (detects the contradiction earlier) - - `kore-rpc-dev` reproduces the exact input as `state` while - `kore-rpc-booster` splits off `substitution` (from input) and `predicate` (from the rule) + - `kore-rpc-booster` and `booster-dev` return `vacuous` after 0 step, substitution `Y` for `X +Int 1` in the state. However, `kore-rpc-booster` and `booster-dev` disagree a little on the value in the substitution, hence the two responses. + - `kore-rpc-dev` returns `vacuous` after 0 steps and reproduces the exact input as `state` + * `state-circular-equations.execute` - starts from `concrete-subst` - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1` @@ -42,6 +41,6 @@ NB: Booster applies the given substitution before performing any action. * `state-symbolic-bottom-predicate.execute` - starts from `symbolic-subst` - with an equation that is instantly false: `X = 1 +Int X` - - leading to a vacuous state in `kore-rpc-booster` after rewriting once, + - leading to a vacuous state in `booster-dev` and `kore-rpc-booster`, - while `kore-rpc-dev` returns `stuck` instantly after 0 steps, returning the exact input as `state`. diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index b012148190..259a441aeb 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -225,61 +225,13 @@ } }, { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - }, - { - "tag": "App", - "name": "Lbl'Unds'-Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } } ] } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev deleted file mode 100644 index 9aec4d5289..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ /dev/null @@ -1,240 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - ] - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index be972500f9..8196839aaa 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -3,7 +3,7 @@ "id": 1, "result": { "reason": "vacuous", - "depth": 1, + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "a" + "value": "symbolic-subst" } ] }, @@ -115,114 +115,57 @@ "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, - "second": { + { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -231,8 +174,8 @@ } ] } - } - ] + ] + } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev index 40c6e95a24..58a6ab33aa 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev @@ -87,22 +87,22 @@ "sorts": [], "args": [ { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } }, { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" } ] } diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json index b7cf387833..3d880fa432 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json @@ -3,7 +3,7 @@ "id": 1, "result": { "reason": "vacuous", - "depth": 1, + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "d" + "value": "b" } ] }, @@ -129,7 +129,7 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", "sorts": [], "args": [ { @@ -176,33 +176,26 @@ }, "second": { "tag": "App", - "name": "LblnotBool'Unds'", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" } ] } diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json index d3b14044a8..9d4198621d 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json @@ -129,7 +129,7 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", "sorts": [], "args": [ { @@ -176,33 +176,26 @@ }, "second": { "tag": "App", - "name": "LblnotBool'Unds'", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" } ] } From 2483a578470157e892848fca26d90215839543f6 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 12:43:16 +0200 Subject: [PATCH 14/25] Run test-substitutions with booster-dev --- scripts/booster-integration-tests.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh index 3a24d3db64..bde164c195 100755 --- a/scripts/booster-integration-tests.sh +++ b/scripts/booster-integration-tests.sh @@ -28,12 +28,12 @@ for dir in $(ls -d test-*); do name=${dir##test-} echo "Running $name..." case "$name" in - "a-to-f" | "diamond") + "a-to-f" | "diamond" | "substitutions") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; - "substitutions" | "vacuous" | "pathological-add-module") + "vacuous" | "pathological-add-module") SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; From 25afc7320436a2fbe0ad6d02e615973e61c4e0c0 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 15:51:56 +0200 Subject: [PATCH 15/25] Use the same code to update SMT options on retries --- booster/library/Booster/SMT/Interface.hs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 04021d050d..778af0b2b2 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -134,6 +134,10 @@ swapSmtOptions smtOptions = do SMT $ put ctxt{options = smtOptions} runCmd_ $ SetTimeout smtOptions.timeout +-- | 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} + -- | Stop the solver, initialise a new one and put in the @SMTContext@ hardResetSolver :: forall io. Log.LoggerMIO io => SMTOptions -> SMT io () hardResetSolver smtOptions = do @@ -234,8 +238,7 @@ getModelFor ctxt ps subst Unknown{} -> do case opts.retryLimit of Just x | x > 0 -> do - let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1} - lift $ hardResetSolver newOpts + lift $ hardResetSolver (updateOptionsOnRetry opts) solve smtAsserts transState _ -> pure . Left $ response _ -> pure . Left $ response @@ -418,8 +421,7 @@ checkPredicates ctxt givenPs givenSubst psToCheck opts <- lift . SMT $ gets (.options) case opts.retryLimit of Just x | x > 0 -> do - let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1} - lift $ hardResetSolver newOpts + lift $ hardResetSolver (updateOptionsOnRetry opts) solve smtGiven sexprsToCheck transState _ -> failBecauseUnknown reasonUnknown @@ -548,8 +550,7 @@ isSat ctxt psToCheck opts <- lift . SMT $ gets (.options) case opts.retryLimit of Just x | x > 0 -> do - let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1} - lift $ hardResetSolver newOpts + lift $ hardResetSolver (updateOptionsOnRetry opts) Log.logMessage ("Retrying with higher timeout" :: Text) solve' _ -> failBecauseUnknown From c9f107de3bd991cfea51cb3bac6b3a4ce291660e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 15:59:09 +0200 Subject: [PATCH 16/25] Factor-out and unify failBecauseUnknown --- booster/library/Booster/SMT/Interface.hs | 49 +++++++++++------------- 1 file changed, 22 insertions(+), 27 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 778af0b2b2..bd18eb8200 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -192,6 +192,23 @@ finaliseSolver ctxt = do Log.logMessage ("Closing SMT solver" :: Text) destroyContext ctxt +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 + {- | Implementation of get-model request @@ -405,8 +422,8 @@ checkPredicates ctxt givenPs givenSubst psToCheck pure Nothing (Sat, Unsat) -> pure . Just $ True (Unsat, Sat) -> pure . Just $ False - (Unknown reason, _) -> retry smtGiven sexprsToCheck transState reason - (_, Unknown reason) -> retry smtGiven sexprsToCheck transState reason + (Unknown _, _) -> retry smtGiven sexprsToCheck transState + (_, Unknown _) -> retry smtGiven sexprsToCheck transState other -> throwE . GeneralSMTError $ ("Unexpected result while checking a condition: " :: Text) <> Text.pack (show other) @@ -415,16 +432,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck [DeclareCommand] -> [SExpr] -> TranslationState -> - Maybe Text -> ExceptT SMTError (SMT io) (Maybe Bool) - retry smtGiven sexprsToCheck transState reasonUnknown = do + retry smtGiven sexprsToCheck transState = do opts <- lift . SMT $ gets (.options) case opts.retryLimit of Just x | x > 0 -> do lift $ hardResetSolver (updateOptionsOnRetry opts) solve smtGiven sexprsToCheck transState - _ -> failBecauseUnknown reasonUnknown - + _ -> failBecauseUnknown psToCheck >> pure Nothing -- Nothing is unreachable and is here to make the type checker happy translated :: Either Text (([DeclareCommand], [SExpr]), TranslationState) translated = SMT.runTranslator $ do let mkSMTEquation v t = @@ -437,13 +452,6 @@ checkPredicates ctxt givenPs givenSubst psToCheck mapM (SMT.translateTerm . coerce) $ Set.toList psToCheck pure (smtSubst <> smtPs, toCheck) - failBecauseUnknown :: Maybe Text -> ExceptT SMTError (SMT io) (Maybe Bool) - failBecauseUnknown reason = do - Log.withContext Log.CtxAbort $ - Log.logMessage $ - "Returned Unknown. Reason: " <> fromMaybe "UNKNOWN" reason - throwE $ SMTSolverUnknown reason givenPs psToCheck - -- Given the known truth and the expressions to check, -- interact with the solver to establish the validity of the expressions. -- @@ -553,17 +561,4 @@ isSat ctxt psToCheck lift $ hardResetSolver (updateOptionsOnRetry opts) Log.logMessage ("Retrying with higher timeout" :: Text) solve' - _ -> failBecauseUnknown - - failBecauseUnknown :: ExceptT SMTError (SMT io) Bool - failBecauseUnknown = - 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 + _ -> failBecauseUnknown psToCheck From 2ef21abcd3c596855603951e6b2876246709d0f0 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 16:06:28 +0200 Subject: [PATCH 17/25] Update comments --- booster/library/Booster/SMT/Interface.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index bd18eb8200..a80523c155 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -352,9 +352,9 @@ getModelFor ctxt ps subst mkComment :: Pretty (PrettyWithModifiers '[Decoded] a) => a -> BS.ByteString mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded] -{- | Check a predicates, given a set of predicates as known truth. +{- | Check validity of a predicate, given a set of predicates as known truth. -Simplest version: +The set of input predicates @psToCheck@ is interpreted as a conjunction. Given K as known truth and predicates P to check, check whether K => P or K => !P, or neither of those implications holds. The check is done @@ -514,6 +514,9 @@ checkPredicates ctxt givenPs givenSubst psToCheck <> pack (show (positive', negative')) pure (positive', negative') +{- | Check satisfiability of a predicate. + The set of input predicates @psToCheck@ is interpreted as a conjunction. +-} isSat :: forall io. Log.LoggerMIO io => From 64147e3fc169b9ec082f94284ba49234a2a8b2a2 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 16:14:15 +0200 Subject: [PATCH 18/25] Factor-out duration --- booster/library/Booster/JsonRpc.hs | 37 +++++++++++++++--------------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 5245022fa2..31a9062e48 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -167,13 +167,13 @@ respond stateVar request = case evaluatedInitialPattern of (Left ApplyEquations.SideConditionFalse{}, _) -> do stop <- liftIO $ getTime Monotonic - let duration = - if fromMaybe False req.logTiming - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ execResponse duration req (0, mempty, RewriteTrivial substPat) substitution unsupported + pure $ + execResponse + (duration req.logTiming start stop) + req + (0, mempty, RewriteTrivial substPat) + substitution + unsupported (Left other, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) (Right newPattern, _simplifierCache) -> do @@ -199,13 +199,7 @@ respond stateVar request = performRewrite rewriteConfig newPattern SMT.finaliseSolver solver stop <- liftIO $ getTime Monotonic - let duration = - if fromMaybe False req.logTiming - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ execResponse duration req result substitution unsupported + pure $ execResponse (duration req.logTiming start stop) req result substitution unsupported RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar @@ -271,9 +265,9 @@ respond stateVar request = start <- liftIO $ getTime Monotonic let internalised = runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term - let mkTraces duration + let mkTraces durationLog | Just True <- req.logTiming = - Just [ProcessingTime (Just Booster) duration] + Just [ProcessingTime (Just Booster) durationLog] | otherwise = Nothing @@ -351,11 +345,11 @@ respond stateVar request = SMT.finaliseSolver solver stop <- liftIO $ getTime Monotonic - let duration = + let durationLog = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 mkSimplifyResponse state = RpcTypes.Simplify - RpcTypes.SimplifyResult{state, logs = mkTraces duration} + RpcTypes.SimplifyResult{state, logs = mkTraces durationLog} pure $ second mkSimplifyResponse result RpcTypes.GetModel req -> withModule req._module $ \case (_, _, Nothing, _) -> do @@ -591,6 +585,13 @@ respond stateVar request = , logs = Nothing } + duration mLogTiming start stop = + if fromMaybe False mLogTiming + then + Just $ + fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 + else Nothing + handleSmtError :: JsonRpcHandler handleSmtError = JsonRpcHandler $ \case SMT.GeneralSMTError err -> runtimeError "problem" err From 24b812631f4472528978988956d86f060143fca4 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 16:17:29 +0200 Subject: [PATCH 19/25] comment --- booster/library/Booster/JsonRpc.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 31a9062e48..2da7bacbf1 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -166,6 +166,7 @@ respond stateVar request = case evaluatedInitialPattern of (Left ApplyEquations.SideConditionFalse{}, _) -> do + -- input pattern's constrains are Bottom, return Bottom stop <- liftIO $ getTime Monotonic pure $ execResponse From 10f6b186422f383cd619257665b48db0664b0a78 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 16:24:34 +0200 Subject: [PATCH 20/25] Pass initial simplifier cache to performRewrite --- booster/library/Booster/JsonRpc.hs | 5 ++--- booster/library/Booster/Pattern/Rewrite.hs | 19 ++++++++++--------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 2da7bacbf1..4e20b2c42e 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -177,8 +177,7 @@ respond stateVar request = unsupported (Left other, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) - (Right newPattern, _simplifierCache) -> do - -- FIXME do not throw away @simplifierCache@, pass it to performRewrite somehow + (Right newPattern, simplifierCache) -> do logger <- getLogger prettyModifiers <- getPrettyModifiers let rewriteConfig = @@ -197,7 +196,7 @@ respond stateVar request = } result <- - performRewrite rewriteConfig newPattern + performRewrite rewriteConfig simplifierCache newPattern SMT.finaliseSolver solver stop <- liftIO $ getTime Monotonic pure $ execResponse (duration req.logTiming start stop) req result substitution unsupported diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 8e30383f97..c162bd7676 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -704,9 +704,10 @@ performRewrite :: forall io. LoggerMIO io => RewriteConfig -> + SimplifierCache -> Pattern -> io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) -performRewrite rewriteConfig pat = do +performRewrite rewriteConfig initialCache pat = do (rr, RewriteStepsState{counter, traces}) <- flip runStateT rewriteStart $ doSteps False pat pure (counter, traces, rr) @@ -722,6 +723,14 @@ performRewrite rewriteConfig pat = do , terminalLabels } = rewriteConfig + rewriteStart :: RewriteStepsState + rewriteStart = + RewriteStepsState + { counter = 0 + , traces = mempty + , simplifierCache = initialCache + } + logDepth = withContext CtxDepth . logMessage depthReached n = maybe False (n >=) mbMaxDepth @@ -919,11 +928,3 @@ data RewriteStepsState = RewriteStepsState , traces :: !(Seq (RewriteTrace ())) , simplifierCache :: SimplifierCache } - -rewriteStart :: RewriteStepsState -rewriteStart = - RewriteStepsState - { counter = 0 - , traces = mempty - , simplifierCache = mempty - } From 7f7d667f6c7dc2890d565a5315e036d1e67d934b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 16:35:25 +0200 Subject: [PATCH 21/25] Correct comments --- booster/library/Booster/JsonRpc.hs | 2 +- booster/library/Booster/Pattern/ApplyEquations.hs | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 4e20b2c42e..3620a12bf0 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -166,7 +166,7 @@ respond stateVar request = case evaluatedInitialPattern of (Left ApplyEquations.SideConditionFalse{}, _) -> do - -- input pattern's constrains are Bottom, return Bottom + -- input pattern's constraints are Bottom, return Vacuous stop <- liftIO $ getTime Monotonic pure $ execResponse diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 4a66fc3bcf..e9e8500284 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -463,7 +463,7 @@ evaluatePattern' :: EquationT io Pattern evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do solver <- (.smtSolver) <$> getConfig - -- check initial constraints for consistency, reporting an error if they are Bottom + -- check the pattern's constraints for consistency, reporting an error if they are Bottom withContext CtxConstraint . withContext CtxDetail . withTermContext (coerce $ collapseAndBools pat.constraints) @@ -479,7 +479,7 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do throw . SideConditionFalse . collapseAndBools $ pat.constraints Left SMT.SMTSolverUnknown{} -> do -- unlikely case of an Unknown response to a consistency check. - -- What to do here? continue for now to preserver the old behaviour. + -- continue to preserver the old behaviour. withContext CtxConstraint . logWarn . Text.pack $ "Constraints consistency UNKNOWN: " <> show consistent continue @@ -487,7 +487,7 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ liftIO $ Exception.throw other Right True -> do - -- constrains are consistent, continue + -- constraints are consistent, continue continue where continue = do From 80d1675092008704dae9f35111764a635ae0b80d Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 5 Aug 2024 17:08:43 +0200 Subject: [PATCH 22/25] Fix unit tests --- booster/unit-tests/Test/Booster/Pattern/Rewrite.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs index 3c295c7ebe..63d9b70f7b 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -294,7 +294,7 @@ runRewrite t = do conf <- testConf (counter, _, res) <- runNoLoggingT $ - performRewrite conf $ + performRewrite conf mempty $ Pattern_ t pure (counter, fmap (.term) res) @@ -438,7 +438,7 @@ supportsDepthControl = rewritesToDepth (MaxDepth depth) (Steps n) t t' f = do conf <- testConf (counter, _, res) <- - runNoLoggingT $ performRewrite conf{mbMaxDepth = Just depth} $ Pattern_ t + runNoLoggingT $ performRewrite conf{mbMaxDepth = Just depth} mempty $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t') supportsCutPoints :: TestTree @@ -492,7 +492,7 @@ supportsCutPoints = conf <- testConf (counter, _, res) <- runNoLoggingT $ - performRewrite conf{cutLabels = [lbl]} $ + performRewrite conf{cutLabels = [lbl]} mempty $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t') @@ -524,5 +524,5 @@ supportsTerminalRules = rewritesToTerminal lbl (Steps n) t t' f = do conf <- testConf (counter, _, res) <- - runNoLoggingT $ performRewrite conf{terminalLabels = [lbl]} $ Pattern_ t + runNoLoggingT $ performRewrite conf{terminalLabels = [lbl]} mempty $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t') From 1fce2541c1cacf502493c651d0b6d91df4efb247 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 6 Aug 2024 16:17:23 +0200 Subject: [PATCH 23/25] Use record field punning to access the constraints --- booster/library/Booster/Pattern/ApplyEquations.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index e9e8500284..58377eee8a 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -461,14 +461,14 @@ evaluatePattern' :: LoggerMIO io => Pattern -> EquationT io Pattern -evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do +evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do solver <- (.smtSolver) <$> getConfig -- check the pattern's constraints for consistency, reporting an error if they are Bottom withContext CtxConstraint . withContext CtxDetail - . withTermContext (coerce $ collapseAndBools pat.constraints) + . withTermContext (coerce $ collapseAndBools constraints) $ pure () - consistent <- withContext CtxConstraint $ SMT.isSat solver pat.constraints + consistent <- withContext CtxConstraint $ SMT.isSat solver constraints withContext CtxConstraint $ do logMessage $ "Constraints consistency check returns: " <> show consistent @@ -476,7 +476,7 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do case consistent of Right False -> do -- the constraints are unsatisfiable, which means that the patten is Bottom - throw . SideConditionFalse . collapseAndBools $ pat.constraints + throw . SideConditionFalse . collapseAndBools $ constraints Left SMT.SMTSolverUnknown{} -> do -- unlikely case of an Unknown response to a consistency check. -- continue to preserver the old behaviour. From d82576f8e88555ef60296e6325a74d52492cdf4d Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 6 Aug 2024 16:25:12 +0200 Subject: [PATCH 24/25] Improve control-flow in evaluatePattern' --- .../library/Booster/Pattern/ApplyEquations.hs | 41 +++++++++---------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 58377eee8a..a2da5ce771 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -463,16 +463,15 @@ evaluatePattern' :: EquationT io Pattern evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do solver <- (.smtSolver) <$> getConfig - -- check the pattern's constraints for consistency, reporting an error if they are Bottom - withContext CtxConstraint - . withContext CtxDetail - . withTermContext (coerce $ collapseAndBools constraints) - $ pure () - consistent <- withContext CtxConstraint $ SMT.isSat solver constraints - withContext CtxConstraint $ do - logMessage $ - "Constraints consistency check returns: " <> show consistent - + -- check the pattern's constraints for satisfiability to ensure they are consistent + consistent <- + withContext CtxConstraint $ do + withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure () + consistent <- SMT.isSat solver constraints + withContext CtxConstraint $ + logMessage $ + "Constraints consistency check returns: " <> show consistent + pure consistent case consistent of Right False -> do -- the constraints are unsatisfiable, which means that the patten is Bottom @@ -482,23 +481,21 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon -- continue to preserver the old behaviour. withContext CtxConstraint . logWarn . Text.pack $ "Constraints consistency UNKNOWN: " <> show consistent - continue + pure () Left other -> -- fail hard on SMT error other than @SMT.SMTSolverUnknown@ liftIO $ Exception.throw other - Right True -> do + Right True -> -- 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} + 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} + where -- when TooManyIterations exception occurred while evaluating the top-level term, -- i.e. not in a recursive evaluation of a side-condition, -- it is safe to keep the partial result and ignore the exception. From 575428c912bc1674bc5bdc0753cb12645d148a26 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 6 Aug 2024 16:34:39 +0200 Subject: [PATCH 25/25] Rename test case --- booster/test/rpc-integration/test-vacuous/README.md | 2 +- ...s-but-rewritten.json => response-vacuous-not-rewritten.json} | 0 ...kore-rpc-dev => response-vacuous-not-rewritten.kore-rpc-dev} | 0 ...ut-rewritten.execute => state-vacuous-not-rewritten.execute} | 0 4 files changed, 1 insertion(+), 1 deletion(-) rename booster/test/rpc-integration/test-vacuous/{response-vacuous-but-rewritten.json => response-vacuous-not-rewritten.json} (100%) rename booster/test/rpc-integration/test-vacuous/{response-vacuous-but-rewritten.kore-rpc-dev => response-vacuous-not-rewritten.kore-rpc-dev} (100%) rename booster/test/rpc-integration/test-vacuous/{state-vacuous-but-rewritten.execute => state-vacuous-not-rewritten.execute} (100%) diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md index 00c6823dc4..9464e3a6de 100644 --- a/booster/test/rpc-integration/test-vacuous/README.md +++ b/booster/test/rpc-integration/test-vacuous/README.md @@ -38,7 +38,7 @@ Rules `init` and `AC` introduce constraints on this variable: _Expected:_ - The rewrite is stuck with `dN \and...(contradiction)` - The result is simplified and discovered to be `vacuous` (with state `d`). -1) _vacuous-but-rewritten_ +1) _vacuous-not-rewritten_ _Input:_ - `execute` request with initial state `bN \and N diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.json similarity index 100% rename from booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json rename to booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.json diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.kore-rpc-dev b/booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.kore-rpc-dev similarity index 100% rename from booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.kore-rpc-dev rename to booster/test/rpc-integration/test-vacuous/response-vacuous-not-rewritten.kore-rpc-dev diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute similarity index 100% rename from booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute rename to booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute