静态分析错误地报告越界访问
Static Analysis erroneously reports out of bounds access
在审查代码库时，我发现了一段特定的代码，它触发了有关“越界访问”的警告。查看代码后，我看不出报告的访问发生的方式 - 并尝试最小化代码以创建可重现的示例。然后，我使用我有权访问的两个商业静态分析器以及开源 Frama-C 检查了这个示例。
他们 3 个人都看到相同的“越界”访问。
我不知道。一起来看看：
3 extern int checker(int id);
4 extern int checker2(int id);
5
6 int compute(int *q)
7 {
8 int res = 0, status;
9
10 status = checker2(12);
11 if (!status) {
12 status = 1;
13 *q = 2;
14 for(int i=0; i<2 && 0!=status; i++) {
15 if (checker(i)) {
16 res = i;
17 status=checker2(i);
18 }
19 }
20 }
21 if (!status)
22 *q = res;
23 return status;
24 }
25
26 int someFunc(int id)
27 {
28 int p;
29 extern int data[2];
30
31 int status = checker2(132);
32 status |= compute(&p);
33 if (status == 0) {
34 return data[p];
35 } else
36 return -1;
37 }
请不要试图判断代码的质量，或者它为什么以这种方式做事。这是原始版本的黑客、裁剪和变异版本，其唯一目的是提供一个小示例来演示该问题。
我有权访问的所有分析器都报告了同样的事情——第 34 行调用者中的索引，执行 return data[p] 可能通过无效索引“2”读取。这是 Frama-C 的输出——但请注意，两个商业静态分析器提供完全相同的评估：
$ frama-c -val -main someFunc -rte why.c |& grep warning
...
why.c:34:[value] warning: accessing out of bounds index. assert p < 2;
让我们反向执行代码，看看第 34 行的越界访问是如何发生的：
- 要在第 34 行结束，对
checker2 和 compute 的 returned status 应该为 0。
- 对于
compute到return0（在调用者的第32行，在被调用者的第23行），这意味着我们已经在第22行执行了赋值——因为它在第 21 行检查 status 是否为 0。所以我们在传入的指针 q 中写入任何存储在变量 res 中的内容。该指针指向用于执行索引的变量——假定的越界索引。
- 因此，要体验对
data 的越界访问，它的尺寸恰好包含两个元素，我们必须向 res 写入一个既不是 0 也不是 1 的值。
- 我们在 14 处通过
for 循环写入 res；这将有条件地分配给 res；如果它 确实 分配，它将写入的值将是两个有效索引 0 或 1 之一 - 因为这些是 for 循环允许通过的值（它与 i<2). 绑定
- 由于在第12行初始化了
status，所以如果真的到了第12行，肯定至少会进入循环一次。如果我们写入 res，我们将写入一个很好的有效索引。
- 但是如果我们不写入呢？第 13 行的“默认”设置已将“2”写入我们的目标 - 这可能是让分析器感到恐惧的原因。那个“2”真的可以逃到调用者那里吗？
- 好吧，它似乎不是这样......如果
status 检查 - 在第 11 行或第 21 行失败，我们将 return 与非零 status;因此，无论我们写入（或未写入，并未初始化）到传入的 q 中的任何值都是无关紧要的；由于第 33 行的检查，调用者不会读取该值。
因此，要么我遗漏了一些东西，并且确实存在导致第 34 行索引 2 越界访问的情况（如何？），要么这是主流形式验证限制的示例。
帮忙？
在处理像== 0和!= 0在一个范围内的情况，比如[INT_MIN; INT_MAX]，需要告诉Frama-C/Eva拆分案例。
通过在适当的位置添加 //@ split 注释，您可以告诉 Frama-C/Eva 保持单独的状态，从而防止在评估 status 之前合并它们。
在本例中，您的代码如下所示（由@Virgile 提供）：
extern int checker(int id);
extern int checker2(int id);
int compute(int *q)
{
int res = 0, status;
status = checker2(12);
//@ split status <= 0;
//@ split status == 0;
if (!status) {
status = 1;
*q = 2;
for(int i=0; i<2 && 0!=status; i++) {
if (checker(i)) {
res = i;
status=checker2(i);
}
}
}
//@ split status <= 0;
//@ split status == 0;
if (!status)
*q = res;
return status;
}
int someFunc(int id)
{
int p;
extern int data[2];
int status = checker2(132);
//@ split status <= 0;
//@ split status == 0;
status |= compute(&p);
if (status == 0) {
return data[p];
} else
return -1;
}
在每个案例中，第一个 split 注释告诉 Eva 分别考虑案例 status <= 0 和 status > 0；这允许将区间 [INT_MIN, INT_MAX]“打破”为 [INT_MIN, 0] 和 [1, INT_MAX]；第二个注释允许将 [INT_MIN, 0] 分成 [INT_MIN, -1] 和 [0, 0]。当这 3 个状态分别传播时，Eva 能够准确区分代码中的不同情况，避免虚假警报。
您还需要允许 Frama-C/Eva 一些余量来保持状态分离（默认情况下，Eva 会优化效率，稍微积极地合并状态）；这是通过添加 -eva-precision 1 完成的（您的原始方案可能需要更高的值）。
相关选项：-eva-domains sign（以前是-eva-sign-domain）和-eva-partition-history N
Frama-C/Eva还有其他与分裂状态相关的选项；其中之一是 符号域 ，它计算有关变量符号的信息，可用于区分 0 值和非零值。在某些情况下（例如代码的稍微简化版本，其中 status |= compute(&p); 替换为 status = compute(&p);），符号域可能有助于拆分而无需注释。使用 -eva-domains sign 启用它（-eva-sign-domain for Frama-C <= 20）。
另一个相关选项是 -eva-partition history N，它告诉 Frama-C 将状态分区保持更长时间。
请注意，保持状态分离在分析方面的成本有点高，因此如果它包含多个分支，则在应用于“真实”代码时可能无法扩展。增加 -eva-precision 和 -eva-partition-history 的值可能会有帮助，同时添加 @ split 注释。
我想补充一些希望在将来有用的评论：
有效地使用Frama-C/Eva
Frama-C 包含几个插件和分析。特别是在这里，您使用的是 Eva 插件。它基于抽象解释执行分析，报告程序中所有可能的运行时错误（未定义行为，正如 C 标准所说）。因此，使用 -rte 是不必要的，并且会增加结果的噪音。如果 Eva 不能确定不存在某些警报，它会报告它。
将 -val 选项替换为 -eva。是一样的东西，只是前者被弃用了。
如果您想提高精度（以消除误报），请添加 -eva-precision N，其中 0 <= N <= 11。在您的示例程序中，它没有太大变化，但在具有多个调用堆栈的复杂程序中，额外的精度将花费更长的时间，但会最大限度地减少误报的数量。
此外，考虑为外部函数提供最小规范，以避免警告；这里它们不包含指针，但如果它们包含指针，您需要提供一个 assigns 子句来明确告诉 Frama-C 函数是否修改此类指针（或任何全局变量，例如).
使用 GUI 和 Studia
使用 Frama-C 图形界面和 Studia 插件（通过右键单击感兴趣的表达式并选择弹出菜单 Studia -> Writes 访问），并使用 Values 面板，您可以轻松跟踪分析推断的内容，并更好地了解警报和值的来源。唯一的缺点是，它不会 确切地 报告合并发生的位置。为了尽可能获得最精确的结果，您可能需要添加对 Eva 内置 Frama_C_show_each(exp) 的调用，并将其放入循环中以使 Eva 在其分析的每次迭代中显示 exp.
参见 Eva user manual 的第 9.3 节（显示中间结果）了解更多详细信息，包括类似的内置函数（例如 Frama_C_domain_show_each 和 Frama_C_dump_each，它们显示有关抽象域的信息).您可能需要在程序中 #include "__fc_builtin.h"。您可以使用 #ifdef __FRAMAC__ 允许在包含此 Frama-C 特定文件时编译原始代码。
吹毛求疵误报
Frama-C 是一种基于语义的工具，其主要分析详尽，但可能包含误报：Frama-C 可能在警报没有发生时报告警报，但它不应该忘记任何可能的警报。这是一种权衡，您不能在所有情况下都拥有精确的工具（尽管在此示例中，具有足够的 -eva-precision，Frama-C 是精确的，因为仅报告可能实际发生的问题）。
从这个意义上说，错误 意味着 Frama-C“忘记”指出某些问题，我们会非常关注它。在可能不会发生的地方指示警报对用户来说仍然是个问题（我们正在努力改进它，所以这种情况应该不会经常发生），但不是 Frama-C 中的 bug，所以我们更喜欢使用术语不精确，例如“Frama-C/Eva 不准确地报告越界访问”。
在审查代码库时，我发现了一段特定的代码，它触发了有关“越界访问”的警告。查看代码后，我看不出报告的访问发生的方式 - 并尝试最小化代码以创建可重现的示例。然后，我使用我有权访问的两个商业静态分析器以及开源 Frama-C 检查了这个示例。
他们 3 个人都看到相同的“越界”访问。
我不知道。一起来看看：
3 extern int checker(int id);
4 extern int checker2(int id);
5
6 int compute(int *q)
7 {
8 int res = 0, status;
9
10 status = checker2(12);
11 if (!status) {
12 status = 1;
13 *q = 2;
14 for(int i=0; i<2 && 0!=status; i++) {
15 if (checker(i)) {
16 res = i;
17 status=checker2(i);
18 }
19 }
20 }
21 if (!status)
22 *q = res;
23 return status;
24 }
25
26 int someFunc(int id)
27 {
28 int p;
29 extern int data[2];
30
31 int status = checker2(132);
32 status |= compute(&p);
33 if (status == 0) {
34 return data[p];
35 } else
36 return -1;
37 }
请不要试图判断代码的质量，或者它为什么以这种方式做事。这是原始版本的黑客、裁剪和变异版本，其唯一目的是提供一个小示例来演示该问题。
我有权访问的所有分析器都报告了同样的事情——第 34 行调用者中的索引，执行 return data[p] 可能通过无效索引“2”读取。这是 Frama-C 的输出——但请注意，两个商业静态分析器提供完全相同的评估：
$ frama-c -val -main someFunc -rte why.c |& grep warning
...
why.c:34:[value] warning: accessing out of bounds index. assert p < 2;
让我们反向执行代码，看看第 34 行的越界访问是如何发生的：
- 要在第 34 行结束，对
checker2和compute的 returnedstatus应该为 0。 - 对于
compute到return0（在调用者的第32行，在被调用者的第23行），这意味着我们已经在第22行执行了赋值——因为它在第 21 行检查status是否为 0。所以我们在传入的指针q中写入任何存储在变量res中的内容。该指针指向用于执行索引的变量——假定的越界索引。 - 因此，要体验对
data的越界访问，它的尺寸恰好包含两个元素，我们必须向res写入一个既不是 0 也不是 1 的值。 - 我们在 14 处通过
for循环写入res；这将有条件地分配给res；如果它 确实 分配，它将写入的值将是两个有效索引 0 或 1 之一 - 因为这些是for循环允许通过的值（它与i<2). 绑定
- 由于在第12行初始化了
status，所以如果真的到了第12行，肯定至少会进入循环一次。如果我们写入res，我们将写入一个很好的有效索引。 - 但是如果我们不写入呢？第 13 行的“默认”设置已将“2”写入我们的目标 - 这可能是让分析器感到恐惧的原因。那个“2”真的可以逃到调用者那里吗？
- 好吧，它似乎不是这样......如果
status检查 - 在第 11 行或第 21 行失败，我们将 return 与非零status;因此，无论我们写入（或未写入，并未初始化）到传入的q中的任何值都是无关紧要的；由于第 33 行的检查，调用者不会读取该值。
因此，要么我遗漏了一些东西，并且确实存在导致第 34 行索引 2 越界访问的情况（如何？），要么这是主流形式验证限制的示例。
帮忙？
在处理像== 0和!= 0在一个范围内的情况，比如[INT_MIN; INT_MAX]，需要告诉Frama-C/Eva拆分案例。
通过在适当的位置添加 //@ split 注释，您可以告诉 Frama-C/Eva 保持单独的状态，从而防止在评估 status 之前合并它们。
在本例中，您的代码如下所示（由@Virgile 提供）：
extern int checker(int id);
extern int checker2(int id);
int compute(int *q)
{
int res = 0, status;
status = checker2(12);
//@ split status <= 0;
//@ split status == 0;
if (!status) {
status = 1;
*q = 2;
for(int i=0; i<2 && 0!=status; i++) {
if (checker(i)) {
res = i;
status=checker2(i);
}
}
}
//@ split status <= 0;
//@ split status == 0;
if (!status)
*q = res;
return status;
}
int someFunc(int id)
{
int p;
extern int data[2];
int status = checker2(132);
//@ split status <= 0;
//@ split status == 0;
status |= compute(&p);
if (status == 0) {
return data[p];
} else
return -1;
}
在每个案例中，第一个 split 注释告诉 Eva 分别考虑案例 status <= 0 和 status > 0；这允许将区间 [INT_MIN, INT_MAX]“打破”为 [INT_MIN, 0] 和 [1, INT_MAX]；第二个注释允许将 [INT_MIN, 0] 分成 [INT_MIN, -1] 和 [0, 0]。当这 3 个状态分别传播时，Eva 能够准确区分代码中的不同情况，避免虚假警报。
您还需要允许 Frama-C/Eva 一些余量来保持状态分离（默认情况下，Eva 会优化效率，稍微积极地合并状态）；这是通过添加 -eva-precision 1 完成的（您的原始方案可能需要更高的值）。
相关选项：-eva-domains sign（以前是-eva-sign-domain）和-eva-partition-history N
Frama-C/Eva还有其他与分裂状态相关的选项；其中之一是 符号域 ，它计算有关变量符号的信息，可用于区分 0 值和非零值。在某些情况下（例如代码的稍微简化版本，其中 status |= compute(&p); 替换为 status = compute(&p);），符号域可能有助于拆分而无需注释。使用 -eva-domains sign 启用它（-eva-sign-domain for Frama-C <= 20）。
另一个相关选项是 -eva-partition history N，它告诉 Frama-C 将状态分区保持更长时间。
请注意，保持状态分离在分析方面的成本有点高，因此如果它包含多个分支，则在应用于“真实”代码时可能无法扩展。增加 -eva-precision 和 -eva-partition-history 的值可能会有帮助，同时添加 @ split 注释。
我想补充一些希望在将来有用的评论：
有效地使用Frama-C/Eva
Frama-C 包含几个插件和分析。特别是在这里，您使用的是 Eva 插件。它基于抽象解释执行分析，报告程序中所有可能的运行时错误（未定义行为，正如 C 标准所说）。因此，使用 -rte 是不必要的，并且会增加结果的噪音。如果 Eva 不能确定不存在某些警报，它会报告它。
将 -val 选项替换为 -eva。是一样的东西，只是前者被弃用了。
如果您想提高精度（以消除误报），请添加 -eva-precision N，其中 0 <= N <= 11。在您的示例程序中，它没有太大变化，但在具有多个调用堆栈的复杂程序中，额外的精度将花费更长的时间，但会最大限度地减少误报的数量。
此外，考虑为外部函数提供最小规范，以避免警告；这里它们不包含指针，但如果它们包含指针，您需要提供一个 assigns 子句来明确告诉 Frama-C 函数是否修改此类指针（或任何全局变量，例如).
使用 GUI 和 Studia
使用 Frama-C 图形界面和 Studia 插件（通过右键单击感兴趣的表达式并选择弹出菜单 Studia -> Writes 访问），并使用 Values 面板，您可以轻松跟踪分析推断的内容，并更好地了解警报和值的来源。唯一的缺点是，它不会 确切地 报告合并发生的位置。为了尽可能获得最精确的结果，您可能需要添加对 Eva 内置 Frama_C_show_each(exp) 的调用，并将其放入循环中以使 Eva 在其分析的每次迭代中显示 exp.
参见 Eva user manual 的第 9.3 节（显示中间结果）了解更多详细信息，包括类似的内置函数（例如 Frama_C_domain_show_each 和 Frama_C_dump_each，它们显示有关抽象域的信息).您可能需要在程序中 #include "__fc_builtin.h"。您可以使用 #ifdef __FRAMAC__ 允许在包含此 Frama-C 特定文件时编译原始代码。
吹毛求疵误报
Frama-C 是一种基于语义的工具，其主要分析详尽，但可能包含误报：Frama-C 可能在警报没有发生时报告警报，但它不应该忘记任何可能的警报。这是一种权衡，您不能在所有情况下都拥有精确的工具（尽管在此示例中，具有足够的 -eva-precision，Frama-C 是精确的，因为仅报告可能实际发生的问题）。
从这个意义上说，错误 意味着 Frama-C“忘记”指出某些问题，我们会非常关注它。在可能不会发生的地方指示警报对用户来说仍然是个问题（我们正在努力改进它，所以这种情况应该不会经常发生），但不是 Frama-C 中的 bug，所以我们更喜欢使用术语不精确，例如“Frama-C/Eva 不准确地报告越界访问”。