fold/docs/research/prior-art.md
trvon f0fe006d6b
fix(docs,tests): correct the pre-push hook claim, a dead link, MCP cleanup
Problem: the README said setup enables "tracked ... OpenGrep pre-push
hooks", but only .githooks/pre-commit is tracked, so fresh clones get no
pre-push hook. docs/research/prior-art.md pointed to prior-art-full.md,
which has never been in the repository. test_mcp_stdio's TempDir
destructor called the throwing remove_all overload; a failure during
unwinding terminates the test binary and leaves .fold-mcp-test-*
directories behind.

Fix: the README names only the tracked pre-commit hook. The pre-push
hook is not committed: it runs `opengrep --config auto`, which needs the
network. The dead reference is removed. TempDir uses the error_code
remove_all overload. It stays under the working directory, because the
MCP server rejects paths outside its workspace root (moving it to
temp_directory_path broke three MCP tests).

Test: mcp_stdio passes.
2026-09-24 20:57:32 -06:00

5.7 KiB
Raw Permalink Blame History

Prior Art (condensed)

Key papers grounding fold's design.

Buffer overflow

  • Xu et al. (2020) ELAID. doi:10.1186/s42400-020-00058-2 — interprocedural call graph + SMT on Juliet sinks.
  • Khedker (2014) Buffer Overflow Analysis. arXiv:1412.5400 — buffer lattice with size + null-position sets.

Dead code

  • Naug (2020) Useless Code Identification with SE. doi:10.5373/jardcs/v12sp3/20201233 — dead-branch precedent.
  • Patil (2025) Opti-Blend. doi:10.12732/ijam.v38i5.424 — unified framework for dead code + clones.

Clones

  • Tronicek (2026) DrDupLex3. doi:10.37190/e-inf260105 — Type-3 SOTA baseline.
  • Hummel et al. (2010) Index-based clone detection. doi:10.1109/icsm.2010.5609665 — incremental clone caching.

Code Property Graphs

  • Yamaguchi et al. (2014) Modeling Vulnerabilities with CPG. doi:10.1109/sp.2014.44 — AST+CFG+PDG join.

Null pointer analysis

  • Das & Lal (2017) GVN for null checking. arXiv:1702.05807 — GVN makes alias analysis path-aware; the access-path/guarded-fact substrate is fold's analogue.
  • Estep et al. (2021) Gradual Program Analysis for Null Pointers. arXiv:2105.06081 — gradual static/dynamic null analysis cuts FPs vs Infer; backs fold's latent/precondition_required tier for unguarded raw-pointer params (yams #13, #19).
  • Raad et al. (2020) Incorrectness Separation Logic. doi:10.1007/978-3-030-53291-8_14 — under-approximate reasoning = no FP by construction; theory behind manifest-vs-latent reporting (Infer Pulse lineage).

Recall lift

  • Gens et al. (2018) K-Miner. NDSS. doi:10.14722/ndss.2018.23326 — kernel-scale interprocedural memory safety.
  • Miné (2007) Symbolic Methods for Numerical Abstract Domains. — interval domain alongside BV.
  • Illous et al. (2020) Separation Logic Summaries. doi:10.1007/978-3-030-65474-0_12 — pre/post summaries.
  • Zhang et al. (2025) CG-FSPTA. arXiv:2508.01974 — flow-sensitive points-to without CFG.

Heap model

  • Fischer et al. (2022) CBMC-SSM. doi:10.1145/3551349.3559523 — symbolic shadow memory.
  • Feist et al. (2016) Finding the needle in the heap. doi:10.1145/3015135.3015137 — UaF via static+SE.
  • Trabish et al. (2020) Past-sensitive pointer analysis. doi:10.1145/3368089.3409698 — allocation-history disambiguation.
  • Nowack (2019) Fine-Grain Memory Object Representation. doi:10.1109/ase.2019.00089 — granularity tradeoffs.

