Skip to content

Commit c70148e

Browse files
kroeningkroening
committed
undefined shifts are now fatal
There are various criteria for shift expressions that render them undefined behavior. The corresponding assertions are now fatal.
1 parent 621fe05 commit c70148e

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)