Abstract
Compilers are error-prone due to their high complexity. They are relevant for not only general purpose programming languages, but also for many domain specific languages. Bugs in compilers can potentially render all programs at risk. It is thus crucial that compilers are systematically tested, if not verified. Recently, a number of efforts have been made to formalise and standardise programming language semantics, which can be applied to verify the correctness of the respective compilers. In this work, we present a novel specification-based testing method named SpecTest to better utilise these semantics for testing. By applying an executable semantics as test oracle, SpecTest can discover deep semantic errors in compilers. Compared to existing approaches, SpecTest is built upon a novel test coverage criterion called semantic coverage which brings together mutation testing and fuzzing to specifically target less tested language features. We apply SpecTest to systematically test two compilers, i.e., the Java compiler and the Solidity compiler. SpecTest improves the semantic coverage of both compilers considerably and reveals multiple previously unknown bugs.
Chapter PDF
Similar content being viewed by others
References
Casting a floating-point number to an integer, https://github.com/kframework/java-semantics/issues/64
Casting double to int and long to int produce different results, https://bugs.java.com/bugdatabase/view_bug.do?bug_id=JDK-8246334
Division by zero exception, https://github.com/kframework/java-semantics/issues/63
Incorrect output from bitwise and unary operation function call, https://github.com/Conflux-Chain/conflux-rust/issues/988
Minus sign issues for hex octal and binary literals, https://bugs.java.com/bugdatabase/view_bug.do?bug_id=8236406
Missing error message incompatible types: possible lossy conversion, https://bugs.java.com/bugdatabase/view_bug.do?bug_id=JDK-8244681
More specific error message for division by zero, https://github.com/ethereum/solidity/issues/8064
New string leads to timeout, https://github.com/kframework/java-semantics/issues/62
Octal values in double/float arrays, https://github.com/kframework/java-semantics/issues/61
Out of bounds array access, https://github.com/ethereum/solidity/issues/8364
Parsing issue for hexadecimal, https://github.com/kframework/java-semantics/issues/60
Type error for short computations, https://bugs.java.com/bugdatabase/view_bug.do?bug_id=JDK-8240371
Typeerror too restrictive or inconsistent?, https://github.com/ethereum/solidity/issues/8139
Wrong modulo computation for negative doubles, https://github.com/kframework/java-semantics/issues/58
Wrong precision for float variables, https://github.com/kframework/java-semantics/issues/59
Wrong representation of floating point numbers, https://github.com/kframework/java-semantics/issues/66
Conflux: High-efficiency public blockchain (2019), https://www.conflux-chain.org
Remix: Ethereum ide and tools for the web (2019), https://remix.ethereum.org
Specify and enforce evaluation order on sub-expressions (2019), https://github.com/ethereum/solidity/issues/7820
Discover, track and compare open source (2020), https://www.openhub.net
Truffle suite: Sweet tools for smart contracts (2020), http://truffleframework.com
Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Yoo, S.: The oracle problem in software testing: A survey. IEEE Trans. Software Eng. 41(5), 507–525 (2015)
Bauer, J.A., Finger, A.B.: Test plan generation using formal grammars. In: Proceedings of the 4th International Conference on Software Engineering, Munich, Germany, September 1979. pp. 425–432. IEEE Computer Society (1979), http://dl.acm.org/citation.cfm?id=802969
Bogdanas, D., Rosu, G.: K-Java: A complete semantics of java. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015. pp. 445–456. ACM (2015). https://doi.org/10.1145/2676726.2676982
Boujarwah, A.S., Saleh, K.: Compiler test case generation methods: a survey and assessment. Information & Software Technology 39(9), 617–625 (1997). https://doi.org/10.1016/S0950-5849(97)00017-7
Chen, J., Hu, W., Hao, D., Xiong, Y., Zhang, H., Zhang, L., Xie, B.: An empirical comparison of compiler testing techniques. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14–22, 2016. pp. 180–190. ACM (2016). https://doi.org/10.1145/2884781.2884878
Chen, Y., Su, T., Su, Z.: Deep differential testing of JVM implementations. In: Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25–31, 2019. pp. 1257–1268. IEEE / ACM (2019). https://doi.org/10.1109/ICSE.2019.00127
Cummins, C., Petoumenos, P., Murray, A., Leather, H.: Compiler fuzzing through deep learning. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, Amsterdam, The Netherlands, July 16–21, 2018. pp. 95–105. ACM (2018). https://doi.org/10.1145/3213846.3213848
Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22–28, 2012. pp. 533–544. ACM (2012). https://doi.org/10.1145/2103656.2103719, https://doi.org/10.1145/2103656.2103719
Fowler, T.: How many computer languages are there? (2020), https://careerkarma.com/blog/how-many-coding-languages-are-there
Hanford, K.V.: Automatic generation of test cases. IBM Systems Journal 9(4), 242–257 (1970). https://doi.org/10.1147/sj.94.0242
Jackson, D., Damon, C.: Elements of style: Analyzing a software design feature with a counterexample detector. In: Proceedings of the 1996 International Symposium on Software Testing and Analysis, ISSTA 1996, San Diego, CA, USA, January 8–10, 1996. pp. 239–249. ACM (1996). https://doi.org/10.1145/229000.226322
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Software Eng. 37(5), 649–678 (2011). https://doi.org/10.1109/TSE.2010.62
Jiao, J., Kan, S., Lin, S., Sanan, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: Executable operational semantics of solidity. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18–20, 2020. IEEE (2020), accepted for publication
Kalinov, A., Kossatchev, A., Posypkin, M., Shishkov, V.: Using ASM specification for automatic test suite generation for mpC parallel programming language compiler. Action Semantics AS 2002 p. 99 (2002)
Kalinov, A., Kossatchev, A.S., Petrenko, A.K., Posypkin, M., Shishkov, V.: Coverage-driven automated compiler test suite generation. Electr. Notes Theor. Comput. Sci. 82(3), 500–514 (2003). https://doi.org/10.1016/S1571-0661(05)82625-8
Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22–28, 2012. pp. 285–296. ACM (2012). https://doi.org/10.1145/2103656.2103691
Köroglu, Y., Wotawa, F.: Fully automated compiler testing of a reasoning engine via mutated grammar fuzzing. In: Proceedings of the 14th International Workshop on Automation of Software Test, AST@ICSE 2019, May 27, 2019, Montreal, QC, Canada. pp. 28–34. IEEE / ACM (2019). https://doi.org/10.1109/AST.2019.00010
Kossatchev, A.S., Posypkin, M.: Survey of compiler testing methods. Programming and Computer Software 31(1), 10–19 (2005). https://doi.org/10.1007/s11086-005-0008-6
Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09–11, 2014. pp. 216–226. ACM (2014). https://doi.org/10.1145/2594291.2594334
Le, V., Sun, C., Su, Z.: Finding deep compiler bugs via guided stochastic program mutation. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25–30, 2015. pp. 386–399. ACM (2015). https://doi.org/10.1145/2814270.2814319
Le, V., Sun, C., Su, Z.: Randomized stress-testing of link-time optimizers. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, MD, USA, July 12–17, 2015. pp. 327–337. ACM (2015). https://doi.org/10.1145/2771783.2771785
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814
Lin, S.W.: KSolidity semantics (2018), https://github.com/kframework/solidity-semantics
McKeeman, W.M.: Differential testing for software. Digital Technical Journal 10(1), 100–107 (1998), http://www.hpl.hp.com/hpjournal/dtj/vol10num1/vol10num1art9.pdf
Nguyen, D.T., Pham, L.H., Sun, J., Lin, Y., Tran, M.Q.: sFuzz: An efficient adaptive fuzzer for solidity smart contracts. In: Proceedings of the 42nd International Conference on Software Engineering, ICSE 2020. IEEE / ACM (2020)
Park, D., Stefanescu, A., Rosu, G.: KJS: a complete formal semantics of javascript. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15–17, 2015. pp. 346–356. ACM (2015). https://doi.org/10.1145/2737924.2737991, https://doi.org/10.1145/2737924.2737991
Prechtel, D., Groß, T., Müller, T.: Evaluating spread of ‘gasless send’ in ethereum smart contracts. In: 10th IFIP International Conference on New Technologies, Mobility and Security, NTMS 2019, Canary Islands, Spain, June 24–26, 2019. pp. 1–6. IEEE (2019). https://doi.org/10.1109/NTMS.2019.8763848
Purdom, P.: A sentence generator for testing parsers. BIT Numerical Mathematics 12(3), 366–375 (1972)
Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010). https://doi.org/10.1016/j.jlap.2010.03.012
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: Effective tool support for the working semanticist. J. Funct. Program. 20(1), 71–122 (2010). https://doi.org/10.1017/S0956796809990293
Sheridan, F.: Practical testing of a C99 compiler using output comparison. Softw., Pract. Exper. 37(14), 1475–1488 (2007). https://doi.org/10.1002/spe.812
Su, Z., Sun, C.: Emi-based compiler testing (2018), https://web.cs.ucdavis.edu/~su/emi-project
Sun, C., Le, V., Su, Z.: Finding and analyzing compiler warning defects. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14–22, 2016. pp. 203–213. ACM (2016). https://doi.org/10.1145/2884781.2884879
Sun, C., Le, V., Su, Z.: Finding compiler bugs via live code mutation. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016. pp. 849–863. ACM (2016). https://doi.org/10.1145/2983990.2984038
Tang, Y., Ren, Z., Kong, W., Jiang, H.: Compiler testing: A systematic literature analysis. CoRR abs/1810.02718 (2018), http://arxiv.org/abs/1810.02718
Tao, Q., Wu, W., Zhao, C., Shen, W.: An automatic testing approach for compiler based on metamorphic testing technique. In: 17th Asia Pacific Software Engineering Conference, APSEC 2010, Sydney, Australia, November 30 - December 3, 2010. pp. 270–279. IEEE Computer Society (2010). https://doi.org/10.1109/APSEC.2010.39
Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3) (1995), http://compscinet.dcs.kcl.ac.uk/JP/jp030301.abs.html
Wang, C., Kang, S.: ADFL: an improved algorithm for american fuzzy lop in fuzz testing. In: Cloud Computing and Security - 4th International Conference, ICCCS 2018, Haikou, China, June 8–10, 2018, Revised Selected Papers, Part V. Lecture Notes in Computer Science, vol. 11067, pp. 27–36. Springer (2018). https://doi.org/10.1007/978-3-030-00018-9_3
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4–8, 2011. pp. 283–294. ACM (2011). https://doi.org/10.1145/1993498.1993532
Zelenov, S.V., Zelenova, S.A.: Automated generation of positive and negative tests for parsers. In: Formal Approaches to Software Testing, 5th International Workshop, FATES 2005, Edinburgh, UK, July 11, 2005, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3997, pp. 187–202. Springer (2005). https://doi.org/10.1007/11759744_13
Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Software Eng. 28(2), 183–200 (2002). https://doi.org/10.1109/32.988498
Acknowledgments
This research is supported by the National Research Foundation Singapore under its NSoE Programme (Award Number.: NSOE-TSS2019-03).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Schumi, R., Sun, J. (2021). SpecTest: Specification-Based Compiler Testing. In: Guerra, E., Stoelinga, M. (eds) Fundamental Approaches to Software Engineering. FASE 2021. Lecture Notes in Computer Science(), vol 12649. Springer, Cham. https://doi.org/10.1007/978-3-030-71500-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-71500-7_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71499-4
Online ISBN: 978-3-030-71500-7
eBook Packages: Computer ScienceComputer Science (R0)