Lifting On-Demand Analysis to Higher-Order Languages
In this paper, we present an approach to lift on-demand analysis to higher-order languages. Specifically, our approach bootstraps an on-demand call graph construction by leveraging a pair of on-demand data flow analyses. While static analysis is increasingly applied to find subtle bugs or prove deep properties in large, industrial code bases, to effectively find bugs or prove properties at scale, analyzers both need to resolve function calls in a precise manner (i.e., construct a precise call graph) and to examine only the relevant portion of the program (i.e., be on-demand). A strawman strategy to this problem is to use fast, approximate, whole-program call graph construction algorithms. However, this strategy is generally not adequate for modern languages like JavaScript that rely heavily on higher-order features, such as callbacks and closures, where scalable approximations often introduce unacceptable imprecision. This strategy also limits increasingly sophisticated on-demand analyses, which scale by analyzing only parts of a program as needed: the scalability advantages of an on-demand analysis may be thwarted by the need to construct a whole-program call graph. The key insight of this paper is that existing on-demand data flow analyses can themselves be applied in a black-box manner to construct call graphs on demand. We propose a soundness condition for the existing on-demand analyses with respect to partial call graphs, formalize our algorithm as an abstract domain combinator, and prove it sound in Isabelle/HOL. Furthermore, we evaluate a prototype implementation of the resulting on-demand call graph construction algorithm for a subset of JavaScript (using the Synchronized Push-Down Systems framework as the underlying data flow analysis) on benchmarks making heavy use of higher-order functions.
Mon 23 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 60mKeynote | Abstract Interpretation in Industry - Experience and Lessons LearnedKeynote SAS 2023 Pre-print | ||
10:00 30mTalk | Lifting On-Demand Analysis to Higher-Order Languages SAS 2023 Daniel Schoepe Amazon, David Seekatz Unaffiliated, Ilina Stoilkovska Amazon, Sandro Stucki Amazon, Daniel Tattersall Amazon, Pauline Bolignano Amazon, Franco Raimondi Amazon, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon Link to publication Pre-print |