Skip to content

Commit edde779

Browse files
goodlyrottenapplegithub-actionsrv-jenkins
authored
Booster implies endpoint improvements (#4026)
Fixes #3941 along with a host of tests from the pyk testsuite, which exercise corner cases, such as `#Bottom` being sent as antecedent or inconsistent conditions. Whilst these haven't really been observed in practice, passing these tests should give is more confidence that the booster does the same thing as kore. --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 3d7e91d commit edde779

28 files changed

+73827
-1655
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 3 additions & 119 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ import Crypto.Hash (SHA256 (..), hashWith)
2525
import Data.Bifunctor (second)
2626
import Data.Foldable
2727
import Data.List (singleton)
28-
import Data.List.NonEmpty qualified as NonEmpty
2928
import Data.Map.Strict (Map)
3029
import Data.Map.Strict qualified as Map
3130
import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
@@ -37,7 +36,6 @@ import Data.Text qualified as Text
3736
import Data.Text.Encoding qualified as Text
3837
import GHC.Records
3938
import Numeric.Natural
40-
import Prettyprinter (comma, hsep, punctuate, (<+>))
4139

4240
import Booster.CLOptions (RewriteOptions (..))
4341
import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
@@ -48,8 +46,7 @@ import Booster.Log
4846
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
4947
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
5048
import Booster.Pattern.Base qualified as Pattern
51-
import Booster.Pattern.Bool (pattern TrueBool)
52-
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
49+
import Booster.Pattern.Implies (runImplies)
5350
import Booster.Pattern.Pretty
5451
import Booster.Pattern.Rewrite (
5552
RewriteConfig (..),
@@ -64,7 +61,7 @@ import Booster.Pattern.Util (
6461
substituteInPredicate,
6562
substituteInTerm,
6663
)
67-
import Booster.Prettyprinter (renderDefault, renderText)
64+
import Booster.Prettyprinter (renderText)
6865
import Booster.SMT.Interface qualified as SMT
6966
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
7067
import Booster.Syntax.Json.Externalise
@@ -84,7 +81,6 @@ import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (.
8481
import Booster.Syntax.ParsedKore.Internalise (
8582
addToDefinitions,
8683
definitionErrorToRpcError,
87-
extractExistentials,
8884
)
8985
import Booster.Util (Flag (..), constructorName)
9086
import Kore.JsonRpc.Error qualified as RpcError
@@ -416,86 +412,7 @@ respond stateVar request =
416412
{ satisfiable = RpcTypes.Unknown
417413
, substitution = Nothing
418414
}
419-
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxImplies $ do
420-
-- internalise given constrained term
421-
let internalised =
422-
runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials
423-
424-
case (internalised req.antecedent.term, internalised req.consequent.term) of
425-
(Left patternError, _) -> do
426-
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
427-
pure $
428-
Left $
429-
RpcError.backendError $
430-
RpcError.CouldNotVerifyPattern
431-
[ patternErrorToRpcError patternError
432-
]
433-
(_, Left patternError) -> do
434-
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
435-
pure $
436-
Left $
437-
RpcError.backendError $
438-
RpcError.CouldNotVerifyPattern
439-
[ patternErrorToRpcError patternError
440-
]
441-
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
442-
unless (null unsupportedL && null unsupportedR) $ do
443-
logMessage'
444-
("aborting due to unsupported predicate parts" :: Text)
445-
unless (null unsupportedL) $
446-
withContext CtxDetail $
447-
logMessage
448-
(Text.unwords $ map prettyPattern unsupportedL)
449-
unless (null unsupportedR) $
450-
withContext CtxDetail $
451-
logMessage
452-
(Text.unwords $ map prettyPattern unsupportedR)
453-
let
454-
-- apply the given substitution before doing anything else
455-
substPatL =
456-
Pattern
457-
{ term = substituteInTerm substitutionL patL.term
458-
, constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
459-
, ceilConditions = patL.ceilConditions
460-
}
461-
substPatR =
462-
Pattern
463-
{ term = substituteInTerm substitutionR patR.term
464-
, constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
465-
, ceilConditions = patR.ceilConditions
466-
}
467-
468-
case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
469-
MatchFailed (SubsortingError sortError) ->
470-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
471-
show sortError
472-
MatchFailed{} ->
473-
doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term
474-
MatchIndeterminate remainder ->
475-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
476-
"match remainder: "
477-
<> renderDefault
478-
( hsep $
479-
punctuate comma $
480-
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
481-
NonEmpty.toList remainder
482-
)
483-
MatchSuccess subst -> do
484-
let filteredConsequentPreds =
485-
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
486-
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
487-
488-
if null filteredConsequentPreds
489-
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
490-
else
491-
ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
492-
(Right newPreds, _) ->
493-
if all (== Pattern.Predicate TrueBool) newPreds
494-
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
495-
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
496-
(Left other, _) ->
497-
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
498-
415+
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> runImplies def mLlvmLibrary mSMTOptions req.antecedent req.consequent
499416
-- this case is only reachable if the cancel appeared as part of a batch request
500417
RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
501418
where
@@ -512,39 +429,6 @@ respond stateVar request =
512429
Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
513430
Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions)
514431

515-
doesNotImply s l r =
516-
pure $
517-
Right $
518-
RpcTypes.Implies
519-
RpcTypes.ImpliesResult
520-
{ implication = addHeader $ Syntax.KJImplies (externaliseSort s) l r
521-
, valid = False
522-
, condition = Nothing
523-
, logs = Nothing
524-
}
525-
526-
implies s' l r subst =
527-
let s = externaliseSort s'
528-
in pure $
529-
Right $
530-
RpcTypes.Implies
531-
RpcTypes.ImpliesResult
532-
{ implication = addHeader $ Syntax.KJImplies s l r
533-
, valid = True
534-
, condition =
535-
Just
536-
RpcTypes.Condition
537-
{ predicate = addHeader $ Syntax.KJTop s
538-
, substitution =
539-
addHeader
540-
$ (\xs -> if null xs then Syntax.KJTop s else Syntax.KJAnd s xs)
541-
. map (uncurry $ externaliseSubstitution s)
542-
. Map.toList
543-
$ subst
544-
}
545-
, logs = Nothing
546-
}
547-
548432
handleSmtError :: JsonRpcHandler
549433
handleSmtError = JsonRpcHandler $ \case
550434
SMT.GeneralSMTError err -> runtimeError "problem" err

0 commit comments

Comments
 (0)