Skip to content

Commit

Permalink
Booster implies endpoint improvements (#4026)
Browse files Browse the repository at this point in the history 
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 <github-actions@github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
  • Loading branch information
@goodlyrottenapple @rv-jenkins
3 people authored Aug 15, 2024
1 parent 3d7e91d commit edde779
Show file tree
Hide file tree
Showing 28 changed files with 73,827 additions and 1,655 deletions.
122 changes: 3 additions & 119 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ import Crypto.Hash (SHA256 (..), hashWith)
import Data.Bifunctor (second)
import Data.Foldable
import Data.List (singleton)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
Expand All @@ -37,7 +36,6 @@ import Data.Text qualified as Text
import Data.Text.Encoding qualified as Text
import GHC.Records
import Numeric.Natural
import Prettyprinter (comma, hsep, punctuate, (<+>))

import Booster.CLOptions (RewriteOptions (..))
import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
Expand All @@ -48,8 +46,7 @@ import Booster.Log
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
import Booster.Pattern.Base qualified as Pattern
import Booster.Pattern.Bool (pattern TrueBool)
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
import Booster.Pattern.Implies (runImplies)
import Booster.Pattern.Pretty
import Booster.Pattern.Rewrite (
RewriteConfig (..),
Expand All @@ -64,7 +61,7 @@ import Booster.Pattern.Util (
substituteInPredicate,
substituteInTerm,
)
import Booster.Prettyprinter (renderDefault, renderText)
import Booster.Prettyprinter (renderText)
import Booster.SMT.Interface qualified as SMT
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
import Booster.Syntax.Json.Externalise
Expand All @@ -84,7 +81,6 @@ import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (.
import Booster.Syntax.ParsedKore.Internalise (
addToDefinitions,
definitionErrorToRpcError,
extractExistentials,
)
import Booster.Util (Flag (..), constructorName)
import Kore.JsonRpc.Error qualified as RpcError
Expand Down Expand Up @@ -416,86 +412,7 @@ respond stateVar request =
{ satisfiable = RpcTypes.Unknown
, substitution = Nothing
}
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxImplies $ do
-- internalise given constrained term
let internalised =
runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials

case (internalised req.antecedent.term, internalised req.consequent.term) of
(Left patternError, _) -> do
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(_, Left patternError) -> do
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
unless (null unsupportedL && null unsupportedR) $ do
logMessage'
("aborting due to unsupported predicate parts" :: Text)
unless (null unsupportedL) $
withContext CtxDetail $
logMessage
(Text.unwords $ map prettyPattern unsupportedL)
unless (null unsupportedR) $
withContext CtxDetail $
logMessage
(Text.unwords $ map prettyPattern unsupportedR)
let
-- apply the given substitution before doing anything else
substPatL =
Pattern
{ term = substituteInTerm substitutionL patL.term
, constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
, ceilConditions = patL.ceilConditions
}
substPatR =
Pattern
{ term = substituteInTerm substitutionR patR.term
, constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
, ceilConditions = patR.ceilConditions
}

case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
MatchFailed (SubsortingError sortError) ->
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
show sortError
MatchFailed{} ->
doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term
MatchIndeterminate remainder ->
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
"match remainder: "
<> renderDefault
( hsep $
punctuate comma $
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
NonEmpty.toList remainder
)
MatchSuccess subst -> do
let filteredConsequentPreds =
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions

if null filteredConsequentPreds
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
else
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
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)

RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> runImplies def mLlvmLibrary mSMTOptions req.antecedent req.consequent
-- this case is only reachable if the cancel appeared as part of a batch request
RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
where
Expand All @@ -512,39 +429,6 @@ respond stateVar request =
Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions)

doesNotImply s l r =
pure $
Right $
RpcTypes.Implies
RpcTypes.ImpliesResult
{ implication = addHeader $ Syntax.KJImplies (externaliseSort s) l r
, valid = False
, condition = Nothing
, logs = Nothing
}

implies s' l r subst =
let s = externaliseSort s'
in pure $
Right $
RpcTypes.Implies
RpcTypes.ImpliesResult
{ implication = addHeader $ Syntax.KJImplies s l r
, valid = True
, condition =
Just
RpcTypes.Condition
{ predicate = addHeader $ Syntax.KJTop s
, substitution =
addHeader
$ (\xs -> if null xs then Syntax.KJTop s else Syntax.KJAnd s xs)
. map (uncurry $ externaliseSubstitution s)
. Map.toList
$ subst
}
, logs = Nothing
}

handleSmtError :: JsonRpcHandler
handleSmtError = JsonRpcHandler $ \case
SMT.GeneralSMTError err -> runtimeError "problem" err
Expand Down
Loading

0 comments on commit edde779

Please sign in to comment.