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 eight real-world C/C++ projects totaling over 3.6M lines of code, MemHint detects 54 unique memory leaks (53 confirmed/fixed) 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 的验证确认每个剩余告警是否为真正的缺陷。在八个现实世界 C/C++ 项目(总计超过 360 万行代码)上,MemHint 检测出 54 个独特的内存泄漏(53 个已确认/修复),每个检测到的缺陷成本约为 1.7 美元,而未修改的 CodeQL 和 Infer 分别只能检测出 19 个和 3 个。