SMOKE (ICSE 2019) made path-sensitive static detection of C/C++ memory leaks scale to projects of up to 8 million lines of code by staging a sparse, polynomial-time use-flow-graph candidate enumeration under an SMT-solver-based path-feasibility verification, at the acknowledged cost of a 24.4% average false-positive rate, explicit unsound assumptions, and three stated precision gaps: missing library specifications, inherited pointer/alias imprecision, and residual infeasible paths involving complex arithmetic, data dependence, or deep interprocedural effects. The open question is whether a static memory-leak detector can simultaneously achieve industrial-scale scalability, precision that survives library-rich and alias-heavy code (through automatic modeling of library and project-specific allocation semantics and alias-precise heap tracking), refutation of semantically infeasible warning paths, and reduced or configurable unsoundness. The problem remains open.

Background

A memory leak is a program defect in which a dynamically allocated heap block is no longer reachable through any pointer yet is never returned to the allocator; in long-running C/C++ software, leaks accumulate and eventually cause resource exhaustion and denial of service. Because C and C++ delegate memory management to the programmer, leaks must be found by analysis rather than by a garbage collector. Dynamic tools (runtime leak detectors, fuzzers) only observe the executions they happen to trigger, so static analysis, which reasons about all program paths without running the code, is the natural complement; its weakness is warnings about defects that cannot actually occur, called false positives, and missed defects, called false negatives.

A static analysis is path-sensitive when it distinguishes different execution paths through the program (e.g., which branch of an if was taken) instead of merging the facts of all paths together; path sensitivity is what lets an analysis recognize that a report sits on an infeasible path — one that no real execution can follow, for instance because two correlated branches can never both be taken. Value-flow analysis tracks how values move through the program via data dependences on a sparse value-flow graph; the use-flow graph (UFG) used by SMOKE is such a sparse representation tailored to memory-allocation and deallocation events. An SMT solver (satisfiability modulo theories) is a constraint solver that decides whether a Boolean combination of arithmetic and other constraints — here, the conditions gathered along a candidate path — is satisfiable; if the path constraints are unsatisfiable, the path is infeasible and the warning is suppressed. Pointer (alias) analysis determines which pointers may denote the same memory address; when it conflates two distinct heap objects, operations on one may spuriously change the state of the other.

SMOKE (Fan, Wu, Shi, Xiao, Zhou, and Zhang, ICSE 2019) resolved a then-unresolved paradox — precise analyses do not scale, imprecise ones drown users in false positives — with a staged design: a scalable but imprecise flow- and context-sensitive analysis computes a succinct set of candidate leak paths on the UFG, and a dedicated SMT-based verifier then checks only those candidates' feasibility. It checked projects up to 8 million lines of code in about forty minutes with a 24.4% average false-positive rate and found thirty previously unknown leaks, one assigned a CVE identifier. The paper's own Limitations section and implementation notes state what the design does not achieve: (1) without specifications of library functions, branch correlations hidden inside libraries cannot be detected, producing false positives; (2) imprecision inherited from the underlying pointer analysis can conflate distinct heap objects and corrupt state propagation; (3) some infeasible paths — those involving complex arithmetic in branch conditions, complicated data dependence, or deep interprocedural effects — survive both the linear-time contradiction filter and the SMT check, and enriching the collected path constraints would reduce these false positives only at the price of efficiency; and (4) the tool makes explicit unsound trade-offs for practicality — paths flowing to global pointers or containers (e.g., std::list, std::vector) are assumed safe, paths ending in exit() are not reported, heap objects passed to externally defined library functions stop the search, allocation failures (a null return from malloc) are ignored, and free(p+y) is treated as free(p) — all of which can hide real leaks.

These gaps are not specific to one tool: they are the general frontier of industrial static leak detection, and the same axes recur in the successor literature — under-constrained symbolic execution (symbolic execution of a function in isolation, without its calling context) for scalable per-function checking; typestate analysis (tracking an object through a sequence of states such as allocated/freed, generalized from its original formulation for checking API-usage protocols) with alias awareness; function summaries that record allocation and ownership behavior so libraries and wrappers need not be reanalyzed; and, most recently, large-language-model-generated annotations and summaries that aim to automate library specification. The unresolved scientific question is whether these axes can be closed jointly rather than traded off against one another.

Problem Statement

Can static detection of memory leaks in C/C++ software achieve, simultaneously and with rigorous empirical evidence at industrial scale (on the order of millions of lines of code analyzed in practical time on commodity hardware), the following jointly held properties, whose tension SMOKE's staged design only partially negotiated?

(1) Library-aware precision: the analysis must account for the semantics of external library functions and project-specific allocation/deallocation wrappers — through automatically derived, validated specifications or summaries — so that branch correlations and ownership transfers hidden in libraries neither create false positives (infeasible paths reported as leaks) nor hide real leaks.

(2) Alias-precise heap tracking: the underlying pointer/alias analysis must keep distinct heap objects distinct, so that operations on one object do not corrupt the tracked allocation state of another.

