Consider known predicates in Booster's simplifier API #3953

geo2a · 2024-06-20T15:03:29Z

The runEquationT function now takes a Set Predicate, which are the "predicates known to be true" and are populated into the initial EquationState. Their origin is intended to be the rewriting path condition.

There's now a possibility to supply prior knowledge to the following API functions in Booster.Pattern.Rewrite:

evaluateTerm
simplifyConstraint

There's also a light change in evaluatePattern, which is now passes the pattern's constraints as an argument to runEuationT rather then using pushConstraint.

geo2a · 2024-06-20T17:58:25Z

KEVM performance:

Test	georgy-check-constraint-with-known time	master-fb59a8493 time	(georgy-check-constraint-with-known/master-fb59a8493) time
erc20/ds/balanceOf-spec.k	60.16	63.91	0.9413237365044594
erc20/ds/approve-failure-spec.k	70.64	73.41	0.962266721155156
kontrol/test-storetest-testaccesses-0-spec.k	84.24	77.61	1.085427135678392
TOTAL	215.04000000000002	214.93	1.0005117945377566

jberthold · 2024-06-21T02:24:00Z

booster/library/Booster/Pattern/ApplyEquations.hs

-evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
-    pushConstraints constraints
+evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
    newTerm <- withTermContext term $ evaluateTerm' BottomUp term
    -- after evaluating the term, evaluate all (existing and
    -- newly-acquired) constraints, once


Maybe we should still start empty and push the path condition as the first step.
The code here returns all stored predicates as constraints of the pattern (in line 424) which may or may not be correct depending on how the function was called. This is correct for the current use of the function but might not be correct in all future use cases.
Alternatively, how about we inline all of evaluatedPattern' into evaluatePattern (so no mistakes are possible).

jberthold · 2024-06-21T02:29:29Z

booster/library/Booster/Pattern/Rewrite.hs

@@ -331,7 +331,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                "Known true side conditions (won't check):" <+> pretty knownTrue

    unclearRequires <-
-        catMaybes <$> mapM (checkConstraint id notAppliedIfBottom) toCheck
+        catMaybes <$> mapM (checkConstraint id notAppliedIfBottom (Set.fromList knownTrue)) toCheck


knownTrue are just the requires clauses from the rule that syntactically occur in the path condition after substituting.
I think we want the entire path condition (pat.constraints) instead here, and it comes from the subject, so no substitutions are required.

Suggested change

catMaybes <$> mapM (checkConstraint id notAppliedIfBottom (Set.fromList knownTrue)) toCheck

catMaybes <$> mapM (checkConstraint id notAppliedIfBottom prior) toCheck

This means the argument can actually be fixed in the local checkConstraint definition but we can also keep them as an argument for clarity.

jberthold · 2024-06-21T02:29:46Z

booster/library/Booster/Pattern/Rewrite.hs

@@ -376,7 +376,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                Set.toList rule.ensures
        trivialIfBottom = RewriteRuleAppT $ pure Trivial
    newConstraints <-
-        catMaybes <$> mapM (checkConstraint id trivialIfBottom) ruleEnsures
+        catMaybes <$> mapM (checkConstraint id trivialIfBottom (Set.fromList knownTrue)) ruleEnsures


Suggested change

catMaybes <$> mapM (checkConstraint id trivialIfBottom (Set.fromList knownTrue)) ruleEnsures

catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures

jberthold · 2024-06-21T02:33:41Z

booster/library/Booster/Pattern/Rewrite.hs

        RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
        oldCache <- lift . RewriteT . lift $ get
        (simplified, cache) <-
            withContext CtxConstraint $
-                simplifyConstraint definition llvmApi smtSolver oldCache p
+                simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p


As mentioned, one could just use pat.constraints here...

Suggested change

simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p

simplifyConstraint definition llvmApi smtSolver oldCache pat.constraints p

jberthold · 2024-06-21T02:34:03Z

