通过神经符号增强静态分析查找 C/C++ 程序中的内存泄漏

内存泄漏在现实世界的 C/C++ 软件中仍然普遍存在。 CodeQL 等静态分析器提供可扩展的程序分析，但经常会错过此类错误，因为它们无法识别特定于项目的自定义内存管理函数，并且缺乏路径敏感的控制流建模。我们提出了 MemHint，一种神经符号管道，通过将 LLM 对代码的语义理解与基于 Z3 的符号推理相结合来解决这两个限制。 MemHint 解析目标代码库并应用 LLM 将每个函数分类为内存分配器、释放器或两者都不是，生成记录哪个参数或返回值携带内存所有权的函数摘要，从而将分析器的内置知识扩展到标准原语（例如 malloc 和 free）之外。基于 Z3 的验证步骤根据函数的控制流图检查每个摘要，丢弃那些在任何可行路径上都无法访问其声明的内存操作的摘要。经过验证的摘要通过各自的扩展机制注入到 CodeQL 和 Infer 中。然后，Z3 路径可行性过滤消除了不可行路径上的警告，最后基于 LLM 的验证步骤确认每个剩余的警告是否是真正的错误。在总共超过 360 万行代码的 8 个真实 C/C++ 项目中，MemHint 检测到 54 个独特的内存泄漏（53 个已确认/已修复），每个检测到的错误大约花费 1.7 美元，而普通 CodeQL 为 19 个，普通 Infer 为 3 个。