Skip to content

Commit 241b566

Browse files
geo2ageo2a
committed
Remove handling of simplification RPC traces
1 parent a15cbe1 commit 241b566

File tree

4 files changed

+40
-285
lines changed

4 files changed

+40
-285
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 12 additions & 195 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ import Control.Monad.Logger.CallStack qualified as Log
2424
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
2525
import Crypto.Hash (SHA256 (..), hashWith)
2626
import Data.Bifunctor (second)
27-
import Data.Coerce (coerce)
2827
import Data.Foldable
2928
import Data.List (singleton)
3029
import Data.Map.Strict (Map)
@@ -135,8 +134,6 @@ respond stateVar =
135134
(fromMaybe False)
136135
[ req.logSuccessfulRewrites
137136
, req.logFailedRewrites
138-
, req.logSuccessfulSimplifications
139-
, req.logFailedSimplifications
140137
, req.logFallbacks
141138
]
142139
-- apply the given substitution before doing anything else
@@ -224,31 +221,11 @@ respond stateVar =
224221
start <- liftIO $ getTime Monotonic
225222
let internalised =
226223
runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
227-
let mkEquationTraces
228-
| coerce doTracing =
229-
Just
230-
. mapMaybe
231-
( mkLogEquationTrace
232-
( fromMaybe False req.logSuccessfulSimplifications
233-
, fromMaybe False req.logFailedSimplifications
234-
)
235-
)
236-
| otherwise =
237-
const Nothing
238-
mkTraces duration traceData
224+
let mkTraces duration
239225
| Just True <- req.logTiming =
240-
Just $
241-
[ProcessingTime (Just Booster) duration]
242-
<> fromMaybe [] (mkEquationTraces traceData)
226+
Just [ProcessingTime (Just Booster) duration]
243227
| otherwise =
244-
mkEquationTraces traceData
245-
doTracing =
246-
Flag $
247-
any
248-
(fromMaybe False)
249-
[ req.logSuccessfulSimplifications
250-
, req.logFailedSimplifications
251-
]
228+
Nothing
252229

253230
solver <- traverse (SMT.initSolver def) mSMTOptions
254231

@@ -287,10 +264,10 @@ respond stateVar =
287264
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
288265
[] -> term
289266
ps -> KoreJson.KJAnd tSort $ term : ps
290-
pure $ Right (addHeader result, [])
267+
pure $ Right (addHeader result)
291268
(Left ApplyEquations.SideConditionFalse{}, _) -> do
292269
let tSort = externaliseSort $ sortOfPattern pat
293-
pure $ Right (addHeader $ KoreJson.KJBottom tSort, [])
270+
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
294271
(Left (ApplyEquations.EquationLoop _terms), _) ->
295272
pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
296273
(Left other, _) ->
@@ -300,7 +277,7 @@ respond stateVar =
300277
| null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported ->
301278
pure $
302279
Right
303-
(addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term), [])
280+
(addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term))
304281
| otherwise -> do
305282
Log.logInfoNS "booster" "Simplifying predicates"
306283
unless (null ps.unsupported) $ do
@@ -329,18 +306,18 @@ respond stateVar =
329306
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
330307
<> ps.unsupported
331308

332-
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
309+
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
333310
(Left something, _) ->
334311
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
335312
whenJust solver SMT.closeSolver
336313
stop <- liftIO $ getTime Monotonic
337314

338315
let duration =
339316
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
340-
mkSimplifyResponse state traceData =
317+
mkSimplifyResponse state =
341318
RpcTypes.Simplify
342-
RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData}
343-
pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result)
319+
RpcTypes.SimplifyResult{state, logs = mkTraces duration}
320+
pure $ second mkSimplifyResponse result
344321
RpcTypes.GetModel req -> withModule req._module $ \case
345322
(_, _, Nothing) -> do
346323
Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
@@ -727,7 +704,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
727704
let abortRewriteLog =
728705
mkLogRewriteTrace
729706
(logSuccessfulRewrites, logFailedRewrites)
730-
(logSuccessfulSimplifications, logFailedSimplifications)
731707
(RewriteStepFailed failure)
732708
in logs <|> abortRewriteLog
733709
, state = toExecState p originalSubstitution unsupported Nothing
@@ -738,8 +714,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
738714
where
739715
logSuccessfulRewrites = fromMaybe False req.logSuccessfulRewrites
740716
logFailedRewrites = fromMaybe False req.logFailedRewrites
741-
logSuccessfulSimplifications = fromMaybe False req.logSuccessfulSimplifications
742-
logFailedSimplifications = fromMaybe False req.logFailedSimplifications
743717
depth = RpcTypes.Depth d
744718

