mirror of
https://github.com/radareorg/r2sleigh.git
synced 2026-11-07 06:36:00 -10:00
Priyanshu KumarandClaude Sonnet 5.5
09d2bb4fc1
`x = c ? a : b;` and the `if` that assigns it are the same C when both arms are
side-effect free and their operands are values, and AGENTS rule 8 forbids control
the machine did not have. The ADR separates the three owners of a `?:` in a
rendering (an r2il Select, the renderer's own overshift guard in `terms.rs::shift`,
and a branch-born selection `shape::select` writes from a diamond), states what
the machine had for each, and measures the counterfactual on the mined set.
Mined set, 1,595 scored, build 23728d11: 2,708 `x = c ? a : b;` statements in 555
of 1,639 functions, 50 of them branch-born (2 functions), 1,755 overshift guards
by the shape of their condition, 903 data selects. Respelling every `?:` as an
`if` (the counterfactual script's transform): perfect 268 to 282, total GED 70,040
to 67,122, 369 better and 22 worse. Respelling only the 50 branch-born ones (a
build with `shape::select` not run): perfect 268 to 268, total GED +59, 11 better
and 27 worse. So the lever sits in selects the machine has no branch for and in
guards that are not selects at all. Folding the 150 overshift guards whose count is
a literal (`(uint32_t)8U >= (uint32_t)32U ? 0 : x << 8`, 40 functions) is a text
counterfactual of 70,040 to 68,852, 40 better and 0 worse, and spells no control:
recorded in ROADMAP D75 as found, not built.
Recommendation: keep `?:` (A); the one subset a CFG fact licenses is worth nothing
on the score; reading the source's shape from DWARF line tables (C) is the only
sound route to the rest and does nothing for the stripped DecBench binaries.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
r2sleigh
A binary analysis engine and certifying decompiler in Rust, with r2s as its
shell. Semantics come from Ghidra's Sleigh specifications rather than
hand-written per-architecture models, and the decompiler refuses rather than
guesses when it cannot prove what it would print. r2s speaks radare2's
command language with no radare2 in the process; radare2 is the differential
target the engine is graded against.
bytes --> Sleigh --> r2il (low) --> r2ssa (medium) --> r2dec (high) --> C
| | |
r2image r2types r2rewrite
ELF/Mach-O/DWARF type inference term rewriting
Quick start
cargo build --release -p r2s --features sleigh
target/release/r2s -q -c 'afl' /bin/ls # functions, and why each is believed
target/release/r2s -q -c 'iz' /bin/ls # strings
target/release/r2s -q -c 'axt 0x100003f10' /bin/ls # references to an address
target/release/r2s -q -c 's main; pdd' /bin/ls # decompile
target/release/r2s -q -c 's main; wx 9090; pdd' /bin/ls # patch in memory, then decompile
target/release/r2s -q -c 's main; pd 16' /bin/ls # disassemble
target/release/r2s /bin/ls # interactive; V for the visual mode
pdil prints r2il as lifted and pddo a function's source obligations, so a
defect is either in the lift or in the rendering. R2DEC_TRACE_REFUSAL=1 names
the predicate and site behind a refusal.
Architectures
| Architecture | Feature | Status |
|---|---|---|
| x86-64, x86 | x86 |
decompiles |
| aarch64 | arm |
decompiles |
| ARM 32-bit | arm |
disassembles; pdd not yet admitted |
| RISC-V, MIPS | riscv, mips |
lift |
Crates
| Crate | Purpose |
|---|---|
r2s |
The shell: radare2's command language over the engine |
r2s-tui |
The visual mode |
r2engine |
Query orchestration, discovery, routes, summaries |
r2image |
ELF and Mach-O parsing, DWARF through gimli |
r2abi |
Library prototypes, syscalls, cited ABI rows |
r2sleigh-lift |
Sleigh decoding to r2il; the machine profile from the .cspec |
r2il |
The low IL (Varnode, R2ILOp, R2ILBlock) and its semantics |
r2ssa |
The IR: SSA, indexes, liveness, values, memory, certificates |
r2source |
Contracts between the layers |
r2types |
Type inference, layouts, signatures |
r2rewrite |
Term rewriting with proved rules |
r2dec |
Structuring, binding and C rendering |
r2sleigh-cli |
The Sleigh toolchain and the instruction exporter |
Extending
- An opcode:
R2ILOpincrates/r2il/src/opcode.rs, its P-code translation incrates/r2sleigh-lift/src/translate.rs, text intext.rs,SSAOpincrates/r2ssa/src/op.rs, its C incrates/r2dec/src/render/terms.rs. - An architecture: a trusted language in
crates/r2sleigh-lift(TrustedSleighProfile,embedded_machine) whose compiler specification theLanguageProfileparses; nothing below the lifter matches its name (doc/adr-machine-profile.md). - A command: one entry in
VERBSincrates/r2s/src/commands.rs, spelled as radare2 spells it.
Documentation
| Document | What |
|---|---|
| ROADMAP.md | What is done, what is left, in order |
| AGENTS.md | Working rules: ownership, anti-hack standard, validation bar |
| BUILDING.md | Build, features, profiles, troubleshooting |
| CONTRIBUTING.md | Issues, commits, pull requests |
| doc/engine-vision.md | What this is becoming, and why |
| doc/testing.md | Gates and where a test goes |
doc/r2il.md, doc/ssa.md, doc/decompiler.md, doc/types.md |
The tiers |
doc/adr-*.md |
One design decision each, linked from the roadmap |
doc/drafts/ |
Designs not yet adopted |
Requirements
Rust 1.99 (edition 2024, pinned in rust-toolchain.toml). radare2 only for the differential harnesses. Z3
optional. License: LGPL-3.0-only.