Skip to content

Commit d6150ce

Browse files
tautschnigtautschnig
authored
Merge pull request #8304 from diffblue/undefined-shift-fatal
Undefined shifts are now fatal
2 parents 4f73590 + c70148e commit d6150ce

File tree

8 files changed

+110
-42
lines changed

8 files changed

+110
-42
lines changed

‎regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE
22
shift_right.c
33
--trace
44
\[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
5-
\[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
6-
\[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
5+
\[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: UNKNOWN
6+
\[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: UNKNOWN
77
second=128
88
result_unsigned=(64|'@')
99
^EXIT=10$

‎regression/cbmc/Undefined_Shift1/main.c‎

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,20 @@ void negative_operand()
2020
int s = -1 << ((sizeof(int) - 1) * 8); // negative operand
2121
}
2222

23+
int nondet_int();
24+
2325
int main()
2426
{
25-
shift_distance_too_large();
26-
shift_distance_negative();
27-
negative_operand();
27+
switch(nondet_int())
28+
{
29+
case 0:
30+
shift_distance_too_large();
31+
break;
32+
case 1:
33+
shift_distance_negative();
34+
break;
35+
case 2:
36+
negative_operand();
37+
break;
38+
}
2839
}

‎regression/cbmc/Undefined_Shift1/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ main.c
77
^\[.*\] line 5 shift operand is negative in .*: SUCCESS$
88
^\[.*\] line 7 shift distance too large in .*: FAILURE$
99
^\[.*\] line 15 shift distance is negative in .*: FAILURE$
10-
^\[.*\] line 15 shift distance too large in .*: SUCCESS$
10+
^\[.*\] line 15 shift distance too large in .*: UNKNOWN$
1111
^\[.*\] line 20 shift operand is negative in .*: FAILURE$
1212
^\*\* 4 of 9 failed
1313
^VERIFICATION FAILED$

‎regression/cbmc/overflow/leftshift_overflow-c89.desc‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ leftshift_overflow.c
33
--c89
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$
7-
^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$
8-
^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$
9-
^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$
10-
^\[.*\] line 30 arithmetic overflow on signed shl in .*: SUCCESS$
6+
^\[leftshift_overflow1\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
7+
^\[leftshift_overflow2\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: SUCCESS$
8+
^\[leftshift_overflow4\.overflow\.2\] line \d+ arithmetic overflow on signed shl in .*: UNKNOWN$
9+
^\[leftshift_overflow5\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
10+
^\[leftshift_overflow8\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: SUCCESS$
1111
^\*\* 6 of \d+ failed
1212
^VERIFICATION FAILED$
1313
--
1414
^warning: ignoring
15-
^\[.*\] line 14 arithmetic overflow on signed shl in .*: .*
16-
^\[.*\] line 23 arithmetic overflow on signed shl in .*: .*
17-
^\[.*\] line 26 arithmetic overflow on signed shl in .*: .*
15+
^\[leftshift_overflow3\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$
16+
^\[leftshift_overflow6\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$
17+
^\[leftshift_overflow7\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$

‎regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ leftshift_overflow.c
33
--c99 --full-slice
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$
7-
^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$
8-
^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$
9-
^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$
10-
^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$
11-
^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$
6+
^\[leftshift_overflow1\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
7+
^\[leftshift_overflow2\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: SUCCESS$
8+
^\[leftshift_overflow4\.overflow\.2\] line \d+ arithmetic overflow on signed shl in .*: UNKNOWN$
9+
^\[leftshift_overflow5\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
10+
^\[leftshift_overflow7\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
11+
^\[leftshift_overflow8\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
1212
^\*\* 8 of \d+ failed
1313
^VERIFICATION FAILED$
1414
--
1515
^warning: ignoring
16-
^\[.*\] line 14 arithmetic overflow on signed shl in .*: .*
17-
^\[.*\] line 23 arithmetic overflow on signed shl in .*: .*
16+
^\[leftshift_overflow3\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$
17+
^\[leftshift_overflow6\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$

‎regression/cbmc/overflow/leftshift_overflow-c99.desc‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ leftshift_overflow.c
33
--c99
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$
7-
^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$
8-
^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$
9-
^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$
10-
^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$
11-
^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$
6+
^\[leftshift_overflow1\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
7+
^\[leftshift_overflow2\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: SUCCESS$
8+
^\[leftshift_overflow4\.overflow\.2\] line \d+ arithmetic overflow on signed shl in .*: UNKNOWN$
9+
^\[leftshift_overflow5\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
10+
^\[leftshift_overflow7\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
11+
^\[leftshift_overflow8\.overflow\.1\] line \d+ arithmetic overflow on signed shl in .*: FAILURE$
1212
^\*\* 8 of \d+ failed
1313
^VERIFICATION FAILED$
1414
--
1515
^warning: ignoring
16-
^\[.*\] line 14 arithmetic overflow on signed shl in .*: .*
17-
^\[.*\] line 23 arithmetic overflow on signed shl in .*: .*
16+
^\[leftshift_overflow3\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$
17+
^\[leftshift_overflow6\.overflow\..*\] line \d+ arithmetic overflow on signed shl in .*: .*$

‎regression/cbmc/overflow/leftshift_overflow.c‎

Lines changed: 65 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,90 @@
11
#include <inttypes.h>
22

3-
int main()
3+
void leftshift_overflow1(unsigned char x)
44
{
5-
unsigned char x;
6-
75
// signed, owing to promotion, and may overflow
86
unsigned r = x << ((sizeof(unsigned) - 1) * 8 + 1);
7+
}
98

9+
void leftshift_overflow2(unsigned char x)
10+
{
1011
// signed, owing to promotion, and cannot overflow
11-
r = x << ((sizeof(unsigned) - 1) * 8 - 1);
12+
unsigned r = x << ((sizeof(unsigned) - 1) * 8 - 1);
13+
}
1214

15+
void leftshift_overflow3(unsigned char x)
16+
{
1317
// unsigned
14-
r = (unsigned)x << ((sizeof(unsigned) - 1) * 8);
18+
unsigned r = (unsigned)x << ((sizeof(unsigned) - 1) * 8);
19+
}
1520

21+
void leftshift_overflow4(unsigned char x)
22+
{
1623
// negative value or zero, not an overflow
1724
int s = -x << ((sizeof(int) - 1) * 8);
25+
}
1826

27+
void leftshift_overflow5(unsigned char x)
28+
{
1929
// overflow
20-
s = 1 << x;
30+
int s = 1 << x;
31+
}
32+
33+
int nondet_int();
2134

35+
void leftshift_overflow6(unsigned char x)
36+
{
2237
// distance too far, not an overflow
23-
s = s << 100;
38+
int s = nondet_int();
39+
int t = s << 100;
40+
}
2441

42+
void leftshift_overflow7(unsigned char x)
43+
{
2544
// not an overflow in ANSI-C, but undefined in C99
26-
s = 1 << (sizeof(int) * 8 - 1);
45+
int s = 1 << (sizeof(int) * 8 - 1);
46+
}
2747

48+
void leftshift_overflow8(unsigned char x)
49+
{
2850
// overflow in an expression where operand and distance types are different
2951
uint32_t u32;
3052
int64_t i64 = ((int64_t)u32) << 32;
53+
}
54+
55+
unsigned char nondet_uchar();
56+
57+
int main()
58+
{
59+
unsigned char x = nondet_uchar();
60+
61+
switch(nondet_uchar())
62+
{
63+
case 1:
64+
leftshift_overflow1(x);
65+
break;
66+
case 2:
67+
leftshift_overflow2(x);
68+
break;
69+
case 3:
70+
leftshift_overflow3(x);
71+
break;
72+
case 4:
73+
leftshift_overflow4(x);
74+
break;
75+
case 5:
76+
leftshift_overflow5(x);
77+
break;
78+
case 6:
79+
leftshift_overflow6(x);
80+
break;
81+
case 7:
82+
leftshift_overflow7(x);
83+
break;
84+
case 8:
85+
leftshift_overflow8(x);
86+
break;
87+
}
3188

3289
return 0;
3390
}

‎src/ansi-c/goto-conversion/goto_check_c.cpp‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -583,7 +583,7 @@ void goto_check_ct::undefined_shift_check(
583583
inequality,
584584
"shift distance is negative",
585585
"undefined-shift",
586-
false, // fatal
586+
true, // fatal
587587
expr.find_source_location(),
588588
expr,
589589
guard);
@@ -600,7 +600,7 @@ void goto_check_ct::undefined_shift_check(
600600
binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
601601
"shift distance too large",
602602
"undefined-shift",
603-
false, // fatal
603+
true, // fatal
604604
expr.find_source_location(),
605605
expr,
606606
guard);
@@ -614,7 +614,7 @@ void goto_check_ct::undefined_shift_check(
614614
inequality,
615615
"shift operand is negative",
616616
"undefined-shift",
617-
false, // fatal
617+
true, // fatal
618618
expr.find_source_location(),
619619
expr,
620620
guard);
@@ -626,7 +626,7 @@ void goto_check_ct::undefined_shift_check(
626626
false_exprt(),
627627
"shift of non-integer type",
628628
"undefined-shift",
629-
false, // fatal
629+
true, // fatal
630630
expr.find_source_location(),
631631
expr,
632632
guard);

0 commit comments

Comments
 (0)