Skip to content

Implies endpoint in booster #3846

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 22 commits into from
May 8, 2024
Merged

Implies endpoint in booster #3846

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
b33755c
change satisfiable -> valid in implies response
goodlyrottenapple May 2, 2024
0a40b69
Add the ability to only run certain types of request from a tarball
goodlyrottenapple May 2, 2024
f4fcc3b
implement implies endpoint in booster
goodlyrottenapple May 2, 2024
b45ffa4
revert changes to booster/library/Booster/JsonRpc/Utils.hs
goodlyrottenapple May 2, 2024
908544c
Format with fourmolu
invalid-email-address May 2, 2024
e10e47f
update rpc client with better reading of run-only options
goodlyrottenapple May 3, 2024
2eefa9e
Merge branch 'master' into sam/implication
goodlyrottenapple May 3, 2024
fa0d73b
add tests for implication mode when matching
goodlyrottenapple May 3, 2024
6be8498
emit substitution when implication is valid
goodlyrottenapple May 3, 2024
e5b55ba
update bug reports
goodlyrottenapple May 3, 2024
a5f740c
Format with fourmolu
invalid-email-address May 3, 2024
e7ac98a
Format with fourmolu
invalid-email-address May 3, 2024
5154be2
cleanup
goodlyrottenapple May 3, 2024
4d7a127
fix kore tests
goodlyrottenapple May 3, 2024
b1408eb
fix responses again
goodlyrottenapple May 7, 2024
9c21c9c
Merge branch 'master' into sam/implication
goodlyrottenapple May 7, 2024
bf0ea9f
fix responses again
goodlyrottenapple May 7, 2024
d6666b7
fix rpcJsonConfig
goodlyrottenapple May 7, 2024
bd01cae
merge master
goodlyrottenapple May 7, 2024
40c0488
revert to first fixed tests
goodlyrottenapple May 7, 2024
9bef22d
cleanup
goodlyrottenapple May 8, 2024
7ef58ee
remve redundant imports
goodlyrottenapple May 8, 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
158 changes: 150 additions & 8 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ import Data.Text qualified as Text
import Data.Text.Encoding qualified as Text
import GHC.Records
import Numeric.Natural
import Prettyprinter (pretty)
import Prettyprinter (pretty, vsep)
import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)

import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
Expand All @@ -48,14 +48,21 @@ 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.Rewrite (
RewriteFailed (..),
RewriteResult (..),
RewriteTrace (..),
performRewrite,
)
import Booster.Pattern.Util (sortOfPattern, substituteInPredicate, substituteInTerm)
import Booster.Prettyprinter (renderText)
import Booster.Pattern.Util (
freeVariables,
sortOfPattern,
substituteInPredicate,
substituteInTerm,
)
import Booster.Prettyprinter (renderDefault, renderText)
import Booster.SMT.Base qualified as SMT
import Booster.SMT.Interface qualified as SMT
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
Expand All @@ -73,7 +80,11 @@ import Booster.Syntax.Json.Internalise (
import Booster.Syntax.ParsedKore (parseKoreModule)
import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError)
import Booster.Syntax.ParsedKore.Internalise (
addToDefinitions,
definitionErrorToRpcError,
extractExistentials,
)
import Booster.Util (Flag (..), constructorName)
import Kore.JsonRpc.Error qualified as RpcError
import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
Expand Down Expand Up @@ -455,11 +466,109 @@ respond stateVar =
{ satisfiable = RpcTypes.Sat
, substitution
}
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ 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
Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(_, Left patternError) -> do
Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
unless (null unsupportedL && null unsupportedR) $ do
Log.logWarnNS
"booster"
"Implies: aborting due to unsupported predicate parts"
unless (null unsupportedL) $
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(Text.unlines $ map prettyPattern unsupportedL)
unless (null unsupportedR) $
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(Text.unlines $ map prettyPattern unsupportedR)
let doTracing =
Flag $
any
(fromMaybe False)
[ req.logSuccessfulSimplifications
, req.logFailedSimplifications
]
-- 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
Comment on lines +524 to +525
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The legacy backend would first simplify both patterns and return the simplified implication.

Not sure whether we would want to keep that behaviour (did it matter in the tests?)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i guess this would matter if e.g. the antecedent goes to #bottom? i guess here i am assuming things are defined and the constraints don't contradict each other

MatchIndeterminate remainder ->
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
"match remainder: "
<> renderDefault (pretty remainder)
MatchSuccess subst -> do
-- check it is a "matching" substitution (substitutes variables
-- from the subject term only). Return does not imply if not.
let violatingItems = Map.restrictKeys subst (Map.keysSet subst `Set.difference` freeVariables substPatR.term)
if not $ null violatingItems
then do
pure
. Left
. RpcError.backendError
. RpcError.ImplicationCheckError
. RpcError.ErrorWithContext "does-not-imply2"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the "2" in "does-not-imply2" spurious?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah, that's now a pointless check. thanks for pointing out. After the matching code re-factor, we already throw this error earlier via SubjectVariableMatch and return not implies.

$ [ "not matching substitution"
, pack $ renderDefault $ vsep [pretty k <> "->" <> pretty v | (k, v) <- Map.toList violatingItems]
]
else -- doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term
do
let filteredConsequentPreds =
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
solver <- traverse (SMT.initSolver def) mSMTOptions

if null filteredConsequentPreds
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
else -- pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $ "implies"

