Finding Memory Leaks in C/C++ Programs via Neuro-Symbolic Augmented Static Analysis

Abstract

Memory leaks remain prevalent in real-world C/C++ software. Static analyzers such as CodeQL provide scalable program analysis but frequently miss such bugs because they cannot recognize project-specific custom memory-management functions and lack path-sensitive control-flow modeling. We present MemHint, a neuro-symbolic pipeline that addresses both limitations by combining LLMs' semantic understanding of code with Z3-based symbolic reasoning. MemHint parses the target codebase and applies an LLM to classify each function as a memory allocator, deallocator, or neither, producing function summaries that record which argument or return value carries memory ownership, extending the analyzer's built-in knowledge beyond standard primitives such as malloc and free. A Z3-based validation step checks each summary against the function's control-flow graph, discarding those whose claimed memory operation is unreachable on any feasible path. The validated summaries are injected into CodeQL and Infer via their respective extension mechanisms. Z3 path feasibility filtering then eliminates warnings on infeasible paths, and a final LLM-based validation step confirms whether each remaining warning is a genuine bug. On seven real-world C/C++ projects totaling over 3.4M lines of code, MemHint detects 52 unique memory leaks (49 confirmed/fixed, 4 CVEs submitted) at approximately $1.7 per detected bug, compared to 19 by vanilla CodeQL and 3 by vanilla Infer.

Figures (5)

• Figure 1: A memory leak in OpenSSL (v3.6.1) openssl. tree_init allocates a policy tree ➊. The green path frees it correctly, but at ➋ the function returns without freeing tree (red). 24 hours of fuzzing with LeakSanitizer failed to trigger this path.
• Figure 2: A memory leak in FreeRDP (v3.23.0) freerdp. If freerdp_settings_set_pointer_len fails (➋), the object allocated by the custom allocator freerdp_certificate_clone (➊) is never freed. Static analyzers miss this bug as neither the allocator nor its paired deallocator (➍) is a known MM function.
• Figure 3: Overview of the MemHint pipeline. Stage 1 (Summary Generation): extract metadata, generate summaries with an LLM, and validate with Z3 SMT solver. Stage 2 (Summary-Augmented Analysis): inject validated summaries into static analyzers (e.g., CodeQL, Infer). Stage 3 (Warning Validation): filter infeasible warnings with Z3 and validate remaining ones using an LLM.
• Figure 4: Z3-based Summary Validation. (a)--(b) Allocator: (a) SAT: memory allocated at return; (b) UNSAT: memory is freed on all paths. (c)--(d) Deallocator: (c) SAT: target argument is freed; (d) UNSAT: only internal fields (e.g., arg0->f) are freed.
• Figure 5: Z3-based memory-leak feasibility checking (Phase 5) on the FreeRDP bug in Figure \ref{['fig:motivating-example-freerdp']}. Left: flagged function with key CFG nodes (allocation ➊, branches ➋, ➌, return ➍). Right: intra-procedural CFG with Z3 encoding. Along the dashed path, cert is allocated ($\mathit{alloc}=\mathit{true}$) but neither freed nor escaped; Z3 returns SAT, indicating a feasible leak.