Module machine 

P-code → IrStmt lifter (strict, sound subset).

Soundness boundary: only the Z flag is mapped to the canonical ZF the branch-condition composer reads (P-code ZR ≡ zero, no polarity ambiguity). P-code NG/CY/OV are not mapped to the canonical SF/CF/OF, because ARM NZCV polarity differs from the per-mnemonic AArch64 model and a name-level merge would be unsound. They are lifted into distinct pc_* vars instead, so a branch that needs C/V/N simply leaves the canonical flag a free input downstream → the solver returns BothPossible (sound, never a fabricated verdict). Branches that read only Z (eq/ne, cbz/cbnz, test;jz, …) get a precise decompiler-grade slice. Any opcode outside the modelled subset returns PcodeError so the caller falls back to the ESIL / per-mnemonic lifter.

Structs

PcodeLift

Lifter output — mirrors r2smt_esil::EsilLift so callers can splice it into their statement list directly.

Enums

PcodeError

Reasons the P-code lifter declines (caller falls back to ESIL).

Functions

lift_pcode

Lift a pdgsd dump under arch into IR statements.