This milestone improved the performance of Skribe's coverage tracking and added several usability enhancements.
Performance Improvements
In Milestone 4: Coverage Metrics, coverage data was stored in large byte arrays, and K made a full copy of the array on every mutation during concrete execution. This made coverage tracking slow for larger contracts.
runtimeverification/skribe#95 replaces the byte array, which marked every executed byte offset individually, with a set of executed ranges. Since K's set data type is persistent, mutations no longer trigger large copies.
runtimeverification/llvm-backend#1218 fixed a bug in the upstream kore_block_dump output that had required a workaround in Skribe since an earlier milestone. The dependency updates in runtimeverification/skribe#96 bring this fix in, allowing the workaround to be removed.
The combined effect of these changes is significant. Benchmarking 100 fuzzer iterations against the test_end_to_end_intense endpoint of the 9lives smart contract (#5) shows a ~40% reduction in runtime for the LibAFL-based fuzzer with coverage enabled, dropping from 682s to 389s compared to the previous milestone.
Usability Improvements
runtimeverification/skribe#93 adds a --deadline option to skribe run, letting users cap the time spent on each fuzzer iteration for the Python fuzzer.
runtimeverification/skribe#94 adds a --fuzz-spec option to skribe run, allowing users to supply a pre-computed specification file to the Python fuzzer instead of having Skribe derive one automatically at startup. This is useful in workflows where the specification is stable across runs and recomputing it each time is unnecessary overhead.
runtimeverification/skribe#97 makes coverage tracking opt-in via a --coverage flag (disabled by default) for all three fuzzers. Runs that do not need coverage feedback pay little to no cost for it.
Future Work
The main remaining performance target is eliminating a costly round trip in the fuzzer hot path. Currently, after each execution step, the resulting kllvm::Block is converted back to a kore::Pattern by first serializing it to text and then parsing that text back. A direct kllvm::Block -> kllvm::Pattern conversion is already implemented, so if coverage extraction and exit code reading could be made to work directly on kllvm::Pattern or kllvm::Block, the serialization and parsing steps could be eliminated entirely. Alternatively, a de-marshalling step should be implemented from kllvm::Block or kllvm::Pattern into kore::Pattern, which would equally avoid the text round trip. Either approach requires upstream work in kframework-rs.
This milestone improved the performance of Skribe's coverage tracking and added several usability enhancements.
Performance Improvements
In
Milestone 4: Coverage Metrics, coverage data was stored in large byte arrays, and K made a full copy of the array on every mutation during concrete execution. This made coverage tracking slow for larger contracts.runtimeverification/skribe#95 replaces the byte array, which marked every executed byte offset individually, with a set of executed ranges. Since K's set data type is persistent, mutations no longer trigger large copies.
runtimeverification/llvm-backend#1218 fixed a bug in the upstream
kore_block_dumpoutput that had required a workaround in Skribe since an earlier milestone. The dependency updates in runtimeverification/skribe#96 bring this fix in, allowing the workaround to be removed.The combined effect of these changes is significant. Benchmarking 100 fuzzer iterations against the
test_end_to_end_intenseendpoint of the9livessmart contract (#5) shows a ~40% reduction in runtime for the LibAFL-based fuzzer with coverage enabled, dropping from 682s to 389s compared to the previous milestone.Usability Improvements
runtimeverification/skribe#93 adds a
--deadlineoption toskribe run, letting users cap the time spent on each fuzzer iteration for the Python fuzzer.runtimeverification/skribe#94 adds a
--fuzz-specoption toskribe run, allowing users to supply a pre-computed specification file to the Python fuzzer instead of having Skribe derive one automatically at startup. This is useful in workflows where the specification is stable across runs and recomputing it each time is unnecessary overhead.runtimeverification/skribe#97 makes coverage tracking opt-in via a
--coverageflag (disabled by default) for all three fuzzers. Runs that do not need coverage feedback pay little to no cost for it.Future Work
The main remaining performance target is eliminating a costly round trip in the fuzzer hot path. Currently, after each execution step, the resulting
kllvm::Blockis converted back to akore::Patternby first serializing it to text and then parsing that text back. A directkllvm::Block -> kllvm::Patternconversion is already implemented, so if coverage extraction and exit code reading could be made to work directly onkllvm::Patternorkllvm::Block, the serialization and parsing steps could be eliminated entirely. Alternatively, a de-marshalling step should be implemented fromkllvm::Blockorkllvm::Patternintokore::Pattern, which would equally avoid the text round trip. Either approach requires upstream work inkframework-rs.