Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript
Support for regular expressions in symbolic execution-based tools for test generation and bug finding is insufficient. Common aspects of mainstream regular expression engines, such as backreferences or greedy matching, are ignored or imprecisely approximated, leading to poor test coverage or missed bugs. In this paper, we present a model for the complete regular expression language of ECMAScript 2015 (ES6), which is sound for dynamic symbolic execution of the test and exec functions. We model regular expression operations using string constraints and classical regular expressions and use a refinement scheme to address the problem of matching precedence and greediness. We implemented our model in ExpoSE, a dynamic symbolic execution engine for JavaScript, and evaluated it on over 1,000 Node.js packages containing regular expressions, demonstrating that the strategy is effective and can significantly increase the number of successful regular expression queries and therefore boost coverage.
Tue 25 JunDisplayed time zone: Tijuana, Baja California change
08:30 - 09:30 | Bug Finding & Testing IPLDI Research Papers at 229AB Chair(s): Cindy Rubio-González University of California, Davis | ||
08:30 20mTalk | Lazy Counterfactual Symbolic Execution PLDI Research Papers William T. Hallahan Yale University, Anton Xue Yale University, Maxwell Troy Bland University of California at San Diego, USA, Ranjit Jhala University of California, San Diego, Ruzica Piskac Yale University, USA Media Attached | ||
08:50 20mTalk | Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript PLDI Research Papers Blake Loring , Duncan Mitchell Royal Holloway, University of London, Johannes Kinder Bundeswehr University Munich Media Attached | ||
09:10 20mTalk | Effective Floating-Point Analysis via Weak-Distance Minimization PLDI Research Papers |