ApplyEquations.evaluateConstraints doTracing def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would have expected that the substPatL.constraints be used as preconditions when checking that substPatR.constraints (minus the identical ones, i.e., filteredConsequentPreds) hold here. evaluateConstraints should probably take an additional argument for things that are assumed true when checking.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yeah i was surprised even this most naive version seems to work reasonably well especially in KEVM. don't know if we should try more complex versions in this PR or follow up later. What do you think?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So we are essentially throwing the known constraints away. We should definitely have a follow-up PR to see if considering the substPatL.constraints allows us to cover the rest of the cases that Kore is still needed for.

(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.ImplicationCheckError . RpcError.ErrorOnly $ "implies"
pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)

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

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 Expand Up @@ -764,7 +906,7 @@ mkLogRewriteTrace
| logSuccessfulRewrites ->
Just $
singleton $
Rewrite
Kore.JsonRpc.Types.Log.Rewrite
{ result =
Success
{ rewrittenTerm = Nothing
Expand All @@ -778,7 +920,7 @@ mkLogRewriteTrace
| logFailedRewrites ->
Just $
singleton $
Rewrite
Kore.JsonRpc.Types.Log.Rewrite
{ result = case reason of
NoApplicableRules{} -> Failure{reason = "No applicable rules found", _ruleId = Nothing}
TermIndexIsNone{} -> Failure{reason = "Term index is None for term", _ruleId = Nothing}
Expand Down
22 changes: 12 additions & 10 deletions booster/library/Booster/JsonRpc/Utils.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ module Booster.JsonRpc.Utils (
rpcTypeOf,
typeString,
diffBy,
methodOfRpcCall,
) where

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

rpcTypeOf :: KoreRpcJson -> KoreRpcType
rpcTypeOf = \case
RpcRequest req -> RpcReq $ methodOf req
RpcResponse r -> RpcResp $ methodOf r
RpcRequest req -> RpcReq $ methodOfRpcCall req
RpcResponse r -> RpcResp $ methodOfRpcCall r
RpcError{} -> RpcErr
RpcKoreJson{} -> RpcKore
RpcJson{} -> RpcJs
NotRpcJson{} -> NotRpcJs
where
methodOf = \case
Execute _ -> ExecuteM
Implies _ -> ImpliesM
Simplify _ -> SimplifyM
AddModule _ -> AddModuleM
GetModel _ -> GetModelM
Cancel -> error "Cancel"

methodOfRpcCall :: API r -> APIMethod
methodOfRpcCall = \case
Execute _ -> ExecuteM
Implies _ -> ImpliesM
Simplify _ -> SimplifyM
AddModule _ -> AddModuleM
GetModel _ -> GetModelM
Cancel -> error "Cancel"

-------------------------------------------------------------------
-- doing the actual diff when output is requested
Expand Down
43 changes: 34 additions & 9 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ module Booster.Pattern.ApplyEquations (
simplifyConstraints,
SimplifierCache,
logWarn,
evaluateConstraints,
) where

import Control.Applicative (Alternative (..))
Expand Down Expand Up @@ -560,7 +561,7 @@ evaluatePattern doTracing def mLlvmLibrary smtSolver cache =

-- version for internal nested evaluation
evaluatePattern' ::
MonadLoggerIO io =>
LoggerMIO io =>
Pattern ->
EquationT io Pattern
evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
Expand All @@ -572,14 +573,38 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
-- this may yield additional new constraints, left unevaluated
evaluatedConstraints <- predicates <$> getState
pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
where
-- evaluate the given predicate assuming all others
simplifyAssumedPredicate p = withContext "constraint" $ do
allPs <- predicates <$> getState
let otherPs = Set.delete p allPs
eqState $ modify $ \s -> s{predicates = otherPs}
newP <- simplifyConstraint' True $ coerce p
pushConstraints $ Set.singleton $ coerce newP

-- evaluate the given predicate assuming all others
simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
simplifyAssumedPredicate p = do
allPs <- predicates <$> getState
let otherPs = Set.delete p allPs
eqState $ modify $ \s -> s{predicates = otherPs}
newP <- simplifyConstraint' True $ coerce p
pushConstraints $ Set.singleton $ coerce newP

evaluateConstraints ::
LoggerMIO io =>
Flag "CollectEquationTraces" ->
KoreDefinition ->
Maybe LLVM.API ->
Maybe SMT.SMTContext ->
SimplifierCache ->
Set Predicate ->
io (Either EquationFailure (Set Predicate), SimplifierCache)
evaluateConstraints doTracing def mLlvmLibrary smtSolver cache =
runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints'

evaluateConstraints' ::
LoggerMIO io =>
Set Predicate ->
EquationT io (Set Predicate)
evaluateConstraints' constraints = do
pushConstraints constraints
-- evaluate all existing constraints, once
traverse_ simplifyAssumedPredicate . predicates =<< getState
-- this may yield additional new constraints, left unevaluated
predicates <$> getState
Comment on lines +610 to +615
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wrt. the comment above in JsonRpc about the constraints of the antecedent:
This function would need to push the constraints from the antecedent, but then only check the ones from the consequent, and we want them all to be TrueBool (independent of each other). This is different from the simplifyAssumedPredicate idea which was to simplify (not remove) constraints.
Probably we should put the antecedent constraints into the state, and then call simplifyConstraint' on each (substituted) predicate of the consequent to check that it yields true.


----------------------------------------

Expand Down
Loading