Execute instructions for Ghidra-supported processors using concrete or symbolic execution of Ghidra p-code.
The public API for this library has not yet been finalized. See x86-64 integration tests for examples using library primitives.
This section document which p-code operations are currently supported by the emulator.
| Opcode | Opcode | Opcode | Opcode |
|---|---|---|---|
✅ COPY |
✅ INT_SLESS |
✅ INT_LESS |
⬜ FLOAT_LESS |
✅ LOAD |
✅ INT_SLESSEQUAL |
✅ INT_LESSEQUAL |
⬜ FLOAT_LESSEQUAL |
✅ STORE |
✅ INT_EQUAL |
✅ INT_NOTEQUAL |
⬜ FLOAT_ABS |
✅ BOOL_NEGATE |
✅ INT_NEGATE |
✅ INT_2COMP |
⬜ FLOAT_NEG |
✅ BOOL_XOR |
✅ INT_XOR |
✅ INT_ADD |
⬜ FLOAT_ADD |
✅ BOOL_AND |
✅ INT_OR |
✅ INT_SUB |
⬜ FLOAT_SUB |
✅ BOOL_OR |
✅ INT_AND |
✅ INT_MULT |
⬜ FLOAT_MULT |
✅ BRANCH |
✅ INT_SDIV |
✅ INT_DIV |
⬜ FLOAT_DIV |
✅ CBRANCH |
✅ INT_SREM |
✅ INT_REM |
⬜ FLOAT_SQRT |
✅ BRANCHIND |
✅ INT_SCARRY |
✅ INT_CARRY |
⬜ FLOAT_CEIL |
✅ CALL |
✅ INT_SEXT |
✅ INT_ZEXT |
⬜ FLOAT_FLOOR |
✅ CALLIND |
✅ INT_SBORROW |
✅ INT_LEFT |
⬜ FLOAT_ROUND |
✅ RETURN |
✅ INT_SRIGHT |
✅ INT_RIGHT |
⬜ FLOAT_NAN |
✅ PIECE |
⬜ INT2FLOAT |
||
✅ SUBPIECE |
⬜ FLOAT2INT |
||
✅ POPCOUNT |
⬜ TRUNC |
This uses libsla to interface with Ghidra's SLEIGH library for translating native code to p-code. SLEIGH is a processor specification language developed for the NSA's Ghidra project used to describe microprocessors with enough detail to facilitate disassembly and decompilation. The processor-specific instructions are translated to p-code, which captures the instruction semantics independent of the specific processor.
The details on how to perform this translation are captured by the compiled SLEIGH specification for the processor. Precompiled specifications from Ghidra can be found in the sleigh-config crate.
The test fixtures are Rust components built targeting specific architectures. Make sure you have the following targets installed via rustup target:
- x86_64-unknown-none
- x86_64-unknown-linux-musl
- aarch64-unknown-none
- aarch64-unknown-linux-musl. This also requires the aarch64-linux-gnu-gcc compiler to be installed for linking.
The Linux musl variants are used by integration tests with a Linux kernel model.
The integration tests use Z3 to perform constraint solving and expects the Z3 shared library to be installed. Alternatively the integration test Cargo.toml can be updated to build and statically link Z3. See the comments in that file for more details.