article

Public Access

Achieving high coverage for floating-point code via unconstrained programming

Authors:

Zhendong SuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 6

Pages 306 - 319

https://doi.org/10.1145/3140587.3062383

Published: 14 June 2017 Publication History

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.

References

[1]

AFL: American Fuzzy Lop. http://lcamtuf.coredump.cx/ afl/. Retrieved: 01 Novermber, 2016.

[2]

Clang: a C language family frontend for LLVM. http: //clang.llvm.org/. Retrieved: 24 March 2016.

[3]

Class StrictMath of Java SE 8. https://docs.oracle.com/ javase/8/docs/api/java/lang/StrictMath.html. Retrieved: 09 Novermber, 2016.

[4]

Code coverage analysis tool for AFL. https://github.com/ mrash/afl-cov. Retrieved: 01 Novermber, 2016.

[5]

An extended version of this paper. https://arxiv.org/pdf/ 1704.03394.

[6]

Fdlibm: Freely Distributed Math Library. http://www. netlib.org/fdlibm/. Retrieved: 01 Nov, 2016.

[7]

Gcov: GNU compiler collection tool. https://gcc.gnu.org/ onlinedocs/gcc/Gcov.html/. Retrieved: 24 March 2016.

[8]

klee-dev mailing list. http://www.mail-archive.com/ [email protected]/msg02334.html. Retrieved: 09 Novermber, 2016.

[9]

llvm::pass class reference. http://llvm.org/docs/doxygen/ html/classllvm_1_1Pass.html. Retrieved: 24 March 2016.

[10]

Scipy optimization package. http://docs.scipy.org/doc/ scipy-dev/reference/optimize.html. Retrieved: 24 March 2016.

[11]

Christophe Andrieu, Nando de Freitas, Arnaud Doucet, and Michael I. Jordan. An introduction to MCMC for machine learning. Machine Learning, 50(1-2):5–43, 2003.

[12]

Arthur Baars, Mark Harman, Youssef Hassoun, Kiran Lakhotia, Phil McMinn, Paolo Tonella, and Tanja Vos. Symbolic searchbased testing. In Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE ’11, pages 53–62, Washington, DC, USA, 2011.

Digital Library

[13]

Earl T. Barr, Thanh Vo, Vu Le, and Zhendong Su. Automatic detection of floating-point exceptions. In POPL, pages 549– 560, 2013.

Digital Library

[14]

D. L. Bird and C. U. Munoz. Automatic generation of random self-checking test cases. IBM Syst. J., 22(3):229–245, 1983.

[15]

Jacob Burnim and Koushik Sen. Heuristics for scalable dynamic test generation. In 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 15-19 September 2008, L’Aquila, Italy, pages 443–446, 2008.

Digital Library

[16]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, pages 209–224, Berkeley, CA, USA, 2008.

Digital Library

[17]

Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. Commun. ACM, 56(2):82– 90, 2013.

Digital Library

[18]

Peter Collingbourne, Cristian Cadar, and Paul HJ Kelly. Symbolic crosschecking of floating-point and simd code. In Proceedings of the sixth conference on Computer systems, pages 315–328, 2011.

Digital Library

[19]

John E Dennis Jr and Robert B Schnabel. Numerical methods for unconstrained optimization and nonlinear equations, volume 16. 1996.

Digital Library

[20]

Jonathan Eckstein and Dimitri P Bertsekas. On the Douglas—Rachford splitting method and the proximal point algorithm for maximal monotone operators. Mathematical Programming, 55(1-3):293–318, 1992.

Digital Library

[21]

Roger Ferguson and Bogdan Korel. The chaining approach for software test data generation. ACM Trans. Softw. Eng. Methodol., 5(1):63–86, 1996.

Digital Library

[22]

Vijay Ganesh and David L Dill. A decision procedure for bitvectors and arrays. In International Conference on Computer Aided Verification, pages 519–531. Springer, 2007.

Digital Library

[23]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, pages 213–223, 2005.

Digital Library

[24]

James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394, 1976.

Digital Library