(3) Semantic path feasibility: warning paths that are infeasible under complex arithmetic in branch conditions, complicated data dependence, or deep interprocedural effects must be refuted — by constraint collection and solving that is rich enough for these cases — without giving up the scalability that made the staged approach practical; the precision-efficiency exchange that SMOKE documents ('more control and data dependence in the path constraints ... at the price of being less efficient') must be substantially improved on both sides rather than traded.

(4) Reduced or configurable unsoundness: the pragmatic assumptions that paths flowing to global pointers or containers are safe, that paths ending in exit() need no report, that unknown external calls end the search, and that allocation always succeeds, must be removed or made configurable, so that the detector's false-negative behavior with respect to escaping ownership and allocation failure is characterized and bounded rather than silently assumed.

These four requirements are facets of one overarching objective — a leak detector that is at once scalable, precise, and (at least configurably) sound — and they are scientifically linked: the same mechanism families (sparse value-flow representations, function summaries, path-condition collection, symbolic reasoning, alias precision) determine progress on all of them, which is why each successor tool relocates rather than removes the trade-off. They must be achieved jointly, relative to the published state of the art, rather than traded off against one another. The problem is not restricted to any single benchmark, toolchain, or method class. Because the question above is a feasibility question, a rigorous negative answer is equally a complete answer — an impossibility or lower-bound argument that some of properties (1)-(4) cannot be jointly achieved at industrial scale.

References

  1. Gang Fan, Rongxin Wu, Qingkai Shi, Xiao Xiao, Jinguo Zhou, Charles Zhang. SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code. In: Proceedings of the 41st IEEE/ACM International Conference on Software Engineering (ICSE), 2019, pp. 72-82. DOI: 10.1109/ICSE.2019.00025. https://doi.org/10.1109/ICSE.2019.00025
  2. Hongliang Liang, Luming Yin, Guohao Wu, Yuxiang Li, Qiuping Yi, Lei Wang. LeakGuard: Detecting Memory Leaks Accurately and Scalably. 2025. arXiv:2504.04422. https://arxiv.org/abs/2504.04422
  3. Huihui Huang, Jieke Shi, Bo Wang, Zhou Yang, David Lo. Finding Memory Leaks in C/C++ Programs via Neuro-Symbolic Augmented Static Analysis. 2026. arXiv:2603.27224. https://arxiv.org/abs/2603.27224
  4. Ekaterina Shemetova, Ilya Shenbin, Ivan Smirnov, Anton Alekseev, Alexey Rukhovich, Sergey Nikolenko, Vadim Lomshakov, Irina Piontkovskaya. LAMeD: LLM-generated Annotations for Memory Leak Detection. 2025. arXiv:2505.02376. https://arxiv.org/abs/2505.02376
  5. Wensheng Tang, Dejun Dong, Shijie Li, Chengpeng Wang, Peisen Yao, Jinguo Zhou, Charles Zhang. Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path Conditions. ACM Transactions on Software Engineering and Methodology, 2024, 33(3): 1-33. DOI: 10.1145/3632743. https://doi.org/10.1145/3632743
  6. Yuxuan He, Ruilin Jiang, He Zhang, Qingkai Shi, Huaxun Huang, Rongxin Wu. Hermes: Making Path-Sensitive Pointer Analysis Scalable for Sparse Value-Flow Analysis. Proceedings of the ACM on Programming Languages, 2026, 10(OOPSLA1): 314-342. DOI: 10.1145/3798211. https://doi.org/10.1145/3798211
  7. Tuo Li, Jia-Ju Bai, Yulei Sui, Shi-Min Hu. SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate Analysis. ACM Transactions on Computer Systems, 2024, 42(3-4): 1-40. DOI: 10.1145/3695250. https://doi.org/10.1145/3695250
  8. Tuo Li, Jia-Ju Bai, Yulei Sui, Shi-Min Hu. Path-sensitive and alias-aware typestate analysis for detecting OS bugs. ASPLOS 2022. DOI: 10.1145/3503222.3507770. https://doi.org/10.1145/3503222.3507770
  9. Yongchao Wang, Yuandao Cai, Charles Zhang. Boosting Path-Sensitive Value Flow Analysis Via Removal of Redundant Summaries. ICSE 2025. DOI: 10.1109/ICSE55347.2025.00195 (preprint arXiv:2502.04952). https://doi.org/10.1109/ICSE55347.2025.00195
  10. Wen Li, Haipeng Cai, Yulei Sui, David Manz. PCA: memory leak detection using partial call-path analysis. ESEC/FSE 2020. DOI: 10.1145/3368089.3417923. https://doi.org/10.1145/3368089.3417923
  11. Hayk Aslanyan, Hovhannes Movsisyan, Hripsime Hovhannisyan, Zhora Gevorgyan, Ruslan Mkoyan, Arutyun Avetisyan, Sevak Sargsyan. Combining Static Analysis With Directed Symbolic Execution for Scalable and Accurate Memory Leak Detection. IEEE Access, 2024, 12: 80128-80137. DOI: 10.1109/ACCESS.2024.3409838. https://doi.org/10.1109/ACCESS.2024.3409838