Achieving High Coverage for Floating-point Code via Unconstrained Programming (Extended Version)
Zhoulai Fu, Zhendong Su
TL;DR
This paper introduces a novel approach using unconstrained programming to achieve high coverage in testing floating-point code, transforming the challenge of floating-point constraints into an optimization problem.
Contribution
The paper presents a new method and tool, CoverMe, that leverages unconstrained programming to efficiently generate test inputs for high coverage of floating-point programs.
Findings
CoverMe achieves 90.8% branch coverage on average.
CoverMe outperforms random testing, AFL, and Austin in coverage and speed.
The approach effectively handles floating-point constraints in testing.
Abstract
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbolic execution. This paper turns the challenge of testing floating-point code into the opportunity of applying unconstrained programming --- the mathematical solution for calculating function minimum points over the entire search space. Our core insight is to derive a representing function from the floating-point program, any of whose minimum points is a test input guaranteed to exercise a new branch of the tested program. This guarantee allows us to achieve high coverage of the floating-point program by repeatedly minimizing the representing function. We have realized this approach in a tool called CoverMe and conducted an extensive evaluation of it on Sun's C math…
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7
Figure 8
Figure 9
Figure 10
Figure 11
Figure 12
Figure 13
Figure 14
Figure 20151011
Figure 20151011
Figure 20151103
Figure 20151103
Figure 1
Figure 2
Figure 21
Figure 22
Figure 23
Figure 24
Figure 25
Figure 26
Figure 27
Figure 28
Figure 29
Figure 30
Figure 31| Benchmark | Time (s) | Branch (%) | Improvement (%) | |||||||
| File | Function | #Branches | Rand | AFL | CoverMe | Rand | AFL | CoverMe | CoverMe vs. Rand | CoverMe vs. AFL |
| e_acos.c | ieee754_acos(double) | 12 | 78 | 78 | 7.8 | 16.7 | 100.0 | 100.0 | 83.3 | 0.0 |
| e_acosh.c | ieee754_acosh(double) | 10 | 23 | 23 | 2.3 | 40.0 | 100.0 | 90.0 | 50.0 | -10.0 |
| e_asin.c | ieee754_asin(double) | 14 | 80 | 80 | 8.0 | 14.3 | 85.7 | 92.9 | 78.6 | 7.1 |
| e_atan2.c | ieee754_atan2(double,double) | 44 | 174 | 174 | 17.4 | 34.1 | 86.4 | 63.6 | 29.6 | -22.7 |
| e_atanh.c | ieee754_atanh(double) | 12 | 81 | 81 | 8.1 | 8.8 | 75.0 | 91.7 | 82.8 | 16.7 |
| e_cosh.c | ieee754_cosh(double) | 16 | 82 | 82 | 8.2 | 37.5 | 81.3 | 93.8 | 56.3 | 12.5 |
| e_exp.c | ieee754_exp(double) | 24 | 84 | 84 | 8.4 | 20.8 | 83.3 | 96.7 | 75.8 | 13.3 |
| e_fmod.c | ieee754_fmod(double,double) | 60 | 221 | 221 | 22.1 | 48.3 | 53.3 | 70.0 | 21.7 | 16.7 |
| e_hypot.c | ieee754_hypot(double,double) | 22 | 156 | 156 | 15.6 | 40.9 | 54.5 | 90.9 | 50.0 | 36.4 |
| e_j0.c | ieee754_j0(double) | 18 | 90 | 90 | 9.0 | 33.3 | 88.9 | 94.4 | 61.1 | 5.6 |
| ieee754_y0(double) | 16 | 7 | 7 | 0.7 | 56.3 | 75.0 | 100.0 | 43.8 | 25.0 | |
| e_j1.c | ieee754_j1(double) | 16 | 102 | 102 | 10.2 | 50.0 | 75.0 | 93.8 | 43.8 | 18.8 |
| ieee754_y1(double) | 16 | 7 | 7 | 0.7 | 56.3 | 75.0 | 100.0 | 43.8 | 25.0 | |
| e_log.c | ieee754_log(double) | 22 | 34 | 34 | 3.4 | 59.1 | 72.7 | 90.9 | 31.8 | 18.2 |
| e_log10.c | ieee754_log10(double) | 8 | 11 | 11 | 1.1 | 62.5 | 75.0 | 87.5 | 25.0 | 12.5 |
| e_pow.c | ieee754_pow(double,double) | 114 | 188 | 188 | 18.8 | 15.8 | 88.6 | 81.6 | 65.8 | -7.0 |
| e_rem_pio2.c | ieee754_rem_pio2(double,double*) | 30 | 11 | 11 | 1.1 | 33.3 | 86.7 | 93.3 | 60.0 | 6.7 |
| e_remainder.c | ieee754_remainder(double,double) | 22 | 22 | 22 | 2.2 | 45.5 | 50.0 | 100.0 | 54.6 | 50.0 |
| e_scalb.c | ieee754_scalb(double,double) | 14 | 85 | 85 | 8.5 | 50.0 | 42.9 | 92.9 | 42.9 | 50.0 |
| e_sinh.c | ieee754_sinh(double) | 20 | 6 | 6 | 0.6 | 35.0 | 70.0 | 95.0 | 60.0 | 25.0 |
| e_sqrt.c | iddd754_sqrt(double) | 46 | 156 | 156 | 15.6 | 69.6 | 71.7 | 82.6 | 13.0 | 10.9 |
| k_cos.c | kernel_cos(double,double) | 8 | 154 | 154 | 15.4 | 37.5 | 87.5 | 87.5 | 50.0 | 0.0 |
| s_asinh.c | asinh(double) | 12 | 84 | 84 | 8.4 | 41.7 | 83.3 | 91.7 | 50.0 | 8.3 |
| s_atan.c | atan(double) | 26 | 85 | 85 | 8.5 | 19.2 | 15.4 | 88.5 | 69.2 | 73.1 |
| s_cbrt.c | cbrt(double) | 6 | 4 | 4 | 0.4 | 50.0 | 66.7 | 83.3 | 33.3 | 16.7 |
| s_ceil.c | ceil(double) | 30 | 88 | 88 | 8.8 | 10.0 | 83.3 | 83.3 | 73.3 | 0.0 |
| s_cos.c | cos (double) | 8 | 4 | 4 | 0.4 | 75.0 | 87.5 | 100.0 | 25.0 | 12.5 |
| s_erf.c | erf(double) | 20 | 90 | 90 | 9.0 | 30.0 | 85.0 | 100.0 | 70.0 | 15.0 |
| erfc(double) | 24 | 1 | 1 | 0.1 | 25.0 | 79.2 | 100.0 | 75.0 | 20.8 | |
| s_expm1.c | expm1(double) | 42 | 11 | 11 | 1.1 | 21.4 | 85.7 | 97.6 | 76.2 | 11.9 |
| s_floor.c | floor(double) | 30 | 101 | 101 | 10.1 | 10.0 | 83.3 | 83.3 | 73.3 | 0.0 |
| s_ilogb.c | ilogb(double) | 12 | 83 | 83 | 8.3 | 16.7 | 16.7 | 75.0 | 58.3 | 58.3 |
| s_log1p.c | log1p(double) | 36 | 99 | 99 | 9.9 | 38.9 | 77.8 | 88.9 | 50.0 | 11.1 |
| s_logb.c | logb(double) | 6 | 3 | 3 | 0.3 | 50.0 | 16.7 | 83.3 | 33.3 | 66.7 |
| s_modf.c | modf(double, double*) | 10 | 35 | 35 | 3.5 | 33.3 | 80.0 | 100.0 | 66.7 | 20.0 |
| s_nextafter.c | nextafter(double,double) | 44 | 175 | 175 | 17.5 | 59.1 | 65.9 | 79.6 | 20.5 | 13.6 |
| s_rint.c | rint(double) | 20 | 30 | 30 | 3.0 | 15.0 | 75.0 | 90.0 | 75.0 | 15.0 |
| s_sin.c | sin (double) | 8 | 3 | 3 | 0.3 | 75.0 | 87.5 | 100.0 | 25.0 | 12.5 |
| s_tan.c | tan(double) | 4 | 3 | 3 | 0.3 | 50.0 | 75.0 | 100.0 | 50.0 | 25.0 |
| s_tanh.c | tanh(double) | 12 | 7 | 7 | 0.7 | 33.3 | 75.0 | 100.0 | 66.7 | 25.0 |
| MEAN | 23 | 69 | 69 | 6.9 | 38.0 | 72.9 | 90.8 | 52.9 | 17.9 | |
| Benchmark | Time (second) | Branch coverage(%) | Improvement | ||||
|---|---|---|---|---|---|---|---|
| Program | Entry function | Austin | CoverMe | Austin | CoverMe | Speedup | Coverage (%) |
| e_acos.c | ieee754_acos(double) | 6058.8 | 7.8 | 16.7 | 100.0 | 776.4 | 83.3 |
| e_acosh.c | ieee754_acosh(double) | 2016.4 | 2.3 | 40.0 | 90.0 | 887.5 | 50.0 |
| e_asin.c | ieee754_asin(double) | 6935.6 | 8.0 | 14.3 | 92.9 | 867.0 | 78.6 |
| e_atan2.c | ieee754_atan2(double, double) | 14456.0 | 17.4 | 34.1 | 63.6 | 831.2 | 29.6 |
| e_atanh.c | ieee754_atanh(double) | 4033.8 | 8.1 | 8.3 | 91.7 | 495.4 | 83.3 |
| e_cosh.c | ieee754_cosh(double) | 27334.5 | 8.2 | 37.5 | 93.8 | 3327.7 | 56.3 |
| e_exp.c | ieee754_exp(double) | 2952.1 | 8.4 | 75.0 | 96.7 | 349.7 | 21.7 |
| e_fmod.c | ieee754_frmod(double, double) | timeout | 22.1 | n/a | 70.0 | n/a | n/a |
| e_hypot.c | ieee754_hypot(double, double) | 5456.8 | 15.6 | 36.4 | 90.9 | 350.9 | 54.6 |
| e_j0.c | ieee754_j0(double) | 6973.0 | 9.0 | 33.3 | 94.4 | 776.5 | 61.1 |
| ieee754_y0(double) | 5838.3 | 0.7 | 56.3 | 100.0 | 8243.5 | 43.8 | |
| e_j1.c | ieee754_j1(double) | 4131.6 | 10.2 | 50.0 | 93.8 | 403.9 | 43.8 |
| ieee754_y1(double) | 5701.7 | 0.7 | 56.3 | 100.0 | 8411.0 | 43.8 | |
| e_log.c | ieee754_log(double) | 5109.0 | 3.4 | 59.1 | 90.9 | 1481.9 | 31.8 |
| e_log10.c | ieee754_log10(double) | 1175.5 | 1.1 | 62.5 | 87.5 | 1061.3 | 25.0 |
| e_pow.c | ieee754_pow(double, double) | timeout | 18.8 | n/a | 81.6 | n/a | n/a |
| e_rem_pio2.c | ieee754_rem_pio2(double, double*) | timeout | 1.1 | n/a | 93.3 | n/a | n/a |
| e_remainder.c | ieee754_remainder(double, double) | 4629.0 | 2.2 | 45.5 | 100.0 | 2146.5 | 54.6 |
| e_scalb.c | ieee754_scalb(double, double) | 1989.8 | 8.5 | 57.1 | 92.9 | 233.8 | 35.7 |
| e_sinh.c | ieee754_sinh(double) | 5534.8 | 0.6 | 35.0 | 95.0 | 9695.9 | 60.0 |
| e_sqrt.c | iddd754_sqrt(double) | crash | 15.6 | n/a | 82.6 | n/a | n/a |
| k_cos.c | kernel_cos(double, double) | 1885.1 | 15.4 | 37.5 | 87.5 | 122.6 | 50.0 |
| s_asinh.c | asinh(double) | 2439.1 | 8.4 | 41.7 | 91.7 | 290.8 | 50.0 |
| s_atan.c | atan(double) | 7584.7 | 8.5 | 26.9 | 88.5 | 890.6 | 61.6 |
| s_cbrt.c | cbrt(double) | 3583.4 | 0.4 | 50.0 | 83.3 | 9109.4 | 33.3 |
| s_ceil.c | ceil(double) | 7166.3 | 8.8 | 36.7 | 83.3 | 812.3 | 46.7 |
| s_cos.c | cos (double) | 669.4 | 0.4 | 75.0 | 100.0 | 1601.6 | 25.0 |
| s_erf.c | erf(double) | 28419.8 | 9.0 | 30.0 | 100.0 | 3166.8 | 70.0 |
| erfc(double) | 6611.8 | 0.1 | 25.0 | 100.0 | 62020.9 | 75.0 | |
| s_expm1.c | expm1(double) | timeout | 1.1 | n/a | 97.6 | n/a | n/a |
| s_floor.c | floor(double) | 7620.6 | 10.1 | 36.7 | 83.3 | 757.8 | 46.7 |
| s_ilogb.c | ilogb(double) | 3654.7 | 8.3 | 16.7 | 75.0 | 438.7 | 58.3 |
| s_log1p.c | log1p(double) | 11913.7 | 9.9 | 61.1 | 88.9 | 1205.7 | 27.8 |
| s_logb.c | logb(double) | 1064.4 | 0.3 | 50.0 | 83.3 | 3131.8 | 33.3 |
| s_modf.c | modf(double, double*) | 1795.1 | 3.5 | 50.0 | 100.0 | 507.0 | 50.0 |
| s_nextafter.c | nextafter(double, double) | 7777.3 | 17.5 | 50.0 | 79.6 | 445.4 | 29.6 |
| s_rint.c | rint(double) | 5355.8 | 3.0 | 35.0 | 90.0 | 1808.3 | 55.0 |
| s_sin.c | sin (double) | 667.1 | 0.3 | 75.0 | 100.0 | 1951.4 | 25.0 |
| s_tan.c | tan(double) | 704.2 | 0.3 | 50.0 | 100.0 | 2701.9 | 50.0 |
| s_tanh.c | tanh(double) | 2805.5 | 0.7 | 33.3 | 100.0 | 4075.0 | 66.7 |
| MEAN | 6058.4 | 6.9 | 42.8 | 90.8 | 3868.0 | 48.9 | |
| File name | Function name | Explanation |
|---|---|---|
| e_gamma_r.c | ieee754_gamma_r(double) | no branch |
| e_gamma.c | ieee754_gamma(double) | no branch |
| e_j0.c | pzero(double) | static C function |
| qzero(double) | static C function | |
| e_j1.c | pone(double) | static C function |
| qone(double) | static C function | |
| e_jn.c | ieee754_jn(int, double) | unsupported input type |
| ieee754_yn(int, double) | unsupported input type | |
| e_lgamma_r.c | sin_pi(double) | static C function |
| ieee754_lgammar_r(double, int*) | unsupported input type | |
| e_lgamma.c | ieee754_lgamma(double) | no branch |
| k_rem_pio2.c | kernel_rem_pio2(double*, double*, int, int, const int*) | unsupported input type |
| k_sin.c | kernel_sin(double, double, int) | unsupported input type |
| k_standard.c | kernel_standard(double, double, int) | unsupported input type |
| k_tan.c | kernel_tan(double, double, int) | unsupported input type |
| s_copysign.c | copysign(double) | no branch |
| s_fabs.c | fabs(double) | no branch |
| s_finite.c | finite(double) | no branch |
| s_frexp.c | frexp(double, int*) | unsupported input type |
| s_isnan.c | isnan(double) | no branch |
| s_ldexp.c | ldexp(double, int) | unsupported input type |
| s_lib_version.c | lib_versioin(double) | no branch |
| s_matherr.c | matherr(struct exception*) | unsupported input type |
| s_scalbn.c | scalbn(double, int) | unsupported input type |
| s_signgam.c | signgam(double) | no branch |
| s_significand.c | significand(double) | no branch |
| w_acos.c | acos(double) | no branch |
| w_acosh.c | acosh(double) | no branch |
| w_asin.c | asin(double) | no branch |
| w_atan2.c | atan2(double, double) | no branch |
| w_atanh.c | atanh(double) | no branch |
| w_cosh.c | cosh(double) | no branch |
| w_exp.c | exp(double) | no branch |
| w_fmod.c | fmod(double, double) | no branch |
| w_gamma_r.c | gamma_r(double, int*) | no branch |
| w_gamma.c | gamma(double, int*) | no branch |
| w_hypot.c | hypot(double, double) | no branch |
| w_j0.c | j0(double) | no branch |
| y0(double) | no branch | |
| w_j1.c | j1(double) | no branch |
| y1(double) | no branch | |
| w_jn.c | jn(double) | no branch |
| yn(double) | no branch | |
| w_lgamma_r.c | lgamma_r(double, int*) | no branch |
| w_lgamma.c | lgamma(double) | no branch |
| w_log.c | log(double) | no branch |
| w_log10.c | log10(double) | no branch |
| w_pow.c | pow(double, double) | no branch |
| w_remainder.c | remainder(double, double) | no branch |
| w_scalb.c | scalb(double, double) | no branch |
| w_sinh.c | sinh(double) | no branch |
| w_sqrt.c | sqrt(double) | no branch |
| Benchmark | Time (s) | Line (%) | improvement (%) | |||||||
|---|---|---|---|---|---|---|---|---|---|---|
| File | Function | #Lines | Rand | AFL | CoverMe | Rand | AFL | CoverMe | CoverMe vs. Rand | CoverMe vs. AFL |
| e_acos.c | ieee754_acos(double) | 33 | 78 | 78 | 7.8 | 18.2 | 100.0 | 100.0 | 81.8 | 0.0 |
| e_acosh.c | ieee754_acosh(double) | 15 | 23 | 23 | 2.3 | 46.7 | 100.0 | 93.3 | 46.7 | -6.7 |
| e_asin.c | ieee754_asin(double) | 31 | 80 | 80 | 8.0 | 19.4 | 96.8 | 100.0 | 80.7 | 3.2 |
| e_atan2.c | ieee754_atan2(double,double) | 39 | 174 | 174 | 17.4 | 59.0 | 97.4 | 79.5 | 20.5 | -17.9 |
| e_atanh.c | ieee754_atanh(double) | 15 | 81 | 81 | 8.1 | 40.0 | 86.7 | 100.0 | 60.0 | 13.3 |
| e_cosh.c | ieee754_cosh(double) | 20 | 82 | 82 | 8.2 | 50.0 | 95.0 | 100.0 | 50.0 | 5.0 |
| e_exp.c | ieee754_exp(double) | 31 | 84 | 84 | 8.4 | 25.8 | 93.5 | 96.8 | 71.0 | 3.2 |
| e_fmod.c | ieee754_fmod(double,double) | 70 | 221 | 221 | 22.1 | 54.3 | 60.0 | 77.1 | 22.9 | 17.1 |
| e_hypot.c | ieee754_hypot(double,double) | 50 | 156 | 156 | 15.6 | 66.0 | 58.0 | 100.0 | 34.0 | 42.0 |
| e_j0.c | ieee754_j0(double) | 29 | 90 | 90 | 9.0 | 55.2 | 100.0 | 100.0 | 44.8 | 0.0 |
| ieee754_y0(double) | 26 | 7 | 7 | 0.7 | 69.2 | 96.2 | 100.0 | 30.8 | 3.8 | |
| e_j1.c | ieee754_j1(double) | 26 | 102 | 102 | 10.2 | 65.4 | 100.0 | 100.0 | 34.6 | 0.0 |
| ieee754_y1(double) | 26 | 7 | 7 | 0.7 | 69.2 | 96.2 | 100.0 | 30.8 | 3.8 | |
| e_log.c | ieee754_log(double) | 39 | 34 | 34 | 3.4 | 87.7 | 87.2 | 100.0 | 12.3 | 12.8 |
| e_log10.c | ieee754_log10(double) | 18 | 11 | 11 | 1.1 | 83.3 | 88.9 | 100.0 | 16.7 | 11.1 |
| e_pow.c | ieee754_pow(double,double) | 139 | 188 | 188 | 18.8 | 15.8 | 92.1 | 92.7 | 76.9 | 0.6 |
| e_rem_pio2.c | ieee754_rem_pio2(double,double*) | 64 | 11 | 11 | 1.1 | 29.7 | 82.8 | 92.2 | 62.5 | 9.4 |
| e_remainder.c | ieee754_remainder(double,double) | 27 | 22 | 22 | 2.2 | 77.8 | 77.8 | 100.0 | 22.2 | 22.2 |
| e_scalb.c | ieee754_scalb(double,double) | 9 | 85 | 85 | 8.5 | 66.7 | 77.8 | 100.0 | 33.3 | 22.2 |
| e_sinh.c | ieee754_sinh(double) | 19 | 6 | 6 | 0.6 | 57.9 | 84.2 | 100.0 | 42.1 | 15.8 |
| e_sqrt.c | iddd754_sqrt(double) | 68 | 156 | 156 | 15.6 | 85.3 | 85.3 | 94.1 | 8.8 | 8.8 |
| k_cos.c | kernel_cos(double,double) | 15 | 154 | 154 | 15.4 | 73.3 | 100.0 | 100.0 | 26.7 | 0.0 |
| s_asinh.c | asinh(double) | 14 | 84 | 84 | 8.4 | 57.1 | 100.0 | 100.0 | 42.9 | 0.0 |
| s_atan.c | atan(double) | 28 | 85 | 85 | 8.5 | 25.0 | 25.0 | 96.4 | 71.4 | 71.4 |
| s_cbrt.c | cbrt(double) | 24 | 4 | 4 | 0.4 | 87.5 | 91.7 | 91.7 | 4.2 | 0.0 |
| s_ceil.c | ceil(double) | 29 | 88 | 88 | 8.8 | 27.6 | 100.0 | 100.0 | 72.4 | 0.0 |
| s_cos.c | cos (double) | 12 | 4 | 4 | 0.4 | 100.0 | 100.0 | 100.0 | 0.0 | 0.0 |
| s_erf.c | erf(double) | 38 | 90 | 90 | 9.0 | 21.1 | 78.9 | 100.0 | 79.0 | 21.1 |
| erfc(double) | 43 | 1 | 1 | 0.1 | 18.6 | 95.3 | 100.0 | 81.4 | 4.7 | |
| s_expm1.c | expm1(double) | 56 | 11 | 11 | 1.1 | 21.4 | 94.6 | 100.0 | 78.6 | 5.4 |
| s_floor.c | floor(double) | 30 | 101 | 101 | 10.1 | 26.7 | 100.0 | 100.0 | 73.3 | 0.0 |
| s_ilogb.c | ilogb(double) | 12 | 83 | 83 | 8.3 | 33.3 | 50.0 | 91.7 | 58.3 | 41.7 |
| s_log1p.c | log1p(double) | 46 | 99 | 99 | 9.9 | 71.7 | 91.3 | 100.0 | 28.3 | 8.7 |
| s_logb.c | logb(double) | 8 | 3 | 3 | 0.3 | 87.5 | 50.0 | 87.5 | 0.0 | 37.5 |
| s_modf.c | modf(double, double*) | 32 | 35 | 35 | 3.5 | 31.2 | 78.1 | 100.0 | 68.8 | 21.9 |
| s_nextafter.c | nextafter(double,double) | 36 | 175 | 175 | 17.5 | 72.2 | 88.9 | 88.9 | 16.7 | 0.0 |
| s_rint.c | rint(double) | 34 | 30 | 30 | 3.0 | 26.5 | 94.1 | 100.0 | 73.5 | 5.9 |
| s_sin.c | sin (double) | 12 | 3 | 3 | 0.3 | 100.0 | 100.0 | 100.0 | 0.0 | 0.0 |
| s_tan.c | tan(double) | 8 | 3 | 3 | 0.3 | 100.0 | 100.0 | 100.0 | 0.0 | 0.0 |
| s_tanh.c | tanh(double) | 16 | 7 | 7 | 0.7 | 43.8 | 87.5 | 100.0 | 56.3 | 12.5 |
| MEAN | 32 | 69 | 69 | 6.9 | 54.2 | 87.0 | 97.0 | 42.9 | 10.0 | |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Teaching and Learning Programming · Formal Methods in Verification
\authorinfo
Zhoulai Fu Zhendong SuUniversity of California, Davis, [email protected] [email protected]
Achieving High Coverage for Floating-point Code
via Unconstrained Programming (Extended Version)
Abstract
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbolic execution. This paper turns the challenge of testing floating-point code into the opportunity of applying unconstrained programming — the mathematical solution for calculating function minimum points over the entire search space. Our core insight is to derive a representing function from the floating-point program, any of whose minimum points is a test input guaranteed to exercise a new branch of the tested program. This guarantee allows us to achieve high coverage of the floating-point program by repeatedly minimizing the representing function.
We have realized this approach in a tool called CoverMe and conducted an extensive evaluation of it on Sun’s C math library. Our evaluation results show that CoverMe achieves, on average, 90.8% branch coverage in 6.9 seconds, drastically outperforming our compared tools: (1) Random testing, (2) AFL, a highly optimized, robust fuzzer released by Google, and (3) Austin, a state-of-the-art coverage-based testing tool designed to support floating-point code.
1 Introduction
Test coverage criteria attempt to quantify the quality of test data. Coverage-based testing DBLP:dblp_books/daglib/0012071 has become the state-of-the-practice in the software industry. The higher expectation for software quality and the shrinking development cycle have driven the research community to develop a spectrum of automated testing techniques for achieving high code coverage.
A significant challenge in coverage-based testing lies in the testing of numerical code, e.g., programs with floating-point arithmetic, non-linear variable relations, or external function calls, such as logarithmic and trigonometric functions. Existing solutions include random testing Bird:1983:AGR:1662311.1662317 ; DBLP:conf/pldi/GodefroidKS05 , symbolic execution King:1976:SEP:360248.360252 ; Boyer:1975:SFS:800027.808445 ; Clarke:1976:SGT:1313320.1313532 ; DBLP:journals/cacm/CadarS13 , and various search-based strategies Korel:1990:AST:101747.101755 ; McMinn:2004:SST:1077276.1077279 ; Baars:2011:SST:2190078.2190152 ; Lakhotia:2010:FSF:1928028.1928039 , which have found their way into many mature implementations Cadar:2008:KUA:1855741.1855756 ; DBLP:conf/kbse/BurnimS08 ; Sen:2005:CCU:1081706.1081750 . Random testing is easy to employ and fast, but ineffective in finding deep semantic issues and handling large input spaces; symbolic execution and its variants can perform systematic path exploration, but suffer from path explosion and are weak in dealing with complex program logic involving numerical constraints.
Our Work
This paper considers the problem of coverage-based testing for floating-point code and focuses on the coverage of program branches. We turn the challenge of testing floating-point programs into the opportunity of applying unconstrained programming — the mathematical solution for calculating function minima over the entire search space Zoutendijk76 ; Minoux86 .
Our approach has two unique features. First, it introduces the concept of representing function, which reduces the branch coverage based testing problem to the unconstrained programming problem. Second, the representing function is specially designed to achieve the following theoretical guarantee: Each minimum point of the representing function is an input to the tested floating-point program, and the input necessarily triggers a new branch unless all branches have been covered. This guarantee is critical not only for the soundness of our approach, but also for its efficiency — the unconstrained programming process is designed to cover only new branches; it does not waste efforts on covering already covered branches.
We have implemented our approach into a tool called CoverMe. CoverMe first derives the representing function from the program under test. Then, it uses an existing unconstrained programming algorithm to compute the minimum points. Note that the theoretical guarantee mentioned above allows us to apply any unconstrained programming algorithm as a black box. Our implementation uses an off-the-shelf Monte Carlo Markov Chain (MCMC) DBLP:dblp_journals/ml/AndrieuFDJ03 tool.
CoverMe has achieved high or full branch coverage for the tested floating-point programs. Fig. 1 lists the program s_tanh.c from our benchmark suite Fdlibm fdlibm:web . The program takes a double input. In Line 3, variable jx is assigned with the high word of x according to the comment given in the source code; the right-hand-side expression in the assignment takes the address of x (&x), cast it as a pointer-to-int (int*), add 1, and dereference the resulting pointer. In Line 4, variable ix is assigned with jx whose sign bit is masked off. Lines 5-15 are two nested conditional statements on ix and jx, which contain 16 branches in total according to Gcov gcov:web . Testing this type of programs is beyond the capabilities of traditional symbolic execution tools such as Klee Cadar:2008:KUA:1855741.1855756 . CoverMe achieves full coverage within 0.7 seconds, dramatically outperforming our compared tools, including random testing, Google’s AFL, and Austin (a tool that combines symbolic execution and search-based heuristics). See details in Sect. 6.
Contributions
This work introduces a promising automated testing solution for programs that are heavy on floating-point computation. Our approach designs the representing function whose minimum points are guaranteed to exercise new branches of the floating-point program. This guarantee allows us to apply any unconstrained programming solution as a black box, and to efficiently generate test inputs for covering program branches.
Our implementation, CoverMe, proves to be highly efficient and effective. It achieves 90.8% branch coverage on average, which is substantially higher than those obtained by random testing (38.0%), AFL afl:web (72.9%), and Austin lakhotia2013austin (42.8%).
Paper Outline
We structure the rest of the paper as follows. Sect. 2 presents background material on unconstrained programming. Sect. 3 gives an overview of our approach, and Sect. 4 presents the algorithm. Sect. 5 describes our implementation CoverMe, and Sect. 6 describes our evaluation. Sect. 7 surveys related work and Sect. 8 concludes the paper. For completeness, Sect. A-D provide additional details on our approach.
Notation
We write for floating-point numbers, for integers, for strictly positive integers. we use the ternary operation to denote an evaluation to if holds, or otherwise. The lambda terms in the form of may denote mathematical function or its machine implementation according to the given context.
2 Background
This section presents the definition and algorithms of unconstrained programming that will be used in this paper. As mentioned in Sect. 1, we will treat the unconstrained programming algorithms as black boxes.
Unconstrained Programming
We formalize unconstrained programming as the problem below dennis1996numerical :
[TABLE]
where is the objective function; , if found, is called a minimum point; and is the minimum. An example is
[TABLE]
which has the minimum point .
Unconstrained Programming Algorithms
We consider two kinds of algorithms, known as local optimization and global optimization. Local optimization focuses on how functions are shaped near a given input and where a minimum can be found at local regions. It usually involves standard techniques such as Newton’s or the steepest descent methods citeulike:2621649 . Fig. 2(a) shows a common local optimization method with the objective function that equals [math] if , or otherwise. The algorithm uses tangents of to converge to a minimum point quickly. In general, local optimization is usually fast. If the objective function is smooth to some degree, the local optimization can deduce function behavior in the neighborhood of a particular point by using information at only (the tangent here).
Global optimization for unconstrained programming searches for minimum points over . Many global optimization algorithms have been developed. This work uses Monte Carlo Markov Chain (MCMC) DBLP:dblp_journals/ml/AndrieuFDJ03 . MCMC is a sampling method that targets (usually unknown) probability distributions. A fundamental fact is that MCMC sampling follows the target distributions asymptotically, which is formalized by the lemma below. For simplicity, we present the lemma in the form of discrete-valued probabilities DBLP:dblp_journals/ml/AndrieuFDJ03 .
Lemma 2.1**.**
Let be a random variable, be an enumerable set of the possible values of , be a target probability distribution for , i.e., the probability of taking value is . Then, an MCMC sampling sequence satisfies the property that .
For example, consider the target distribution of coin tossing with probability of getting a head. An MCMC sampling is a sequence of random variables ,…, , such that the probability of being head converges to .
Using MCMC to solve unconstrained programming problems provides multiple advantages in practice. First, Lem. 2.1 ensures that MCMC sampling can be configured to attain the minimum points with higher probability than the other points. Second, MCMC integrates well with local optimization. An example is the Basinhopping algorithm leitner1997global used in Sect. 5. Third, MCMC techniques are robust; some variants can even handle high dimensional problems robbins1951stochastic or non-smooth objective functions eckstein1992douglas . Our approach uses unconstrained optimization as a black box. Fig. 2(b) provides a simple example. Steps , , and employ local optimization; Steps and , known as Monte-Carlo moves DBLP:dblp_journals/ml/AndrieuFDJ03 , avoid the MCMC sampling being trapped in the local minimum points.
3 Overview
This section states the problem and illustrates our solution.
Notation
Let FOO be the program under test with conditional statements, labeled by ,…,. Each has a true branch and a false branch . We write to denote the input domain of program FOO.
3.1 Problem Statement
Definition 3.1**.**
The problem of branch coverage-based testing aims to find a set of inputs that covers all branches of FOO. Here, we say a branch is “covered” by if it is passed through by executing FOO with an input of .
We scope the problem with three assumptions. They will be partially relaxed in our implementation (Sect. 5):
- (a)
The inputs of FOO are floating-point numbers;
- (b)
Each Boolean condition in FOO is an arithmetic comparison between two floating-point variables or constants; and
- (c)
Each branch of FOO is feasible, i.e., it is covered by an input of program FOO.
The concept below is crucial. It allows us to rewrite the branch coverage-based testing problem as defined in Def. 3.1 to an equivalent, but easier-to-solve one.
Definition 3.2**.**
Let be a set of inputs generated during the testing process. We say that a branch is saturated by if the branch itself and all its descendant branches, if any, are covered by . Here, a branch is called a descendant branch of if there exists a control flow from to . We write
[TABLE]
for the set of branches saturated by .
The control-flow graph on the right illustrates Def. 3.2. Suppose that an input set covers . Then . Branch is not saturated because it is not covered; branch is not saturated neither because its descendant branch is not covered.
Our approach reformulates the branch coverage-based testing problem with the lemma below.
Lemma 3.3**.**
Let FOO be the program under test. Assume Def. 3.1(a-c) hold. Then, a set of inputs saturates all FOO’s branches iff covers all FOO’s branches.
By consequence, the goal of branch coverage-based testing defined in Def. 3.1 can be equivalently stated: To find a set of inputs that saturates all FOO’s branches.
3.2 Illustration of Our Approach
Fig. 3 illustrates our approach. The program under test has two conditional statements and . Our objective is to find an input set that saturates all branches, namely, , , , and . Our approach proceeds in three steps:
Step 1
We inject the global variable r in FOO, and, immediately before each control point , we inject the assignment
[TABLE]
where invokes a code segment with parameters associated with . The idea of is to capture the distance of the program input from saturating a branch that has not yet been saturated. Observe that in Fig. 3, both injected return different values depending on whether the branches at are saturated or not. FOO_I denotes the instrumented program.
Step 2
This step constructs the representing function that we have mentioned in Sect. 1. The representing function is the driver program FOO_R shown in Fig. 3. It initializes r to , invokes FOO_I and then returns r as the output of FOO_R. That is to say, for a given input calculates the value of r at the end of executing .
The key in Steps 1 and 2 is to design so that FOO_R meets the two conditions below:
C1.
for all , and
C2.
iff saturates a new branch. In other words, a branch that has not been saturated by the generated input set becomes saturated with , i.e., .
Conditions C1 and C2 are essential because they allow us to transform a branch coverage-based testing problem to an unconstrained programming problem. Ideally, we can then saturate all branches of FOO by repeatedly minimizing FOO_R as shown in the step below.
Step 3
We calculate the minimum points of FOO_R via unconstrained programming algorithms described in Sect. 2. Typically, we start with an input set and . We minimize FOO_R and obtain a minimum point which necessarily saturates a new branch by condition C2. Then we have and we minimize FOO_R again which gives another input and saturates a branch that is not saturated by . We continue this process until all branches are saturated. Note that when Step 3 terminates, must be strictly positive for any input , due to C1 and C2.
Tab. 1 illustrates a scenario of how our approach saturates all branches of program FOO given in Fig. 3. Each “#n” below corresponds to a line in the table. We write and to distinguish the two injected at and respectively. (#1) Initially, no branch has been saturated. Both and set , and FOO_R returns [math] for any input. Suppose is found as the minimum point. (#2) The branch is now saturated and is not. Thus, sets . Minimizing FOO_R gives , , or . We have illustrated how these minimum points can be computed in unconstrained programming in Fig. 2(b). Suppose is found. (#3) Both and , as well as , are saturated by the generated inputs . Thus, returns the previous r and FOO_R amounts to , which returns [math] if or otherwise, where is a small predefined constant (Sect. 4). Suppose is found as the minimum point. (#4) All branches have been saturated. In this case, both and return r. FOO_R returns for all since FOO_R initializes r as . Suppose the minimum found is . It necessarily satisfies , which confirms that all branches have been saturated (due to C1 and C2).
4 Algorithm
We provide details corresponding to the three steps in Sect. 3.2. The algorithm is summarized in Algo. 1.
Algorithm for Step 1
The outcome of this step is the instrumented program FOO_I. As explained in Sect. 3.2, the essence is to inject the variable r and the assignment before each conditional statement (Algo. 1, Lines 1-4).
To define , we first introduce a set of helper functions that are sometimes known as branch distance. There are many different forms of branch distance in the literature Korel:1990:AST:101747.101755 ; McMinn:2004:SST:1077276.1077279 . We define ours with respect to an arithmetic condition .
Definition 4.1**.**
Let , , . We define branch distance as follows:
[TABLE]
and , . We use to denote a small positive floating-point close to machine epsilon. The idea is to treat a strict floating-point inequality as a non-strict inequality , etc. We will drop the explicit reference to when using the branch distance.
The intention of is to quantify how far and are from attaining . For example, is strictly positive when , becomes smaller when and go closer, and vanishes when . The following property holds:
[TABLE]
As an analogue, we set to quantify how far an input is from saturating a new branch. We define following Algo. 1, Lines 14-23.
Definition 4.2**.**
For branch coverage-based testing, the function has four parameters, namely, the label of the conditional statement , , and and from the arithmetic condition .
- (a)
If neither of the two branches at is saturated, we let return [math] because any input saturates a new branch (Lines 16-17).
- (b)
If one branch at is saturated but the other is not, we set r to be the distance to the unsaturated branch (Lines 18-21).
- (c)
If both branches at have already been saturated, returns the previous value of the global variable r (Lines 22-23).
For example, at and are invoked as and respectively in Fig. 3.
Algorithm for Step 2
This step constructs the representing function FOO_R (Algo. 1, Line 5). Its input domain is the same as that of FOO_I and FOO, and its output domain is double, so to simulate a real-valued mathematical function which can then be processed by the unconstrained programming backend.
FOO_R initializes r to 1. This is essential for the correctness of the algorithm because we expect FOO_R returns a non-negative value when all branches are saturated (Sect. 3.2, Step 2). FOO_R then calls and records the value of r at the end of executing . This r is the returned value of FOO_R.
As mentioned in Sect. 3.2, it is important to ensure that FOO_R meets conditions C1 and C2. The condition C1 holds true since FOO_R returns the value of the instrumented r, which is never assigned a negative quantity. The theorem below states FOO_R also satisfies C2.
Theorem 4.3**.**
Let FOO_R be the program constructed in Algo. 1, and the branches that have been saturated. Then, for any input , saturates a branch that does not belong to .
Proof.
We first prove the direction. Take an arbitrary such that . Let be the path in FOO passed through by executing . We know, from Lines 2-4 of the algorithm, that each is preceded by an invocation of in FOO_R. We write for the one injected before and divide into three groups. For the given input , we let P1, P2 and P3 denote the groups of that are defined in Def. 4.2(a), (b) and (c), respectively. Then, we can always have a prefix path of , with such that each for belongs to P3, and each for belongs to either P1 or P2. Here, we can guarantee the existence of such an because, otherwise, all belong in P3, and FOO_R becomes . The latter contradicts the assumption that . Because each for does nothing but performs , we know that equals to the exact value of r that assigns. Now consider two disjunctive cases on . If is in P1, we immediately conclude that saturates a new branch. Otherwise, if is in P2, we obtains the same from Eq. (8). Thus, we have established the direction of the theorem.
To prove the direction, we use the same notation as above, and let be the input that saturates a new branch, and be the exercised path. Assume that where corresponds to the newly saturated branch. We know from the algorithm that (1) updates r to [math], and (2) each such that maintains the value of r because their descendant branches have been saturated. We have thus proven the direction of the theorem. ∎
Algorithm for Step 3
The main loop (Algo. 1, Lines 8-12) relies on an existing MCMC engine. It takes an objective function and a starting point and outputs that it regards as a minimum point. Each iteration of the loop launches MCMC from a randomly selected starting point (Line 9). From each starting point, MCMC computes the minimum point (Line 10). If , is to be added to (Line 11). Thm. 4.3 ensures that saturates a new branch if . Therefore, in theory, we only need to set where denotes the number of conditional statements, so to saturate all branches. In practice, however, we set because MCMC cannot guarantee that its output is a true global minimum point.
The MCMC procedure (Algo. 1, Lines 24-34) is also known as the Basinhopping algorithm leitner1997global . It is an MCMC sampling over the space of the local minimum points Li01101987 . The random starting point is first updated to a local minimum point (Line 25). Each iteration (Lines 26-33) is composed of the two phases that are classic in the Metropolis-Hastings algorithm family of MCMC citeulike:831786 . In the first phase (Lines 27-28), the algorithm proposes a sample from the current sample . The sample is obtained with a perturbation followed by a local minimization, i.e., (Line 28), where LM denotes a local minimization in Basinhopping, and is the objective function. The second phase (Lines 29-33) decides whether the proposed should be accepted as the next sampling point. If , the proposed will be sampled; otherwise, may still be sampled, but only with the probability of , in which (called the annealing temperature Kirkpatrick83optimizationby ) is set to in Algo. 1 for simplicity.
5 Implementation
As a proof-of-concept demonstration, we have implemented Algo. 1 into the tool CoverMe. This section presents its implementation and technical details.
5.1 Frontend of CoverMe
The frontend implements Steps 1 and 2 of Algo. 1. CoverMe compiles the program under test FOO to LLVM IR with Clang clang:web . Then it uses an LLVM pass llvmpass:web to inject assignments. The program under test can be in any LLVM-supported language, e.g., Ada, the C/C++ language family, or Julia, etc. Our implementation has been tested on C code.
Fig. 4 illustrates FOO as a function of signature type_t FOO (type_t1 x1, type_t2 x2, …). The return type (output) of the function, type_t, can be any kind of types supported by C, whereas the types of the input parameters, type_t1, type_t2, …, are restricted to double or double*. We have explained the signature of in Def. 4.2. Note that CoverMe does not inject itself into FOO, but instead injects assignments that invoke . We implement in a separate C++ file.
The frontend also links FOO_I and FOO_R with a simple program loader into a shared object file libr.so, which is the outcome of the frontend. It stores the representing function in the form of a shared object file (.so file).
5.2 Backend of CoverMe
The backend implements Step 3 of Algo. 1. It invokes the representing function via libr.so. The kernel of the backend is an external MCMC engine. It uses the off-the-shelf implementation known as Basinhopping from the Scipy Optimization package scipy:web . Basinhopping takes a range of input parameters. Fig. 4 shows the important ones for our implementation basinhopping(f, sp, n_iter, call_back), where f refers to the representing function from libr.so, sp is a starting point as a Python Numpy array, n_iter is the iteration number used in Algo. 1 and call_back is a client-defined procedure. Basinhopping invokes call_back at the end of each iteration (Algo. 1, Lines 24-34). The call_back procedure allows CoverMe to terminate if it saturates all branches. In this way, CoverMe does not need to wait until passing all iterations (Algo. 1, Lines 8-12).
5.3 Technical Details
Sect. 3 assumes Def. 3.1(a-c) for the sake of simplification. This section discusses how CoverMe relaxes the assumptions when handling real-world floating-point code. We also show how CoverMe handles function calls at the end of this section.
Handling Pointers (Relaxing Def. 3.1(a))
We consider only pointers to floating-point numbers. They may occur (1) in an input parameter, (2) in a conditional statement, or (3) in the code body but not in the conditional statement.
CoverMe inherently handles case (3) because it is execution-based and does not need to analyze pointers and their effects. CoverMe currently does not handle case (2) and ignores these conditional statements by not injecting before them.
Below we explain how CoverMe deals with case (1). A branch coverage testing problem for a program whose inputs are pointers to doubles, can be regarded as the same problem with a simplified program under test. For instance, finding test inputs to cover branches of program void FOO(double* p) {if (*p <= 1)... } can be reduced to testing the program void FOO_with_no_pointer (double x) {if (x <= 1)... }. CoverMe transforms program FOO to FOO_with_no_pointer if a FOO’s input parameter is a floating-point pointer.
Handling Comparison between Non-floating-point Expressions (Relaxing Def. 3.1(b))
We have encountered situations where a conditional statement invokes a comparison between non floating-point numbers. CoverMe handles these situations by first promoting the non floating-point numbers to floating-point numbers and then injecting as described in Algo. 1. For example, before a conditional statement like if (xi op yi) where xi and yi are integers, CoverMe injects r = pen (i, op, (double) x, (double) y));. Note that such an approach does not allow us to handle data types that are incompatible with floating-point types, e.g., conditions like if (p != Null), which CoverMe has to ignore.
Handling Infeasible Branches (Relaxing Def. 3.1(c))
Infeasible branches are branches that cannot be covered by any input. Attempts to cover infeasible branches are useless and time-consuming.
Detecting infeasible branches is a difficult problem in general. CoverMe uses a heuristic to detect infeasible branches. When CoverMe finds a minimum that is not zero, it deems the unvisited branch of the last conditional to be infeasible and adds it to , the set of unvisited and deemed-to-be infeasible branches.
Imagine that we modify of the program FOO in Fig. 3 to the conditional statement if (y == -1). Then the branch becomes infeasible. We rewrite this modified program below and illustrate how we deal with infeasible branches.
l0: if (x <= 1) {x++};
y = square(x);
l1: if (y == -1) {...}
where we omit the concrete implementation of square.
Let FOO_R denote the representing function constructed for the program. In the minimization process, whenever CoverMe obtains such that , CoverMe selects a branch that it regards infeasible. CoverMe selects the branch as follows: Suppose exercises a path whose last conditional statement is denoted by , and, without loss of generality, suppose is passed through by , then CoverMe regards as an infeasible branch.
In the modified program above, if has been saturated, the representing function evaluates to or , where equals to the non-negative square(x). Thus, the minimum point must satisfy and its triggered path ends with branch . CoverMe then regards as an infeasible branch.
CoverMe then regards the infeasible branches as already saturated. It means, in line 12 of Algo. 1, CoverMe updates with saturated branches and infeasible branches (more precisely, branches that CoverMe regards infeasible).
The presented heuristic works well in practice (See Sect. 6), but we do not claim that our heuristic always correctly detects infeasible branches.
Handling Function Calls
By default, CoverMe injects only in the entry function to test. If the entry function invokes other external functions, they will not be transformed. For example, in the program FOO of Fig. 3, we do not transform square(x). In this way, CoverMe only attempts to saturate all branches for a single function at a time.
However, CoverMe can also easily handle functions invoked by its entry function. As a simple example, consider:
void FOO (double x) { GOO(x); }
void GOO (double x) { if (sin(x) <= 0.99) ... }
If CoverMe aims to saturate FOO and GOO but not sin, and it sets FOO as the entry function, then it instruments both FOO and GOO. Only GOO has a conditional statement, and CoverMe injects an assignment on r in GOO.
6 Evaluation
This section presents our extensive evaluation of CoverMe. All experiments are performed on a laptop with a 2.6 GHz Intel Core i7 running a Ubuntu 14.04 virtual machine with 4GB RAM. The main results are presented in Tab. 2, 3 and Fig. 5.
6.1 Experimental Setup
Benchmarks
Our benchmarks are C floating-point programs from the Freely Distributable Math Library (Fdlibm) 5.3, developed by Sun Microsystems, Inc. These programs are available from the network library netlib. We choose Fdlibm because it represents a set of floating-point programs with reference quality and a large user group. For example, the Java SE 8’s math library is defined with respect to Fdlibm 5.3. javastrictmath:web , Fdlibm is also ported to Matlab, JavaScript, and has been integrated in Android.
Fdlibm 5.3 has 80 programs. Each program defines one or multiple math functions. In total, Fdlibm 5.3 contains 92 math functions. Among them, we exclude 36 functions that have no branch, 11 functions involving input parameters that are not floating-point, and 5 static C functions. Our benchmarks include all remaining 40 functions. Sect. A lists all excluded functions in Fdlibm 5.3.
Parameter Settings of CoverMe
CoverMe supports three parameters: (1) the number of Monte-Carlo iterations , (2) the local optimization algorithm LM, and (3) the number of starting points . They correspond to the three input parameters of Algo. 1. Our experiment sets , , and LM = “powell” (which refers to Powell’s algorithm Press:2007:NRE:1403886 ).
Tools for Comparison
We have compared CoverMe with three tools that support floating-point coverage-based testing:
- •
Rand is a pure random testing tool. We have implemented Rand using a pseudo-random number generator.
- •
AFL afl:web is a gray-box testing tool released by the Google security team. It integrates a variety of guided search strategies and employs genetic algorithms to efficiently increase code coverage.
- •
Austin lakhotia2013austin is a coverage-based testing tool that implements symbolic execution and search-based heuristics. Austin has been shown lakhotia2010empirical to be more effective than the testing tool called CUTE Sen:2005:CCU:1081706.1081750 (which is not publicly available).
We have decided to not consider the following tools:
- •
Klee Cadar:2008:KUA:1855741.1855756 is the state-of-the-art implementation of symbolic execution. We do not consider Klee because its expression language does not support floating-point constraints. In addition, many operations in our benchmark programs, such as pointer reference, dereference, type casting, are not supported by Klee’s backend solver STP ganesh2007decision , or any other backend solvers compatible with the Klee Multi-solver extension palikareva2013multi .111 In the recent Klee-dev mailing list, the Klee developers stated that Klee or its variant Klee-FP only has basic floating-point support and they are still ”working on full FP support for Klee” kleedev:web .
- •
Klee-FP collingbourne2011symbolic is a variant of Klee geared toward reasoning about floating-point value equivalence. It determines equivalence by checking whether two floating-point values are produced by the same operations collingbourne2011symbolic . We do not consider Klee-FP because its special-purpose design does not support coverage-based testing.
- •
Pex Tillmann:2008:PWB:1792786.1792798 is a coverage tool based on dynamic symbolic execution. We do not consider Pex because it can only run for .NET programs on Windows whereas our tested programs are in C, and our testing platform is Linux.
- •
FloPSy Lakhotia:2010:FSF:1928028.1928039 is a floating-point testing tool that combines search based testing and symbolic execution. We do not consider this tool because it is developed by the same author of Austin and before Austin is released, and the tool is not available to us.
Coverage Measurement
Our evaluation focuses on branch coverage. Sect. C also shows our line coverage results. For CoverMe and Rand, we use the Gnu coverage tool Gcov gcov:web . For AFL, we use AFL-cov aflcov:web , a Gcov-based coverage analysis tool for AFL. For Austin, we calculate the branch coverage by the number of covered branches provided in the .csv file produced by Austin when it terminates.
Time Measurement
To compare the running time of CoverMe with the other tools requires careful design. CoverMe, Rand, and AFL all have the potentials to achieve higher coverage if given more time or iteration cycles. CoverMe terminates when it exhausts its iterations or achieves full coverage, whereas Random testing and AFL do not terminate by themselves. In our experiment, we first run CoverMe until it terminates using the parameters provided above. Then, we run Rand and AFL with ten times of the CoverMe time.
Austin terminates when it decides that no more coverage can be attained. It reports no coverage results until it terminates its calculation. Thus, it is not reasonable to set the same amount of time for Austin as AFL and Rand. The time for Austin refers to the time Austin spends when it stops running.
6.2 Quantitative Results
6.2.1 CoverMe versus Random testing
As a sanity check, we first compare CoverMe with Rand. In Tab. 2, we sort all programs (Col. 1) and functions (Col. 2) by their names and give the numbers of branches (Col. 3).
Tab. 2, Col. 6 gives the time spent by CoverMe. The time refers to the wall time reported by the Linux command time. Observe that the time varies considerably, ranging from 0.1 second (s_erf.c, erfc) to 22.1 seconds (e_fmod.c). Besides, the time is not necessarily correlated with the number of branches. For example, CoverMe takes 1.1 seconds to run s_expm1.c (42 branches) and 10.1 seconds to run s_floor.c (30 branches). It shows the potential for real-world program testing since CoverMe may not be very sensitive to the number of lines or branches.
Tab. 2, Col. 4 gives the time spent by Rand. Since Rand does not terminate by itself, the time refers to the timeout bound. As mentioned above, we set the bound as ten times of the CoverMe time.
Tab. 2, Col. 7 and 9 show the branch coverage results of Rand and CoverMe respectively. The coverage is reported by the Gnu coverage tool Gcov gcov:web . CoverMe achieves 100% coverage for 11 out of 40 tested functions with an average of 90.8% coverage, while Rand does not achieve any 100% coverage and attains only 38.0% coverage on average. The last row of the table shows the mean values. Observe that all values in Col. 9 are larger than the corresponding values in Col. 7. It means that CoverMe achieves higher branch coverage than Rand for every benchmark program. The result validates our sanity check.
Col. 10 is the improvement of CoverMe versus Rand. We calculate the coverage improvement as the difference between their percentages. CoverMe provides 52.9% coverage improvement on average.
Remark 6.1**.**
Tab. 2 shows that CoverMe achieves partial coverage for some tested programs. The incompleteness occurs in two situations: (1) The program under test has unreachable branches; (2) The representing function fails to confirm when it in fact holds (Thm. 4.3). The latter can be caused by a weak optimization backend, which produces sub-optimal minimum points, or by floating-point inaccuracy when evaluating FOO_R. Sect. D illustrates these two situations.
6.2.2 CoverMe versus AFL
Tab. 2 also gives the experimental results of AFL. Col. 5 corresponds to the “run time” statistics provided by the frontend of AFL. Col. 8 shows the branch coverage of AFL. As mentioned in Sect. 6.1, we terminate AFL once it spends ten times of the CoverMe time. Sect. B gives additional details on our AFL settings.
Our results show that AFL achieves 100% coverage for 2 out of 40 tested functions with an average of 72.9% coverage, while CoverMe achieves 100% coverage for 11 out of 40 tested functions with an average of 90.8% coverage. The average improvement is 17.9% (shown in the last row).
The last column is the improvement of CoverMe versus AFL. We calculate the coverage improvement as the difference between their percentages. Observe that CoverMe outperforms AFL for 33 out of 40 tested functions. The largest improvement is 73.1% with program s_atan.c. For five of tested functions, CoverMe achieves the same coverage as AFL. There are three tested functions where CoverMe achieves less (e_acosh.c, e_atan2.c, and e_pow.c).
Remark 6.2**.**
We have further studied CoverMe’s coverage on these three programs versus that of AFL. We have run AFL with the same amount of time as CoverMe (rather than ten times as much as CoverMe). With this setting, AFL does not achieves 70.0% for e_acosh.c, 63.6% for e_atan2.c, and 54.4% for e_pow.c, which are less than or equal to CoverMe’s coverage.
That being said, comparing CoverMe and AFL by running them using the same amount of time may be unfair because AFL usually requires much time to obtain good code coverage — the reason why we have set AFL to run ten times as much time as CoverMe for the results reported in Tab. 2.
6.2.3 CoverMe versus Austin
Tab. 3 compares the results of CoverMe and Austin. We use the same set of benchmarks as Tab. 2 (Col. 1-2). We use the time (Col. 3-4) and the branch coverage metric (Col. 5-6) to evaluate the efficiency and the coverage. The branch coverage of Austin (Col. 5) is provided by Austin itself rather than by Gcov. Gcov needs to have access to the generated test inputs to report the coverage, but Austin does not provide a viable way to access the generated test inputs.
Austin shows large performance variances over different benchmarks, from 667.1 seconds (s_sin.c) to hours. As shown in the last row of Tab. 3, Austin needs 6058.4 seconds on average for the testing. The average time does not include the benchmarks where Austin crashes222Austin raised an exception when testing e_sqrt.c. The exception was triggered by AustinOcaml/symbolic/symbolic.ml from Austin’s code, at line 209, Column 1. or times out. Compared with Austin, CoverMe is faster (Tab. 3, Col. 4) with 6.9 seconds on average.
CoverMe achieves a higher branch coverage (90.8%) than Austin (42.8%). We also compare across Tab. 3 and Tab. 2. On average, Austin provides slightly higher branch coverage (42.8%) than Rand (38.0%), but lower than AFL (72.9%).
Col. 7-8 are the improvement metrics of CoverMe against Austin. We calculate the Speedup (Col. 7) as the ratio of the time spent by Austin and the time spent by CoverMe, and the coverage improvement (Col. 7) as the difference between the branch coverage of CoverMe and that of Austin. We observe that CoverMe provides 3,868X speed-up and 48.9% coverage improvement on average.
Remark 6.3**.**
Three reasons contribute to CoverMe’s effectiveness. First, Thm. 4.3 allows the search process to target the right test inputs only (each minimum point found in the minimization process corresponds to a new branch until all branches are saturated). Most random search techniques do not have such guarantee, so they may waste time searching for irrelevant test inputs. Second, SMT-based methods run into difficulties in certain kinds of programs, in particular, those with nonlinear arithmetic. As a result, it makes sense to use unconstrained programming in programs that are heavy on floating-point computation. In particular, the representing function for CoverMe is carefully designed to be smooth to some degree (e.g., the branch distances defined in Def. 4.1 are quadratic expressions), which allows CoverMe to leverage the power of local optimization and MCMC. Third, compared with symbolic execution based solutions, such as Austin, CoverMe invokes the unconstrained programming backend for minimizing a single representing function, whereas symbolic execution usually needs to invoke SMT solvers for solving a large number of paths.
Since CoverMe has achieved high code coverage on most tested programs, one may wonder whether our generated inputs have triggered any latent bugs. Note that when no specifications are given, program crashes have frequently been used as an oracle for finding bugs in integer programs. Floating-point programs, on the other hand, can silently produce wrong results without crashing. Thus, when testing floating-point programs, program crashes cannot be used as a simple, readily available oracle as for integer programs. Our experiments, therefore, have focused on assessing the effectiveness of CoverMe in solving the problem defined in Def. 3.1 and do not evaluate its effectiveness in finding bugs, which is orthogonal and exciting future work.
7 Related Work
Many survey papers McMinn:2004:SST:1077276.1077279 ; sharma2014survey ; utting2012taxonomy have reviewed the algorithms and implementations for coverage-based testing.
Random Testing
The most generic automated testing solution may be to sample from the input space randomly. Pure random testing is usually ineffective if the input space is large, such as in the case of testing floating-point programs. Adaptive random testing chen2004adaptive evenly spreads the randomly generated test cases, which is motivated by the observation that neighboring inputs often exhibit similar failure behavior. AFL afl:web is another improved random testing. Its sampling is aided with a set of heuristics. AFL starts from a random seed and repeatedly mutates it to inputs that can attain more program coverage.
Symbolic Execution
Most branch coverage based testing algorithms follow the pattern of symbolic execution King:1976:SEP:360248.360252 . It selects a target path , derives a path condition , and calculates a model of the path condition with an SMT solver. The symbolic execution approach is attractive because of its theoretical guarantee, that is, each model of the path condition necessarily exercises its associated target path . In practice, however, symbolic execution can be ineffective if there are too many target paths (a.k.a. path explosion), or if the SMT backend has difficulties in handling the path condition. When analyzing floating-point programs, symbolic execution and its DSE (Dynamic Symbolic Execution) variants conf/cav/SenA06 ; song2013bitblaze ; DBLP:conf/kbse/BurnimS08 typically reduce floating-point SMT solving to Boolean satisfiability solving Peleska:2011:ATC:1986308.1986333 , or approximate the constraints over floats by those over rationals Lakhotia:2010:FSF:1928028.1928039 or reals DBLP:dblp_conf/popl/BarrVLS13 .
Fig. 6 compares symbolic execution approaches and CoverMe. Their major difference lies in that, while symbolic execution solves a path condition with an SMT backend for each target path , CoverMe minimizes a single representing function FOO_R with unconstrained programming. Because of this difference, CoverMe does not have path explosion issues and in addition, it does not need to analyze program semantics. Similar to symbolic execution, CoverMe also comes with a theoretical guarantee, namely, each minimum that attains 0 must trigger a new branch, guarantee that contributes to its effectiveness (Sect. 6).
Search-based Testing
Miller et al. Miller:1976:AGF:1313320.1313530 probably are among the first to introduce optimization methods in automated testing. They reduce the problem of testing straight-line floating-point programs into constrained programming Zoutendijk76 ; Minoux86 , that is, optimization problems in which one needs to both minimize an objective function and satisfy a set of constraints. Korel Korel:1990:AST:101747.101755 ; Ferguson:1996:CAS:226155.226158 extends Miller et al.’s to general programs, leading to the development of search-based testing McMinn:2011:SST:2004685.2005495 . It views a testing problem as a sequence of subgoals where each subgoal is associated with a fitness function; the search process is then guided by minimizing those fitness functions. Search-based techniques have been integrated into symbolic execution, such as FloPSy Lakhotia:2010:FSF:1928028.1928039 and Austin lakhotia2013austin .
CoverMe’s representing function is similar to the fitness function of search-based testing in the sense that both reduce testing into function minimization. However, CoverMe uses the more efficient unconstrained programming rather than the constrained programming used in search-based testing. Moreover, CoverMe’s use of representing function comes up with a theoretical guarantee, which also opens the door to a whole suite of optimization backends.
8 Conclusion
We have introduced a new branch coverage based testing algorithm for floating-point code. We turn the challenge of testing floating-point programs into the opportunity of applying unconstrained programming. Our core insight is to introduce the representing function so that Thm. 4.3 holds, which guarantees that the minimum point of the representing function is an input that exercises a new branch of the tested program. We have implemented this approach into the tool CoverMe. Our evaluation on Sun’s math library Fdlibm shows that CoverMe is highly effective, achieving 90.8% of branch coverage in 6.9 seconds on average, which largely outperforms random testing, AFL, and Austin.
For future work, we plan to investigate the potential synergies between CoverMe and symbolic execution, and extend this work to programs beyond floating-point code.
Acknowledgment
This research was supported in part by the United States National Science Foundation (NSF) Grants 1319187, 1528133, and 1618158, and by a Google Faculty Research Award. The information presented here does not necessarily reflect the position or the policy of the Government and no official endorsement should be inferred. We would like to thank our shepherd, Sasa Misailovic, and the anonymous reviewers for valuable feedback on earlier drafts of this paper, which helped improve its presentation.
Appendix A Untested programs in Fdlibm and Explanation
Tab. 4 lists all untested programs and functions and explains the reasons. Three types of the functions are excluded from the evaluation. They are (1) functions without any branch, (2) functions input parameters that are not floating-point, and (3) static C functions.
Appendix B AFL Settings
We run AFL following the instructions from its readme file 333http://lcamtuf.coredump.cx/afl/README.txt: We first instrument the source program using afl-gcc, 444We use AFL-clang, the alternative of afl-gcc, for programs e_j0.c and e_j1.c. afl-gcc crashes on the two due a linking issue; we are unsure whether this is due to bugs in afl-gcc or our misusing it. then we generate the test data using afl-fuzz. We terminate afl-fuzz when it spends ten times of the CoverMe time.
We show our test harness programs when we run AFL on Fdlibm programs. Test harness for Fdlibm programs that accept a single double parameter, e.g., e_acos.c:
#include <stdio.h>
//LCOV_EXCL_START
int main(int argc, char *argv[])
{
double x = 0;
scanf("%lf", &x);
fdlibm_program(x);
return 0;
}
//LCOV_EXCL_STOP
Test harness for Fdlibm programs that accept two double parameters, e.g., e_atan2.c:
#include <stdio.h>
//LCOV_EXCL_START
int main(int argc, char *argv[])
{
double x = 0;
double y = 0;
scanf("%lf␣%lf", &x, &y);
fdlibm_program(x,y);
return 0;
}
//LCOV_EXCL_STOP
Test harness for Fdlibm programs that accept a double and a double* parameters, e.g., e_rem_pio2.c:
#include <stdio.h>
//LCOV_EXCL_START
int main(int argc, char *argv[])
{
double x = 0;
double y = 0;
scanf("%lf␣%lf", &x, &y);
fdlibm_program(x,&y);
return 0;
}
//LCOV_EXCL_STOP
Above, the LCOV_EXCL_START and LCOV_EXCL_STOP parts mark the beginning and the end of an excluded section. It allows the coverage analysis tool GCov gcov:web to ignore the lines in between when reporting the coverage data.
Appendix C Line Coverage Results
The algorithm presented in the paper focuses on branch coverage. CoverMe can also achieve high line coverage. The line coverage refers to the percentage of source lines covered by the generated test data. Tab. 5 provides the line coverage results of CoverMe, AFL, and Rand. The line coverage of CoverMe, AFL, and Rand are shown in Col. 7, 8, 9 respectively. The time is the same as in Tab. 2. In particular, CoverMe has achieved 100% line coverage for 28 out of 40 tested functions. On average, CoverMe, AFL, and Rand get line coverage of 97.0%, 87.0%, and 54.2%, respectively.
Appendix D Illustration of the Incompleteness
This section discusses two benchmark programs where CoverMe did not attain full coverage. The first one is related to infeasible branches; the second one is due to the weakness of the unconstrained programming backend Basinhopping in sampling subnormal numbers.
Missed branches in k_cos.c
Fig. 7 lists one of the smallest programs in our tested benchmarks, k_cos.c. The program operates on two double inputs. It first takes |x|’s high word by bit twiddling, including a bitwise AND (), a point reference (&) and a dereference (*) operator. The bit twiddling result is then stored in an integer variable ix (Line 3), following which four conditional statements depend on ix (Lines 4-15). As shown in Tab. 2, CoverMe attained branch coverage.
By investigating the reason of the partial coverage, we found that the program had one out of the eight branches that could not be reached: In Line 5, the condition if ((int) x) == 0) always holds because it is nested within the branch. (We presume that Sun’s developers decided to use this statement to trigger the floating-point inexact exception as a side effect.) Since no inputs of __kernel_cos can trigger the opposite branch of if (((int) x) == 0), the branch coverage is in fact optimal.
Missed branches in e_fmod.c
Fig. 8 lists a segment of program e_fmod.c from line 57 to 72. As shown in Tab. 3, CoverMe covered 28 out of the 44 branches in the program.
The comment is copied from the original program directly. Line 57 (resp. Line 66) is a condition that can be triggered only if its input (resp. ) is subnormal. With our current settings specified in Sect. 6.1, CoverMe could not generate any subnormal number because its optimization backend could not. Thus, CoverMe missed the two branches in Lines 57 and 66 and all the nested branches, which are 12 in total.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] AFL: American Fuzzy Lop. http://lcamtuf.coredump.cx/afl/ . Retrieved: 01 Novermber, 2016.
- 2[2] Clang: a C language family frontend for LLVM. http://clang.llvm.org/ . Retrieved: 24 March 2016.
- 3[3] Class Strict Math of Java SE 8. https://docs.oracle.com/javase/8/docs/api/java/lang/Strict Math.html . Retrieved: 09 Novermber, 2016.
- 4[4] Code coverage analysis tool for AFL. https://github.com/mrash/afl-cov . Retrieved: 01 Novermber, 2016.
- 5[5] Fdlibm: Freely Distributed Math Library. http://www.netlib.org/fdlibm/ . Retrieved: 01 Nov, 2016.
- 6[6] Gcov: GNU compiler collection tool. https://gcc.gnu.org/onlinedocs/gcc/Gcov.html/ . Retrieved: 24 March 2016.
- 7[7] klee-dev mailing list. http://www.mail-archive.com/[email protected]/msg 02334.html . Retrieved: 09 Novermber, 2016.
- 8[8] llvm::pass class reference. http://llvm.org/docs/doxygen/html/classllvm_1_1Pass.html . Retrieved: 24 March 2016.