Skip to content

Commit e00a1bd

Browse files
kroeningkroening
committed
division-by-zero on float
This separates the division-by-zero check for floating-point operations from the division-by-zero check for integers. The new division-by-zero check for floating-point operations is off by default, and is enabled by --float-div-by-zero-check. The case for doing so is weak. ISO/IEC 9899:2021 (C21) and predecessors clealy state (Sec 6.5.5 par 5) "In both operations, if the value of the second operand is zero, the behavior is undefined." However, Annex F (IEC 60559 floating-point arithmetic) states that implementations that define __STDC_IEC_559__ must implement IEC 60559 division, which clearly defines the behavior when dividing floating-point numbers by zero. This behavior can be observed on all architectures that we support.
1 parent 7d01374 commit e00a1bd

File tree

14 files changed

+176
-69
lines changed

14 files changed

+176
-69
lines changed

‎doc/man/cbmc.1

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,10 @@ enable array bounds checks
6262
check shift greater than bit\-width
6363
.TP
6464
\fB\-\-div\-by\-zero\-check\fR
65-
enable division by zero checks
65+
enable division by zero checks for integer division
66+
.TP
67+
\fB\-\-float\-div\-by\-zero\-check\fR
68+
enable division by zero checks for floating-point division
6669
.TP
6770
\fB\-\-pointer\-primitive\-check\fR
6871
checks that all pointers in pointer primitives are valid or null

‎doc/man/goto-analyzer.1

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -521,7 +521,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
521521
explicitly freed before terminating the program.
522522
.TP
523523
\fB\-\-div\-by\-zero\-check\fR
524-
enable division by zero checks
524+
enable division by zero checks for integer division
525+
.TP
526+
\fB\-\-float\-div\-by\-zero\-check\fR
527+
enable division by zero checks for floating-point division
525528
.TP
526529
\fB\-\-signed\-overflow\-check\fR
527530
enable signed arithmetic over\- and underflow checks

‎doc/man/goto-diff.1

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
5252
explicitly freed before terminating the program.
5353
.TP
5454
\fB\-\-div\-by\-zero\-check\fR
55-
enable division by zero checks
55+
enable division by zero checks for integer division
56+
.TP
57+
\fB\-\-float\-div\-by\-zero\-check\fR
58+
enable division by zero checks for floating-point division
5659
.TP
5760
\fB\-\-signed\-overflow\-check\fR
5861
enable signed arithmetic over\- and underflow checks

‎doc/man/goto-instrument.1

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
192192
explicitly freed before terminating the program.
193193
.TP
194194
\fB\-\-div\-by\-zero\-check\fR
195-
enable division by zero checks
195+
enable division by zero checks for integer division
196+
.TP
197+
\fB\-\-float\-div\-by\-zero\-check\fR
198+
enable division by zero checks for floating-point division
196199
.TP
197200
\fB\-\-signed\-overflow\-check\fR
198201
enable signed arithmetic over\- and underflow checks

‎regression/cbmc/Division/floating_point_division1.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
int main()
5+
{
6+
assert(1.0 / 2 == 0.5);
7+
assert(1.0 / 0 == INFINITY);
8+
assert(-1.0 / 0 == -INFINITY);
9+
assert(isnan(NAN / 0));
10+
assert(1.0 / INFINITY == 0);
11+
assert(isnan(INFINITY / INFINITY));
12+
}

‎regression/cbmc/Division/floating_point_division1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
floating_point_division1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc/Division/floating_point_division2.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
double nondet_double();
5+
6+
int main()
7+
{
8+
double y = nondet_double();
9+
10+
if(y == 0)
11+
{
12+
// we expect to catch this with --float-div-by-zero-check
13+
double x = 1.0 / y;
14+
}
15+
}

‎regression/cbmc/Division/floating_point_division2.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE no-new-smt
2+
floating_point_division2.c
3+
--float-div-by-zero-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main\.float-division-by-zero\.1\] line \d+ floating-point division by zero in 1\.0 / y: FAILURE$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring

