We design a string analysis within abstract interpretation framework. To this end, we invent novel predicates which are derived from the reference pushdown automaton. Using these predicates, we design a conjunctive domain whose element is a conjunction of the predicates. We establish the correctness relation by Galois connection and define a correct abstract concatenation operation on the domain. We also present a family of pushdown automata called $\epsilon$ bounded pushdown automata. This family covers all context-free languages. By using this family of pushdown automata, we can prevent abstract values from becoming infinite conjunctions and make sure that all the operations required in the analyzer are computable.
We also present a technique for embracing various string operations other than concatenation. We introduce small refinement to the conjunctive domain to design the abstract replace operation. Other various string operations that require more detailed information about the contents of the string are handled by grammar transformations. After all, these grammars are also accommodated to our analysis after abstracting the language of the grammar.
Our analysis can be used for any context-free reference language. Using our string analyzer designed in abstract interpretation framework, we can easily compose the string analysis with other analyses to improve the precision, and it is also possible to design modular string analyzer.
본 논문에서는 요약해석 프레임워크 안에서 표현된 문자열 분석을 제시한다. 이를 위해 우리는 참조 푸시다운 오토마타로부터 문자열에 대한 술어를 만들어 내고, 이를 기반으로 논리곱 도메인을 만들어 낸다. 논리곱 도메인의 요약값은 일반적으로 무한한 갯수의 술어를 가질 수 있다. 이 경우를 방지하기 위해 $\epsilon$ 제한 푸시다운 오토마타를 제시한다. 이 오토마타를 이용할 경우, 분석에서 필요한 모든 연산이 계산가능해지며, 무한한 크기의 요약값을 이용할 필요가 없어진다.
논리곱 도메인은 문자열 접합 연산을 정확하게 요약 도메인에서 디자인하기 위해 만들어진 도메인이다. 우리는 이 도메인을 개량하여 문자열 치환 연산에서 필요한 정보 추가하였다. 이 요약 문자열 치환 연산은 의미있는 문자열 치환 연산 사용례를 정확하게 분석할 수 있게 해준다. 그리고 그 외의 다양한 문자열 연산은, 문맥자유 문법으로 가능한 문자열 값을 나타내는 기법과, 그에 대한 문자열 연산을 문법 변환으로 표현하는 기법을 이용한다. 문법으로 나타나 있는 가능한 문자열 값도 마지막에는 우리가 만든 도메인의 요약값으로 수용하여 분석에 이용한다. 이를 위해 문맥자유 문법으로 표현된 언어를 안전하게 요약하는 알고리즘을 제시하였다.
본 논문에서 제시한 요약 기법은 모든 문맥자유 참조 언어에 대해 적용가능하다. 우리 분석은 다른 분석기와 결합하여 정확도를 쉽게 올릴 수 있으며, 모듈 단위의 문자열 분석을 가능하게 해준다.
