Skip to content

Commit b6ab541

Browse files
kroeningkroening
authored
Merge pull request #8233 from diffblue/float-div-by-zero
division-by-zero on float
2 parents 7d01374 + e00a1bd commit b6ab541

14 files changed

+176
-69
lines changed

‎doc/man/cbmc.1

+4-1
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

+4-1
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

+4-1
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

+4-1
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

+12
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

+8
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

+15
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

+9
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

+8-4
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

+21-19
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.

‎src/ansi-c/goto_check_c.cpp

+41-1
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ class goto_check_ct
5858
enable_memory_cleanup_check =
5959
_options.get_bool_option("memory-cleanup-check");
6060
enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
61+
enable_float_div_by_zero_check =
62+
_options.get_bool_option("float-div-by-zero-check");
6163
enable_enum_range_check = _options.get_bool_option("enum-range-check");
6264
enable_signed_overflow_check =
6365
_options.get_bool_option("signed-overflow-check");
@@ -179,6 +181,7 @@ class goto_check_ct
179181
void bounds_check_index(const index_exprt &, const guardt &);
180182
void bounds_check_bit_count(const unary_exprt &, const guardt &);
181183
void div_by_zero_check(const div_exprt &, const guardt &);
184+
void float_div_by_zero_check(const div_exprt &, const guardt &);
182185
void mod_by_zero_check(const mod_exprt &, const guardt &);
183186
void mod_overflow_check(const mod_exprt &, const guardt &);
184187
void enum_range_check(const exprt &, const guardt &);
@@ -262,6 +265,7 @@ class goto_check_ct
262265
bool enable_memory_leak_check;
263266
bool enable_memory_cleanup_check;
264267
bool enable_div_by_zero_check;
268+
bool enable_float_div_by_zero_check;
265269
bool enable_enum_range_check;
266270
bool enable_signed_overflow_check;
267271
bool enable_unsigned_overflow_check;
@@ -282,6 +286,7 @@ class goto_check_ct
282286
{"memory-leak-check", &enable_memory_leak_check},
283287
{"memory-cleanup-check", &enable_memory_cleanup_check},
284288
{"div-by-zero-check", &enable_div_by_zero_check},
289+
{"float-div-by-zero-check", &enable_float_div_by_zero_check},
285290
{"enum-range-check", &enable_enum_range_check},
286291
{"signed-overflow-check", &enable_signed_overflow_check},
287292
{"unsigned-overflow-check", &enable_unsigned_overflow_check},
@@ -508,6 +513,27 @@ void goto_check_ct::div_by_zero_check(
508513
guard);
509514
}
510515

516+
void goto_check_ct::float_div_by_zero_check(
517+
const div_exprt &expr,
518+
const guardt &guard)
519+
{
520+
if(!enable_float_div_by_zero_check)
521+
return;
522+
523+
// add divison by zero subgoal
524+
525+
exprt zero = from_integer(0, expr.op1().type());
526+
const notequal_exprt inequality(expr.op1(), std::move(zero));
527+
528+
add_guarded_property(
529+
inequality,
530+
"floating-point division by zero",
531+
"float-division-by-zero",
532+
expr.find_source_location(),
533+
expr,
534+
guard);
535+
}
536+
511537
void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
512538
{
513539
if(!enable_enum_range_check)
@@ -1850,7 +1876,21 @@ void goto_check_ct::check_rec_div(
18501876
const div_exprt &div_expr,
18511877
const guardt &guard)
18521878
{
1853-
div_by_zero_check(to_div_expr(div_expr), guard);
1879+
if(
1880+
div_expr.type().id() == ID_signedbv ||
1881+
div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
1882+
{
1883+
// Division by zero is undefined behavior for all integer types.
1884+
div_by_zero_check(to_div_expr(div_expr), guard);
1885+
}
1886+
else if(div_expr.type().id() == ID_floatbv)
1887+
{
1888+
// Division by zero on floating-point numbers may be undefined behavior.
1889+
// Annex F of the ISO C21 suggests that implementations that
1890+
// define __STDC_IEC_559__ follow IEEE 754 semantics,
1891+
// which defines the outcome of division by zero.
1892+
float_div_by_zero_check(to_div_expr(div_expr), guard);
1893+
}
18541894

18551895
if(div_expr.type().id() == ID_signedbv)
18561896
integer_overflow_check(div_expr, guard);

‎src/ansi-c/goto_check_c.h

+7-2
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,8 @@ void goto_check_c(
3939

4040
#define OPT_GOTO_CHECK \
4141
"(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \
42-
"(div-by-zero-check)(enum-range-check)" \
42+
"(div-by-zero-check)(float-div-by-zero-check)" \
43+
"(enum-range-check)" \
4344
"(signed-overflow-check)(unsigned-overflow-check)" \
4445
"(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
4546
"(float-overflow-check)(nan-check)(no-built-in-assertions)" \
@@ -61,7 +62,10 @@ void goto_check_c(
6162
" {y--no-pointer-check} \t disable pointer checks\n" \
6263
" {y--memory-leak-check} \t enable memory leak checks\n" \
6364
" {y--memory-cleanup-check} \t enable memory cleanup checks\n" \
64-
" {y--div-by-zero-check} \t enable division by zero checks (default on)\n" \
65+
" {y--div-by-zero-check} \t " \
66+
"enable division by zero checks on integers (default on)\n" \
67+
" {y--float-div-by-zero-check} \t " \
68+
"enable division by zero checks on floating-point numbers (default off)\n" \
6569
" {y--no-div-by-zero-check} \t disable division by zero checks\n" \
6670
" {y--signed-overflow-check} \t " \
6771
"enable signed arithmetic over- and underflow checks (default on)\n" \
@@ -123,6 +127,7 @@ void goto_check_c(
123127
PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
124128
PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
125129
PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
130+
PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
126131
PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
127132
PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
128133
PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \

0 commit comments

Comments
 (0)