依赖于无符号整数溢出的代码的证明？

Question

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

#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.

Answer 1

\n

我正在使用 Frama-C Fluorine-20130601

\n

\n\n

很高兴看到您找到了使用最新版本的方法。

\n\n

以下是一些随机信息，尽管它们不能完全回答您的问题，但不适合 StackOverflow 评论：

\n\n

杰西有：

\n\n

#pragma JessieIntegerModel(modulo)\n

\n\n

上面的编译指示使它认为所有溢出（未定义的有符号溢出和已定义的无符号溢出）都会回绕（与有符号溢出相同，在 2 的补码算术中）。生成的证明义务要困难得多，因为它们到处都包含额外的模运算。在自动定理证明器中，通常只有 Simplify 能够用它们做一些事情。

\n\n

在 Fluorine 中，RTE 默认情况下不会警告 a + b：

\n\n

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

\n\n

可以使用 RTE 选项来警告未签名的加法-warn-unsigned-overflow：

\n\n

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

\n\n

但这与你想要的恰恰相反，所以我不明白你为什么要这样做。

\n