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 (47 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个独特的内存泄漏(47个已确认/修复,4个已提交CVE),每个检测到的缺陷成本约为1.7美元,而原始CodeQL和Infer分别检测到19个和3个。