Skip to content

Commit bc25955

Browse files
geo2ageo2a
committed
Revert "Implies endpoint in booster (#3846)"
This reverts commit a0ca443.
1 parent 40c912b commit bc25955

File tree

20 files changed

+34779
-34712
lines changed

20 files changed

+34779
-34712
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 7 additions & 126 deletions
Original file line numberDiff line numberDiff line change
@@ -48,20 +48,14 @@ import Booster.Log
4848
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
4949
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
5050
import Booster.Pattern.Base qualified as Pattern
51-
import Booster.Pattern.Bool (pattern TrueBool)
52-
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
5351
import Booster.Pattern.Rewrite (
5452
RewriteFailed (..),
5553
RewriteResult (..),
5654
RewriteTrace (..),
5755
performRewrite,
5856
)
59-
import Booster.Pattern.Util (
60-
sortOfPattern,
61-
substituteInPredicate,
62-
substituteInTerm,
63-
)
64-
import Booster.Prettyprinter (renderDefault, renderText)
57+
import Booster.Pattern.Util (sortOfPattern, substituteInPredicate, substituteInTerm)
58+
import Booster.Prettyprinter (renderText)
6559
import Booster.SMT.Base qualified as SMT
6660
import Booster.SMT.Interface qualified as SMT
6761
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
@@ -79,11 +73,7 @@ import Booster.Syntax.Json.Internalise (
7973
import Booster.Syntax.ParsedKore (parseKoreModule)
8074
import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
8175
import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
82-
import Booster.Syntax.ParsedKore.Internalise (
83-
addToDefinitions,
84-
definitionErrorToRpcError,
85-
extractExistentials,
86-
)
76+
import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError)
8777
import Booster.Util (Flag (..), constructorName)
8878
import Kore.JsonRpc.Error qualified as RpcError
8979
import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
@@ -465,87 +455,11 @@ respond stateVar =
465455
{ satisfiable = RpcTypes.Sat
466456
, substitution
467457
}
468-
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ do
469-
-- internalise given constrained term
470-
let internalised =
471-
runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials
472-
473-
case (internalised req.antecedent.term, internalised req.consequent.term) of
474-
(Left patternError, _) -> do
475-
Log.logDebug $ "Error internalising antecedent" <> Text.pack (show patternError)
476-
pure $
477-
Left $
478-
RpcError.backendError $
479-
RpcError.CouldNotVerifyPattern
480-
[ patternErrorToRpcError patternError
481-
]
482-
(_, Left patternError) -> do
483-
Log.logDebug $ "Error internalising consequent" <> Text.pack (show patternError)
484-
pure $
485-
Left $
486-
RpcError.backendError $
487-
RpcError.CouldNotVerifyPattern
488-
[ patternErrorToRpcError patternError
489-
]
490-
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
491-
unless (null unsupportedL && null unsupportedR) $ do
492-
Log.logWarnNS
493-
"booster"
494-
"Implies: aborting due to unsupported predicate parts"
495-
unless (null unsupportedL) $
496-
Log.logOtherNS
497-
"booster"
498-
(Log.LevelOther "ErrorDetails")
499-
(Text.unlines $ map prettyPattern unsupportedL)
500-
unless (null unsupportedR) $
501-
Log.logOtherNS
502-
"booster"
503-
(Log.LevelOther "ErrorDetails")
504-
(Text.unlines $ map prettyPattern unsupportedR)
505-
let
506-
-- apply the given substitution before doing anything else
507-
substPatL =
508-
Pattern
509-
{ term = substituteInTerm substitutionL patL.term
510-
, constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
511-
, ceilConditions = patL.ceilConditions
512-
}
513-
substPatR =
514-
Pattern
515-
{ term = substituteInTerm substitutionR patR.term
516-
, constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
517-
, ceilConditions = patR.ceilConditions
518-
}
519-
520-
case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
521-
MatchFailed (SubsortingError sortError) ->
522-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
523-
show sortError
524-
MatchFailed{} ->
525-
doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term
526-
MatchIndeterminate remainder ->
527-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
528-
"match remainder: "
529-
<> renderDefault (pretty remainder)
530-
MatchSuccess subst -> do
531-
let filteredConsequentPreds =
532-
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
533-
doTracing = Flag False
534-
solver <- traverse (SMT.initSolver def) mSMTOptions
535-
536-
if null filteredConsequentPreds
537-
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
538-
else
539-
ApplyEquations.evaluateConstraints doTracing def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
540-
(Right newPreds, _) ->
541-
if all (== Pattern.Predicate TrueBool) newPreds
542-
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
543-
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
544-
(Left other, _) ->
545-
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
546458

547459
-- this case is only reachable if the cancel appeared as part of a batch request
548460
RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
461+
-- using "Method does not exist" error code
462+
_ -> pure $ Left RpcError.notImplemented
549463
where
550464
withModule ::
551465
Maybe Text ->
@@ -560,39 +474,6 @@ respond stateVar =
560474
Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
561475
Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions)
562476

