Add CSE verification script with KCFG minimization and K module generation #668
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Add 5 tests with varying function call counts (1, 10, 100, 1000, 10000) - Tests evaluate composable symbolic execution with repeated function calls - All tests use loop-based implementation for scalability - Set depth limit to 50 for controlled symbolic execution 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <[email protected]>
- Added pytest-timeout dependency to dev requirements - Set default 300s timeout for test-integration target in Makefile - Allows overriding timeout via TEST_ARGS parameter 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <[email protected]>
This script demonstrates how to: - Use KMIR to verify Rust functions with arbitrary entry points - Generate and save APRProof objects - Create proof show output for visualization - Support both add1 and main function verification The script correctly handles both passing (main with assertions) and failing/stuck (add1 with potential overflow) verification cases. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <[email protected]>
Added new features to the verification script: - KCFG minimization using apr_proof.minimize_kcfg() to reduce redundant nodes - K module generation from minimized KCFG using to_module() - Save both original and minimized proof show outputs - Track minimization statistics in summary file Results show: - add1 function: reduced from 7 nodes/3 edges to 6 nodes/2 edges - main function: already optimal at 3 nodes/1 edge (no reduction) - Generated K modules saved as .k files for reuse This enhancement enables more efficient proof representation and provides reusable K modules for future verification work. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <[email protected]>
Changed from Python object string representation to proper K syntax: - Use kmir.pretty_print() to format KFlatModule as valid K code - Reduced file sizes significantly (80KB→19KB, 53KB→13KB) - Generated modules now follow K language syntax with proper formatting - Modules can be directly imported/used in other K specifications The generated .k files now contain valid K module definitions with: - Proper module/endmodule structure - Correctly formatted rules with labels and priorities - K cell structure with proper XML-like notation - Valid K term syntax instead of Python repr strings 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <[email protected]>
|
|
Here is the performance with no-summary rule of 300.10s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-10000time-haskell]
300.07s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-1000time-haskell]
234.22s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-100time-haskell]
25.33s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-10time-haskell]
5.38s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-1time-haskell]
3.23s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-100time-llvm]
3.09s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-1time-llvm]
2.96s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-10time-llvm]
2.33s call src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-1000time-llvm]
(18 durations < 0.005s hidden. Use -vv to show these durations.)
====================================================== short test summary info =======================================================
FAILED src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-1000time-haskell] - Failed: Timeout (>300.0s) from pytest-timeout.
FAILED src/tests/integration/test_integration.py::test_exec_smir[cse-call-add1-10000time-haskell] - Failed: Timeout (>300.0s) from pytest-timeout.SETUP: Macbook Air, Apple M2, 16GB, Sequoia 15.6 |
|
Execution time without summary rule: |
|
Execution time with summary rule |
|
Execution result without pretty_print for llvm (add1 summary): |
|
Execution result without pretty_print for llvm (without add1 summary): |
|
save |
|
|
What if we summarize the main of the |
|
Actually, for the summarized program for this concrete ouput value. The time for run it is just use cat to see it? |
|
run with main summary. !!!!!! |
|
run without main summary: |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds a Python script for verifying Rust functions using KMIR, with support for KCFG minimization and K module generation.
Features
mainTest Results
Tested with
cse_call_add1_1time.rs:add1function:mainfunction:Usage
Output Files
The script generates the following in
add1_proof/:.show- Original proof show output.minimized.show- Minimized proof show output.k- K module for reuse.summary- Verification statisticsImplementation Details
APRProof.minimize_kcfg()to reduce proof complexityKCFG.to_module()with proper defunctionalization🤖 Generated with Claude Code