search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
204 stars 39 forks source link

Consider known predicates in Booster's simplifier API #3953

Open geo2a opened 1 week ago

geo2a commented 1 week ago

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:

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 commented 1 week ago
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 commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

... 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...