In this thesis, we address two problems in compiling high-level static analysis specifications into executable analyzers: how to check the correctness of the specifications and how to achieve the efficiency of the generated analyzers. Our research is motivated from our work on a static program-analyzer generating system (named Zoo), in which the specification of static analysis (input to Zoo) consists of finite-height lattice definitions and function definitions over the lattices. In order to make our system be used in practice, we need to generate a correct and efficient program analyzer.
We present a static analysis to examine the extensivity of functions as a solution of the first problem, how to check the correctness of the specifications. One of the sufficient conditions for terminating program analysis is the extensivity of analysis function. Once extensivity of the function is ascertained, the generated analyzer is guaranteed to terminate. The extensivity analysis consists of a syntax-driven deductive rules whose satisfiability check is done by a constraint solving procedure.
We also present a differential fixpoint iteration method as a solution of the second problem, how to achieve the efficiency of the generated analyzers. Computing a static program analysis is done by the fixpoint iterations ("repeat until no-change"), and by "differential" we mean that the method tries to compute only the difference between iterations in order to avoid redundancies. Our method is fully automatic and does not require that the given analysis function or its input/output lattices should be distributive. By subtracting previous results from intermediate results, we can reduce the differences as small as possible and, by transforming the given program analysis function into differential one, we can automatically eliminate use-less computations caused by differential method.
본 논문은 프로그램 분석 명세를 컴파일(compile)하여 실행가능한 분석기를 생성하는 과정에 필요한 다음의 두가지 문제를 해결하는 데 초점을 맞추었다. 첫번째 문제는 프로그램 분석이 항상 종료하도록 제대로 정의 되었는 지를 검사하는 것이고, 두번째 문제는 생성된 분석기가 효율적으로 실행될 수 있도록 하는 것이다. 프로그램 분석 명세는 유한 높이를 가지는 래티스(lattice) 정의와, 그 래티스 상에서 정의된 분석 함수의 정의로 이루어진다. 본 연구는 프로그램 분석 명세로부터 분석기를 자동으로 생성하는 도구인 Zoo를 개발하는 과정에서 시작되었다. 우리가 개발하는 도구가 실제로 사용되기 위해서는 정확하고 (항상 종료하고), 효율적인 분석기가 생성되도록 해야한다.
첫번째 문제인 프로그램 분석의 종료를 검사하기 위한 방법으로 분석 함수의 포괄성을 분석하는 방법을 제안한다. 함수의 포괄성(extensivity)이란, 함수의 결과가 항상 입력을 포함하는 것을 말한다. 분석 함수의 포괄성은 프로그램 분석이 항상 종료하기 위한 하나의 충분조건이기 때문에, 분석 함수의 포괄성 분석을 통해서 프로그램 분석의 종료를 보장할 수 있다. 포괄성 추론 규칙은 문법 구조에 따라, 모든 식(expression)마다 그 식의 결과가 입력과 가질 수 있는 포함관계(partial order relation)를 모두 포함(include)하도록 정의된다. 이렇게 정의된 추론 규칙에 따라 제약식(constraints)을 만들어낸 후, 만들어진 제약식을 풂으로써 포괄성 분석이 이루어진다.
두번째 문제인 효율적인 분석기를 생성하기 위한 방법으로 증가분 함수를 이용한 고정점(fixpoint) 계산 방법을 제안한다. 프로그램 분석 과정은 분석 함수를 최소값에서부터 반복적으로 적용해서 그 결과가 변하지 않는 고정점을 찾아가는 것이다. 매 반복과정의 증가분만을 계산함으로써 중복된 계산을 줄일 수 있다. 제안된 방법은 자동적으로 이루어지며, 분석 함수가 분배적(distributive)이지 않아도 적용될 수 있다. 제안된 방법은 이전 연구에 비해 분석 함수를 증가분 함수로 변환(transform)함으로써 증가분 계산법을 사용할 때 야기되는 불필요한 계산을 자동으로 제거할 수 있고, 계산된 증가분에서 이전 결과를 빼 줌으로써 더 정확한 차이를 얻을 수 있다.
