绕过 CBMC 检测到的无符号加法溢出答案

【问题标题】：Bypassing an unsigned addition overflow detected by CBMC绕过 CBMC 检测到的无符号加法溢出
【发布时间】：2015-06-26 04:54:56
【问题描述】：

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

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

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

【问题讨论】：

标签： c integer integer-overflow model-checking cbmc

【解决方案1】：

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

完整答案：

一般而言： 据我所知，CBMC 不允许排除特定属性（另一方面，您可以使用--property 标志仅检查一个特定属性）。如果您想获得官方答案/意见或提出功能请求，我建议您在CProver Support group 发帖。

_{（当然，可以使用__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 中未定义的行为，或者，正如 this answer 对问题 How to check integer overflow in C? 所说的那样：

[O]一旦你执行 x + y，如果它溢出，你已经被冲洗了。太晚了做任何检查 - 你的程序可能已经崩溃了。考虑到它就像检查除以零 - 如果你等到之后已执行除法检查，已经晚了。

另请参阅 Integer overflow and undefined behavior 和 How disastrous is integer overflow in 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);

给了

变体 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)

并且尝试将其转换为 signed int 很麻烦，因为它超出了范围（另请参阅 Does cast between signed and unsigned int maintain exact bit pattern of variable in memory? ）。

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

【讨论】：