booster/library/Booster/Pattern/Rewrite.hs

        -- update cache
        lift . RewriteT . lift . modify $ const cache
-        -- TODO should we keep the traces? Or only on success?


jberthold · 2024-06-21T02:35:07Z

KEVM performance:

Test georgy-check-constraint-with-known time master-fb59a8493 time (georgy-check-constraint-with-known/master-fb59a8493) time
erc20/ds/balanceOf-spec.k 60.16 63.91 0.9413237365044594
erc20/ds/approve-failure-spec.k 70.64 73.41 0.962266721155156
kontrol/test-storetest-testaccesses-0-spec.k 84.24 77.61 1.085427135678392
TOTAL 215.04000000000002 214.93 1.0005117945377566

Maybe this did not have much impact because only the knownTrue rule requires were passed ...

geo2a · 2024-06-21T09:50:38Z

To my disappointment, there's still no difference:

Test	georgy-check-constraint-with-known time	master-fb59a8493 time	(georgy-check-constraint-with-known/master-fb59a8493) time
benchmarks/functional-spec.k	596.33	575.15	1.036825176041033
erc20/ds/balanceOf-spec.k	63.79	60.94	1.0467673121102725
erc20/ds/approve-success-spec.k	92.41	86.48	1.0685707678075855
erc20/ds/approve-failure-spec.k	71.99	67.09	1.073036220002981
erc20/ds/transfer-success-2-spec.k	94.19	86.76	1.0856385431074227
TOTAL	918.71	876.42	1.0482531206499168

jberthold

LGTM
Would be good to craft a simple integration test that demonstrates the utility...

jberthold · 2024-06-24T01:16:10Z

... a simple integration test that demonstrates the utility...

I was trying something related (but not quite sufficient) recently, using code like this:

  configuration
    <k> $PGM:Thing ~> .K </k>
    <i> 42 </i>
  rule <k>AA(X) => BB(X) ... </k>
       <i> I </i>
    requires X ==Int I
  rule AA(X) => CC(X) [owise]

I tested that we are able to rewrite AA(X) to BB(X) if side conditions imply (but not state syntactically) that X == 42.
Maybe we could test your change with an additional function f and f(X) ==Int I in the side condition, and simplification f(X) => X requires X ==Int 42. A bit contrived, though...

…aint-with-known

geo2a · 2024-07-09T08:06:25Z

@jberthold I've added two integration tests that make sure we use the path condition when trying simplifications:

the first test applies a simplification whose side condition is syntactically present in the path condition. I've checked that this test aborts on master;
the second test is a slight modification of the first one which actually needs SMT to infer the simplification's side condition from the path condition. This test aborts on both master and this PR. It will not abort anymore when we start using the solver when applying equations.

The change in #3953 introduced additional arguments to evaluation functions which allow callers to supply some "known true" predicates for the simplification and evaluation. However, doing so means that the cache will get populated with associations that might only be true if this known truth does not change. The case in point was a predicate being cached as "true" because of an earlier evaluation, and then _removed_ from the path condition. This change removes returning the cache from any inteface functions that take known truth arguments, and runs internal computations that modify the predicates with a fresh empty cache.