[25]

B. Korel. Automated software test data generation. IEEE Trans. Softw. Eng., 16(8):870–879, 1990.

Digital Library

[26]

Kiran Lakhotia, Mark Harman, and Hamilton Gross. Austin: An open source tool for search based software testing of C programs. Information and Software Technology, 55(1):112– 125, 2013.

Digital Library

[27]

Kiran Lakhotia, Phil McMinn, and Mark Harman. An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. Journal of Systems and Software, 83(12):2379–2391, 2010.

Digital Library

[28]

Kiran Lakhotia, Nikolai Tillmann, Mark Harman, and Jonathan De Halleux. FloPSy: Search-based floating point constraint solving for symbolic execution. ICTSS’10, pages 142–157, Berlin, Heidelberg, 2010.

Digital Library

[29]

DM Leitner, C Chakravarty, RJ Hinde, and DJ Wales. Global optimization by basin-hopping and the lowest energy structures of lennard-jones clusters containing up to 110 atoms. Phys. Rev. E, 56:363, 1997.

[30]

Z. Li and H. A. Scheraga. Monte Carlo-minimization approach to the multiple-minima problem in protein folding. Proceedings of the National Academy of Sciences of the United States of America, 84(19):6611–6615, 1987.

[31]

Phil McMinn. Search-based software test data generation: A survey: Research articles. Softw. Test. Verif. Reliab., 14(2):105– 156, 2004.

[32]

W. Miller and D. L. Spooner. Automatic generation of floatingpoint test data. IEEE Trans. Softw. Eng., 2(3):223–226, 1976.

Digital Library

[33]

Glenford J. Myers. The art of software testing (2nd ed.). pages I–XV, 1–234, 2004.

Digital Library

[34]

Jorge Nocedal and Stephen J. Wright. Numerical Optimization. 2006.

[35]

Hristina Palikareva and Cristian Cadar. Multi-solver support in symbolic execution. In Computer Aided Verification, pages 53–68. Springer, 2013.

[36]

Jan Peleska, Elena Vorobev, and Florian Lapschies. Automated test case generation with smt-solving and abstract interpretation. NFM’11, pages 298–312, Berlin, Heidelberg, 2011.

Digital Library

[37]

William H. Press, Saul A. Teukolsky, William T. Vetterling, and Brian P. Flannery. Numerical Recipes 3rd Edition: The Art of Scientific Computing. New York, NY, USA, 2007.

Digital Library

[38]

Herbert Robbins and Sutton Monro. A stochastic approximation method. The annals of mathematical statistics, pages 400–407, 1951.

[39]

Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A concolic unit testing engine for C. ESEC/FSE-13, pages 263– 272, New York, NY, USA, 2005.

Digital Library

[40]

Chayanika Sharma, Sangeeta Sabharwal, and Ritu Sibal. A survey on software testing techniques using genetic algorithm. arXiv:1411.1154, 2014.

[41]

Dawn Song, D Brumley, H Yin, J Caballero, I Jager, MG Kang, Z Liang, J Newsome, P Poosankam, and P Saxena. Bitblaze: Binary analysis for computer security, 2013.

[42]

Nikolai Tillmann and Jonathan De Halleux. Pex: White box test generation for .net. TAP’08, pages 134–153, Berlin, Heidelberg, 2008.

Digital Library

[43]

Mark Utting, Alexander Pretschner, and Bruno Legeard. A taxonomy of model-based testing approaches. Software Testing, Verification and Reliability, 22(5):297–312, 2012.

Digital Library

[44]

G. Zoutendijk. Mathematical programming methods. North-Holland, Amsterdam, 1976.

Cited By

