如何在 Frama-C + EVA 中证明非确定性值的简单等式？

Posted 2023-03-31

【中文标题】如何在 Frama-C + EVA 中证明非确定性值的简单等式？

【英文标题】：How does one prove simple equalities of non-deterministic values in Frama-C + EVA?

【发布时间】：2019-10-04 03:19:58

【问题描述】：

我对 Frama-C 版本 18.0 (Argon) 的行为有点困惑。

给定以下程序：

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() 

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;

我希望任何跟踪相等性的抽象域都可以很容易地证明该断言。但是，调用

frama-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给予：

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_interval
[eva] using specification for function __FC_assert
[eva:alarm] foo.c:20: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  i ∈ [--..--]
  j ∈ [--..--]
  __retres ∈ 0

我错过了什么吗？

【参考方案1】：

有趣。您的示例不是由-eva -eva-equality-domain 处理的，这是出于其他目的而编写的。因此，当x 和y 已知相等时，x == y 的特殊情况尚未编写。这很容易添加。

（考虑到域的名称，这可能会让人感到惊讶。当我们有无趣的别名（例如内核添加的临时变量）时，相等域更适合于实现更多的反向传播。）

关于来自 Apron 的域，这更令人惊讶。我修改了你的例子：

  j = i;

  int b = j - i;
  int c = j == i;
  Frama_C_dump_each_domain();

运行frama-c -eva -eva-polka-equalities foo.c -value-msg-key d-apron 会得到以下结果：

[eva] c/eq.c:23: 
  Frama_C_dump_each_domain:
  # Cvalue domain:
  i ∈ [--..--]
  j ∈ [--..--]
  b ∈ 0
  c ∈ 0; 1
  __retres ∈ UNINITIALIZED
  # Polka linear equalities domain:
  [|-i_44+j_45=0; b_46=0|]

如您所见，Apron 已经推断出i 和j 之间的关系（后缀为行号），将b 简化为0，但并没有将c 简化为1。这令人惊讶对我来说，但解释了你观察到的不精确。它也不适用于八边形域。

我对关系域中的抽象转换器不太熟悉，所以这可能是意料之中的，但这确实令人费解。处理关系运算符的代码存在于 Frama-C/Eva/Apron 中，但部分是自己编写的（它不仅仅是对 Apron 原语的简单调用）。特别是，它调用运算符进行减法，并分析结果与 0 的相等性。很难理解为什么b 会精确，而c 会不精确。