mirror of
https://github.com/radareorg/r2sleigh.git
synced 2026-11-07 06:36:00 -10:00
Priyanshu KumarandClaude Sonnet 5.5
8d719d4e7d
doc/adr-structure-dominator-tree.md gains "the guards and the spelling order, stacked": where D59 and D60 meet D58 (an edge's copy is spelled as EdgeText::Copies and marked as a statement of the block it leaves, the latch hoist's reads are counted once and its copy test asks Placed::edge_copy, a chain member is a test whose text is nothing else), what the effects add and the table of the mined set. Over 25,735 functions of bash, ls-toybox, pigz, 0pack and pumasim 17 change under the guards alone and 55 under the spelling order alone, none under both, none newly refused. Residual sites: 0pack 47,850 to 47,898, pumasim 67,628 to 67,644, the guards add none. Mined set: 206 perfect, 43.795 mean GED and 57,153 total GED at the base, with the guards and with the tip (eight zlib `inflateCopy` renderings renumber a local, no graph moves); held out gotos 2,100, 2,098, 2,098 with the same 338 refused. Write orders O1, O2, O3 differ 0, 0, 0 at the tip against 0, 120, 187 on the base with the knobs alone. Release pdd instructions retired -0.02% to +0.10% on six large functions, renderings byte-identical. The equivalence gate holds all 828 baseline records on x86-64 (744 equal) and AArch64 (750 equal), none differing. ROADMAP: the SD row records the stack's numbers. D61 (3) gains the one function the stack makes gain a goto: bash 0x48140, 1 to 2, because D58's rule reads its tail's r13_4 as a residual and a tail that holds one is not copied. 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.