Helal STao ZRubio-González CGygi FThakur A(2024)Towards Verifying Exact Conditions for Implementations of Density Functional ApproximationsSC24-W: Workshops of the International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SCW63240.2024.00027(160-169)Online publication date: 17-Nov-2024
https://doi.org/10.1109/SCW63240.2024.00027
Wang M(2023)Network information security and legal management based on embedded real-time task processing and high-frequency acquisition systemInternational Journal of System Assurance Engineering and Management10.1007/s13198-023-02136-3Online publication date: 25-Sep-2023
https://doi.org/10.1007/s13198-023-02136-3
Ma CChen LYi XFan GWang J(2022)NuMFUZZ: A Floating-Point Format Aware Fuzzer for Numerical Programs2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00046(338-347)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00046
Show More Cited By

Recommendations

Achieving high coverage for floating-point code via unconstrained programming
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
Effective floating-point analysis via weak-distance minimization
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

This work studies the connection between the problem of analyzing floating-point code and that of function minimization. It formalizes this connection as a reduction theory, where the semantics of a floating-point program is measured as a generalized ...
Detecting floating-point errors via atomic conditions

This paper tackles the important, difficult problem of detecting program inputs that trigger large floating-point errors in numerical code. It introduces a novel, principled dynamic analysis that leverages the mathematically rigorously analyzed condition ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 6

PLDI '17

June 2017

708 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3140587

Editor:
Matthew Fluet

Issue’s Table of Contents

PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2017
708 pages
ISBN:9781450349888
DOI:10.1145/3062341
General Chair:
Albert Cohen
Inria, France
,
Program Chair:
Martin Vechev
DeepCode, Switzerland / ETH Zurich, Switzerland

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 June 2017

Published in SIGPLAN Volume 52, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

National Science Foundation
Google Faculty Research Award

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
3,283
Total Downloads

Downloads (Last 12 months)1,655
Downloads (Last 6 weeks)30

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Helal STao ZRubio-González CGygi FThakur A(2024)Towards Verifying Exact Conditions for Implementations of Density Functional ApproximationsSC24-W: Workshops of the International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SCW63240.2024.00027(160-169)Online publication date: 17-Nov-2024
https://doi.org/10.1109/SCW63240.2024.00027
Wang M(2023)Network information security and legal management based on embedded real-time task processing and high-frequency acquisition systemInternational Journal of System Assurance Engineering and Management10.1007/s13198-023-02136-3Online publication date: 25-Sep-2023
https://doi.org/10.1007/s13198-023-02136-3
Ma CChen LYi XFan GWang J(2022)NuMFUZZ: A Floating-Point Format Aware Fuzzer for Numerical Programs2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00046(338-347)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00046
Mansur MMariano BChristakis MNavas JWüstholz V(2021)Automatically Tailoring Abstract Interpretation to Custom Usage ScenariosComputer Aided Verification10.1007/978-3-030-81688-9_36(777-800)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_36
Gadelha MCordeiro LNicole D(2020)An Efficient Floating-Point Bit-Blasting API for Verifying C ProgramsSoftware Verification10.1007/978-3-030-63618-0_11(178-195)Online publication date: 6-Dec-2020
https://doi.org/10.1007/978-3-030-63618-0_11
Lee WSharma RAiken A(2017)On automatically proving the correctness of math.h implementationsProceedings of the ACM on Programming Languages10.1145/31581352:POPL(1-32)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158135
Menendez H(2021)Software Testing or The Bugs’ NightmareOpen Journal of Software Engineering10.46723/ojse.1.1.1(1-21)Online publication date: 4-Apr-2021
https://doi.org/10.46723/ojse.1.1.1
He XWang XShi JLiu YKhurshid SPăsăreanu C(2020)Testing high performance numerical simulation programs: experience, lessons learned, and open issuesProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3395363.3397382(502-515)Online publication date: 18-Jul-2020
https://dl.acm.org/doi/10.1145/3395363.3397382
Vanover JDeng XRubio-González CKhurshid SPăsăreanu C(2020)Discovering discrepancies in numerical librariesProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3395363.3397380(488-501)Online publication date: 18-Jul-2020
https://dl.acm.org/doi/10.1145/3395363.3397380
Guo HRubio-González CRothermel GBae D(2020)Efficient generation of error-inducing floating-point inputs via symbolic executionProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380359(1261-1272)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380359
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Issue’s Table of Contents