fold/docs/internal/m31-phase3-concolic.md

M31 Phase 3 — Concolic execution scoping

Goal

Close the last gap in fold's symbolic-execution + fuzzer loop. M31 Phase 1+2 ships:

• Scan-time symbolic execution. Z3 produces a satisfying model for every flagged sink; the model is packed as concrete bytes and written to the libFuzzer corpus.
• Runtime fuzzing. libFuzzer mutates the seed bytes, ASan reports crashes, fold ingests the crash and promotes the corresponding Finding to Confidence::ConcreteWitness.

What we don't do today: when libFuzzer takes a new path the encoder never explored (because the encoder bailed, or because the real path depends on an environmental input fold didn't model), there is no feedback. The fuzzer keeps mutating the bytes it has; fold never learns the new path predicate.

Concolic execution (DART, KLEE, SymCC) closes that gap. As the target binary runs on a concrete input, a parallel symbolic interpreter tracks the path predicate. At each branch the runtime asks Z3 to negate the last branch and emit a new input that would take the sibling edge. That input goes back into the corpus.

Phase 3's question is not "should we add concolic." That's the right direction once Phase 2 stabilizes. The question is which runtime do we adopt, given:

• License: fold will be GPL-3.0 when OSS'd. LGPL runtimes are compatible if dynamically linked.
• Toolchain: fold builds against LLVM 22 (Homebrew llvm@22).
• Architecture: fold already orchestrates fuzzer children via posix_spawn (src/fuzz/runner.cpp). A concolic runtime needs to attach to the same child process.
• Maintenance posture: fold is a one-developer project. Vendoring a 30k-LOC pass we'd then have to maintain against every LLVM release is not free.

Option A — Vendor symcc-rt + write our own LLVM-22 pass

eurecom-s3/symcc splits into two halves:

1. Compiler pass (symcc_pass): a clang LLVM pass that instruments each LLVM IR instruction with a call into the runtime. Currently capped at LLVM 18.
2. Runtime (symcc-rt): a shared library that maintains the symbolic shadow store, asks Z3 to solve at branches, and emits new inputs.

License: the runtime is LGPL-3.0; the pass is GPL-3.0. Both compatible with fold's planned GPL-3.0.

The work this option requires:

• Port symcc_pass from LLVM 18 to LLVM 22. New TypedPointerType, removal of getInt8PtrTy, opaque pointers everywhere — a real rewrite of every IRBuilder call that materializes a pointer. Conservatively: 2-3 weeks of focused work, then maintenance every LLVM release.
• Vendor symcc-rt into third_party/symcc-rt/ and link dynamically (LGPL-compliant).
• Add a meson option -Dwith-concolic=true that builds the pass as a .dylib (or .so) loaded via -fpass-plugin=.
• Extend runner.cpp to compile the target through the instrumenting pass when --concolic is set, and to pick up symcc's SYMCC_OUTPUT_DIR so the new inputs land in the corpus.

Wins:

• Full control over instrumentation. We could specialize the pass for fold's specific needs (e.g. skip instrumentation in code reached only by paths the encoder already proved sat).
• No new runtime dependency beyond what we already have (LLVM 22, Z3).
• One language (C++) end-to-end. Reviewable by anyone fluent in the rest of fold.

Costs:

• 2-3 weeks of porting work plus ongoing per-LLVM-release maintenance. fold's M30 refactor took 12 sessions; this is a comparable commitment with worse ROI because the upstream doesn't move.
• We absorb every SymCC bug into our issue tracker.

Option B — LibAFL symcc_runtime bridge

LibAFL is the modern AFL++ successor written in Rust. It ships a libafl_targets::symcc_runtime module that talks to symcc-rt over a well-defined IPC interface, plus a concolic feature flag and a ConcolicTracingStage that drives the runtime from a Rust harness.

License: LibAFL is Apache-2.0/MIT dual-licensed; symcc-rt is LGPL-3.0. Both compatible with our GPL-3.0 (Apache-2.0 + GPL-3.0 = GPL-3.0; LGPL-3.0 dynamically linked stays clear).

The work this option requires:

