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 检测到 19 个,原生 Infer 检测到 3 个。