Skip to content

Add CoBRA simplifier backend and simplify chain composition #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mrexodia wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Add CoBRA simplifier backend and simplify chain composition #7

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
be9d03e
Integrate CoBRA as a certified MBA simplifier backend
claude Aug 24, 2026
fab6b28
Fix chunks_exact_to_as_chunks clippy lint on current stable
claude Aug 25, 2026
3673f7b
Return UNKNOWN when the simplify chain observes cancellation
claude Aug 25, 2026
9141605
Surface cancellation observed during the final chain stage
claude Aug 25, 2026
6a32626
Bound island conversion work across a cobra simplify request
claude Aug 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 73 additions & 5 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ smt-wire = { path = "crates/smt-wire" }
# gh-release feature downloads a matching prebuilt solver for each.
binbit = { git = "https://github.com/bint-disasm/binbit", rev = "b4996145c06f39ce5bbc79a959975d7d20b6cf5e" }
blake3 = "1"
# The crates.io package is `cobra-mba`; the library itself is named `cobra`.
cobra = { package = "cobra-mba", version = "0.3.0" }
dashu = { version = "0.4.2", features = ["num-traits"] }
rumba-core = "1.0.0"
rusqlite = { version = "0.32", features = ["bundled"] }
Expand Down
4 changes: 2 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ It targets binary analysis, lifting, symbolic execution, and IR experiments wher
## Backends

- Solve and optimize: [`z3`](https://docs.rs/z3/latest/z3/), [`binbit`](https://github.com/bint-disasm/binbit), and the standalone `qfbvsmtrs` crate.
- Simplify: [Rumba](https://github.com/thalium/rumba) for supported 64-bit-or-smaller MBA expression islands.
- Simplify: [Rumba](https://github.com/thalium/rumba) and [CoBRA](https://github.com/binsnake/cobra) run as a chain over supported 64-bit-or-smaller MBA expression islands; CoBRA adopts only Lean-certified rewrites by default.
- Text compatibility: SMT-LIB `QF_BV` scripts are parsed into the same binary IR used by binary clients.

The binary protocol is the main API. SMT-LIB support exists for tooling compatibility and test reuse.
Expand Down Expand Up @@ -225,7 +225,7 @@ See `docs/qfbvsmtrs-validation.md` for maintainer validation gates and corpus-ru

- `crates/smt-wire` — Rust high-level client API plus server-side wire-format internals and validators.
- `crates/qfbvsmtrs` — standalone pure-Rust `QF_BV` bit-blasting solver crate and CLI.
- `crates/smt-server` — TCP server, Rumba simplifier integration, solver backend integration, SMT-LIB frontend.
- `crates/smt-server` — TCP server, Rumba and CoBRA simplifier integrations, solver backend integration, SMT-LIB frontend.
- `python` — Python client package and tests.
- `cpp` — C++17 header-only package, CMake target, and tests.
- `docs/architecture.md` — current crate/server/backend architecture.
Expand Down
1 change: 1 addition & 0 deletions crates/smt-server/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ license.workspace = true

[dependencies]
binbit.workspace = true
cobra.workspace = true
qfbvsmtrs = { workspace = true, features = ["wire"] }
rumba-core.workspace = true
smt-qfbv-smtlib.workspace = true
Expand Down
Loading
Loading