…ite (#4103) The change in #3953 introduced additional arguments to evaluation functions which allow callers to supply some "known true" predicates for the simplification and evaluation. However, doing so means that the cache will get populated with associations that might only be true if this known truth does not change. The case in point was a predicate being cached as "true" because of an earlier evaluation, and then _removed_ from the path condition (see added integration test). This change * refactors `checkConstraint` functions to fix the pattern constraints * skips the cache update if any additional "known truth" arguments were supplied to `checkConstraint`, and * runs internal computations that manipulate the predicates with a fresh empty cache. Furthermore, to avoid a significant performance penalty, we * simplify the pattern constraints once before starting to rewrite * only simplify the pattern _term_ during rewriting - the pattern constraints are already evaluated and stay the same - if a new constraint is added (by way of an `ensures`), this constraint is evaluated before adding it * At the end of the rewrite, we still simplify everything again (including the entire path condition). We are not using the SMT solver to detect a vacuous state at the start, though, could add that separately if desired. At the moment, the behaviour is largely the same as before (integration test expectations identical except for some evaluation in vacuous states). --------- Co-authored-by: github-actions <[email protected]>

Add known predicates to simplifier API

9afbc46

geo2a changed the title ~~Consider known predicates to Booster's simplifier API~~ Consider known predicates in Booster's simplifier API Jun 20, 2024

geo2a requested review from jberthold and goodlyrottenapple June 20, 2024 17:58

geo2a marked this pull request as ready for review June 20, 2024 17:58

jberthold reviewed Jun 21, 2024

View reviewed changes

Actually use the patterns constraints

3170762

jberthold approved these changes Jun 24, 2024

View reviewed changes

geo2a added 2 commits July 9, 2024 09:11

Merge remote-tracking branch 'origin/master' into georgy/check-constr…

a2f86a9

…aint-with-known

Add integration tests

1e56d5c

Typos

7e87f2c

geo2a requested a review from jberthold July 9, 2024 08:08

Only run test-use-path-condition-in-equations with booster-dev

93658a8

geo2a added the automerge label Jul 9, 2024

jberthold approved these changes Jul 9, 2024

View reviewed changes

Merge branch 'master' into georgy/check-constraint-with-known

cfb80b5

rv-jenkins merged commit 6862e0b into master Jul 9, 2024
6 checks passed

rv-jenkins deleted the georgy/check-constraint-with-known branch July 9, 2024 12:02

jberthold mentioned this pull request Apr 11, 2025

HOTFIX invalidate cache when modifying known predicates #4103

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Consider known predicates in Booster's simplifier API #3953

Consider known predicates in Booster's simplifier API #3953

Uh oh!

geo2a commented Jun 20, 2024 •

edited

Loading

Uh oh!

geo2a commented Jun 20, 2024

Uh oh!

jberthold Jun 21, 2024

Uh oh!

jberthold Jun 21, 2024

Uh oh!

geo2a Jun 21, 2024

Uh oh!

jberthold Jun 21, 2024

Uh oh!

jberthold Jun 21, 2024

Uh oh!

jberthold Jun 21, 2024

Uh oh!

jberthold commented Jun 21, 2024

Uh oh!

geo2a commented Jun 21, 2024 •

edited

Loading

Uh oh!

jberthold left a comment

Uh oh!

jberthold commented Jun 24, 2024

Uh oh!

geo2a commented Jul 9, 2024 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

	catMaybes <$> mapM (checkConstraint id notAppliedIfBottom (Set.fromList knownTrue)) toCheck
	catMaybes <$> mapM (checkConstraint id notAppliedIfBottom prior) toCheck

	catMaybes <$> mapM (checkConstraint id trivialIfBottom (Set.fromList knownTrue)) ruleEnsures
	catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures

	simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p
	simplifyConstraint definition llvmApi smtSolver oldCache pat.constraints p

Consider known predicates in Booster's simplifier API #3953

Consider known predicates in Booster's simplifier API #3953

Uh oh!

Conversation

geo2a commented Jun 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

geo2a commented Jun 20, 2024

Uh oh!

jberthold Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

jberthold Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

geo2a Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

jberthold Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

jberthold Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

jberthold Jun 21, 2024

Choose a reason for hiding this comment

Uh oh!

jberthold commented Jun 21, 2024

Uh oh!

geo2a commented Jun 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

jberthold commented Jun 24, 2024

Uh oh!

geo2a commented Jul 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

geo2a commented Jun 20, 2024 •

edited

Loading

geo2a commented Jun 21, 2024 •

edited

Loading

geo2a commented Jul 9, 2024 •

edited

Loading