‎regression/cbmc/pragma_cprover_enable_all/main.c

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ int main()
1616
#pragma CPROVER check disable "bounds"
1717
#pragma CPROVER check disable "pointer"
1818
#pragma CPROVER check disable "div-by-zero"
19+
#pragma CPROVER check disable "float-div-by-zero"
1920
#pragma CPROVER check disable "enum-range"
2021
#pragma CPROVER check disable "signed-overflow"
2122
#pragma CPROVER check disable "unsigned-overflow"
@@ -36,7 +37,7 @@ int main()
3637
ABC e;
3738
bool readable;
3839
char i;
39-
signed int j;
40+
signed int j, k;
4041
readable = __CPROVER_r_ok(q, 1);
4142
q = p + 2000000000000;
4243
q = r;
@@ -45,14 +46,16 @@ int main()
4546
else
4647
den = 1.0;
4748
y = x / den;
49+
j = 10 / 0;
4850
e = 10;
4951
i += 1;
50-
j += 1;
52+
k += 1;
5153
}
5254
#pragma CPROVER check push
5355
#pragma CPROVER check enable "bounds"
5456
#pragma CPROVER check enable "pointer"
5557
#pragma CPROVER check enable "div-by-zero"
58+
#pragma CPROVER check enable "float-div-by-zero"
5659
#pragma CPROVER check enable "enum-range"
5760
#pragma CPROVER check enable "signed-overflow"
5861
#pragma CPROVER check enable "unsigned-overflow"
@@ -73,7 +76,7 @@ int main()
7376
ABC e;
7477
bool readable;
7578
char i;
76-
signed int j;
79+
signed int j, k;
7780
readable = __CPROVER_r_ok(q, 1);
7881
q = p + 2000000000000;
7982
q = r;
@@ -82,9 +85,10 @@ int main()
8285
else
8386
den = 1.0;
8487
y = x / den;
88+
j = 10 / 0;
8589
e = 10;
8690
i += 1;
87-
j += 1;
91+
k += 1;
8892
}
8993
#pragma CPROVER check pop
9094
#pragma CPROVER check pop

‎regression/cbmc/pragma_cprover_enable_all/test.desc

Lines changed: 21 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,29 @@
11
CORE no-new-smt
22
main.c
3-
--object-bits 8 --enum-range-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --nan-check
4-
^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
5-
^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
6-
^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
7-
^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
8-
^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
9-
^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
10-
^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
11-
^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
12-
^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
3+
--object-bits 8 --enum-range-check --div-by-zero-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --float-div-by-zero-check --conversion-check --nan-check
4+
^\[main\.pointer_primitives\.\d+\] line 80 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
5+
^\[main\.pointer_primitives\.\d+\] line 80 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
6+
^\[main\.pointer_arithmetic\.\d+\] line 81 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
7+
^\[main\.NaN\.\d+\] line 87 NaN on / in x / den: FAILURE
8+
^\[main\.float-division-by-zero\.\d+\] line 87 floating-point division by zero in x / den: FAILURE
9+
^\[main\.overflow\.\d+\] line 87 arithmetic overflow on floating-point division in x / den: FAILURE
10+
^\[main\.division-by-zero\.\d+\] line 88 division by zero in 10 / 0: FAILURE$
11+
^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: FAILURE
12+
^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
13+
^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: FAILURE
1314
^VERIFICATION FAILED$
1415
^EXIT=10$
1516
^SIGNAL=0$
1617
--
17-
^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
18-
^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
19-
^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
20-
^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
21-
^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
22-
^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE
23-
^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE
24-
^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
25-
^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
18+
^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
19+
^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
20+
^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
21+
^\[main\.NaN\.\d+\] line 48 NaN on / in x / den: FAILURE
22+
^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den: FAILURE
23+
^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den: FAILURE
24+
^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0: FAILURE$
25+
^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10: FAILURE
26+
^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
27+
^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1: FAILURE
2628
--
2729
This test uses all possible named-checks to maximize coverage.

0 commit comments

Comments
 (0)