static-analysis - 使用 ACSL/Frama-C 引入数学函数规范

Question

是否可以在 ACSL 中为通常在使用 -lm 编译时调用的函数实现规范，如 sqrt ？我将它用于 Frama-C 的插件 WP。

这是一个小例子来说明我想要做什么。

/*@ requires sqrt_spec: \forall float x; 
             \model(sqrt(x)) * \model(sqrt(x)) == \model(x);  
    ensures [...] */  

void f (...) {
double y = sqrt x;
[...]
}

显然，如果我这样做 WP 会哭，因为当我在注释中使用 sqrt 时它不存在。

[kernel] user error: unbound function sqrt in annotation

所以我想定义一个抽象的 sqrt，但我的测试都没有工作:

#define sqrt(x) (...)

对于这个，我看不到我可以放入 (...) 的内容，因为我想要一个抽象的定义，而不是重新实现整个 float sqrt。

/*@  axiomatic SqrtSpec {
logic real sqrt (real x);
} */

而这个并不能解决我的问题:

Neither code nor specification for function sqrt, generating default assigns from the prototype.

Answer 1

Frama-C 内置逻辑功能 \sqrt运行于 real数字(请注意，内置函数和谓词通常以反斜杠 \ 为前缀，以避免与现有 C 标识符发生任何冲突)。也就是说，为 sqrt 提供一个公理定义并不难。 :

axiomatic Sqrt {
  logic real sqrt(real);
  axiom real_def: \forall real x; x >= 0 ==> x == sqrt(x) * sqrt(x);
}

另外请注意，Gappa ( http://gappa.gforge.inria.fr/ ) 是唯一知道浮点数(与实数相反)的自动证明器，但即使您已经安装了它，解除处理浮点计算的证明义务也可能非常困难.

更新

如果你想公理化 double sqrt(double) (和/或 float sqrt(float) )，想法是表征相对于 \sqrt 的结果的误差在实数上操作，即类似于

axiomatic Sqrt {
  logic float sqrt(float sqrt);
  axiom sqrt_def: \forall float x; \is_finite(x) && x>= 0.0 ==> sqrt(x) ==  (float)\sqrt(x);
}

当然，这种特征可能有点限制。你可能想要类似 \abs(sqrt(x) - \sqrt(x)) <= err_bound * \sqrt(x) 的东西，但我不得不承认我在浮点计算方面不够流利，无法给出 err_bound 的适当值。从我的头顶。

更新 2

假设你有一个 逻辑 sqrt有你想要的属性，说 C sqrt具有相同的行为只是给它一个契约(Contract)的问题:

/*@ requires \is_finite(x); //unless you want to play with NaN or infinities 
    assigns \nothing;
    ensures \result == sqrt(x);
 */
extern float sqrt(float x);

一个函数的规范是在链接阶段合并的，所以这个合约是否写在 math.h中无关紧要。 (注意:在标准头文件 sqrt 接受(并返回)一个 double ，它是 sqrtf 在 float 上运行)或在您自己的文件中。