TL; DR Tùy thuộc vào loại biến thực tế là gì. Trong mọi trường hợp, CBMC phát hiện một lỗi thực sự có thể gây ra hành vi không xác định. Điều này có nghĩa là bạn nên sửa mã của mình thay vì tắt thông báo trong CBMC.
Full câu trả lời:
chung: Để theo sự hiểu biết của tôi, CBMC không cho phép loại trừ các tài sản cụ thể (mặt khác, bạn có thể kiểm tra chỉ có một tài sản cụ thể đơn lẻ sử dụng --property cờ). Nếu bạn muốn một câu trả lời chính thức/ý kiến hoặc đưa ra yêu cầu tính năng, tôi khuyên bạn nên đăng bài trong số CProver Support group.
(Tất nhiên, người ta có thể sử dụng __CPROVER_assume để làm CBMC loại trừ dấu vết dẫn đến lỗi này, nhưng đây sẽ là một rất, rất, rất xấu ý tưởng, vì điều này có thể làm cho các vấn đề khác không thể truy cập.)
Biến thể 1: tôi giả sử mã của bạn trông giống như sau (liên quan đến điều này: xin vui lòng, xin vui lòng gửi khép kín ví dụ và giải thích một cách chính xác những gì vấn đề là, thật khó để đoán những điều này)
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);
}
và bạn đang chạy
cbmc --signed-overflow-check test.c
đưa ra một sản lượng tương tự như dưới đây không?
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
Tôi không nghĩ bạn nên vô hiệu hóa tính năng kiểm tra tài sản này, ngay cả khi bạn có thể. Lý do cho điều này là, như bạn nói, rằng việc bổ sung này có thể tràn, và, integer overflow là hành vi không xác định trong C, hoặc, như this answer cho câu hỏi How to check integer overflow in C? độc đáo đặt nó:
[O] nce bạn đã thực hiện x + y, nếu nó tràn, bạn đã được ẩn. Đã quá muộn để thực hiện bất kỳ kiểm tra nào - chương trình của bạn có thể đã bị lỗi. Hãy suy nghĩ của nó giống như kiểm tra phân chia bằng số không - nếu bạn chờ đợi cho đến khi sau khi các phân chia đã được thực hiện để kiểm tra, nó đã quá muộn.
Xem thêm Integer overflow and undefined behavior và How disastrous is integer overflow in C++?.
Vì vậy, đây là lỗi thực tế và CBMC có lý do chính đáng để thông báo cho bạn. Những gì bạn thực sự nên làm là điều chỉnh mã của bạn để không có tràn tiềm năng! Câu trả lời nêu trên cho thấy một cái gì đó tương tự (nhớ để bao gồm 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);
/* ... */
}
Biến thể 2: Ở đây, tôi giả định, mã của bạn trông giống như sau:
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);
}
và bạn đang chạy
cbmc --unsigned-overflow-check test.c
cho kết quả tương tự như sau?
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
Một lần nữa, đây là lỗi thực tế và CBMC có lý do chính đáng để thông báo cho bạn. Cái này có thể được cố định bởi
l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);
mang đến cho
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
Variant 3: Nếu mọi thứ như trước đó, nhưng bạn phải signed int thay vì unsigned int, mọi thứ trở nên một chút phức tạp hơn. Ở đây, giả sử bạn sử dụng (bằng văn bản theo một cách hơi phức tạp hơn để xem rõ hơn những gì đang xảy ra)
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);
}
và chạy
cbmc --signed-overflow-check test.c
bạn sẽ nhận đượ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
Hoặc viết chính xác hơn, nếu bạn có
t == -2147483648 (0b10000000000000000000000000000000)
s == 1 (0b00000000000000000000000000000001)
sau đó
temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)
và một nỗ lực để chuyển đổi này vào một signed int là rắc rối, bởi vì nó nằm ngoài phạm vi (xem thêm Does cast between signed and unsigned int maintain exact bit pattern of variable in memory?).
Như bạn thấy, counterexample này cũng là một lỗi thực tế, và một lần nữa, CBMC là ngay trong nói với bạn về nó. Điều này có nghĩa là mặt nạ/toán học của bạn không hoạt động như mong đợi (mặt nạ của bạn biến số âm thành số dương ngoài giới hạn) và bạn cần sửa mã của mình để kết quả nằm trong phạm vi cần thiết. (Có thể đáng để suy nghĩ cẩn thận về những gì bạn thực sự muốn làm để đảm bảo bạn có được kết quả đúng.)