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

Question

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

Aci*_*urn 5 c integer model-checking integer-overflow cbmc

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

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

Run Code Online (Sandbox Code Playgroud)

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

Answer 1

god*_*lka 3

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

完整答案：

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

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

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

Run Code Online (Sandbox Code Playgroud)

你正在跑步

    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 检查器：否定的主张是可满足的，即不成立
    决策过程运行时间：0.006s
    构建错误跟踪

    反例：

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

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

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

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

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

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

    状态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
      t + *b 中的有符号 + 算术溢出
      !overflow("+", 有符号长整型, t, *b)

    验证失败

我认为您不应该禁用此属性检查，即使您可以。其原因是，正如您所说，此加法可能会溢出，并且整数溢出是 C 中未定义的行为，或者，正如问题How to check integer Overflow in C? 的答案一样。很好地说：

一旦你执行了 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);
    /* ... */
}

Run Code Online (Sandbox Code Playgroud)

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

Run Code Online (Sandbox Code Playgroud)

你正在跑步

    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 检查器：否定的主张是可满足的，即不成立
决策过程运行时间：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 (00000000000000000000000000000000)

状态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
  t + *b 中无符号 + 算术溢出
  !overflow("+", 无符号整数, t, *b)

验证失败

再次强调，这是一个实际的错误，CBMC 有充分的理由告诉您这一点。这个问题可以通过以下方式修复

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

Run Code Online (Sandbox Code Playgroud)

这使

CBMC 版本 5.1 64 位 x86_64 macos
解析test.c
转换
型式检验测试
生成GOTO程序
添加 CPROVER 库
函数指针移除
部分内联
通用属性仪表
开始有界模型检查
程序表达式大小：42步
简单的切片删除了 3 个分配
生成 3 个 VCC，简化后剩余 3 个
将问题传递给命题还原
转换SSA
运行命题还原
后期处理
使用带有简化器的 MiniSAT 2.2.0 求解
542 个变量，1561 个子句
SAT 检查器不一致：否定的声明不可满足，即成立
决策过程运行时间：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);
}

Run Code Online (Sandbox Code Playgroud)

并运行

    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 检查器：否定的主张是可满足的，即不成立
决策过程运行时间：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 (00000000000000000000000000000000)

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

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

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

状态27文件test.c第10行函数主线程0
-------------------------------------------------- --
  多头 = 0 (0000000000000000000000000000000000000000000000000000000000000000)

状态28文件test.c第10行函数主线程0
-------------------------------------------------- --
  多头 = 1 (0000000000000000000000000000000000000000000000000000000000000001)

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

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

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

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

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

验证失败

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

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

Run Code Online (Sandbox Code Playgroud)

然后

temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)

Run Code Online (Sandbox Code Playgroud)

尝试将其转换为 a 会signed int很麻烦，因为它超出了范围（另请参阅Does cast betweensigned and unsigned int keep精确位模式的变量在内存中？）。

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

归档时间：	10 年，2 月前
查看次数：	246 次
最近记录：	10 年，1 月前