We present a characteristic type-inference algorithm for Rabbit. Rabbit is the program-analysis-specfication language for System Zoo. Rabbit has some overloaded operators and allows implicit type castings. Owing to these features of the language, we cannot apply a simple type-inference algorithm based on unification.
We present a lattice-validation algorithm for Rabbit. Rabbit provides various syntax to define lattices. Among those, providing user-defined join operator to a set sometimes results in an invalid lattice definition. We want to detect the invalid lattice definition, for it may result in an incorrect program analysis.
우리는 시스템 Zoo라고 명명한 시스템을 개발하고 있다.시스템 Zoo는 프로그램 분석을 기술한 명세로부터 프로그램 분석기를 자동으로 생성해주는 유용한 프로그래밍 환경이다. 래빗 언어(Rabbit)는 프로그램 분석을 기술하기 위한 명세 언어로서, 시스템 Zoo의 입력이 될 명세를 작성하는 데 이용된다.
이 논문에서는 래빗 프로그램을 위한 타입 유추 알고리즘을 제안하였다. 래빗 언어는 타입 유추를 어렵게 만드는 두 가지 특성을 지니고 있다. 첫째는, 몇몇 연산자가 여러가지 타입의 값에 적용될 수 있다는 것이고, 둘째는, 프로그래머가 명시하지 않은 타입 변환을 허용하는 경우가 있다는 것이다. 타입의 동일화(unification) 과정을 바탕으로 하는 기존의 타입 유추 알고리즘은 래빗 언어에 적용할 수 없었다. 우리의 알고리즘은 타입에 대한 제약 조건을 다양한 형태로 도출하고, 모든 제약 조건을 만족하는 타입을 찾아내는 것이다. 그 과정에서 우리는 제약 조건을 보다 간단한 형태로 변환해 가는데, 최종적으로는 모든 제약 조건을 집합 식으로 바꾸어 해를 얻는다.
덧붙여, 올바르지 않은 래빗 프로그램을 판단하는 또 하나의 방법을 제안하였다. 래빗 언어는 사용자가 다양한 래티스(lattice)를 정의하고 사용할 수 있도록, 새로운 래티스를 정의하기 위한 다양한 문법을 제공한다. 한 가지 방법은 집합의 원소들에 대해 결합 연산(the join operator)을 정의함으로써 새로운 래티스를 정의하는 방법이다. 그러나 사용자가 이러한 방법으로 정의한 타입은 실제로는 래티스가 아닌 경우도 있을 수 있다. 잘못된 래티스 정의는 프로그램 분석기의 찾기 힘든 오류로 이어질 수 있으므로, 이러한 경우를 걸러내기 위한 간단한 알고리즘을 제안하였다.
