Pointer analysis statically estimates the runtime pointer behavior of a program. It is an important building block of optimizing compilers and program verifiers for C programs. Various approaches with precision and performance trade-off have been proposed. Among them, two recent techniques have enabled precise, yet scalable analyses. One is cycle elimination for subset-based analysis where cyclic inclusion constraints are detected and collapsed without losing any precision. The other is the use of binary decision diagram (BDD) for cloning-based context-sensitive analysis where all non-recursive invocations are analyzed precisely. Redundancies among exponential contexts are shared automatically through BDD-encoding. Also, constraints are encoded and resolved with BDD. However, it has been shown that such fully BDD-based analysis doesn`t work in synergy with cycle elimination.
In this thesis, we present a new method on cloning-based context-sensitive pointer analysis with an effective application of cycle elimination. Our method is not based on BDD. Instead, we propose a novel constraint-based formulation with context set annotations. Our constraint resolution rules are formulated entirely with set-level context operations only. So, we always handle contexts in large granularities, which replaces the need for fully BDD-based analysis. For context set representation, we directly use an invocation graph structure without BDD-encoding. Then, we make set operations efficient by applying a folklore structure sharing technique known as hash-consing to the invocation graph. Experimental results on 16 C programs ranging from 20000 to 290000 lines show that applying cycle elimination to our new formulation results in 4.5$\times$ speedup over previous fully BDD-based approach.
포인터 분석은 실행 중에 가능한 프로그램의 모든 포인터 동작을 미리 예측하는 분석이다. 이는 C언어에 대한 최적화 컴파일러 및 검증기를 구현하는데 중요한 요소로 작용한다. 따라서 정확도 및 성능을 적절히 조율하는 다양한 연구가 이뤄지고 있다. 이 중 사이클 제거 기법은 부분집합 관계 제약식에 사이클이 있는 경우 이에 속한 모든 변수들이 같은 분석 결과를 갖게 되기 때문에 이를 하나로 합쳐서 정확도를 잃지 않으며 빠른 분석을 가능하게 하는 기법이다. 또한 분석 전체를 이진 의사결정 다이어그램(binary decision diagram - BDD)으로 표현해 모든 비재귀(non-recursive) 호출 문맥을 정확하게 분석하는 기법들이 제시되고 있다. 이러한 정확도의 분석은 지수복잡도를 가지지만 많은 호출 문맥 및 제약식에서 중복이 있게 되고 BDD는 이를 자동으로 공유 하도록 해준다. 하지만 분석 전체가 BDD로 표현이 되는 경우에는 사이클 제거 기법이 효율적이지 않다고 알려져 있다.
본 논문에서는 호출 문맥을 고려하는 분석에 대해 효율적으로 사이클 제거 기법을 적용하는 방법을 제시한다. 이를 위해 BDD를 사용하지 않도록 하였다. 대신에 호출 문맥의 집합을 제약식에 주석으로 달고 제약식을 푸는 과정에서는 집합 단위의 연산을 통해서만 호출 문맥을 다루도록 하는 새로운 분석 방식을 제시한다. 이러한 방식을 통해 많은 문맥을 한 번의 연산으로 다룰 수 있게 되고 이는 BDD를 통해서 가능하였던 효율성을 대체하는 효과가 있게 된다. 또한 효율적인 집합 연산을 위해 호출 그래프(invocation graph) 구조를 통해 호출 문맥의 집합을 표현하는 새로운 방식을 제안한다. 이에 대해 구조적인 중복을 공유하는 일반적인 기법인 해쉬 콘징(hash-consing)을 적용함으로써 BDD를 상회하는 효율성을 얻을 수 있었다. BDD도 일종의 해쉬 콘징 기법이지만 대상 구조를 이진수로 표현해야 한다는 차이가 있다. 제안한 기법들의 효율성을 검증하기 위해 20000-290000 라인의 크기를 가지는 16개의 C 프로그램들에 대해 실험을 수행하였다. 실험 결과 기존의 분석 전체를 BDD로 표현하는 방식에 비해 4.5배의 속도 향상이 있음을 보일 수 있었다.
