Download files
Abstract
Pointer analysis, as a fundamental research, is to identify the possible runtime values of a pointer during compile-time. It paves the way for a wide range of clients, such as compiler optimisations, software bug detection and program verification. Nowadays, with the massive growth of software, analysing large-scale programs is inevitable. It has become vital yet enormously difficult to develop effective techniques to significantly reduce the analysis overhead while maintaining sufficient precision for analysing large code bases in practice.
This thesis addresses a key challenge faced by modern software systems: making practical techniques that enable pointer analysis to analyse large-scale programs efficiently and precisely. Targeting two major clients, optimising compilers and software bug detection, our contributions are three-fold: First, Icon, a fully parameterised context sensitive Andersenʼs analysis, achieves context sensitivity by summarising the side effects of a procedure using one transfer function on virtual variables. Icon analyses large programs efficiently while being sufficiently precise to drive compiler optimisations. Second, Quda, a query-directed adaptive heap cloning analysis, performs k-callsite- sensitive heap cloning iteratively, starting without heap cloning, so that an abstract heap object is cloned at the next iteration only if some may-alias queries that are not answered positively at the current iteration. Quda obtains the precision of full heap cloning while being significantly more scalable. Third, Saber, a value-flow analysis for memory leak detection, is the first full-sparse analysis to resolve a classical source-sink problem by capturing value flows of all memory locations represented by both top-level and address-taken pointers. Saber is also the first major client for validating effectiveness of sparse pointer analysis. By exploiting field-, flow- and context-sensitivity during different phases of the analysis, Saber detects memory leaks in a program by solving a graph reachability problem on its sparse value-flow graph.