首页 文章

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

提问于
浏览 次
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 .

frama-c alt-ergo

2 回答

  • 1

    我正在使用Frama-C Fluorine-20130601

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

    以下是一些随机信息，虽然它们没有完全回答您的问题，但不适合StackOverflow注释：

    杰西有：

    #pragma JessieIntegerModel(modulo)

    上面的编译指示使得它考虑所有溢出（未定义的有符号的和已定义的无符号的）都包围（在有符号的溢出中，在2的补码算法中） . 生成的证明义务要困难得多，因为它们在任何地方都包含额外的模运算 . 在自动化定理证明器中，通常只有Simplify能够对它们做一些事情 .

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

    $ 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;
}

    可以使用选项 -warn-unsigned-overflow 对RTE进行无符号添加警告：

    $ 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;
  …

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

    回复于
  • 1

    您没有提供您一直使用的确切命令行 . 我想这是 frama-c -wp -wp-rte file.c -pp-annot . 实际上，在这种情况下，生成了RTE可能发出的所有断言 . 然而，您可以通过指示frama-c首先仅生成您感兴趣的RTE类别来对其进行更精细的控制（请注意它们由两种选项控制： frama-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);
    回复于

相关问题