From 0f3148308108446f7b202bb980accf4839e9c7f2 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 21 May 2024 18:26:48 +0200 Subject: [PATCH] RPC trace cleanup: remove simplification logs (#3880) Fixes https://github.com/runtimeverification/haskell-backend/issues/3871 Note that removing the simplification log request parameters and the simplification log entries form the response is same, because `pyk` is already modified to not recognize them, see: - the `LogEntry` [type](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L543) - the parameters for [execute](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1003), [simplify](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1049) and [implies](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1030) request But even considering that, we should run `pyk`'s integration tests before merging. --- booster/library/Booster/Definition/Ceil.hs | 2 +- booster/library/Booster/JsonRpc.hs | 213 ++---------------- .../library/Booster/Pattern/ApplyEquations.hs | 51 +---- booster/library/Booster/Pattern/Rewrite.hs | 32 +-- booster/tools/booster/Proxy.hs | 10 +- .../Test/Booster/Pattern/ApplyEquations.hs | 10 +- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 6 - kore/src/Kore/JsonRpc.hs | 102 +++------ 8 files changed, 71 insertions(+), 355 deletions(-) diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs index 8ce401238a..c13a8356fd 100644 --- a/booster/library/Booster/Definition/Ceil.hs +++ b/booster/library/Booster/Definition/Ceil.hs @@ -101,7 +101,7 @@ computeCeilRule :: computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes} | null computedAttributes.notPreservesDefinednessReasons = pure Nothing | otherwise = do - (res, _) <- runEquationT (Flag False) def mllvm Nothing mempty $ do + (res, _) <- runEquationT def mllvm Nothing mempty $ do lhsCeils <- Set.fromList <$> computeCeil lhs requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires) let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 6d1a7f8dea..dc514961e2 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -24,7 +24,6 @@ import Control.Monad.Logger.CallStack qualified as Log import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT) import Crypto.Hash (SHA256 (..), hashWith) import Data.Bifunctor (second) -import Data.Coerce (coerce) import Data.Foldable import Data.List (singleton) import Data.Map.Strict (Map) @@ -136,8 +135,6 @@ respond stateVar = (fromMaybe False) [ req.logSuccessfulRewrites , req.logFailedRewrites - , req.logSuccessfulSimplifications - , req.logFailedSimplifications , req.logFallbacks ] -- apply the given substitution before doing anything else @@ -225,31 +222,11 @@ respond stateVar = start <- liftIO $ getTime Monotonic let internalised = runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term - let mkEquationTraces - | coerce doTracing = - Just - . mapMaybe - ( mkLogEquationTrace - ( fromMaybe False req.logSuccessfulSimplifications - , fromMaybe False req.logFailedSimplifications - ) - ) - | otherwise = - const Nothing - mkTraces duration traceData + let mkTraces duration | Just True <- req.logTiming = - Just $ - [ProcessingTime (Just Booster) duration] - <> fromMaybe [] (mkEquationTraces traceData) + Just [ProcessingTime (Just Booster) duration] | otherwise = - mkEquationTraces traceData - doTracing = - Flag $ - any - (fromMaybe False) - [ req.logSuccessfulSimplifications - , req.logFailedSimplifications - ] + Nothing solver <- traverse (SMT.initSolver def) mSMTOptions @@ -281,17 +258,17 @@ respond stateVar = , constraints = Set.map (substituteInPredicate substitution) pat.constraints , ceilConditions = pat.ceilConditions } - ApplyEquations.evaluatePattern doTracing def mLlvmLibrary solver mempty substPat >>= \case + ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case (Right newPattern, _) -> do let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution tSort = externaliseSort (sortOfPattern newPattern) result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of [] -> term ps -> KoreJson.KJAnd tSort $ term : ps - pure $ Right (addHeader result, []) + pure $ Right (addHeader result) (Left ApplyEquations.SideConditionFalse{}, _) -> do let tSort = externaliseSort $ sortOfPattern pat - pure $ Right (addHeader $ KoreJson.KJBottom tSort, []) + pure $ Right (addHeader $ KoreJson.KJBottom tSort) (Left (ApplyEquations.EquationLoop _terms), _) -> pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" (Left other, _) -> @@ -301,7 +278,7 @@ respond stateVar = | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported -> pure $ Right - (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term), []) + (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term)) | otherwise -> do unless (null ps.unsupported) $ do withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do @@ -313,7 +290,6 @@ respond stateVar = let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates withContext "constraint" $ ApplyEquations.simplifyConstraints - doTracing def mLlvmLibrary solver @@ -330,7 +306,7 @@ respond stateVar = <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution) <> ps.unsupported - pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, []) + pure $ Right (addHeader $ Syntax.KJAnd predicateSort result) (Left something, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something whenJust solver SMT.closeSolver @@ -338,10 +314,10 @@ respond stateVar = let duration = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - mkSimplifyResponse state traceData = + mkSimplifyResponse state = RpcTypes.Simplify - RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData} - pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result) + RpcTypes.SimplifyResult{state, logs = mkTraces duration} + pure $ second mkSimplifyResponse result RpcTypes.GetModel req -> withModule req._module $ \case (_, _, Nothing) -> do Log.logErrorNS "booster" "get-model request, not supported without SMT solver" @@ -530,13 +506,12 @@ respond stateVar = MatchSuccess subst -> do let filteredConsequentPreds = Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints - doTracing = Flag False solver <- traverse (SMT.initSolver def) mSMTOptions if null filteredConsequentPreds then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst else - ApplyEquations.evaluateConstraints doTracing def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case + ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case (Right newPreds, _) -> if all (== Pattern.Predicate TrueBool) newPreds then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst @@ -729,7 +704,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c let abortRewriteLog = mkLogRewriteTrace (logSuccessfulRewrites, logFailedRewrites) - (logSuccessfulSimplifications, logFailedSimplifications) (RewriteStepFailed failure) in logs <|> abortRewriteLog , state = toExecState p originalSubstitution unsupported Nothing @@ -740,8 +714,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c where logSuccessfulRewrites = fromMaybe False req.logSuccessfulRewrites logFailedRewrites = fromMaybe False req.logFailedRewrites - logSuccessfulSimplifications = fromMaybe False req.logSuccessfulSimplifications - logFailedSimplifications = fromMaybe False req.logFailedSimplifications depth = RpcTypes.Depth d logs = @@ -750,7 +722,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c fmap ( mkLogRewriteTrace (logSuccessfulRewrites, logFailedRewrites) - (logSuccessfulSimplifications, logFailedSimplifications) ) traces timingLog = @@ -779,105 +750,12 @@ toExecState pat sub unsupported muid = | null unsupported = id | otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported)) -mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace () -> Maybe LogEntry -mkLogEquationTrace - (logSuccessfulSimplifications, logFailedSimplifications) = \case - ApplyEquations.EquationApplied _subjectTerm metadata _rewritten -> - if logSuccessfulSimplifications - then - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = - Success - { rewrittenTerm = Nothing - , substitution = Nothing - , ruleId = fromMaybe "UNKNOWN" _ruleId - } - } - else Nothing - where - originalTerm = Nothing - originalTermIndex = Nothing - origin = Booster - _ruleId = fmap getUniqueId metadata.ruleId - ApplyEquations.EquationNotApplied _subjectTerm metadata result -> - case result of - ApplyEquations.FailedMatch{} - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Failed match", _ruleId} - } - ApplyEquations.IndeterminateMatch - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Indeterminate match", _ruleId} - } - ApplyEquations.IndeterminateCondition{} - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Indeterminate side-condition", _ruleId} - } - ApplyEquations.ConditionFalse{} - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Side-condition is false", _ruleId} - } - ApplyEquations.RuleNotPreservingDefinedness - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "The equation does not preserve definedness", _ruleId} - } - ApplyEquations.MatchConstraintViolated _ varName - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = - Failure - { reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName - , _ruleId - } - } - _ -> Nothing - where - originalTerm = Nothing - originalTermIndex = Nothing - origin = Booster - _ruleId = fmap getUniqueId metadata.ruleId - mkLogRewriteTrace :: - (Bool, Bool) -> (Bool, Bool) -> RewriteTrace () -> Maybe [LogEntry] mkLogRewriteTrace - (logSuccessfulRewrites, logFailedRewrites) - equationLogOpts@(logSuccessfulSimplifications, logFailedSimplifications) = + (logSuccessfulRewrites, logFailedRewrites) = \case RewriteSingleStep _ uid _ _res | logSuccessfulRewrites -> @@ -928,68 +806,5 @@ mkLogRewriteTrace } , origin = Booster } - RewriteSimplified equationTraces Nothing - | logSuccessfulSimplifications || logFailedSimplifications -> - mapM (mkLogEquationTrace equationLogOpts) equationTraces - | otherwise -> Just [] - RewriteSimplified equationTraces (Just failure) - | logFailedSimplifications -> do - let final = singleton $ case failure of - ApplyEquations.IndexIsNone trm -> - Simplification - { originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "No index found for term", _ruleId = Nothing} - } - ApplyEquations.TooManyIterations i _ _ -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "Reached iteration depth limit " <> pack (show i), _ruleId = Nothing} - } - ApplyEquations.EquationLoop _ -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "Loop detected", _ruleId = Nothing} - } - ApplyEquations.TooManyRecursions stk -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = - Failure - { reason = - "Reached recursion limit of " - <> pack (show $ length stk) - , _ruleId = Nothing - } - } - ApplyEquations.InternalError err -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "Internal error: " <> err, _ruleId = Nothing} - } - ApplyEquations.SideConditionFalse _predicate -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "Side conditions false", _ruleId = Nothing} - } - ApplyEquations.UndefinedTerm _t _err -> - Simplification - { originalTerm = Nothing - , originalTermIndex = Nothing - , origin = Booster - , result = Failure{reason = "Undefined term found", _ruleId = Nothing} - } - (<> final) <$> mapM (mkLogEquationTrace equationLogOpts) equationTraces - | otherwise -> Just [] + RewriteSimplified{} -> Just [] _ -> Nothing diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 8ba046b68f..3c1b4cc876 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -15,10 +15,6 @@ module Booster.Pattern.ApplyEquations ( getConfig, EquationPreference (..), EquationFailure (..), - EquationTrace (..), - pattern CollectEquationTraces, - pattern NoCollectEquationTraces, - eraseStates, EquationMetadata (..), ApplyEquationResult (..), ApplyEquationFailure (..), @@ -85,7 +81,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter (renderDefault, renderOneLineText) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) -import Booster.Util (Bound (..), Flag (..)) +import Booster.Util (Bound (..)) import Kore.JsonRpc.Types.Log qualified as KoreRpcLog import Kore.Util (showHashHex) @@ -152,18 +148,11 @@ data EquationConfig = EquationConfig { definition :: KoreDefinition , llvmApi :: Maybe LLVM.API , smtSolver :: Maybe SMT.SMTContext - , doTracing :: Flag "CollectEquationTraces" , maxRecursion :: Bound "Recursion" , maxIterations :: Bound "Iterations" , logger :: Logger LogMessage } -pattern CollectEquationTraces :: Flag "CollectEquationTraces" -pattern CollectEquationTraces = Flag True - -pattern NoCollectEquationTraces :: Flag "CollectEquationTraces" -pattern NoCollectEquationTraces = Flag False - data EquationState = EquationState { termStack :: Seq Term , recursionStack :: [Term] @@ -197,15 +186,6 @@ data EquationTrace term | EquationNotApplied term EquationMetadata ApplyEquationFailure deriving stock (Eq, Show) -{- | For the given equation trace, construct a new one, - removing the heavy-weight information (the states), - but keeping the meta-data (rule labels). --} -eraseStates :: EquationTrace Term -> EquationTrace () -eraseStates = \case - EquationApplied _ metadata _ -> EquationApplied () metadata () - EquationNotApplied _ metadata failureInfo -> EquationNotApplied () metadata failureInfo - instance Pretty (EquationTrace Term) where pretty (EquationApplied subjectTerm metadata rewritten) = vsep @@ -415,14 +395,13 @@ data EquationPreference = PreferFunctions | PreferSimplifications runEquationT :: LoggerMIO io => - Flag "CollectEquationTraces" -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> SimplifierCache -> EquationT io a -> io (Either EquationFailure a, SimplifierCache) -runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do +runEquationT definition llvmApi smtSolver sCache (EquationT m) = do globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions logger <- getLogger (res, endState) <- @@ -434,7 +413,6 @@ runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do { definition , llvmApi , smtSolver - , doTracing , maxIterations = globalEquationOptions.maxIterations , maxRecursion = globalEquationOptions.maxRecursion , logger @@ -537,15 +515,14 @@ llvmSimplify term = do evaluateTerm :: LoggerMIO io => MonadLoggerIO io => - Flag "CollectEquationTraces" -> Direction -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> Term -> io (Either EquationFailure Term, SimplifierCache) -evaluateTerm doTracing direction def llvmApi smtSolver = - runEquationT doTracing def llvmApi smtSolver mempty +evaluateTerm direction def llvmApi smtSolver = + runEquationT def llvmApi smtSolver mempty . evaluateTerm' direction -- version for internal nested evaluation @@ -562,15 +539,14 @@ evaluateTerm' direction = iterateEquations direction PreferFunctions evaluatePattern :: LoggerMIO io => MonadLoggerIO io => - Flag "CollectEquationTraces" -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> SimplifierCache -> Pattern -> io (Either EquationFailure Pattern, SimplifierCache) -evaluatePattern doTracing def mLlvmLibrary smtSolver cache = - runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluatePattern' +evaluatePattern def mLlvmLibrary smtSolver cache = + runEquationT def mLlvmLibrary smtSolver cache . evaluatePattern' -- version for internal nested evaluation evaluatePattern' :: @@ -600,15 +576,14 @@ simplifyAssumedPredicate p = do evaluateConstraints :: LoggerMIO io => MonadLoggerIO io => - Flag "CollectEquationTraces" -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> SimplifierCache -> Set Predicate -> io (Either EquationFailure (Set Predicate), SimplifierCache) -evaluateConstraints doTracing def mLlvmLibrary smtSolver cache = - runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints' +evaluateConstraints def mLlvmLibrary smtSolver cache = + runEquationT def mLlvmLibrary smtSolver cache . evaluateConstraints' evaluateConstraints' :: LoggerMIO io => @@ -1084,28 +1059,26 @@ applyEquation term rule = withRuleContext rule $ fmap (either Failure Success) $ simplifyConstraint :: LoggerMIO io => MonadLoggerIO io => - Flag "CollectEquationTraces" -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> SimplifierCache -> Predicate -> io (Either EquationFailure Predicate, SimplifierCache) -simplifyConstraint doTracing def mbApi mbSMT cache (Predicate p) = do - runEquationT doTracing def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p +simplifyConstraint def mbApi mbSMT cache (Predicate p) = do + runEquationT def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p simplifyConstraints :: LoggerMIO io => MonadLoggerIO io => - Flag "CollectEquationTraces" -> KoreDefinition -> Maybe LLVM.API -> Maybe SMT.SMTContext -> SimplifierCache -> [Predicate] -> io (Either EquationFailure [Predicate], SimplifierCache) -simplifyConstraints doTracing def mbApi mbSMT cache ps = - runEquationT doTracing def mbApi mbSMT cache $ +simplifyConstraints def mbApi mbSMT cache ps = + runEquationT def mbApi mbSMT cache $ concatMap splitAndBools <$> mapM ((coerce <$>) . simplifyConstraint' True . coerce) ps diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 39fdf5228a..433dc640c3 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -57,12 +57,10 @@ import Booster.Log ( ) import Booster.Pattern.ApplyEquations ( EquationFailure (..), - EquationTrace, SimplifierCache, evaluatePattern, simplifyConstraint, ) -import Booster.Pattern.ApplyEquations qualified as ApplyEquations import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index (TermIndex (..), kCellTermIndex) @@ -97,9 +95,6 @@ instance MonadLoggerIO io => LoggerMIO (RewriteT io) where getLogger = RewriteT $ asks logger withLogger modL (RewriteT m) = RewriteT $ withReaderT (\cfg@RewriteConfig{logger} -> cfg{logger = modL logger}) m -castDoTracingFlag :: Flag "CollectRewriteTraces" -> Flag "CollectEquationTraces" -castDoTracingFlag = coerce - pattern CollectRewriteTraces :: Flag "CollectRewriteTraces" pattern CollectRewriteTraces = Flag True @@ -439,11 +434,11 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu Predicate -> RewriteRuleAppT (RewriteT io) (Maybe a) checkConstraint onUnclear onBottom p = do - RewriteConfig{definition, llvmApi, smtSolver, doTracing} <- lift $ RewriteT ask + RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask oldCache <- lift . RewriteT . lift $ get (simplified, cache) <- withContext "constraint" $ - simplifyConstraint (castDoTracingFlag doTracing) definition llvmApi smtSolver oldCache p + simplifyConstraint definition llvmApi smtSolver oldCache p -- update cache lift . RewriteT . lift . modify $ const cache -- TODO should we keep the traces? Or only on success? @@ -547,11 +542,7 @@ data RewriteTrace pat | -- | attempted rewrite failed RewriteStepFailed (RewriteFailed "Rewrite") | -- | Applied simplification to the pattern - RewriteSimplified [EquationTrace (TracePayload pat)] (Maybe EquationFailure) - -type family TracePayload pat where - TracePayload Pattern = Term - TracePayload () = () + RewriteSimplified (Maybe EquationFailure) {- | For the given rewrite trace, construct a new one, removing the heavy-weight information (the states), @@ -562,8 +553,7 @@ eraseStates = \case RewriteSingleStep rule_label mUniqueId _preState _postState -> RewriteSingleStep rule_label mUniqueId () () RewriteBranchingStep _state branchMetadata -> RewriteBranchingStep () branchMetadata RewriteStepFailed failureInfo -> RewriteStepFailed failureInfo - RewriteSimplified equationTraces mbEquationFailure -> - RewriteSimplified (map ApplyEquations.eraseStates equationTraces) mbEquationFailure + RewriteSimplified mbEquationFailure -> RewriteSimplified mbEquationFailure instance Pretty (RewriteTrace Pattern) where pretty = \case @@ -741,25 +731,25 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL st <- get let cache = st.simplifierCache smt = st.smtSolver - evaluatePattern (castDoTracingFlag doTracing) def mLlvmLibrary smt cache p >>= \(res, newCache) -> do + evaluatePattern def mLlvmLibrary smt cache p >>= \(res, newCache) -> do updateCache newCache case res of Right newPattern -> do - emitRewriteTrace $ RewriteSimplified [] Nothing + emitRewriteTrace $ RewriteSimplified Nothing pure $ Just newPattern Left r@(SideConditionFalse _p) -> do logSimplify "A side condition was found to be false, pruning" - emitRewriteTrace $ RewriteSimplified [] (Just r) + emitRewriteTrace $ RewriteSimplified (Just r) pure Nothing Left r@UndefinedTerm{} -> do logSimplify "Term is undefined, pruning" - emitRewriteTrace $ RewriteSimplified [] (Just r) + emitRewriteTrace $ RewriteSimplified (Just r) pure Nothing Left r@(TooManyIterations n _start _result) -> do logSimplify $ "Unable to simplify in " <> Text.pack (show n) <> " iterations, returning original" -- warning has been printed inside ApplyEquation.evaluatePattern - emitRewriteTrace $ RewriteSimplified [] (Just r) + emitRewriteTrace $ RewriteSimplified (Just r) -- NB start/result in this error are terms and might come -- from simplifying one of the constraints. Therefore, the -- original pattern must be returned. @@ -773,11 +763,11 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL <> prettyText l <> ": \n" <> Text.unlines (map (prettyText . fst) termDiffs) - emitRewriteTrace $ RewriteSimplified [] (Just r) + emitRewriteTrace $ RewriteSimplified (Just r) pure $ Just p Left other -> do logError $ "Simplification error during rewrite: " <> (Text.pack . constructorName $ other) - emitRewriteTrace $ RewriteSimplified [] (Just other) + emitRewriteTrace $ RewriteSimplified (Just other) pure $ Just p -- Results may change when simplification prunes a false side diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 447547f405..b1ef6fb345 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -90,9 +90,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re | otherwise -> let logSettings = LogSettings - { logSuccessfulSimplifications = execReq.logSuccessfulSimplifications - , logFailedSimplifications = execReq.logFailedSimplifications - , logSuccessfulRewrites = execReq.logSuccessfulRewrites + { logSuccessfulRewrites = execReq.logSuccessfulRewrites , logFailedRewrites = execReq.logFailedRewrites , logFallbacks = execReq.logFallbacks , logTiming = execReq.logTiming @@ -550,8 +548,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re SimplifyRequest { state = execStateToKoreJson state , _module = mbModule - , logSuccessfulSimplifications = Nothing - , logFailedSimplifications = Nothing , logTiming } @@ -612,9 +608,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re } data LogSettings = LogSettings - { logSuccessfulSimplifications :: Maybe Bool - , logFailedSimplifications :: Maybe Bool - , logSuccessfulRewrites :: Maybe Bool + { logSuccessfulRewrites :: Maybe Bool , logFailedRewrites :: Maybe Bool , logFallbacks :: Maybe Bool , logTiming :: Maybe Bool diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index 614386d42e..3c44f16200 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -98,7 +98,7 @@ test_evaluateFunction = unsafePerformIO . runNoLoggingT . (fst <$>) - . evaluateTerm NoCollectEquationTraces direction funDef Nothing Nothing + . evaluateTerm direction funDef Nothing Nothing isTooManyIterations (Left (TooManyIterations _n _ _)) = pure () isTooManyIterations (Left err) = assertFailure $ "Unexpected error " <> show err @@ -129,7 +129,7 @@ test_simplify = unsafePerformIO . runNoLoggingT . (fst <$>) - . evaluateTerm NoCollectEquationTraces direction simplDef Nothing Nothing + . evaluateTerm direction simplDef Nothing Nothing a = var "A" someSort test_simplifyPattern :: TestTree @@ -159,7 +159,7 @@ test_simplifyPattern = unsafePerformIO . runNoLoggingT . (fst <$>) - . evaluatePattern NoCollectEquationTraces simplDef Nothing Nothing mempty + . evaluatePattern simplDef Nothing Nothing mempty a = var "A" someSort test_simplifyConstraint :: TestTree @@ -229,7 +229,7 @@ test_simplifyConstraint = unsafePerformIO . runNoLoggingT . (fst <$>) - . simplifyConstraint NoCollectEquationTraces testDefinition Nothing Nothing mempty + . simplifyConstraint testDefinition Nothing Nothing mempty test_errors :: TestTree test_errors = @@ -242,7 +242,7 @@ test_errors = loopTerms = [f $ app con1 [a], f $ app con2 [a], f $ app con3 [a, a], f $ app con1 [a]] isLoop loopTerms . unsafePerformIO . runNoLoggingT $ - fst <$> evaluateTerm NoCollectEquationTraces TopDown loopDef Nothing Nothing subj + fst <$> evaluateTerm TopDown loopDef Nothing Nothing subj ] where isLoop ts (Left (EquationLoop ts')) = ts @?= ts' diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index eb262578af..4da0f57b21 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -39,8 +39,6 @@ data ExecuteRequest = ExecuteRequest , assumeStateDefined :: !(Maybe Bool) , logSuccessfulRewrites :: !(Maybe Bool) , logFailedRewrites :: !(Maybe Bool) - , logSuccessfulSimplifications :: !(Maybe Bool) - , logFailedSimplifications :: !(Maybe Bool) , logFallbacks :: !(Maybe Bool) , logTiming :: !(Maybe Bool) } @@ -54,8 +52,6 @@ data ImpliesRequest = ImpliesRequest , consequent :: !KoreJson , _module :: !(Maybe Text) , assumeDefined :: !(Maybe Bool) - , logSuccessfulSimplifications :: !(Maybe Bool) - , logFailedSimplifications :: !(Maybe Bool) , logTiming :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) @@ -66,8 +62,6 @@ data ImpliesRequest = ImpliesRequest data SimplifyRequest = SimplifyRequest { state :: KoreJson , _module :: !(Maybe Text) - , logSuccessfulSimplifications :: !(Maybe Bool) - , logFailedSimplifications :: !(Maybe Bool) , logTiming :: !(Maybe Bool) } deriving stock (Generic, Show, Eq) diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index e0e6370e4b..b5e40fd034 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -22,7 +22,6 @@ import Data.Limit (Limit (..)) import Data.List.Extra (mconcatMap) import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map -import Data.Sequence as Seq (Seq, empty) import Data.Set qualified as Set import Data.String (fromString) import Data.Text (Text, pack) @@ -84,7 +83,6 @@ import Kore.Rewrite.RewriteStep (EnableAssumeInitialDefined (..)) import Kore.Rewrite.RewritingVariable ( RewritingVariableName, getRewritingPattern, - getRewritingTerm, getRewritingVariable, isSomeConfigVariable, isSomeEquationVariable, @@ -97,9 +95,9 @@ import Kore.Rewrite.Timeout ( EnableMovingAverage (..), StepTimeout (..), ) -import Kore.Simplify.API (evalSimplifier, evalSimplifierLogged) +import Kore.Simplify.API (evalSimplifier) import Kore.Simplify.Pattern qualified as Pattern -import Kore.Simplify.Simplify (Simplifier, SimplifierTrace (..)) +import Kore.Simplify.Simplify (Simplifier) import Kore.Syntax (VariableName) import Kore.Syntax.Definition (Definition (..)) import Kore.Syntax.Json qualified @@ -143,7 +141,6 @@ respond serverState moduleName runSMT = , assumeStateDefined , stepTimeout , logSuccessfulRewrites - , logSuccessfulSimplifications , logTiming } -> withMainModule (coerce _module) $ \serializedModule lemmas -> do start <- liftIO $ getTime Monotonic @@ -157,8 +154,7 @@ respond serverState moduleName runSMT = map pack errorContext ] Right verifiedPattern -> do - let tracingEnabled = - fromMaybe False logSuccessfulRewrites || fromMaybe False logSuccessfulSimplifications + let tracingEnabled = fromMaybe False logSuccessfulRewrites traversalResult <- liftIO ( runSMT (Exec.metadataTools serializedModule) lemmas $ @@ -207,25 +203,10 @@ respond serverState moduleName runSMT = in either unLabel getUniqueId <$> Set.lookupMin (requestSet `Set.intersection` ruleSet) mkLogs mbDuration rules | isJust mbDuration - || fromMaybe False logSuccessfulRewrites - || fromMaybe False logSuccessfulSimplifications = + || fromMaybe False logSuccessfulRewrites = Just . concat $ maybe [] (\t -> [ProcessingTime (Just KoreRpc) t]) mbDuration - : [ [ Simplification - { originalTerm = Just $ PatternJson.fromTermLike $ getRewritingTerm originalTerm - , originalTermIndex = Nothing - , result = - Success - { rewrittenTerm = Just $ PatternJson.fromTermLike $ getRewritingTerm $ Pattern.term rewrittenTerm - , substitution = Nothing - , ruleId = fromMaybe "UNKNOWN" $ getUniqueId equationId - } - , origin = KoreRpc - } - | fromMaybe False logSuccessfulSimplifications - , SimplifierTrace{originalTerm, rewrittenTerm, equationId} <- toList simplifications - ] - ++ [ Rewrite + : [ [ Rewrite { result = Success { rewrittenTerm = Nothing @@ -234,9 +215,9 @@ respond serverState moduleName runSMT = } , origin = KoreRpc } - | fromMaybe False logSuccessfulRewrites - ] - | Exec.RuleTrace{simplifications, ruleId} <- toList rules + | fromMaybe False logSuccessfulRewrites + ] + | Exec.RuleTrace{ruleId} <- toList rules ] | otherwise = Nothing @@ -417,7 +398,7 @@ respond serverState moduleName runSMT = a ||| b = \v -> a v || b v -- Step StepRequest{} -> pure $ Right $ Step $ StepResult [] - Implies ImpliesRequest{antecedent, consequent, _module, logSuccessfulSimplifications, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do + Implies ImpliesRequest{antecedent, consequent, _module, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do start <- liftIO $ getTime Monotonic case PatternVerifier.runPatternVerifier (verifierContext serializedModule) verify of Left Error{errorError, errorContext} -> @@ -437,18 +418,17 @@ respond serverState moduleName runSMT = mkRewritingTerm consVerified rightPatt = Pattern.parsePatternFromTermLike consWOExistentials - (logs, result) <- + result <- liftIO . runSMT (Exec.metadataTools serializedModule) lemmas . Log.logWhile (Log.DebugContext "kore") . Log.logWhile (Log.DebugContext "implies") - . (evalInSimplifierContext (fromMaybe False logSuccessfulSimplifications) serializedModule) + . evalInSimplifierContext serializedModule . runExceptT $ Claim.checkSimpleImplication leftPatt rightPatt existentialVars - let simplLogs = mkSimplifierLogs logSuccessfulSimplifications logs stop <- liftIO $ getTime Monotonic let timeLog = ProcessingTime @@ -456,8 +436,8 @@ respond serverState moduleName runSMT = (fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9) allLogs = if (fromMaybe False logTiming) - then maybe (Just [timeLog]) (Just . (timeLog :)) simplLogs - else simplLogs + then Just [timeLog] + else Nothing pure $ buildResult allLogs sort result where verify = do @@ -506,7 +486,7 @@ respond serverState moduleName runSMT = in ImpliesResult jsonTerm False (Just jsonCond) logs Claim.NotImpliedStuck Nothing -> ImpliesResult jsonTerm False (Just . renderCond sort $ Condition.bottom) logs - Simplify SimplifyRequest{state, _module, logSuccessfulSimplifications, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do + Simplify SimplifyRequest{state, _module, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do start <- liftIO $ getTime Monotonic case verifyIn serializedModule state of Left Error{errorError, errorContext} -> @@ -522,15 +502,14 @@ respond serverState moduleName runSMT = mkRewritingPattern $ Pattern.parsePatternFromTermLike stateVerified sort = TermLike.termLikeSort stateVerified - (logs, result) <- + result <- liftIO . runSMT (Exec.metadataTools serializedModule) lemmas . Log.logWhile (Log.DebugContext "kore") . Log.logWhile (Log.DebugContext "simplify") - . evalInSimplifierContext (fromMaybe False logSuccessfulSimplifications) serializedModule + . evalInSimplifierContext serializedModule $ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt - let simplLogs = mkSimplifierLogs logSuccessfulSimplifications logs stop <- liftIO $ getTime Monotonic let timeLog = ProcessingTime @@ -538,8 +517,8 @@ respond serverState moduleName runSMT = (fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9) allLogs = if (fromMaybe False logTiming) - then maybe (Just [timeLog]) (Just . (timeLog :)) simplLogs - else simplLogs + then Just [timeLog] + else Nothing pure $ Right $ Simplify @@ -732,51 +711,22 @@ respond serverState moduleName runSMT = PatternVerifier.verifyStandalonePattern Nothing $ PatternJson.toParsedPattern (PatternJson.term state) - mkSimplifierLogs :: Maybe Bool -> Seq SimplifierTrace -> Maybe [LogEntry] - mkSimplifierLogs Nothing _ = Nothing - mkSimplifierLogs (Just False) _ = Nothing - mkSimplifierLogs (Just True) logs = - Just - [ Simplification - { originalTerm = Just $ PatternJson.fromTermLike $ getRewritingTerm originalTerm - , originalTermIndex = Nothing - , result = - Success - { rewrittenTerm = Just $ PatternJson.fromTermLike $ getRewritingTerm $ Pattern.term rewrittenTerm - , substitution = Nothing - , ruleId = fromMaybe "UNKNOWN" $ getUniqueId equationId - } - , origin = KoreRpc - } - | SimplifierTrace{originalTerm, rewrittenTerm, equationId} <- toList logs - ] - evalInSimplifierContext :: - Bool -> Exec.SerializedModule -> Simplifier a -> SMT.SMT (Seq SimplifierTrace, a) + Exec.SerializedModule -> Simplifier a -> SMT.SMT a evalInSimplifierContext - doTracing Exec.SerializedModule { sortGraph , overloadGraph , metadataTools , verifiedModule , equations - } - | doTracing = - evalSimplifierLogged - verifiedModule - sortGraph - overloadGraph - metadataTools - equations - | otherwise = - fmap (Seq.empty,) - . evalSimplifier - verifiedModule - sortGraph - overloadGraph - metadataTools - equations + } = + evalSimplifier + verifiedModule + sortGraph + overloadGraph + metadataTools + equations data ServerState = ServerState { serializedModules :: Map.Map ModuleName SerializedDefinition