88 lines
4.4 KiB
Markdown
88 lines
4.4 KiB
Markdown
# Vendor Library Decision and Reading List
|
|
|
|
> Date: 2026-05-31; updated after Ghidra x86/x86-64 SLEIGH and P-Code summary work.
|
|
> Purpose: record Fold's vendor posture without duplicating upstream manuals.
|
|
|
|
## Decision
|
|
|
|
Fold should keep a small vendor surface:
|
|
|
|
| Status | Library | Fold role | Rationale |
|
|
|---|---|---|---|
|
|
| Active | Ghidra/SLEIGH | Binary instruction semantics, raw/high P-Code, SSA-style def-use | Already integrated; best fit for binary semantics feeding Fold/Z3. |
|
|
| Candidate | LIEF | Binary metadata for ELF/PE/Mach-O | Complements Ghidra by replacing fragile r2 JSON metadata queries; not a lifter. |
|
|
| Candidate | Souffle | Datalog facts over Fold MidIR | Useful after stable function/block/op/value IDs exist. |
|
|
| Deferred | RetDec | Binary-to-LLVM comparison lane | Revisit only if Ghidra misses a fixture class that LLVM lifting preserves. |
|
|
| Deferred | Remill/McSema | Instruction-accurate LLVM lifting | Powerful but heavy; overlaps Ghidra and adds CFG/toolchain cost. |
|
|
| Deferred | PhASAR | IFDS/IDE analyses over LLVM IR | Useful only after LLVM IR is a first-class Fold input. |
|
|
| Deferred | Crab/Clam | Numeric invariants over LLVM/Fold IR | Revisit only for a concrete loop/range false-positive class. |
|
|
| Track only | LLVM CIR/MLIR | Future source mid-level IR | Follow through Fold's LLVM pin; do not vendor separately. |
|
|
|
|
## External reading
|
|
|
|
### Ghidra/SLEIGH/P-Code
|
|
|
|
Use these as the source of truth for binary semantics:
|
|
|
|
- P-Code reference: https://ghidra.re/ghidra_docs/languages/html/pcoderef.html
|
|
- SLEIGH language manual: https://ghidra.re/ghidra_docs/languages/html/sleigh.html
|
|
- Vendored Fold pin and runtime policy: `third_party/ghidra-decompiler/VENDOR.md`
|
|
- Fold implementation entry points: `src/binary/ghidra_lifter.cpp`,
|
|
`src/binary/pcode_router.cpp`, `src/binary/binary_pcode_scan.cpp`,
|
|
`src/symbolic/pcode_encoder.cpp`, `src/symbolic/pcode_summary.cpp`
|
|
|
|
Fold-specific rule: Ghidra owns binary semantics. Do not decompile to C and route
|
|
binary evidence through source detectors.
|
|
|
|
### LIEF
|
|
|
|
Use these for metadata parsing, not instruction semantics:
|
|
|
|
- C++ API overview: https://lief.re/doc/latest/api/cpp/index.html
|
|
- Binary abstraction parser: https://lief.re/doc/stable/api/binary_abstraction/cpp.html
|
|
- ELF C++ API: https://lief.re/doc/latest/formats/elf/cpp.html
|
|
- PE C++ API: https://lief.re/doc/latest/formats/pe/cpp.html
|
|
- Tutorial: https://lief.re/doc/stable/tutorials/01_play_with_formats.html
|
|
- Fold manifest: `third_party/lief/VENDOR.md`
|
|
|
|
Fold-specific rule: LIEF can replace/supplement r2 metadata for sections,
|
|
symbols, imports, exports, entry points, and format details. It does not replace
|
|
Ghidra/P-Code.
|
|
|
|
### Souffle
|
|
|
|
Use these once MidIR/fact IDs are stable:
|
|
|
|
- C++ interface: https://souffle-lang.github.io/interface
|
|
- Run modes: https://souffle-lang.github.io/execute
|
|
- Interface header reference: https://souffle-lang.github.io/souffle/_souffle_interface_8h.html
|
|
- Fold manifest: `third_party/souffle/VENDOR.md`
|
|
|
|
Fold-specific rule: start standalone with TSV facts and `.dl` rules. Use
|
|
generated C++ only after the relations prove useful and bounded.
|
|
|
|
### Deferred lanes
|
|
|
|
Keep these as reading references only:
|
|
|
|
- RetDec repository overview: https://github.com/avast/retdec/wiki/Repository-Overview
|
|
- RetDec Capstone-to-LLVM IR: https://github.com/avast/retdec/wiki/Capstone2LlvmIr
|
|
- Remill intrinsics: https://github.com/lifting-bits/remill/blob/master/docs/INTRINSICS.md
|
|
- McSema instruction lifecycle: https://github.com/lifting-bits/mcsema/blob/master/docs/LifeOfAnInstruction.md
|
|
- PhASAR overview: https://phasar.org/
|
|
- PhASAR data-flow guide: https://github.com/secure-software-engineering/phasar/wiki/Writing-a-Data-Flow-Analysis
|
|
- Clam/Crab LLVM invariant analyzer: https://github.com/seahorn/crab-llvm
|
|
|
|
Do not add manifests, Meson flags, or fetch-script entries for deferred lanes
|
|
until a reproducible fixture demonstrates need.
|
|
|
|
## Revisit triggers
|
|
|
|
| Trigger | Candidate to revisit |
|
|
|---|---|
|
|
| r2 metadata hangs or inconsistent JSON blocks binary reporting | LIEF |
|
|
| Cross-TU taint/reachability outgrows native graph code | Souffle |
|
|
| Ghidra P-Code misses a required binary semantic class | RetDec or Remill/McSema comparison prototype |
|
|
| Native range summaries cannot close a concrete OOB/division false positive | Crab/Clam |
|
|
| Fold adopts LLVM IR as a committed source/binary input | PhASAR |
|
|
| Installed LLVM exposes stable CIR/MLIR for C/C++ | CIR/MLIR mapping study |
|