Abstract
Programmers use strings to represent variates of data that contain internal structure or syntax. However, existing mainstream programming languages do not provide users with means to further narrow down the set of valid values for a string. An invalid string input may cause runtime errors or even severe security vulnerabilities. To address that, this paper presents a Ph.D. research proposal on the type checking of grammar-based string refinement types, a kind of fine-grained types for specifying the set of valid string values via grammar. The string refinement type system uses subtyping to capture the inclusion relation between the languages of grammars. Based on that, we follow a well-known bidirectional type checking framework to combine the checking and inference of string refinement types into one. Evaluations on real-world codebases will be conducted to measure the practicality of this approach.
References
[1]
T. Freeman and F. Pfenning, "Refinement types for ml," in Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, PLDI '91, (New York, NY, USA), p. 268--277, Association for Computing Machinery, 1991.
[2]
P. Resnick, "Internet Message Format." RFC 5322, Oct. 2008.
[3]
J. Dunfield and N. Krishnaswami, "Bidirectional typing," ACM Comput. Surv., vol. 54, may 2021.
[4]
H. J. Hoogeboom, "Undecidable problems for context-free grammars," Preprint https://liacs.leidenuniv.nl/~hoogeboomhj/second/codingcomputations.pdf, 2015.
[5]
L. de Moura and N. Bjørner, "Z3: An efficient smt solver," in Tools and Algorithms for the Construction and Analysis of Systems (C. R. Ramakrishnan and J. Rehof, eds.), (Berlin, Heidelberg), pp. 337--340, Springer Berlin Heidelberg, 2008.
[6]
M. Schröder and J. Cito, "Grammars for free: Toward grammar inference for ad hoc parsers," in Proceedings of the ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER '22, (New York, NY, USA), p. 41--45, Association for Computing Machinery, 2022.
[7]
A. Leung, J. Sarracino, and S. Lerner, "Interactive parser synthesis by example," in Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, (New York, NY, USA), pp. 565--574, ACM, 2015.
[8]
N. Kulkarni, C. Lemieux, and K. Sen, "Learning highly recursive input grammars," in Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering, ASE '21, p. 456--467, IEEE Press, 2022.
[9]
A. Zeller, R. Gopinath, M. Böhme, G. Fraser, and C. Holler, "The fuzzing book," 2019.
[10]
R. Gopinath, H. Nemati, and A. Zeller, "Input algebras," in Proceedings of the 43rd International Conference on Software Engineering, ICSE '21, p. 699--710, IEEE Press, 2021.
[11]
D. Steinhöfel and A. Zeller, "Input invariants," in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, (New York, NY, USA), p. 583--594, Association for Computing Machinery, 2022.
[12]
P. M. Rondon, M. Kawaguci, and R. Jhala, "Liquid types," in Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '08, (New York, NY, USA), p. 159--169, Association for Computing Machinery, 2008.
[13]
N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton-Jones, "Refinement types for haskell," in Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, (New York, NY, USA), p. 269--282, Association for Computing Machinery, 2014.
[14]
P. Vekris, B. Cosman, and R. Jhala, "Refinement types for typescript," in Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, (New York, NY, USA), p. 310--325, Association for Computing Machinery, 2016.
Recommendations
Gradual refinement types
POPL '17Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Gradual refinement types
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesRefinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Refinement types for Haskell
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program VerificationWe present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
In-Cooperation
- IEEE CS
Publisher
IEEE Press
Publication History
Published: 27 July 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICSE '23
Sponsor:
ICSE '23: 45th International Conference on Software Engineering: Companion Proceedings
May 14 - 20, 2023
Victoria, Melbourne, Australia
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 21Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 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