runtimeverification / haskell-backend

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

Tweak abort logging and counting script, log shutdown using logger #3919

Closed jberthold closed 3 months ago

jberthold commented 3 months ago

Changes to abort logging and counting tool:

Related: #3865

Changes to shutdown

jberthold commented 3 months ago

Most importantly, the script was previously counting match-related aborts that could be recovered from by simplifying the configuration. The amount of data is also greatly reduced by not logging function and simplification details (which may be added to the log by manually passing additional --log-context options).

For comparison, two runs with the same tarball produce different results because fo the mis-count:

jost@freshcode-1:~/work/RV/code/haskell-backend2/scratch/mx-performance-things/fallbacks-20240603$ time ../../../../haskell-backend/.build/kore/bin/count-aborts prior-run/test_change_quorum-spec.json.tar.gz.json.log | grep rewrite 
rewrite ff5975a968f5f4dbd4d8380d21feb3d5ce2bc8631d1f09ec8920af8a3d8eb1ff | ...source/mx-semantics/auto-allocate.md :  (42, 10) | 2102
rewrite 29e54ddd82765fabf32f4287f678edf13b0a29035f3491a822fec5abc1fea12a | ...source/wasm-semantics/wasm.md :  (397, 10) | 1581
rewrite 589c3c20e4b836d6dda752ed925c0b1ea260ac2522ed44713f206bbbe53eeca5 | ...source/wasm-semantics/wasm.md :  (1183, 10) | 1170
rewrite c72d9e5a57bbd608d0d205dc04fb8ef46f4442c4354c2bfd68841692cade93f9 | ...source/wasm-semantics/wasm.md :  (558, 10) | 1170
rewrite af4b7505aec3fe3f670ded8ee7ff1a5db3df064c2cbae4fc97579bdfa790482b | ...source/wasm-semantics/wasm.md :  (1457, 10) | 536
rewrite d728c377ba2e1484cdd58093d1652c409a946801260a292eac621ea5d219396b | ...source/wasm-semantics/wasm.md :  (1398, 10) | 527
rewrite b8c34b79ea287b16d9b42a374de2613784fb6c2dbda8ae4dc89d4e88c4cf5c3b | ...source/wasm-semantics/wasm.md :  (572, 10) | 469
rewrite 5d0f59f4d64c8780d37cd47cbb134501540169dbac8e3ac78a3978bcc635187a | ...source/wasm-semantics/wasm.md :  (512, 10) | 437
rewrite bceb217a6e17ecafb919b8109ad5c3ea632747ada8f0bbbde1bc6985a200935c | ...source/wasm-semantics/wasm.md :  (1386, 10) | 341
rewrite d7a7e5db27c3cf58580d7714aebd716bcb15fe16cb667c982555dfc1f6e446d9 | ...source/wasm-semantics/wasm.md :  (581, 10) | 319
rewrite 28ade7eff892e9c79b1f59c93f24a7804182c62f25227f9b2629616d3da5dbe7 | ...source/wasm-semantics/wasm.md :  (448, 10) | 312
rewrite 74f5a04fb4c61838acaf800052352badf0ec7b6805fa2f4a7301a66657434d26 | ...source/wasm-semantics/wasm.md :  (417, 10) | 226
rewrite 75b1dcd214333bf09ae82b54e1fe4c3fb075704800a3e8d89542a19bb21ab800 | ...source/wasm-semantics/wasm.md :  (505, 10) | 218
rewrite be5509e051c9487c2a31f898b8d6743776729ded22eb877cc5d64cbe3f2fadcc | ...source/wasm-semantics/wasm.md :  (1437, 10) | 206
rewrite da0394cab0e7aa7f03a5662942079432ca7000b6373de193a95c65edf5eb7975 | ...source/wasm-semantics/wasm.md :  (576, 10) | 66
rewrite 153405476c0d3b493312849996a3ad27151797b75d4b2173baf8c7a02af1bc39 | MANBUFOPS.getBuffer | 26
rewrite 68622a8a41b04da93c8b57cb4fff531e5634381a34d22d902a2379cbe593ea71 | ...source/wasm-semantics/wasm.md :  (408, 10) | 18
rewrite 26f0e15242677a31d506bb8e66d637cb92bfe9cfe941b3c6d2e8d0324fd9edd2 | ...mx-semantics/vmhooks/manBufOps.md :  (228, 10) | 9
rewrite 1d98dd223d027f2d7a2b5bc8dabed7597a5791e948ea732b301633b9a5996fd1 | ...mx-semantics/vmhooks/baseOps.md :  (435, 10) | 6
rewrite 4eb1a24ea67c9b325477de904cbace6716117c7d3f394e301fc05c49e5eaf61c | ...source/mx-semantics/elrond-config.md :  (188, 10) | 6
rewrite aa32a51d9daa06aa2f65106bec515056279b56a33ca5cf7914c50ed1a463f956 | ...source/wasm-semantics/wasm.md :  (451, 10) | 5
rewrite e66f1aa4d1a7bae76c2707e9caed85649b9bb0ee5e8a0eaec0f64456d74bed45 | ...source/wasm-semantics/wasm.md :  (521, 10) | 5
rewrite 4d0a1cf4237a2fba90b2be08160e522d4b2edbb62da6d9a090f3ed20ce47e344 | ELROND-NODE.appendToOutAccount | 4
rewrite a5ba04c4ac0886d6751367ea5eeb8476425d8ba5f6727ab0499a4093a7c4e6d7 | ELROND-CONFIG.exception-skip | 3
rewrite a63eed8df4e8e31ce04115aeeb313ee5a80c72d82c710419ebfb322f981e6929 | ELROND-CONFIG.storageLoadFromAddress | 3
rewrite cf8e6d563b0735c2d618c770c16bf98d453a538ca95971e8f15907f00c7673ea | KASMER.startPrank | 3
rewrite 3781ba3dcc9fcdff3234b1d581638a050fc0b1744bd9a2da8a98655c9ae9d446 | ELROND-CONFIG.memLoad-zero-length | 2
rewrite 404dab22ab8f6af3e249356a1ffd0ffb339f3877b44a6cb929ee332bbc9bfc16 | ...source/wasm-semantics/wasm.md :  (388, 10) | 2
rewrite 34ac4f4a345df7eae0f5920f9b5aa40224e081e25c5e79c78255732dee155264 | ...mx-semantics/vmhooks/smallIntOps.md :  (55, 10) | 1
rewrite 746198e7c90e94a9ca8830643317ce696713fceb7738ba97e7c3602e71534595 | ...source/mx-semantics/elrond-config.md :  (307, 10) | 1
rewrite 99eca3b8ea113990099fcd98d5d274c2a5ba2e63240c9fbee822ec0da0113a1f | ELROND-CONFIG.callContract | 1
rewrite eda1fbab65ac61079496e9e0cc5cda77e823190f5673bceca139c7711d0af946 | MANDOS.callTxAux | 1
rewrite f20bc972b88361f0aa88e0840f26525d49d8df6e0dd89c3f6bc28344ccc23fc9 | ...source/wasm-semantics/wasm.md :  (428, 10) | 1

