Skip to content

Commit a0ca443

Browse files
goodlyrottenapplegithub-actions
goodlyrottenapple
and
github-actions
authored
Implies endpoint in booster (#3846)
Closes #3778 #3601 This PR introduces a simple check implication implementation, which uses the matching algorithm to try to find a substitution or fail to unify the given configurations. If matching the RHS configuration to the LHS succeeds and produces a substitution σ, we filter out any predicates in the consequent which appear in the antecedent and then check if all predicates in σ(filtered_preds) evaluate to true/#top. (Question: do we want to apply σ to the RHS preds before filtering?). With this simple algorithm, we can successfully discharge almost 85% of implication checks in KEVM and 88% in Kontrol. --------- Co-authored-by: github-actions <[email protected]>
1 parent 538d079 commit a0ca443

File tree

20 files changed

+43502
-43569
lines changed

20 files changed

+43502
-43569
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 126 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,20 @@ 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)
5153
import Booster.Pattern.Rewrite (
5254
RewriteFailed (..),
5355
RewriteResult (..),
5456
RewriteTrace (..),
5557
performRewrite,
5658
)
57-
import Booster.Pattern.Util (sortOfPattern, substituteInPredicate, substituteInTerm)
58-
import Booster.Prettyprinter (renderText)
59+
import Booster.Pattern.Util (
60+
sortOfPattern,
61+
substituteInPredicate,
62+
substituteInTerm,
63+
)
64+
import Booster.Prettyprinter (renderDefault, renderText)
5965
import Booster.SMT.Base qualified as SMT
6066
import Booster.SMT.Interface qualified as SMT
6167
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
@@ -73,7 +79,11 @@ import Booster.Syntax.Json.Internalise (
7379
import Booster.Syntax.ParsedKore (parseKoreModule)
7480
import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
7581
import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
76-
import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError)
82+
import Booster.Syntax.ParsedKore.Internalise (
83+
addToDefinitions,
84+
definitionErrorToRpcError,
85+
extractExistentials,
86+
)
7787
import Booster.Util (Flag (..), constructorName)
7888
import Kore.JsonRpc.Error qualified as RpcError
7989
import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
@@ -455,11 +465,87 @@ respond stateVar =
455465
{ satisfiable = RpcTypes.Sat
456466
, substitution
457467
}
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)
458546

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

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+
477596
handleSmtError :: JsonRpcHandler
478597
handleSmtError = JsonRpcHandler $ \case
479598
SMT.GeneralSMTError err -> runtimeError "problem" err
@@ -764,7 +883,7 @@ mkLogRewriteTrace
764883
| logSuccessfulRewrites ->
765884
Just $
766885
singleton $
767-
Rewrite
886+
Kore.JsonRpc.Types.Log.Rewrite
768887
{ result =
769888
Success
770889
{ rewrittenTerm = Nothing
@@ -778,7 +897,7 @@ mkLogRewriteTrace
778897
| logFailedRewrites ->
779898
Just $
780899
singleton $
781-
Rewrite
900+
Kore.JsonRpc.Types.Log.Rewrite
782901
{ result = case reason of
783902
NoApplicableRules{} -> Failure{reason = "No applicable rules found", _ruleId = Nothing}
784903
TermIndexIsNone{} -> Failure{reason = "Term index is None for term", _ruleId = Nothing}

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

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

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

201202
rpcTypeOf :: KoreRpcJson -> KoreRpcType
202203
rpcTypeOf = \case
203-
RpcRequest req -> RpcReq $ methodOf req
204-
RpcResponse r -> RpcResp $ methodOf r
204+
RpcRequest req -> RpcReq $ methodOfRpcCall req
205+
RpcResponse r -> RpcResp $ methodOfRpcCall r
205206
RpcError{} -> RpcErr
206207
RpcKoreJson{} -> RpcKore
207208
RpcJson{} -> RpcJs
208209
NotRpcJson{} -> NotRpcJs
209-
where
210-
methodOf = \case
211-
Execute _ -> ExecuteM
212-
Implies _ -> ImpliesM
213-
Simplify _ -> SimplifyM
214-
AddModule _ -> AddModuleM
215-
GetModel _ -> GetModelM
216-
Cancel -> error "Cancel"
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"
217219

218220
-------------------------------------------------------------------
219221
-- doing the actual diff when output is requested

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

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

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

569570
-- version for internal nested evaluation
570571
evaluatePattern' ::
571-
MonadLoggerIO io =>
572+
LoggerMIO io =>
572573
Pattern ->
573574
EquationT io Pattern
574575
evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
@@ -580,14 +581,38 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
580581
-- this may yield additional new constraints, left unevaluated
581582
evaluatedConstraints <- predicates <$> getState
582583
pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
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
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
591616

592617
----------------------------------------
593618

0 commit comments

Comments
 (0)