• Add a Rust harness crate tools/fold-concolic/ that wraps LibAFL's ConcolicTracingStage and exposes a CLI compatible with fold's existing runner.cpp argv shape.
• Vendor or Cargo.toml-depend on symcc-rt. (LibAFL's docs show both vendored and FFI-build patterns.)
• Extend runner.cpp to invoke the Rust harness as a subprocess when --concolic is set; ingest the inputs it produces from a designated output directory.
• Manage the Rust toolchain dependency in CI (cargo + a pinned toolchain version).

Wins:

• Zero LLVM-pass maintenance. LibAFL and symcc-rt upstreams handle the toolchain churn.
• LibAFL's ConcolicTracingStage already implements branch flipping, input minimization, and corpus integration — features we would otherwise rewrite.
• Active upstream (LibAFL releases monthly; AFL++ maintainer is primary author). Bug reports flow to people who care.
• Side benefit: opens a path to swap libFuzzer for LibAFL's own fuzzer in Phase 4 if we want richer scheduling.

Costs:

• A second language in the build. fold becomes "C++ for analysis, Rust for the runtime loop." CI gets a Rust toolchain. Reviewers need to know both.
• Coarser instrumentation. We get whatever LibAFL+symcc-rt do — no path-aware specialization without contributing upstream.
• IPC overhead between the Rust harness and the C++ fold binary. Probably negligible (the dominant cost is Z3 itself), but needs to be measured before committing.

Recommendation

Adopt Option B (LibAFL bridge), staged in three steps.

The decisive factor is maintenance leverage. fold has one maintainer. The encoder already eats most of the available bandwidth. Owning an LLVM pass that requires forklift work every LLVM release would, over a 2-year horizon, cost more than the specialization wins.

The two-language cost is real but bounded: the Rust harness is a single CLI binary the fold C++ code shells out to. The interface is argv + a directory of new inputs — the same shape runner.cpp already uses for libFuzzer. We do not need to learn Rust to use the harness, only to extend it.

If specialization later becomes the bottleneck (we have evidence LibAFL+symcc-rt's default instrumentation is hurting us), the escape hatch is to upstream patches to LibAFL — much cheaper than re-porting the whole pass.

Staging

P3.1 — Plumbing. Wire --concolic through runner.cpp as a no-op flag. Document the contract: when set, after libFuzzer's deadline expires, fold runs a second campaign with the concolic harness, ingests new inputs from <workdir>/concolic-out/, and adds them to the libFuzzer corpus for a final round.

P3.2 — LibAFL harness. Add tools/fold-concolic/ (Rust crate). One binary fold-concolic taking the same harness path, seed dir, and output dir as the libFuzzer runner. Wraps ConcolicTracingStage against symcc-rt.

P3.3 — Promotion path. When the concolic harness produces an input that triggers an ASan crash, the existing crash-ingest pipeline (fuzz_run_runner.cpp) promotes the Finding to ConcreteWitness — no new ingest code; the seed source is already opaque to that stage.

Each step is independently revertable and testable: P3.1 lands without LibAFL, P3.2 lands without integration, P3.3 reuses existing code.

Scope explicitly excluded

• Replacing libFuzzer with LibAFL's own fuzzer. Bigger rewrite, no proven win at fold's scale. Defer to Phase 4.
• Symbolic memory model upgrades (granular byte tracking on pointer parameters). Orthogonal; tracked separately in docs/research/frontier.md follow-ups.
• KLEE adoption. KLEE is GPL-2.0 (incompatible with our planned GPL-3.0 without legal review), interprets its own LLVM IR rather than running natively, and would not slot into our posix_spawn child-process model without significant glue. Re-evaluate only if symcc-rt becomes unmaintained.

Verification checklist

• License audit: confirm LibAFL Apache-2.0/MIT + symcc-rt LGPL-3.0 against fold's planned GPL-3.0. Document in docs/licensing.md.
• Toolchain probe: confirm cargo is available in CI and pick a pinned Rust toolchain version (likely the latest stable; matches LibAFL's MSRV).
• Build proof: cargo build --release of a minimal LibAFL ConcolicTracingStage harness against the same fixture (tests/integration/fuzz_fixtures/null_behind_magic.c) that Phase 1+2 already covers.
• Latency baseline: measure end-to-end wall-clock for one concolic campaign on that fixture. Must not exceed a conservative budget (e.g. 30s) before we commit to wiring it into the default fold fuzz-run pipeline.
• Reproducibility: same fixture must produce the same Finding promotion under --concolic as it does today under plain libFuzzer, given the same time budget.

Open questions

1. Determinism. symcc-rt branches the symbolic store on every conditional. Two runs of the same harness produce different input orders. Does our crash-ingest pipeline care about the ordering? It shouldn't — Finding promotion matches by finding_id — but worth verifying with a small reproducibility test.
2. LibAFL version pin. LibAFL's API has historically been unstable. We should pin a specific tag in Cargo.toml and only bump deliberately, not on cargo update.
3. Build-time impact. Adding Rust to the build raises CI from one toolchain to two. Worth quantifying before P3.2 lands.