Date of Award

August 2016

Degree Type

Thesis

Degree Name

Master of Science

Department

Computer Science

First Advisor

Tian Zhao

Committee Members

John Tang Boyland, Ichiro Suzuki, Susan Mcroy

Keywords

Abstract Interpretation, Control-Flow Analysis, Javascript, Programming Languages, Pushdown Analysis, Static Analysis

Abstract

In control flow analysis (CFA), call/return mismatch is a problem that reduces analysis precision. So-called k-CFA uses bounded call-strings to obtain limited call/return matching, but it has a serious performance problem due to its coupling of call/return matching with context-sensitivity of values. CFA2 and PDCFA are the first two algorithms that bring pushdown (context-free reachability) approach to the CFA area, which provide perfect call/return mathcing. However, CFA2 and PDCFA both need significant engineering effort to implement. The abstracting abstract machine (AAM), a configurable framework for constructing abstract interpreters, introduces store-allocated continuations that make the soundness of abstract interpreters easily obtainable. Recently, two related approaches (AAC and P4F) provide call/return matching using AAM by modeling the call-stack as a pushdown system. However, AAC incurs high overhead and is hard to understand, while P4F cannot compute monovariant analysis. To overcome the above shortcomings, we developed a new method, h-CFA, to address the call/return mismatch problem. h-CFA records the program execution history during abstract interpretation and uses it to avoid control flow merging that causes call/return mismatch. Our method uses AAM and is very easy to implement for ANF style program. ANF is a popular intermediate representation of programs that converts all complex intra-procedural control flows to linear let-bindings and sets a syntactic variable to each sub-expression. In addition, our method reveals an essential property of any pushdown CFA, which we exploited in the development of a static analyzer for JavaScript, named JsCFA. This application of the essential property avoids recording the program execution history, so source programs are no long required being the ANF form. Meanwhile, JsCFA adopts a technique to solve the environment problem or fake rebinding, which eliminates more defects of monovariant analysis. This, in cooperation with exact call/return matching, yield more precise analysis and better performance. Moreover, JsCFA supports a configurable interface to add context-sensitivity to selected areas of programs. JsCFA applies the interface to improve the analysis precision for runtime object extensions. Finally, we quantitatively evaluated the performance of JsCFA.

Share

COinS