r2smt_pcode/lib.rs
1#![deny(missing_docs)]
2//! Ghidra / SLEIGH P-code lifter for r2SMT.
3//!
4//! radare2's r2ghidra plugin emits SLEIGH P-code for a run of
5//! instructions via `pdgsd N` — a decompiler-grade IR with explicit
6//! SSA-style `unique` varnodes, regular ~30-opcode integer/boolean
7//! semantics, and *explicit* flag derivation (no `NZCV` guessing). That
8//! makes it a cleaner analysis source than per-instruction ESIL for
9//! the cases it covers.
10//!
11//! This crate turns that text into a `Vec<r2smt_ir::IrStmt>` so the
12//! existing slicer → SSA → SMT pipeline can consume it unchanged.
13//!
14//! Like the `r2smt_esil` crate it is intentionally a **strict
15//! subset**: [`lift_pcode`] returns a [`PcodeError`] on any opcode or
16//! flag construct whose lowering is not *provably* sound against the
17//! IR model (notably ARM `NZCV` C/V/N polarity, which differs from the
18//! per-mnemonic `AArch64` flag model — only the Z flag maps cleanly).
19//! Callers fall back to the ESIL / per-mnemonic lifter on error, so an
20//! unsupported construct never produces a wrong verdict — it just
21//! declines the P-code path.
22//!
23//! See [`lift_pcode`] for the entry point and [`parse`] for the pure
24//! grammar parser.
25
26pub mod machine;
27pub mod parse;
28
29pub use machine::{PcodeError, PcodeLift, lift_pcode};
30pub use parse::{PcodeInsn, PcodeOp, Varnode, parse_pcode};