c - 绕过 CBMC 检测到的无符号加法溢出

Question

CBMC 在以下行中检测到可能的无符号加法溢出：

l = (t + *b)&(0xffffffffL);
c += (l < t);

我同意第一行有溢出的可能性，但我正在处理 CBMC 无法查看的下一行中的进位。如果出现溢出，我将设置进位 1。因此，由于我知道这一点，这就是我希望我的代码工作的方式，我想继续验证过程。那么，我是如何告诉 CBMC 忽略这个错误并继续前进的呢？

score 3 · Accepted Answer

TL; DR这取决于变量的实际类型。在所有情况下，CBMC 都会检测到可能导致未定义行为的实际错误。这意味着，您应该修复您的代码，而不是禁用 CBMC 中的消息。

完整答案：

一般来说：据我所知，CBMC 不允许排除特定属性（另一方面，您只能使用--property标志检查一个特定属性）。如果您想要官方答案/意见或提出功能请求，我建议您在CProver 支持组中发帖。

_{（当然，可以使用__CPROVER_assume以使 CBMC 排除导致错误的痕迹，但这将是一个非常、非常、非常糟糕的主意，因为这可能会使其他问题无法解决。）}

变体 1：我假设您的代码看起来像（与此相关：请发布独立的示例并准确解释问题所在，很难猜到这些事情）

long nondet_long(void);

void main(void) {
  long l = 0;
  int c = 0;
  long t = nondet_long();
  long s = nondet_long();
  long *b = &s;

  l = (t + *b) & (0xffffffffL); 
  c += (l < t);
}

你正在跑步

    cbmc --signed-overflow-check test.c

