Gold-standard typed session rewrite for radare2 integration#38
Open
0verflowme wants to merge 40 commits into
Open
Gold-standard typed session rewrite for radare2 integration#380verflowme wants to merge 40 commits into
0verflowme wants to merge 40 commits into
Conversation
- Introduced a new `spec` module to define exploration specifications, including predicates, input configurations, and budget constraints. - Enhanced the `PathExplorer` to support running exploration specifications, allowing for more controlled symbolic execution paths. - Added functionality to handle symbolic file descriptor inputs, enabling the exploration of paths based on external input streams. - Updated tests to validate the new exploration specification features, ensuring correct behavior in symbolic execution scenarios. This commit enhances the symbolic execution framework by allowing users to define and run detailed exploration strategies.
- Updated dependencies in Cargo.lock, including new packages such as `anes`, `cast`, `ciborium`, and `criterion`, along with their respective versions and checksums. - Introduced a new benchmark for symbolic execution in `r2sym`, allowing for performance evaluation of hot paths in symbolic execution. - Enhanced the `ExploreConfig` structure to include a `max_completed_paths` option, providing better control over exploration limits. - Added tests to validate the new exploration capabilities and ensure correct behavior in symbolic execution scenarios. This commit improves the dependency management and expands the symbolic execution framework's capabilities, facilitating more efficient exploration strategies.
- Introduced `VmUnaryOp` and `VmBinaryOp` enums to represent unary and binary operations in the symbolic execution context. - Updated `VmValueExpr` to support new operation types, including rendering logic for unary and binary expressions. - Enhanced the `evaluate_u64` method to handle new binary operations, improving the evaluation capabilities of symbolic expressions. - Refactored related code to integrate new operations into the existing symbolic execution framework. This commit expands the symbolic execution capabilities, allowing for more complex expressions and operations to be evaluated during analysis.
- Added functions to format VM guarded exits and memory conditions, improving the representation of symbolic execution states. - Updated the Decompiler to include counts for likely and heuristic transfers, enhancing the semantic analysis capabilities. - Refactored output formatting to include new metrics such as exact exit guards and total memory effects, providing more detailed insights during analysis. This commit expands the symbolic execution framework, allowing for better tracking and representation of VM states and their associated conditions.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e13459cb75
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…-r2sleigh # Conflicts: # Cargo.lock
0verflowme
force-pushed
the
codex/gold-standard-r2sleigh
branch
13 times, most recently
from
6331273 to
c6141c1
Compare
0verflowme
force-pushed
the
codex/gold-standard-r2sleigh
branch
5 times, most recently
from
e11406f to
3cc719d
Compare
0verflowme
force-pushed
the
codex/gold-standard-r2sleigh
branch
from
3cc719d to
3fd4bfb
Compare
Add engine-owned routing and cache policy, expand native worker summaries and type projection, improve summary-backed rendering and public-output hygiene, and extend the benchmark harness for broad Coreutils validation.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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
R2SleighSessionInput, typed session results, and mutation plansPairing requirement
This PR requires the matching radare2 seam branch:
0verflowme/radare2:codex/gold-standard-radare2-seam.Compatibility note
Low-level debug command compatibility is intentionally not preserved; public behavior is the workflow-oriented surface plus debug namespace coverage.
Validation
Z3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo test --workspace --features all-archsZ3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo clippy -p r2ssa --all-targets -- -D warningsZ3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo clippy -p r2sym --all-targets -- -D warningsZ3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo clippy -p r2types --all-targets -- -D warningsZ3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo clippy -p r2dec --all-targets -- -D warningsZ3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h Z3_LIBRARY_PATH_OVERRIDE=/opt/homebrew/lib cargo clippy -p r2sleigh-plugin --features all-archs -- -D warningsmake -C r2plugin RUST_FEATURES=all-archs installPATH="/usr/local/bin:/opt/homebrew/bin:$PATH" make -C tests/r2r run R2R_TIMEOUT=120 R2R_JOBS=1R2R_RADARE2=/Users/priyanshu/code/radare2/binr/radare2/radare2 cargo e2e-testgit diff --check