563-
doesNotImply s l r =
564-
pure $
565-
Right $
566-
RpcTypes.Implies
567-
RpcTypes.ImpliesResult
568-
{ implication = addHeader $ Syntax.KJImplies (externaliseSort s) l r
569-
, valid = False
570-
, condition = Nothing
571-
, logs = Nothing
572-
}
573-
574-
implies s' l r subst =
575-
let s = externaliseSort s'
576-
in pure $
577-
Right $
578-
RpcTypes.Implies
579-
RpcTypes.ImpliesResult
580-
{ implication = addHeader $ Syntax.KJImplies s l r
581-
, valid = True
582-
, condition =
583-
Just
584-
RpcTypes.Condition
585-
{ predicate = addHeader $ Syntax.KJTop s
586-
, substitution =
587-
addHeader
588-
$ (\xs -> if null xs then Syntax.KJTop s else Syntax.KJAnd s xs)
589-
. map (uncurry $ externaliseSubstitution s)
590-
. Map.toList
591-
$ subst
592-
}
593-
, logs = Nothing
594-
}
595-
596477
handleSmtError :: JsonRpcHandler
597478
handleSmtError = JsonRpcHandler $ \case
598479
SMT.GeneralSMTError err -> runtimeError "problem" err
@@ -883,7 +764,7 @@ mkLogRewriteTrace
883764
| logSuccessfulRewrites ->
884765
Just $
885766
singleton $
886-
Kore.JsonRpc.Types.Log.Rewrite
767+
Rewrite
887768
{ result =
888769
Success
889770
{ rewrittenTerm = Nothing
@@ -897,7 +778,7 @@ mkLogRewriteTrace
897778
| logFailedRewrites ->
898779
Just $
899780
singleton $
900-
Kore.JsonRpc.Types.Log.Rewrite
781+
Rewrite
901782
{ result = case reason of
902783
NoApplicableRules{} -> Failure{reason = "No applicable rules found", _ruleId = Nothing}
903784
TermIndexIsNone{} -> Failure{reason = "Term index is None for term", _ruleId = Nothing}

‎booster/library/Booster/JsonRpc/Utils.hs

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ module Booster.JsonRpc.Utils (
1313
rpcTypeOf,
1414
typeString,
1515
diffBy,
16-
methodOfRpcCall,
1716
) where
1817

1918
import Control.Applicative ((<|>))
@@ -201,21 +200,20 @@ typeString = BS.pack . show
201200

202201
rpcTypeOf :: KoreRpcJson -> KoreRpcType
203202
rpcTypeOf = \case
204-
RpcRequest req -> RpcReq $ methodOfRpcCall req
205-
RpcResponse r -> RpcResp $ methodOfRpcCall r
203+
RpcRequest req -> RpcReq $ methodOf req
204+
RpcResponse r -> RpcResp $ methodOf r
206205
RpcError{} -> RpcErr
207206
RpcKoreJson{} -> RpcKore
208207
RpcJson{} -> RpcJs
209208
NotRpcJson{} -> NotRpcJs
210-
211-
methodOfRpcCall :: API r -> APIMethod
212-
methodOfRpcCall = \case
213-
Execute _ -> ExecuteM
214-
Implies _ -> ImpliesM
215-
Simplify _ -> SimplifyM
216-
AddModule _ -> AddModuleM
217-
GetModel _ -> GetModelM
218-
Cancel -> error "Cancel"
209+
where
210+
methodOf = \case
211+
Execute _ -> ExecuteM
212+
Implies _ -> ImpliesM
213+
Simplify _ -> SimplifyM
214+
AddModule _ -> AddModuleM
215+
GetModel _ -> GetModelM
216+
Cancel -> error "Cancel"
219217

220218
-------------------------------------------------------------------
221219
-- doing the actual diff when output is requested

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 9 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ module Booster.Pattern.ApplyEquations (
2929
simplifyConstraint,
3030
simplifyConstraints,
3131
SimplifierCache,
32-
evaluateConstraints,
3332
) where
3433

3534
import Control.Applicative (Alternative (..))
@@ -569,7 +568,7 @@ evaluatePattern doTracing def mLlvmLibrary smtSolver cache =
569568

570569
-- version for internal nested evaluation
571570
evaluatePattern' ::
572-
LoggerMIO io =>
571+
MonadLoggerIO io =>
573572
Pattern ->
574573
EquationT io Pattern
575574
evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
@@ -581,38 +580,14 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
581580
-- this may yield additional new constraints, left unevaluated
582581
evaluatedConstraints <- predicates <$> getState
583582
pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
584-
585-
-- evaluate the given predicate assuming all others
586-
simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
587-
simplifyAssumedPredicate p = do
588-
allPs <- predicates <$> getState
589-
let otherPs = Set.delete p allPs
590-
eqState $ modify $ \s -> s{predicates = otherPs}
591-
newP <- simplifyConstraint' True $ coerce p
592-
pushConstraints $ Set.singleton $ coerce newP
593-
594-
evaluateConstraints ::
595-
LoggerMIO io =>
596-
Flag "CollectEquationTraces" ->
597-
KoreDefinition ->
598-
Maybe LLVM.API ->
599-
Maybe SMT.SMTContext ->
600-
SimplifierCache ->
601-
Set Predicate ->
602-
io (Either EquationFailure (Set Predicate), SimplifierCache)
603-
evaluateConstraints doTracing def mLlvmLibrary smtSolver cache =
604-
runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints'
605-
606-
evaluateConstraints' ::
607-
LoggerMIO io =>
608-
Set Predicate ->
609-
EquationT io (Set Predicate)
610-
evaluateConstraints' constraints = do
611-
pushConstraints constraints
612-
-- evaluate all existing constraints, once
613-
traverse_ simplifyAssumedPredicate . predicates =<< getState
614-
-- this may yield additional new constraints, left unevaluated
615-
predicates <$> getState
583+
where
584+
-- evaluate the given predicate assuming all others
585+
simplifyAssumedPredicate p = withContext "constraint" $ do
586+
allPs <- predicates <$> getState
587+
let otherPs = Set.delete p allPs
588+
eqState $ modify $ \s -> s{predicates = otherPs}
589+
newP <- simplifyConstraint' True $ coerce p
590+
pushConstraints $ Set.singleton $ coerce newP
616591

617592
----------------------------------------
618593

0 commit comments

Comments
 (0)