search

runtimeverification / haskell-backend

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

Retry harder when stopping rewriting due to `RuleConditionUnclear` #4000

Closed geo2a closed 3 months ago

geo2a commented 3 months ago

KEVM performance at f01726a

| Test                                                  | georgy-sanitise-cache time | master-f0b3596f9 time | (georgy-sanitise-cache/master-f0b3596f9) time
|-------------------------------------------------------|----------------------------|-----------------------|-----------------------------------------------
| mcd/end-cash-pass-rough-spec.k                        | 244.33                     | 332.39                | 0.7350702488041158
| erc20/ds/transferFrom-success-2-spec.k                | 65.74                      | 82.78                 | 0.7941531770959168
| erc20/ds/transferFrom-success-1-spec.k                | 71.14                      | 86.91                 | 0.8185479231388794
| mcd/flapper-yank-pass-rough-spec.k                    | 195.12                     | 237.33                | 0.8221463784603716
| erc20/ds/transfer-success-2-spec.k                    | 60.05                      | 68.95                 | 0.8709209572153734
| mcd/flopper-kick-pass-rough-spec.k                    | 144.0                      | 164.71                | 0.8742638576892721
| mcd/end-pack-pass-rough-spec.k                        | 162.36                     | 182.1                 | 0.8915980230642505
| erc20/ds/transfer-success-1-spec.k                    | 62.48                      | 69.68                 | 0.896670493685419
| benchmarks/staticloop00-a0lt10-spec.k                 | 49.17                      | 53.51                 | 0.9188936647355636
| erc20/hkg/transfer-success-1-spec.k                   | 52.57                      | 56.35                 | 0.9329192546583851
| benchmarks/requires01-a0le0-spec.k                    | 46.51                      | 49.69                 | 0.9360032199637754
| mcd/flopper-dent-guy-same-pass-rough-spec.k           | 902.64                     | 945.52                | 0.9546492935104492
| erc20/ds/transfer-failure-1-a-spec.k                  | 71.8                       | 75.07                 | 0.9564406553883043
| erc20/ds/transfer-failure-1-b-spec.k                  | 93.17                      | 97.41                 | 0.956472641412586
| mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k | 1033.79                    | 1079.75               | 0.9574345913405881
| mcd/pot-join-pass-rough-spec.k                        | 240.14                     | 249.48                | 0.9625621292287959
| erc20/hkg/transferFrom-success-2-spec.k               | 62.2                       | 64.51                 | 0.9641915982018291
| benchmarks/encodepacked-keccak01-spec.k               | 50.41                      | 48.41                 | 1.0413137781450115
| benchmarks/staticarray00-spec.k                       | 49.23                      | 47.12                 | 1.044779286926995
| mcd/vow-fess-fail-rough-spec.k                        | 146.17                     | 135.79                | 1.0764415641799838
| TOTAL                                                 | 3803.0199999999995         | 4127.46               | 0.92139475609697
geo2a commented 3 months ago

Closed in favor of https://github.com/runtimeverification/haskell-backend/pull/4002