runtimeverification / haskell-backend

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

add cases for unevaluated keys to MAP hooks #3964

Closed jberthold closed 3 months ago

jberthold commented 3 months ago

Some of the MAP hooks were missing cases for an unevaluated key argument (they were assuming that the argument would already be fully evaluated when the hook is called). In these cases, the hooks should typically return Nothing instead of returning a result.

jberthold commented 3 months ago
Test HOTFIX-lookup-hooks-indeterminate-on-unevaluated-key time master-81762ef9d time (HOTFIX-lookup-hooks-indeterminate-on-unevaluated-key/master-81762ef9d) time
kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k 79.18 114.26 0.6929809207071591
benchmarks/keccak00-spec.k 84.03 116.17 0.7233364896272704
erc20/ds/transfer-success-2-spec.k 98.72 127.46 0.7745174956849208
benchmarks/overflow00-nooverflow-spec.k 76.44 95.83 0.7976625273922571
erc20/ds/transfer-failure-1-c-spec.k 76.61 91.95 0.8331702011963023
kontrol/test-allowchangestest-testallow-0-spec.k 39.82 47.77 0.833577559137534
erc20/hkg/totalSupply-spec.k 36.74 44.05 0.8340522133938707
benchmarks/storagevar02-nooverflow-spec.k 38.81 46.1 0.8418655097613883
mcd/dai-adduu-fail-rough-spec.k 42.13 49.62 0.8490528012898025
erc20/ds/transfer-success-1-spec.k 102.34 119.54 0.8561151079136691
kontrol/test-storetest-teststoreload-0-spec.k 40.84 47.61 0.8578029825666877
erc20/ds/approve-success-spec.k 47.73 55.31 0.8629542578195624
mcd/dsvalue-read-pass-spec.k 47.61 55.0 0.8656363636363636
kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k 107.62 124.06 0.8674834757375464
kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k 80.24 92.41 0.8683042960718537
kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k 46.45 53.26 0.8721366879459257
erc20/ds/transferFrom-success-2-spec.k 53.99 61.85 0.8729183508488279
erc20/ds/transferFrom-failure-2-a-spec.k 54.53 61.89 0.8810793343027953
benchmarks/ecrecoverloop00-sigs-valid-spec.k 52.79 59.86 0.8818910791847644
functional/abi-spec.k 65.86 73.1 0.9009575923392613
examples/sum-to-n-foundry-spec.k 73.84 81.38 0.9073482428115017
mcd/functional-spec.k 810.57 874.17 0.9272452726586363
functional/lemmas-spec.k 865.57 926.75 0.9339843539250068
mcd/vow-flog-fail-rough-spec.k 106.63 114.02 0.9351868093316962
functional/storageRoot-spec.k 116.99 124.13 0.9424796584226215
kontrol/test-expectcalltest-testexpectregularcall-0-spec.k 76.74 80.94 0.9481097108969607
mcd/flopper-kick-pass-rough-spec.k 105.32 110.91 0.9495987737805428
erc20/ds/transfer-failure-1-b-spec.k 142.65 149.91 0.9515709425655394
benchmarks/ecrecoverloop02-sig0-invalid-spec.k 168.57 175.88 0.9584375710711849
functional/lemmas-no-smt-spec.k 163.52 170.52 0.9589490968801314
mcd/flopper-tick-pass-rough-spec.k 156.03 162.54 0.9599483204134367
mcd/flapper-yank-pass-rough-spec.k 126.11 131.19 0.9612775363975913
mcd/flopper-dent-guy-same-pass-rough-spec.k 525.71 546.01 0.9628211937510303
examples/erc721-spec.md 129.91 123.73 1.0499474662571728
kontrol/test-emitcontracttest-testexpectemit-0-spec.k 83.4 78.47 1.0628265579202243
TOTAL 4924.04 5387.65 0.9139494956056908