search

runtimeverification / haskell-backend

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

Explore the remainder branch when Booster is uncertain about rewrite rule conditions #3960

Open geo2a opened 3 months ago

geo2a commented 3 months ago

Part of #3956

geo2a commented 2 months ago

KEVM performance at 7bf75ea: 

| Test                                                                    | georgy-booster-remainders time | master-3b90f2b79 time | (georgy-booster-remainders/master-3b90f2b79) time
|-------------------------------------------------------------------------|--------------------------------|-----------------------|---------------------------------------------------
| mcd/flopper-dent-guy-same-pass-rough-spec.k                             | 923.28                         | 971.42                | 0.9504436803854152
| mcd/end-subuu-pass-spec.k                                               | 58.38                          | 61.04                 | 0.956422018348624
| mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k                   | 1012.77                        | 1056.91               | 0.9582367467428635
| kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k | 57.41                          | 59.82                 | 0.95971247074557
| mcd/flopper-tick-pass-rough-spec.k                                      | 217.44                         | 225.81                | 0.9629334396173774
| erc20/hkg/transferFrom-success-2-spec.k                                 | 60.72                          | 58.62                 | 1.0358239508700102
| kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k    | 77.34                          | 74.53                 | 1.0377029384140615
| erc20/ds/transferFrom-failure-1-c-spec.k                                | 118.03                         | 113.72                | 1.0379001055223356
| kontrol/test-allowchangestest-testallow_fail-0-spec.k                   | 54.75                          | 52.66                 | 1.0396885681731864
| kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k     | 53.58                          | 51.44                 | 1.041601866251944
| erc20/hkg/transferFrom-failure-1-spec.k                                 | 94.08                          | 89.88                 | 1.046728971962617
| mcd/end-cash-pass-rough-spec.k                                          | 229.3                          | 218.66                | 1.0486600201225649
| erc20/ds/transferFrom-failure-1-b-spec.k                                | 151.48                         | 144.06                | 1.0515063168124392
| erc20/ds/transfer-failure-1-a-spec.k                                    | 75.35                          | 71.45                 | 1.0545836249125262
| benchmarks/ecrecoverloop00-sig1-invalid-spec.k                          | 118.31                         | 109.35                | 1.0819387288523092
| TOTAL                                                                   | 3302.22                        | 3359.3699999999994    | 0.9829878816563821