Implement exploration specification support in symbolic execution#36
Implement exploration specification support in symbolic execution#360verflowme wants to merge 10 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.
![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: 1299784e22
ℹ️ 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".
| let can_zero_extend = | ||
| candidate_low == requested_low && candidate.width_bits < requested.width_bits; | ||
| if !covers_requested && !can_zero_extend { |
There was a problem hiding this comment.
resolve_alias_register_value currently treats any narrower alias at the same offset as a zero-extension source (AL/AX/SI/... -> R*), but on x86-64 only 32-bit writes (E*/R*d) clear the upper bits. With this logic, a path that writes AL and later reads RAX is incorrectly constrained to RAX[63:8]==0 instead of preserving prior high bits, which can make feasible branches appear unreachable in symbolic exploration.
Useful? React with 👍 / 👎.
| let Some(bytes) = state.read_symbolic_fd_bytes(fd, count) else { | ||
| return SummaryEffect::Return(Some(SymValue::concrete(0, call.ret_bits))); | ||
| }; |
There was a problem hiding this comment.
ReadSummary::execute returns a concrete 0 whenever the fd is not registered in symbolic_fd_inputs, and with_core now installs this summary for normal a:sym.explore/a:sym.solve runs too. That forces read-gated code down EOF/error paths even when the input should be unconstrained, so targets behind checks like if (read(...) == 1) become spuriously unreachable unless users switch to the new spec flow.
Useful? React with 👍 / 👎.
- 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.
1 participant
specmodule to define exploration specifications, including predicates, input configurations, and budget constraints.PathExplorerto support running exploration specifications, allowing for more controlled symbolic execution paths.This commit enhances the symbolic execution framework by allowing users to define and run detailed exploration strategies.
Checklist
Description