5
CBMC检测如下的可能的无符号此外溢出：绕过由CBMC检测到一个无符号此外溢出
l = (t + *b)&(0xffffffffL);
c += (l < t);
我同意，在第一线溢出的可能性，但我照顾CBMC无法查看的下一行中的进位。 如果万一发生溢出，我将设置进位1.因此，由于我知道这一点，所以我希望我的代码能够工作，所以我想继续进行验证过程。 那么，我是如何告诉CBMC忽略这个bug并继续前进的呢？
A
回答
3
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 version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 41 steps
simple slicing removed 3 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
792 variables, 2302 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.006s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=-9223372036854775808 (1000000000000000000000000000000000000000000000000000000000000000)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001)
State 25 file test.c line 8 function main thread 0
----------------------------------------------------
b=((long int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 8 function main thread 0
----------------------------------------------------
[email protected] (0000001000000000000000000000000000000000000000000000000000000000)
Violated property:
file test.c line 10 function main
arithmetic overflow on signed + in t + *b
!overflow("+", signed long int, t, *b)
VERIFICATION FAILED
我不认为你应该禁用这个属性检查，即使你可以。这样做的原因是，如你所说，这除了可以溢出，并且，整数溢出是未定义的行为用C，或者像this answer的问题How to check integer overflow in C?很好所说的那样：
[O] NCE你已经执行了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 version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 42 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
519 variables, 1306 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.01s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (00000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=4187126263 (11111001100100100111100111110111)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (00000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=3329066504 (11000110011011011000011000001000)
State 25 file test.c line 8 function main thread 0
----------------------------------------------------
b=((unsigned int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 8 function main thread 0
----------------------------------------------------
[email protected] (0000001000000000000000000000000000000000000000000000000000000000)
Violated property:
file test.c line 10 function main
arithmetic overflow on unsigned + in t + *b
!overflow("+", unsigned int, t, *b)
VERIFICATION FAILED
同样，这是一个实际的错误，CBMC有充分的理由告诉你。这其中可以通过
l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);
这给
CBMC version 5.1 64-bit x86_64 macos Parsing test.c Converting Type-checking test Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking size of program expression: 42 steps simple slicing removed 3 assignments Generated 3 VCC(s), 3 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.0 with simplifier 542 variables, 1561 clauses SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds Runtime decision procedure: 0.002s VERIFICATION SUCCESSFUL
变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 version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 48 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
872 variables, 2430 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.008s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (00000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=-2147483648 (10000000000000000000000000000000)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (00000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=1 (00000000000000000000000000000001)
State 25 file test.c line 9 function main thread 0
----------------------------------------------------
longt=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 9 function main thread 0
----------------------------------------------------
longt=-2147483648 (1111111111111111111111111111111110000000000000000000000000000000)
State 27 file test.c line 10 function main thread 0
----------------------------------------------------
longs=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 28 file test.c line 10 function main thread 0
----------------------------------------------------
longs=1 (0000000000000000000000000000000000000000000000000000000000000001)
State 29 file test.c line 11 function main thread 0
----------------------------------------------------
temp1=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 31 file test.c line 11 function main thread 0
----------------------------------------------------
temp1=-2147483647 (1111111111111111111111111111111110000000000000000000000000000001)
State 32 file test.c line 12 function main thread 0
----------------------------------------------------
temp2=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 33 file test.c line 12 function main thread 0
----------------------------------------------------
temp2=2147483649 (0000000000000000000000000000000010000000000000000000000000000001)
Violated property:
file test.c line 14 function main
arithmetic overflow on signed type conversion in (signed int)temp2
temp2 = -2147483648l
VERIFICATION FAILED
或者，写更简洁，如果你有
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再次告诉你它是正确的。这尤其意味着你的掩盖/数学不能按预期工作（你的掩码将负数转换为超出正数的数），并且需要修正代码，以便结果在必要范围内。 （为了确保您获得正确的结果，仔细考虑您真正想要做什么可能是值得的。）
相关问题
- 1. 大数字的C++溢出检测（无符号long long）
- 2. 带有无符号整数溢出检测的表达式
- 3. 无符号整数溢出不会“环绕”
- 4. 无符号long long溢出
- 5. 无符号整型溢出
- 6. 无符号溢出模运算符C
- 7. 在Go中检测带符号的int溢出
- 8. 为什么turbo c环绕有符号整数溢出每次虽然有符号整数溢出未定义？
- 9. 在LotusScript中无符号长整数？如何长时间关闭溢出检测？
- 10. 如何检查溢出转换的char * []为无符号短
- 11. ***检测到缓冲区溢出***
- 12. 信号量无一例外地溢出至最大值
- 13. RuntimeError（符号表溢出（符号_one_time_conditions）。）
- 14. 检测整数溢出
- 15. 检测装配体溢出？
- 16. 检测div何时溢出
- 17. 检测溢出内容
- 18. PHP Mongo库溢出检测
- 19. 如何检测溢出
- 20. 使用qTip2检测溢出
- 21. 装配，溢出检测
- 22. 自定义溢出检测
- 23. 检测标签溢出
- 24. 溢出检测减去2个多头
- 25. 为VHDL定义溢出numeric_std有符号/无符号
- 26. 此汇编语言如何检测签名溢出？
- 27. 无符号整数得到溢出在c
- 28. c整数溢出 - 环绕
- 29. 请问这个代码产生的无符号整数溢出
- 30. SQL Server-TSQL检测由于溢出而导致错过的代理作业