real    1m30.658s
user    1m28.060s
sys 0m2.709s
jost@freshcode-1:~/work/RV/code/haskell-backend2/scratch/mx-performance-things/fallbacks-20240603$ time ../../../.build/kore/bin/count-aborts test_change_quorum-spec.json.tar.gz.json.log 
| rewrite 153405476c0d3b493312849996a3ad27151797b75d4b2173baf8c7a02af1bc39 | MANBUFOPS.getBuffer | condition | 26
| rewrite 5d0f59f4d64c8780d37cd47cbb134501540169dbac8e3ac78a3978bcc635187a | ...source/wasm-semantics/wasm.md :  (512, 10) | condition | 26
| rewrite 26f0e15242677a31d506bb8e66d637cb92bfe9cfe941b3c6d2e8d0324fd9edd2 | ...mx-semantics/vmhooks/manBufOps.md :  (228, 10) | condition | 9
| rewrite 4eb1a24ea67c9b325477de904cbace6716117c7d3f394e301fc05c49e5eaf61c | ...source/mx-semantics/elrond-config.md :  (188, 10) | condition | 6
| rewrite 29e54ddd82765fabf32f4287f678edf13b0a29035f3491a822fec5abc1fea12a | ...source/wasm-semantics/wasm.md :  (397, 10) | match | 5
| rewrite e66f1aa4d1a7bae76c2707e9caed85649b9bb0ee5e8a0eaec0f64456d74bed45 | ...source/wasm-semantics/wasm.md :  (521, 10) | definedness | 5
| rewrite 1d98dd223d027f2d7a2b5bc8dabed7597a5791e948ea732b301633b9a5996fd1 | ...mx-semantics/vmhooks/baseOps.md :  (435, 10) | match | 3
| rewrite 404dab22ab8f6af3e249356a1ffd0ffb339f3877b44a6cb929ee332bbc9bfc16 | ...source/wasm-semantics/wasm.md :  (388, 10) | definedness | 2
| rewrite 34ac4f4a345df7eae0f5920f9b5aa40224e081e25c5e79c78255732dee155264 | ...mx-semantics/vmhooks/smallIntOps.md :  (55, 10) | definedness | 1
| rewrite 3781ba3dcc9fcdff3234b1d581638a050fc0b1744bd9a2da8a98655c9ae9d446 | ELROND-CONFIG.memLoad-zero-length | match | 1
| rewrite 746198e7c90e94a9ca8830643317ce696713fceb7738ba97e7c3602e71534595 | ...source/mx-semantics/elrond-config.md :  (307, 10) | condition | 1

real    0m1.386s
user    0m1.246s
sys 0m0.140s