745719
logs =
@@ -748,7 +722,6 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c
748722
fmap
749723
( mkLogRewriteTrace
750724
(logSuccessfulRewrites, logFailedRewrites)
751-
(logSuccessfulSimplifications, logFailedSimplifications)
752725
)
753726
traces
754727
timingLog =
@@ -777,105 +750,12 @@ toExecState pat sub unsupported muid =
777750
| null unsupported = id
778751
| otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))
779752

780-
mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace () -> Maybe LogEntry
781-
mkLogEquationTrace
782-
(logSuccessfulSimplifications, logFailedSimplifications) = \case
783-
ApplyEquations.EquationApplied _subjectTerm metadata _rewritten ->
784-
if logSuccessfulSimplifications
785-
then
786-
Just $
787-
Simplification
788-
{ originalTerm
789-
, originalTermIndex
790-
, origin
791-
, result =
792-
Success
793-
{ rewrittenTerm = Nothing
794-
, substitution = Nothing
795-
, ruleId = fromMaybe "UNKNOWN" _ruleId
796-
}
797-
}
798-
else Nothing
799-
where
800-
originalTerm = Nothing
801-
originalTermIndex = Nothing
802-
origin = Booster
803-
_ruleId = fmap getUniqueId metadata.ruleId
804-
ApplyEquations.EquationNotApplied _subjectTerm metadata result ->
805-
case result of
806-
ApplyEquations.FailedMatch{}
807-
| logFailedSimplifications ->
808-
Just $
809-
Simplification
810-
{ originalTerm
811-
, originalTermIndex
812-
, origin
813-
, result = Failure{reason = "Failed match", _ruleId}
814-
}
815-
ApplyEquations.IndeterminateMatch
816-
| logFailedSimplifications ->
817-
Just $
818-
Simplification
819-
{ originalTerm
820-
, originalTermIndex
821-
, origin
822-
, result = Failure{reason = "Indeterminate match", _ruleId}
823-
}
824-
ApplyEquations.IndeterminateCondition{}
825-
| logFailedSimplifications ->
826-
Just $
827-
Simplification
828-
{ originalTerm
829-
, originalTermIndex
830-
, origin
831-
, result = Failure{reason = "Indeterminate side-condition", _ruleId}
832-
}
833-
ApplyEquations.ConditionFalse{}
834-
| logFailedSimplifications ->
835-
Just $
836-
Simplification
837-
{ originalTerm
838-
, originalTermIndex
839-
, origin
840-
, result = Failure{reason = "Side-condition is false", _ruleId}
841-
}
842-
ApplyEquations.RuleNotPreservingDefinedness
843-
| logFailedSimplifications ->
844-
Just $
845-
Simplification
846-
{ originalTerm
847-
, originalTermIndex
848-
, origin
849-
, result = Failure{reason = "The equation does not preserve definedness", _ruleId}
850-
}
851-
ApplyEquations.MatchConstraintViolated _ varName
852-
| logFailedSimplifications ->
853-
Just $
854-
Simplification
855-
{ originalTerm
856-
, originalTermIndex
857-
, origin
858-
, result =
859-
Failure
860-
{ reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName
861-
, _ruleId
862-
}
863-
}
864-
_ -> Nothing
865-
where
866-
originalTerm = Nothing
867-
originalTermIndex = Nothing
868-
origin = Booster
869-
_ruleId = fmap getUniqueId metadata.ruleId
870-
871753
mkLogRewriteTrace ::
872-
(Bool, Bool) ->
873754
(Bool, Bool) ->
874755
RewriteTrace () ->
875756
Maybe [LogEntry]
876757
mkLogRewriteTrace
877-
(logSuccessfulRewrites, logFailedRewrites)
878-
equationLogOpts@(logSuccessfulSimplifications, logFailedSimplifications) =
758+
(logSuccessfulRewrites, logFailedRewrites) =
879759
\case
880760
RewriteSingleStep _ uid _ _res
881761
| logSuccessfulRewrites ->
@@ -926,68 +806,5 @@ mkLogRewriteTrace
926806
}
927807
, origin = Booster
928808
}
929-
RewriteSimplified equationTraces Nothing
930-
| logSuccessfulSimplifications || logFailedSimplifications ->
931-
mapM (mkLogEquationTrace equationLogOpts) equationTraces
932-
| otherwise -> Just []
933-
RewriteSimplified equationTraces (Just failure)
934-
| logFailedSimplifications -> do
935-
let final = singleton $ case failure of
936-
ApplyEquations.IndexIsNone trm ->
937-
Simplification
938-
{ originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty mempty Nothing
939-
, originalTermIndex = Nothing
940-
, origin = Booster
941-
, result = Failure{reason = "No index found for term", _ruleId = Nothing}
942-
}
943-
ApplyEquations.TooManyIterations i _ _ ->
944-
Simplification
945-
{ originalTerm = Nothing
946-
, originalTermIndex = Nothing
947-
, origin = Booster
948-
, result = Failure{reason = "Reached iteration depth limit " <> pack (show i), _ruleId = Nothing}
949-
}
950-
ApplyEquations.EquationLoop _ ->
951-
Simplification
952-
{ originalTerm = Nothing
953-
, originalTermIndex = Nothing
954-
, origin = Booster
955-
, result = Failure{reason = "Loop detected", _ruleId = Nothing}
956-
}
957-
ApplyEquations.TooManyRecursions stk ->
958-
Simplification
959-
{ originalTerm = Nothing
960-
, originalTermIndex = Nothing
961-
, origin = Booster
962-
, result =
963-
Failure
964-
{ reason =
965-
"Reached recursion limit of "
966-
<> pack (show $ length stk)
967-
, _ruleId = Nothing
968-
}
969-
}
970-
ApplyEquations.InternalError err ->
971-
Simplification
972-
{ originalTerm = Nothing
973-
, originalTermIndex = Nothing
974-
, origin = Booster
975-
, result = Failure{reason = "Internal error: " <> err, _ruleId = Nothing}
976-
}
977-
ApplyEquations.SideConditionFalse _predicate ->
978-
Simplification
979-
{ originalTerm = Nothing
980-
, originalTermIndex = Nothing
981-
, origin = Booster
982-
, result = Failure{reason = "Side conditions false", _ruleId = Nothing}
983-
}
984-
ApplyEquations.UndefinedTerm _t _err ->
985-
Simplification
986-
{ originalTerm = Nothing
987-
, originalTermIndex = Nothing
988-
, origin = Booster
989-
, result = Failure{reason = "Undefined term found", _ruleId = Nothing}
990-
}
991-
(<> final) <$> mapM (mkLogEquationTrace equationLogOpts) equationTraces
992-
| otherwise -> Just []
809+
RewriteSimplified{} -> Just []
993810
_ -> Nothing

