Skip to content

Commit 15f3a47

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 6ce0ea7 + edde779 commit 15f3a47

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)