Skip to content

Booster implies endpoint improvements #4026

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 19 commits into from
Aug 15, 2024
Merged

Booster implies endpoint improvements #4026

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
8a07a54
add llvm definition for implies-issue-3941
goodlyrottenapple Aug 9, 2024
74ac3f6
overhaul implication endpoint adding support for corner-cases such as…
goodlyrottenapple Aug 9, 2024
77d9c81
udpate docs
goodlyrottenapple Aug 9, 2024
ddf6b55
update tests
goodlyrottenapple Aug 9, 2024
a74034f
merge master
goodlyrottenapple Aug 9, 2024
3f49e48
Format with fourmolu
invalid-email-address Aug 9, 2024
24cdf89
rmove kore file
goodlyrottenapple Aug 9, 2024
f3a1f8f
add secp
goodlyrottenapple Aug 9, 2024
3233def
update kompile script
goodlyrottenapple Aug 12, 2024
9754bb2
Merge branch 'master' into sam/implies-improvements
goodlyrottenapple Aug 12, 2024
a428f15
move implies code into a separate file
goodlyrottenapple Aug 13, 2024
f3ae5c8
Merge branch 'sam/implies-improvements' of github.com:runtimeverifica…
goodlyrottenapple Aug 13, 2024
8666e9f
Format with fourmolu
invalid-email-address Aug 13, 2024
495926e
reverse change to explodeAnd
goodlyrottenapple Aug 13, 2024
477b495
add comments + minor fixes
goodlyrottenapple Aug 14, 2024
79710f8
Merge remote-tracking branch 'origin/master' into sam/implies-improve…
goodlyrottenapple Aug 14, 2024
3382ca0
Format with fourmolu
invalid-email-address Aug 14, 2024
06a1d9b
fix incorrect condition
goodlyrottenapple Aug 15, 2024
9c7abac
Merge branch 'master' into sam/implies-improvements
rv-jenkins Aug 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 3 additions & 119 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
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
Loading