Semantic-Type-Guided Bug Finding
Article No.: 348, Pages 2183 - 2210
Abstract
In recent years, there has been an increased interest in tools that establish incorrectness rather than correctness of program properties. In this work we build on this approach by developing a novel methodology to prove incorrectness of semantic typing properties of functional programs, extending the incorrectness approach to the model theory of functional program typing. We define a semantic type refuter which refutes semantic typings for a simple functional language. We prove our refuter is co-recursively enumerable, and that it is sound and complete with respect to a semantic typing notion. An initial implementation is described which uses symbolic evaluation to efficiently find type errors over a functional language with a rich type system.
Supplemental Material
PDF File - Appendices of Semantic-Type-Guided Bug Finding
Included are appendices of the paper, Semantic-Type-Guided Bug Finding. The appendices contain proofs, additional operational semantics rules, and implementation details that are not covered fully in the paper.
- Download
- 626.45 KB
References
[1]
Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. USA. AAI3136691
[2]
Andrew W. Appel and David McAllester. 2001. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. ACM Trans. Program. Lang. Syst., 23, 5 (2001), sep, 657–683. issn:0164-0925 https://doi.org/10.1145/504709.504712
[3]
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. 2011. Step-Indexed Kripke Models over Recursive Worlds. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 119–132. isbn:9781450304900 https://doi.org/10.1145/1926385.1926401
[4]
Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). Association for Computing Machinery, New York, NY, USA. 268–279. isbn:1581132026 https://doi.org/10.1145/351240.351266
[5]
Derek Dreyer, Amin Timany, Robbert Krebbers, Lars Birkedal, and Ralf Jung. 2019. What Type Soundness Theorem Do You Really Want to Prove? SIGPLAN PL Perspectives. https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/
[6]
Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02). Association for Computing Machinery, New York, NY, USA. 48–59. isbn:1581134878 https://doi.org/10.1145/581478.581484
[7]
Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping. J. ACM, 55, 137 – 146. isbn:0-7695-1483-9 https://doi.org/10.1109/LICS.2002.1029823
[8]
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. SIGPLAN Not., 40, 6 (2005), jun, 213–223. issn:0362-1340 https://doi.org/10.1145/1064978.1065036
[9]
Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-Parametric Polymorphic Contracts. In Proceedings of the 2007 Symposium on Dynamic Languages (DLS ’07). Association for Computing Machinery, New York, NY, USA. 29–40. isbn:9781595938688 https://doi.org/10.1145/1297081.1297089
[10]
William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. 2019. Lazy Counterfactual Symbolic Execution. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 411–424. isbn:9781450367127 https://doi.org/10.1145/3314221.3314618
[11]
Robert Jakob and Peter Thiemann. 2015. A Falsification View of Success Typing. arxiv:1502.01278. arxiv:1502.01278
[12]
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), Article 81, apr, 27 pages. https://doi.org/10.1145/3527325
[13]
Tobias Lindahl and Konstantinos Sagonas. 2006. Practical Type Inference Based on Success Typings. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’06). Association for Computing Machinery, New York, NY, USA. 167–178. isbn:1595933883 https://doi.org/10.1145/1140335.1140356
[14]
Philippe Meunier, Robert Bruce Findler, and Matthias Felleisen. 2006. Modular Set-Based Analysis from Contracts. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). Association for Computing Machinery, New York, NY, USA. 218–231. isbn:1595930272 https://doi.org/10.1145/1111037.1111057
[15]
Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci., 17, 3 (1978), 348–375. issn:0022-0000 https://doi.org/10.1016/0022-0000(78)90014-4
[16]
Phúc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. 2017. Soft Contract Verification for Higher-Order Stateful Programs. Proc. ACM Program. Lang., 2, POPL (2017), Article 51, dec, 30 pages. https://doi.org/10.1145/3158139
[17]
Phúc C. Nguyen and David Van Horn. 2015. Relatively Complete Counterexamples for Higher-Order Programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 446–456. isbn:9781450334686 https://doi.org/10.1145/2737924.2737971
[18]
Phúc C. Nguyen and David Van Horn. 2015. Relatively Complete Counterexamples for Higher-Order Programs (Code Artifact). https://github.com/philnguyen/soft-contract/tree/pldi-2015
[19]
Phúc C. Nguyên, Sam Tobin-Hochstadt, and David Van Horn. 2017. Higher order symbolic execution for contract verification and refutation. Journal of Functional Programming, 27 (2017), e3. https://doi.org/10.1017/S0956796816000216
[20]
Peter W. O’Hearn. 2019. Incorrectness logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 10, dec, 32 pages. https://doi.org/10.1145/3371078
[21]
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng. 2020. Higher-Order Demand-Driven Symbolic Evaluation. Proc. ACM Program. Lang., 4, ICFP (2020), Article 102, aug, 28 pages. https://doi.org/10.1145/3408984
[22]
G. D. Plotkin. 1973. Lambda Definability and Logical Relations. University of Edinburgh. https://homepages.inf.ed.ac.uk/gdp/publications/logical_relations_1973.pdf
[23]
Kelvin Qian, Brandon Stride, Scott Smith, Shiwei Weng, and Ke Wu. 2024. Open-Source Codebase for Semantic-Type-Guided Bug Finding. https://github.com/JHU-PL-Lab/jaylang
[24]
Kelvin Qian, Brandon Stride, Scott Smith, Shiwei Weng, and Ke Wu. 2024. Software Artifact for Semantic-Type-Guided Bug Finding. https://doi.org/10.5281/zenodo.13393058
[25]
Kelvin Qian, Brandon Stride, Scott Smith, Shiwei Weng, and Ke Wu. 2024. Software Artifact for Semantic-Type-Guided Bug Finding. https://archive.softwareheritage.org/swh:1:snp:d10322f66a3531ab7251120395770910fe5980dd;origin=https://github.com/JHU-PL-Lab/jaylang
[26]
Steven Ramsay and Charlie Walpole. 2024. Ill-Typed Programs Don’t Evaluate. Proc. ACM Program. Lang., 8, POPL (2024), Article 67, jan, 31 pages. https://doi.org/10.1145/3632909
[27]
Caitlin Sadowski. 2020. Beyond Code: New Signals for Static Analysis (Keynote). In 9th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP) 2020 (SOAP ’20). https://www.youtube.com/watch?v=PZCoDgEIwm4
[28]
Paritosh Shroff and Scott Smith. 2004. Type inference for first-class messages with match-functions. In FOOL 11.
[29]
Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. In ECOOP 2007 – Object-Oriented Programming, Erik Ernst (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 2–27. isbn:978-3-540-73589-2 https://doi.org/10.1007/978-3-540-73589-2_2
[30]
William W. Tait. 1975. A realizability interpretation of the theory of species. In Logic Colloquium, Rohit Parikh (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 240–251. isbn:978-3-540-37483-1 https://doi.org/10.1007/BFb0064875
[31]
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A Logical Approach to Type Soundness. J. ACM, jul, issn:0004-5411 https://doi.org/10.1145/3676954 Just Accepted
[32]
Dana N. Xu, Simon Peyton Jones, and Koen Claessen. 2009. Static Contract Checking for Haskell. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). Association for Computing Machinery, New York, NY, USA. 41–52. isbn:9781605583792 https://doi.org/10.1145/1480881.1480889
Index Terms
- Semantic-Type-Guided Bug Finding
Recommendations
Machine-checked semantic session typing
CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and ProofsSession types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety ...
Ill-Typed Programs Don’t Evaluate
We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of ...
Type checking beyond type checkers, via slice & run
TAPAS 2020: Proceedings of the 11th ACM SIGPLAN International Workshop on Tools for Automatic Program AnalysisType checkers are the most commonly used form of static analysis, but their design is coupled to the rest of the language, making it hard or impossible to bring new kinds of reasoning to existing, unmodified code. We propose a novel approach to checking ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2024
2691 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 144Total Downloads
- Downloads (Last 12 months)144
- Downloads (Last 6 weeks)68
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in