Warning confirmation

  • Ma et al. (2011) Directed Symbolic Execution. doi:10.1007/978-3-642-23702-7_11 — drive SE to targets.
  • Xu et al. (2025) Static Analysis Error Traces + DSE. doi:10.1145/3713081.3731720 — scan→confirm architecture.
  • Gerasimov (2018) Directed Dynamic SE for Warning Confirmation. doi:10.1134/s036176881805002x.
  • Shafiuzzaman et al. (2026) SAILOR: static-analysis-informed, LLM-orchestrated SE. arXiv:2604.06506 — static targets → SE → concrete replay validation; 379 mem-safety bugs in 6.8M LOC. Mirrors fold's scan→confirm→fuzz-witness lane; motivates LLM-assisted fuzz prep harness synthesis.
  • Li et al. (2025) ColorGo: Directed Concolic Execution. arXiv:2505.21130 — incremental coloration (static reachability + dynamic feasibility), 100× over AFLGo; directedness model for fold confirm/fuzz.

Incremental SE

  • Yang et al. (2014) Directed Incremental SE. doi:10.1145/2629536 — diff-guided exploration.
  • Yi & Yang (2022) Feedback-Driven Incremental SE. doi:10.1109/issre55969.2022.00055 — feedback refinement.
  • Lin et al. (2016) Compositional SE: Incremental Solving Revisited. doi:10.1109/apsec.2016.046 — solver reuse.

Compositional summaries

  • Lin et al. (2015) Compositional SE Using Fine-Grained Summaries. doi:10.1109/aswec.2015.32 — pre/post substitution.

Foundations

  • Ferrante et al. (1987) The program dependence graph. doi:10.1145/24039.24041 — PDG.
  • Braun et al. (2013) Simple Efficient SSA Construction. doi:10.1007/978-3-642-37051-9_6.
  • Marashdih et al. (2022) SSA-based SE Abstraction. doi:10.1007/s10515-022-00342-0.
  • de Moura & Bjørner (2008) Z3. doi:10.1007/978-3-540-78800-3_24.
  • Bjørner et al. (2015) νZ. doi:10.1007/978-3-319-21668-3_5 — push/pop, assumption-based solving.
  • Beyer (2016) BenchExec and Witnesses. doi:10.1007/978-3-662-49674-9_55 — SV-COMP methodology.
  • Gadelha et al. (2018) ESBMC 5.0. doi:10.1145/3238147.3240481 — comparable BMC.
  • Wagner & Sametinger (2014) Juliet comparison methodology. doi:10.5220/0005032902440252.
  • Lenarduzzi et al. (2022) SonarQube precision. doi:10.1007/s10664-022-10141-2 — FP induction rates.
  • Corbett et al. (2000) Bandera. doi:10.1145/337180.337234 — predicate abstraction.

Expression caching

  • Trabish et al. (2021) Address-Aware Query Caching. doi:10.1109/icst49551.2021.00023 — canonical expression reuse.

State merging / path explosion

  • Trabish et al. (2023) State Merging with Quantifiers in SE. arXiv:2308.12068 — partitions states by uniform path-constraint structure and encodes merges with quantifiers, cutting disjunction/ITE blow-up; perf lever for fold's states_merged / env_clone_ms cost.
  • Bailey & Nicholas (2025) Symbolic Execution in Practice (survey). arXiv:2508.06643 — taxonomy of scope-reduction vs guidance-heuristic strategies; anchor for the perf phase.

FP triage / ranking

  • Ohlmer, Schlichtig & Bodden (2026) FP-Predictor. arXiv:2603.10558 — GCN over Code Property Graphs classifies SAST reports TP/FP. fold already has IR + FactProvenance to build comparable features; candidate for a confidence-ranking lane.

Datalog / DSL

  • Bembenek et al. (2020) Formulog. arXiv:2009.08361 — Datalog+SMT for declarative detectors.