geo2a
commented
2 months ago KEVM performance:
| Test | georgy-dont-throw-away-solver time | master-613cb4984 time | (georgy-dont-throw-away-solver/master-613cb4984) time
|---------------------------------------------------------------------|------------------------------------|-----------------------|-------------------------------------------------------
| benchmarks/ecrecoverloop02-sig1-invalid-spec.k | 114.97 | 274.06 | 0.419506677369919
| benchmarks/ecrecoverloop02-sigs-valid-spec.k | 119.43 | 281.42 | 0.4243834837609267
| benchmarks/ecrecoverloop02-sig0-invalid-spec.k | 92.41 | 159.5 | 0.5793730407523511
| mcd/end-cash-pass-rough-spec.k | 221.76 | 331.79 | 0.6683745742789113
| erc20/ds/transferFrom-success-1-spec.k | 69.13 | 87.53 | 0.7897863589626413
| erc20/ds/transferFrom-success-2-spec.k | 65.74 | 82.67 | 0.795209870569735
| mcd/flopper-kick-pass-rough-spec.k | 133.2 | 164.28 | 0.8108108108108107
| mcd/flapper-yank-pass-rough-spec.k | 198.53 | 235.58 | 0.842728584769505
| erc20/ds/transfer-success-2-spec.k | 60.21 | 70.71 | 0.8515061518879933
| erc20/ds/transfer-success-1-spec.k | 61.01 | 70.55 | 0.864776754075124
| mcd/end-pack-pass-rough-spec.k | 162.92 | 181.61 | 0.8970871648037001
| erc20/hkg/transferFrom-success-2-spec.k | 58.96 | 63.95 | 0.9219702892885067
| benchmarks/staticloop00-a0lt10-spec.k | 50.58 | 54.45 | 0.9289256198347107
| mcd/cat-file-addr-pass-rough-spec.k | 57.82 | 62.24 | 0.9289845758354756
| erc20/ds/approve-success-spec.k | 55.46 | 59.3 | 0.9352445193929174
| erc20/ds/transferFrom-failure-1-b-spec.k | 145.94 | 153.72 | 0.9493884985688265
| erc20/hkg/transferFrom-success-1-spec.k | 63.86 | 67.17 | 0.9507220485335715
| erc20/ds/transferFrom-failure-1-c-spec.k | 113.2 | 118.57 | 0.9547102977144304
| erc20/hkg/approve-spec.k | 49.74 | 51.99 | 0.9567224466243508
| erc20/ds/transfer-failure-1-b-spec.k | 92.34 | 96.45 | 0.9573872472783825
| erc20/ds/transferFrom-failure-2-a-spec.k | 75.53 | 78.26 | 0.9651162790697674
| benchmarks/encodepacked-keccak01-spec.k | 50.21 | 48.5 | 1.0352577319587628
| kontrol/test-storetest-teststoreload-0-spec.k | 52.86 | 50.98 | 1.0368772067477443
| kontrol/test-countertest-testincrement-0-spec.k | 100.18 | 96.51 | 1.0380271474458604
| mcd/dsvalue-read-pass-summarize-spec.k | 60.17 | 57.85 | 1.040103716508211
| examples/storage-spec.md | 92.32 | 88.65 | 1.0413987591652565
| kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k | 52.56 | 50.01 | 1.0509898020395922
| benchmarks/staticarray00-spec.k | 49.39 | 46.64 | 1.0589622641509433
| TOTAL | 2520.43 | 3184.94 | 0.7913587069144159
When processing an execute request, we start z3 in
JsonRpc.hsand pass it toperformRewrite. However, we then actually start rewriting without a solver. This PR makes sire the initial state inperformRewriteactually is initialized with a solver.