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. 帶有無符號整數溢出檢測的表達式
- 2. 大數字的C++溢出檢測（無符號long long）
- 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. 檢測div何時溢出
- 16. PHP Mongo庫溢出檢測
- 17. 檢測裝配體溢出？
- 18. 裝配，溢出檢測
- 19. 檢測溢出內容
- 20. 檢測整數溢出
- 21. 自定義溢出檢測
- 22. 使用qTip2檢測溢出
- 23. 檢測標籤溢出
- 24. 溢出檢測減去2個多頭
- 25. 爲VHDL定義溢出numeric_std有符號/無符號
- 26. 此彙編語言如何檢測簽名溢出？
- 27. 無符號整數得到溢出在c
- 28. c整數溢出 - 環繞
- 29. 請問這個代碼產生的無符號整數溢出
- 30. SQL Server-TSQL檢測由於溢出而導致錯過的代理作業