[论文笔记] Interleaving Static Analysis and LLM Prompting

Introduction

来自 PLDI’24 的 workshop SOAP。一种交错使用 LLM 和静态分析工具的方法，应用于 C 语言编写的系统代码中函数的错误规范推断问题。

Background

EESI

C 语言并没有错误处理。开发者会把错误代码作为返回值返回，对这些返回值的处理不当容易引发 bug。错误规范是指函数在发生错误时返回的值的集合。

EESI 就是针对错误规范的一个静态分析工具。EESI 接受多种形式的用户提供的可选初始领域知识：(1) 初始错误规范，(2) 一组已知的错误代码，(3) 成功代码，以及 (4) 仅在错误路径中被调用的错误函数。借助这些初始的领域知识，EESI 使用静态分析推断新的错误规格。推理规则包括：若函数返回一个预定义的错误码，则该值为错误值；若函数调用了“仅错误路径调用的函数”，则其返回值应为错误值等等。

EESI 具有两个固有缺陷：（1）EESI 的推理规则是对惯用的代码模式的建模，提供的近似不足以建模所有的程序，（2）EESI 无法处理第三方代码。

LLM

略

Overview example

EESI 对于 x509_get_attr_type_value 只推断出了 \(\bot\)。LLM 也没有推理出正确的错误规范，推断出错误路径上的返回值是负错误代码 MBEDTLS_ERR_X509_INV_NAME 加上任何非零值，也就是 \(\top\)。如果我们还在LLM提示中包含来自 EESI 的中间结果（图中的 Function Context），那么 LLM 能够返回 x509_get_attr_type_value 在错误时返回的值 \(< 0\)。LLM 也可以帮助 EESI 分析下面的这个代码的错误规范：

LLM 另一个好处是可以通过语义关系推测错误代码和未知外部函数的关系，比如函数 otrng_global_state_instance_tags_read_ from 和代码 OTRNG_ERROR。

Approach

Prompt

提示词包括 common context，function context 和 question。

• Common context 包括问题描述和EESI静态分析器使用的抽象域的解释，共同上下文还包含来自领域知识输入的任何错误代码、成功代码和错误函数。还提供多个基本的思维链示例以便 LLM 生成可解析的输出。
• Function context 与正在被 LLM 查询的函数的任何相关的错误规范有关。

Error specification inference

由于第三方函数没有源代码定义，因此我们无法对其进行静态分析，所以交给 LLM 看是否能学到错误规范。如果 EESI 分析失败了，再次调用 LLM 进行分析。

这个工作的思路比较简单。