search

runtimeverification / hs-backend-booster

Accelerates K Framework's Haskell backend
BSD 3-Clause "New" or "Revised" License
7 stars 0 forks source link

Separate llvm pass from equation evaluator #543

Closed jberthold closed 7 months ago

jberthold commented 8 months ago

This PR changes the iterateEquations procedure to first evaluate all suitable (concrete, unevaluated, evaluatable) subterms using the LLVM library (if one is provided), before simplifying and evaluating the term using equations. Two separate caches are necessary to store the prior results.

Built-in hook evaluation and equation-based evaluation are still combined (trying hooks first) because both should be done bottom-up while the LLVM-based evaluation should traverse top-down (to cut the traversal).

Related to runtimeverification/haskell-backend#3772 (and runtimeverification/haskell-backend#3767 )

jberthold commented 8 months ago

KEVM results (v1.0.478)

Test 517-EXPERIMENT-separate-llvm-pass-from-equation-evaluator time master-cd8bac1 time (517-EXPERIMENT-separate-llvm-pass-from-equation-evaluator/master-cd8bac1) time
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k 40.93 106.77 0.38334738222347103
kontrol/test-allowchangestest-testallow_fail-0-spec.k 43.38 112.29 0.38632113278119157
kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k 55.44 57.83 0.9586719695659692
kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k 112.24 45.51 2.4662711491979783
kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k 109.79 41.55 2.6423586040914566
TOTAL 361.78 363.95 0.9940376425333152
jberthold commented 8 months ago

kontrol measurements (v0.1.182)

Test 517-EXPERIMENT-separate-llvm-pass-from-equation-evaluator time master-cd8bac1 time (517-EXPERIMENT-separate-llvm-pass-from-equation-evaluator/master-cd8bac1) time
SymbolicStorageTest.testFail_SymbolicStorage(uint256) 194.61 210.4 0.9249524714828897
SymbolicStorageTest.testFail_SymbolicStorage1(uint256) 276.91 263.42 1.0512109938501253
TOTAL 471.52 473.82 0.9951458359714659