f0fe006d6b
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.
75 lines
5.7 KiB
Markdown
75 lines
5.7 KiB
Markdown
# 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.
|