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.
5.7 KiB
5.7 KiB
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_requiredtier 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 prepharness 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_mscost. - 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 +
FactProvenanceto build comparable features; candidate for a confidence-ranking lane.
Datalog / DSL
- Bembenek et al. (2020) Formulog. arXiv:2009.08361 — Datalog+SMT for declarative detectors.