5

我应该如何证明如下代码的正确性，为了避免效率低下，它依赖于模运算？

#include <stdint.h>

uint32_t my_add(uint32_t a, uint32_t b) {
    uint32_t r = a + b;
    if (r < a)
        return UINT32_MAX;
    return r;
}

我已经尝试过 WP 的“int”模型，但是，如果我理解正确，该模型配置了 PO 中逻辑整数的语义，而不是 C 代码的正式模型。例如，当使用“int”模型时，WP 和 RTE 插件仍然需要并为上面的无符号加法注入溢出断言 PO。

在这种情况下，我是否可以为语句或基本块添加规定逻辑模型的注释，以便我可以告诉 Frama-C 特定编译器如何实际解释语句？如果是这样，我可以使用其他验证技术来处理已定义但经常导致缺陷的行为，如无符号环绕、编译器定义的行为、非标准行为（内联组件？）等，然后证明周围的代码。我正在描绘类似于（但比）更强大的“断言修复”，用于通知某些静态分析器某些属性在它们无法为自己派生属​​性时保持不变。

我正在使用 Frama-C Fluorine-20130601，作为参考，使用 alt-ergo 95.1。

4

2 回答 2

1

I'm working with Frama-C Fluorine-20130601

Glad to see that you found a way to use the latest version.

Here are some random bits of information that, although they do not completely answer your question, do not fit in a StackOverflow comment:

Jessie has:

#pragma JessieIntegerModel(modulo)

The above pragma makes it consider that all overflows (both the undefined signed ones and the defined unsigned ones) wrap around (in the same of signed overflows, in 2's complement arithmetic). The generated proof obligations are much harder, because they contain additional modulo operations everywhere. Of automated theorem provers, typically only Simplify is able to do something with them.

In Fluorine, RTE does not warn about a + b by default:

$ frama-c -rte t.c -then -print
[kernel] preprocessing with "gcc -C -E -I.  t.c"
[rte] annotating function my_add
/* Generated by Frama-C */
typedef unsigned int uint32_t;
uint32_t my_add(uint32_t a, uint32_t b)
{
  uint32_t __retres;
  uint32_t r;
  r = a + b;
  if (r < a) {
    __retres = 4294967295U;
    goto return_label;
  }
  __retres = r;
  return_label: return __retres;
}

RTE can be made to warn about the unsigned addition with option -warn-unsigned-overflow:

$ frama-c -warn-unsigned-overflow -rte t.c -then -print
[kernel] preprocessing with "gcc -C -E -I.  t.c"
[rte] annotating function my_add
/* Generated by Frama-C */
typedef unsigned int uint32_t;
uint32_t my_add(uint32_t a, uint32_t b)
{
  uint32_t __retres;
  uint32_t r;
  /*@ assert rte: unsigned_overflow: 0 ≤ a+b; */
  /*@ assert rte: unsigned_overflow: a+b ≤ 4294967295; */
  r = a + b;
  …

But that's precisely the opposite of what you want so I don't see why you would do that.

于 2013-08-02T22:29:38.353 回答
1

您没有提供您一直在使用的确切命令行。我猜这是frama-c -wp -wp-rte file.c -pp-annot。在这种情况下，确实会生成 RTE 可能发出的所有断言。但是，您可以对其进行更好的控制，方法是指示 frama-c 首先仅生成您感兴趣的 RTE 类别（注意它们由两种选项控制：offrama-c -rte-help和-warn-{signed,unsigned}-{overflow,downcast}定义在内核），然后在结果上启动 wp。frama-c -rte -pp-annot file.c -then -wp默认情况下，rte 不会将无符号溢出视为错误，因此使用上面的命令行，我可以证明您的函数符合以下规范：

/*@
  behavior no_overflow:
    assumes a + b <= UINT32_MAX;
    ensures \result == a+b;
  behavior saturate:
    assumes a+b > UINT32_MAX;
    ensures \result == UINT32_MAX;
 */
 uint32_t my_add(uint32_t a,uint32_t b);
于 2013-08-08T12:38:47.203 回答