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.
翻译:内存泄漏在现实世界的 C/C++ 软件中依然普遍存在。CodeQL 等静态分析器提供了可扩展的程序分析能力,但由于其无法识别项目特定的自定义内存管理函数以及缺乏路径敏感的流程建模,常常漏检此类缺陷。我们提出 MemHint,一个神经符号流水线,通过结合 LLM 对代码的语义理解与基于 Z3 的符号推理,解决了上述两个局限性。MemHint 解析目标代码库,并应用 LLM 将每个函数分类为内存分配器、释放器或两者皆非,生成记录哪个参数或返回值承载内存所有权的函数摘要,从而将分析器的内置知识扩展到标准原语(如 malloc 和 free)之外。一个基于 Z3 的验证步骤将每个摘要与函数的控制流图进行比对,丢弃那些所声称的内存操作在任何可行路径上均不可达的摘要。验证后的摘要通过各自的扩展机制注入到 CodeQL 和 Infer 中。随后,Z3 路径可行性过滤消除不可行路径上的警告,最后一个基于 LLM 的验证步骤确认每个剩余警告是否为真正的缺陷。在七个总代码量超过 340 万行的现实世界 C/C++ 项目上,MemHint 检测出 52 个独特的内存泄漏(其中 49 个已确认/修复,4 个已提交 CVE),每个检测到的缺陷成本约为 1.7 美元,而原始 CodeQL 和原始 Infer 分别仅检测出 19 个和 3 个。