给出类似于以下的输出？

    CBMC 版本 5.1 64 位 x86_64 macos
    解析test.c
    转换
    型式检查试验
    生成 GOTO 程序
    添加 CPROVER 库
    函数指针移除
    部分内联
    通用属性检测
    开始有界模型检查
    程序表达式的大小：41 步
    简单切片删除了 3 个作业
    生成 2 个 VCC，简化后剩余 2 个
    将问题传递给命题约简
    转换 SSA
    运行命题约简
    后期处理
    使用简化器使用 MiniSAT 2.2.0 求解
    792 个变量，2302 个子句
    SAT 检查器：否定声明是 SATISFIABLE，即不成立
    运行时间决策程序：0.006s
    构建错误跟踪

    反例：

    状态 17 文件 test.c 第 4 行函数主线程 0
    -------------------------------------------------- --
      l=0 (00000000000000000000000000000000000000000000000000000000000000000)

    状态 18 文件 test.c 第 4 行函数主线程 0
    -------------------------------------------------- --
      l=0 (00000000000000000000000000000000000000000000000000000000000000000)

    状态 19 文件 test.c 第 5 行函数主线程 0
    -------------------------------------------------- --
      c=0 (00000000000000000000000000000000)

    状态 20 文件 test.c 第 5 行函数主线程 0
    -------------------------------------------------- --
      c=0 (00000000000000000000000000000000)

    状态 21 文件 test.c 第 6 行函数主线程 0
    -------------------------------------------------- --
      t=0 (00000000000000000000000000000000000000000000000000000000000000000)

    状态 22 文件 test.c 第 6 行函数主线程 0
    -------------------------------------------------- --
      t=-9223372036854775808 (1000000000000000000000000000000000000000000000000000000000000000)

    状态 23 文件 test.c 第 7 行函数主线程 0
    -------------------------------------------------- --
      s=0 (0000000000000000000000000000000000000000000000000000000000000000)

    状态 24 文件 test.c 第 7 行函数主线程 0
    -------------------------------------------------- --
      s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001)

    状态 25 文件 test.c 第 8 行函数主线程 0
    -------------------------------------------------- --
      b=((long int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

    状态 26 文件 test.c 第 8 行函数主线程 0
    -------------------------------------------------- --
      b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000)

    侵权财产：
      文件 test.c 第 10 行函数 main
      有符号 + in t + *b 上的算术溢出
      !overflow("+", 有符号的 long int, t, *b)

    验证失败

我不认为你应该禁用这个属性检查，即使你可以。正如您所说，这样做的原因是，这种加法可能会溢出，并且整数溢出是 C 中未定义的行为，或者，正如对如何在 C 中检查整数溢出问题的回答一样？很好地说：

[O] 一旦你执行了 x + y，如果它溢出，你已经被水洗了。做任何检查都太晚了——你的程序可能已经崩溃了。把它想象成检查除以零 - 如果你等到执行除法之后再检查，那已经太晚了。

另请参阅整数溢出和未定义行为和C++ 中的整数溢出有多灾难性？.

因此，这是一个实际的错误，CBMC 有充分的理由告诉您它。您实际上应该做的是调整您的代码，以便没有潜在的溢出！上面提到的答案暗示了类似（记得包括limits.h）：

if ((*b > 0 && t > LONG_MAX - *b) 
    || (*b < 0 && LONG_MIN < *b && t < LONG_MIN - *b) 
    || (*b==LONG_MIN && t < 0))
{
    /* Overflow will occur, need to do maths in a more elaborate, but safe way! */
    /* ... */
}
else
{
    /* No overflow, addition is safe! */
    l = (t + *b) & (0xffffffffL);
    /* ... */
}

变体 2：在这里，我假设您的代码如下所示：

unsigned int nondet_uint(void);

void main(void) {
  unsigned int l = 0;
  unsigned int c = 0;
  unsigned int t = nondet_uint();
  unsigned int s = nondet_uint();
  unsigned int *b = &s;

  l = (t + *b) & (0xffffffffL);
  c += (l < t);
}

你正在跑步

    cbmc --unsigned-overflow-check test.c

给出类似于以下的输出？

CBMC 版本 5.1 64 位 x86_64 macos
解析test.c
转换
型式检查试验
生成 GOTO 程序
添加 CPROVER 库
函数指针移除
部分内联
通用属性检测
开始有界模型检查
程序表达式的大小：42 步
简单切片删除了 3 个作业
生成 3 个 VCC，简化后剩余 3 个
将问题传递给命题约简
转换 SSA
运行命题约简
后期处理
使用简化器使用 MiniSAT 2.2.0 求解
519 个变量，1306 个子句
SAT 检查器：否定声明是 SATISFIABLE，即不成立
运行时间决策程序：0.01s
构建错误跟踪

反例：

状态 17 文件 test.c 第 4 行函数主线程 0
-------------------------------------------------- --
  l=0 (00000000000000000000000000000000)

状态 18 文件 test.c 第 4 行函数主线程 0
-------------------------------------------------- --
  l=0 (00000000000000000000000000000000)

状态 19 文件 test.c 第 5 行函数主线程 0
-------------------------------------------------- --
  c=0 (00000000000000000000000000000000)

状态 20 文件 test.c 第 5 行函数主线程 0
-------------------------------------------------- --
  c=0 (00000000000000000000000000000000)

状态 21 文件 test.c 第 6 行函数主线程 0
-------------------------------------------------- --
  t=0 (00000000000000000000000000000000)

状态 22 文件 test.c 第 6 行函数主线程 0
-------------------------------------------------- --
  t=4187126263 (11111001100100100111100111110111)

状态 23 文件 test.c 第 7 行函数主线程 0
-------------------------------------------------- --
  s=0 (000000000000000000000000000000000)

状态 24 文件 test.c 第 7 行函数主线程 0
-------------------------------------------------- --
  s=3329066504 (11000110011011011000011000001000)

状态 25 文件 test.c 第 8 行函数主线程 0
-------------------------------------------------- --
  b=((无符号整数 *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

状态 26 文件 test.c 第 8 行函数主线程 0
-------------------------------------------------- --
  b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000)

侵权财产：
  文件 test.c 第 10 行函数 main
  unsigned + in t + *b 上的算术溢出
  !overflow("+", unsigned int, t, *b)

验证失败

同样，这是一个实际的错误，CBMC 有充分的理由告诉您它。这个可以通过

l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);

这使

CBMC 版本 5.1 64 位 x86_64 macos
解析test.c
转换
型式检查试验
生成 GOTO 程序
添加 CPROVER 库
函数指针移除
部分内联
通用属性检测
开始有界模型检查
程序表达式的大小：42 步
简单切片删除了 3 个作业
生成 3 个 VCC，简化后剩余 3 个
将问题传递给命题约简
转换 SSA
运行命题约简
后期处理
使用简化器使用 MiniSAT 2.2.0 求解
542 个变量，1561 个子句
SAT 检查器不一致：否定的声明是 UNSATISFIABLE，即持有
运行时间决策程序：0.002s
验证成功

变体 3：如果事情和前一个一样，但你有signed int而不是unsigned int，事情会变得有点复杂。在这里，假设您使用（以稍微复杂的方式编写以更好地了解发生了什么）

int nondet_int(void);

void main(void) {
  int l = 0;
  int c = 0;
  int t = nondet_int();
  int s = nondet_int();

  long longt = (long)t;
  long longs = (long)s;
  long temp1 = longt + longs;
  long temp2 = temp1 & (0xffffffffL);

  l = temp2;
  c += (l < t);
}

并运行

    cbmc --signed-overflow-check test.c

你会得到

CBMC 版本 5.1 64 位 x86_64 macos
解析test.c
转换
型式检查试验
生成 GOTO 程序
添加 CPROVER 库
函数指针移除
部分内联
通用属性检测
开始有界模型检查
程序表达式的大小：48 步
简单切片删除了 3 个作业
生成 3 个 VCC，简化后剩余 3 个
将问题传递给命题约简
转换 SSA
运行命题约简
后期处理
使用简化器使用 MiniSAT 2.2.0 求解
872 个变量，2430 个子句
SAT 检查器：否定声明是 SATISFIABLE，即不成立
运行时间决策程序：0.008s
构建错误跟踪

反例：

状态 17 文件 test.c 第 4 行函数主线程 0
-------------------------------------------------- --
  l=0 (00000000000000000000000000000000)

状态 18 文件 test.c 第 4 行函数主线程 0
-------------------------------------------------- --
  l=0 (00000000000000000000000000000000)

状态 19 文件 test.c 第 5 行函数主线程 0
-------------------------------------------------- --
  c=0 (00000000000000000000000000000000)

状态 20 文件 test.c 第 5 行函数主线程 0
-------------------------------------------------- --
  c=0 (00000000000000000000000000000000)

状态 21 文件 test.c 第 6 行函数主线程 0
-------------------------------------------------- --
  t=0 (00000000000000000000000000000000)

状态 22 文件 test.c 第 6 行函数主线程 0
-------------------------------------------------- --
  t=-2147483648 (10000000000000000000000000000000)

状态 23 文件 test.c 第 7 行函数主线程 0
-------------------------------------------------- --
  s=0 (000000000000000000000000000000000)

状态 24 文件 test.c 第 7 行函数主线程 0
-------------------------------------------------- --
  s=1 (00000000000000000000000000000001)

状态 25 文件 test.c 第 9 行函数主线程 0
-------------------------------------------------- --
  longt=0 (00000000000000000000000000000000000000000000000000000000000000000)

状态 26 文件 test.c 第 9 行函数主线程 0
-------------------------------------------------- --
  longt=-2147483648 (111111111111111111111111111111110000000000000000000000000000000)

状态 27 文件 test.c 第 10 行函数主线程 0
-------------------------------------------------- --
  多头= 0（00000000000000000000000000000000000000000000000000000000000000000）

状态 28 文件 test.c 第 10 行函数主线程 0
-------------------------------------------------- --
  多头= 1（00000000000000000000000000000000000000000000000000000000000000001）

状态 29 文件 test.c 第 11 行函数主线程 0
-------------------------------------------------- --
  temp1=0 (00000000000000000000000000000000000000000000000000000000000000000)

状态 31 文件 test.c 第 11 行函数主线程 0
-------------------------------------------------- --
  temp1=-2147483647 (111111111111111111111111111111110000000000000000000000000000001)

状态 32 文件 test.c 第 12 行函数主线程 0
-------------------------------------------------- --
  temp2=0 (0000000000000000000000000000000000000000000000000000000000000000)

状态 33 文件 test.c 第 12 行函数主线程 0
-------------------------------------------------- --
  temp2=2147483649 (0000000000000000000000000000000010000000000000000000000000000001)

侵权财产：
  文件 test.c 第 14 行函数 main
  (signed int)temp2 中带符号类型转换的算术溢出
  temp2 = -2147483648l

验证失败

或者，写得更简洁，如果你有

t == -2147483648 (0b10000000000000000000000000000000)
s == 1           (0b00000000000000000000000000000001)

然后

temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)

并且尝试将其转换为 asigned int很麻烦，因为它超出了范围（另请参见是否在有符号和无符号 int 之间进行强制转换保持内存中变量的精确位模式？）。

正如你所看到的，这个反例也是一个实际的错误，而且，CBMC 再次告诉你它是正确的。这尤其意味着，您的屏蔽/数学无法按预期工作（您的屏蔽将负数变为超出范围的正数）并且您需要修复代码，以便结果在必要的范围内。（为了确保获得正确的结果，仔细考虑您实际想要做什么可能是值得的。）

c - 绕过 CBMC 检测到的无符号加法溢出

1 回答 1

Related

Reference