# 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 |