Eva 方法计算区间 [frama-c]

Question

我的目标是了解 Eva 如何缩小变量的区间。例如：

unsigned int nondet_uint(void);
int main()
{
  unsigned int x=nondet_uint();
  unsigned int y=nondet_uint();
  //@ assert x >= 20 && x <= 30;
  //@ assert y <= 60;
  //@ assert(x>=y);
  return 0;
}

所以，我们有 x=[20,30] 和 y=[0,60]。但是，Eva 的结果将 y 缩小到 [0,30]，这是域可能有效的地方。

[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  x ∈ [20..30]
  y ∈ [0..30]
  __retres ∈ {0}

我尝试了 Eva 插件的一些选项，但 none 显示了它的步骤。能否请您提供有关如何计算这些值的方法或出版物？

Answer 1

在抽象解释期间显示值

I tried some options for the Eva plugin, but none showed the steps for it.

跟踪评估的最有效方法不是通过命令行选项，而是通过在代码中添加 Frama_C_show_each(exp) 语句。这些是特殊的函数调用，在分析过程中，它们发出包含在其中的表达式的值。它们在循环中特别有用，例如查看何时触发加宽，循环计数器值会发生什么变化。

请注意，即使对于非常小的程序，显示所有的中间评估和减少步骤也会非常冗长。默认情况下，此信息不会公开，因为它太密集而且很少有用。

对于初学者，尝试添加 Frama_C_show_each 语句，并使用 Frama-C GUI 查看结果。它允许关注代码中的任何表达式，并在 Values 选项卡中显示给定表达式的值，在选定的语句中，对于每个调用堆栈。您还可以按 Ctrl+E 并键入任意表达式以在该语句中计算其值。

如果您想了解有关值、它们的减少和整体机制的更多详细信息，请参阅下面的部分。

有关 Eva 值的详细信息

您的问题与 Eva 中抽象解释引擎使用的值有关。

Eva User Manual 的第 3 章描述了引擎使用的抽象，简而言之：

整数集，最精确但限于元素数量（由选项 -eva-ilevel 修改，在 Frama-C 22 上默认设置为 8）；
具有周期性信息的整数区间（也称为 modulo，或 congruence），例如[2..42],2%10 是包含 {2, 12, 22, 32, 42} 的集合。在简单的情况下，例如[2..42]，包括2到42之间的所有整数；
地址集（对于指针），偏移量使用上述值表示（整数集或区间）；
浮点变量的区间（与整数不同，没有小的浮点值集）。

为什么所有这些都是必要的？因为不了解其中的一些细节，您将很难理解为什么分析有时准确，有时不准确。

请注意，文档中使用的术语是 reduction，而不是 shrinkage。所以在搜索线索的时候在Eva手册中寻找与reduce相关的词

例如，在下面的代码中：

int a = Frama_C_interval(-5, 5);
if (a != 0) {
  //@ assert a != 0;
  int b = 5 / a;
}

默认情况下，分析将不能够从if内的区间中删除0，因为[-5..-1];[1..5]是不是一个区间，而是一个不相交的区间并集。但是，如果元素个数下降到以下-eva-ilevel，那么分析会把它转化为small set，得到一个精确的结果。因此，更改一些分析选项将导致不同的范围和不同的结果。

在某些情况下，您可以强制 Eva 使用析取进行计算，例如通过添加 split ACSL 注释，例如//@ split a < b || a >= b;。但是您仍然需要为分析提供一些“燃料”，以便它分别评估两个分支。最简单的方法是使用 -eva-precision N，其中 N 是 0 到 11 之间的整数。 N 越高，允许发生的分裂越多，但时间越长分析可能需要。

请注意，为了确保分析的终止，使用了一些机制，例如 widening。没有它，一个简单的循环可能需要数十亿个评估步骤才能终止。这种机制可能会引入额外的值，从而导致分析不那么精确。

最后，还有一些抽象域（选项-eva-domains）允许除默认值之外的其他类型的值上面提到的那些。例如，符号域 允许在负值、零值和正值之间拆分值，并且可以避免上例中的不精确性。 Eva 用户手册包含每个域的使用示例，说明它们何时有用。

Eva 方法计算区间 [frama-c]

Eva method to compute intervals [frama-c]

frama-c

在抽象解释期间显示值

有关 Eva 值的详细信息