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

4.4 KiB Raw Permalink Blame History