‎booster/tools/booster/Proxy.hs

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
9090
| otherwise ->
9191
let logSettings =
9292
LogSettings
93-
{ logSuccessfulSimplifications = execReq.logSuccessfulSimplifications
94-
, logFailedSimplifications = execReq.logFailedSimplifications
95-
, logSuccessfulRewrites = execReq.logSuccessfulRewrites
93+
{ logSuccessfulRewrites = execReq.logSuccessfulRewrites
9694
, logFailedRewrites = execReq.logFailedRewrites
9795
, logFallbacks = execReq.logFallbacks
9896
, logTiming = execReq.logTiming
@@ -550,8 +548,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
550548
SimplifyRequest
551549
{ state = execStateToKoreJson state
552550
, _module = mbModule
553-
, logSuccessfulSimplifications = Nothing
554-
, logFailedSimplifications = Nothing
555551
, logTiming
556552
}
557553

@@ -612,9 +608,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
612608
}
613609

614610
data LogSettings = LogSettings
615-
{ logSuccessfulSimplifications :: Maybe Bool
616-
, logFailedSimplifications :: Maybe Bool
617-
, logSuccessfulRewrites :: Maybe Bool
611+
{ logSuccessfulRewrites :: Maybe Bool
618612
, logFailedRewrites :: Maybe Bool
619613
, logFallbacks :: Maybe Bool
620614
, logTiming :: Maybe Bool

‎kore-rpc-types/src/Kore/JsonRpc/Types.hs

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,6 @@ data ExecuteRequest = ExecuteRequest
3939
, assumeStateDefined :: !(Maybe Bool)
4040
, logSuccessfulRewrites :: !(Maybe Bool)
4141
, logFailedRewrites :: !(Maybe Bool)
42-
, logSuccessfulSimplifications :: !(Maybe Bool)
43-
, logFailedSimplifications :: !(Maybe Bool)
4442
, logFallbacks :: !(Maybe Bool)
4543
, logTiming :: !(Maybe Bool)
4644
}
@@ -54,8 +52,6 @@ data ImpliesRequest = ImpliesRequest
5452
, consequent :: !KoreJson
5553
, _module :: !(Maybe Text)
5654
, assumeDefined :: !(Maybe Bool)
57-
, logSuccessfulSimplifications :: !(Maybe Bool)
58-
, logFailedSimplifications :: !(Maybe Bool)
5955
, logTiming :: !(Maybe Bool)
6056
}
6157
deriving stock (Generic, Show, Eq)
@@ -66,8 +62,6 @@ data ImpliesRequest = ImpliesRequest
6662
data SimplifyRequest = SimplifyRequest
6763
{ state :: KoreJson
6864
, _module :: !(Maybe Text)
69-
, logSuccessfulSimplifications :: !(Maybe Bool)
70-
, logFailedSimplifications :: !(Maybe Bool)
7165
, logTiming :: !(Maybe Bool)
7266
}
7367
deriving stock (Generic, Show, Eq)

0 commit comments

Comments
 (0)