Implies endpoint in booster #3846
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jberthold
reviewed
May 3, 2024
There was a problem hiding this comment.
I think we should re-visit emitting right-assoc for collections. I tried to have a look at the diff here, but it is really difficult when it gets so obscured by large sets being re-ordered between kore and booster
|
KEVM
|
jberthold
reviewed
May 7, 2024
|
Kontrol
|
jberthold
reviewed
May 8, 2024
Comment on lines
+531
to
+532
| MatchFailed{} -> | ||
| doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term |
There was a problem hiding this comment.
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?)
There was a problem hiding this comment.
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
booster/library/Booster/JsonRpc.hs
Outdated
| 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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
Comment on lines
+610
to
+615
| evaluateConstraints' constraints = do | ||
| pushConstraints constraints | ||
| -- evaluate all existing constraints, once | ||
| traverse_ simplifyAssumedPredicate . predicates =<< getState | ||
| -- this may yield additional new constraints, left unevaluated | ||
| predicates <$> getState |
There was a problem hiding this comment.
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.
| match1 _ t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 | ||
| match1 _ t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 | ||
| match1 _ t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 | ||
| match1 _ t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 | ||
| match1 _ t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 | ||
| match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2 | ||
| match1 Rewrite t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 | ||
| match1 Eval (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 |
There was a problem hiding this comment.
(off-topic) I was stumbling over this line first... why would we try to match those obviously-different things in Eval mode?
After reading matchSymbolApplication it turns out to be somewhat trivial... since a symbol cannot be both constructor and function, it will always end up in addIndeterminate.
geo2a
approved these changes
May 8, 2024
booster/library/Booster/JsonRpc.hs
Outdated
| . Left | ||
| . RpcError.backendError | ||
| . RpcError.ImplicationCheckError | ||
| . RpcError.ErrorWithContext "does-not-imply2" |
There was a problem hiding this comment.
Is the "2" in "does-not-imply2" spurious?
There was a problem hiding this comment.
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.
booster/library/Booster/JsonRpc.hs
Outdated
| 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 |
There was a problem hiding this comment.
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.
This was referenced May 10, 2024
geo2a
pushed a commit
that referenced
this pull request
May 15, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Closes #3778 #3601
This PR introduces a simple check implication implementation, which uses the matching algorithm to try to find a substitution or fail to unify the given configurations.
If matching the RHS configuration to the LHS succeeds and produces a substitution σ, we filter out any predicates in the consequent which appear in the antecedent and then check if all predicates in σ(filtered_preds) evaluate to true/#top. (Question: do we want to apply σ to the RHS preds before filtering?). With this simple algorithm, we can successfully discharge almost 85% of implication checks in KEVM and 88% in Kontrol.