Skip to main content

Crate r2smt_pcode

Crate r2smt_pcode 

Source
Expand description

Ghidra / SLEIGH P-code lifter for r2SMT.

radare2’s r2ghidra plugin emits SLEIGH P-code for a run of instructions via pdgsd N — a decompiler-grade IR with explicit SSA-style unique varnodes, regular ~30-opcode integer/boolean semantics, and explicit flag derivation (no NZCV guessing). That makes it a cleaner analysis source than per-instruction ESIL for the cases it covers.

This crate turns that text into a Vec<r2smt_ir::IrStmt> so the existing slicer → SSA → SMT pipeline can consume it unchanged.

Like the r2smt_esil crate it is intentionally a strict subset: lift_pcode returns a PcodeError on any opcode or flag construct whose lowering is not provably sound against the IR model (notably ARM NZCV C/V/N polarity, which differs from the per-mnemonic AArch64 flag model — only the Z flag maps cleanly). Callers fall back to the ESIL / per-mnemonic lifter on error, so an unsupported construct never produces a wrong verdict — it just declines the P-code path.

See lift_pcode for the entry point and parse for the pure grammar parser.

Re-exports§

pub use machine::PcodeError;
pub use machine::PcodeLift;
pub use machine::lift_pcode;
pub use parse::PcodeInsn;
pub use parse::PcodeOp;
pub use parse::Varnode;
pub use parse::parse_pcode;

Modules§

machine
P-code → IrStmt lifter (strict, sound subset).
parse
Pure parser for r2ghidra pdgsd P-code text.