선별적 문맥 구분 분석을 위한 예비분석의 자동생성

Abstract

이 논문은 요약해석에 기반한 선별적 문맥 구분 분석(selective context-sensitive analysis)을 수행할때 이를 위한 예비분석(impact pre-analysis)을 자동으로 생성해주는 방법과 생성을 위해 필요한 입력의 올바름을 검사하는 방법을 제시한다. 선별적 문맥 구분 분석을 위한 예비분석은 여러 알고리즘을 필요로 하기 때문에 설계하고 만드는데 많은 비용이 든다. 또한 대상으로하는 본분석(main analysis)에 따라 예비분석의 디자인이 달라지기 때문에 미리 고정하여 만들 수 없다. 예비분석을 만들 때 본분석에 따라 달라지는 부분은 요약실행 의미이다. 예비분석의 요약 실행 의미 디자인중 일부를 사용자에게 입력으로 받아 예비분석을 자동생성하는 방법을 소개한다. 이 때 사용자에게 받은 입력이 올바로 설계 되었는지 검사하여 생성된 예비분석이 옳은 입력에서만 동작 하도록 한다. 검사는 입력으로 받은 요약 실행 의미에 대한 정적 분석을 통해 효과적으로 수행할 수 있다. 이를 위해 예비분석의 요약 실행 의미를 기술하는 핵심 언어(core language)와 이에 대한 분석 디자인을 제시한다.

This paper presents a way to generate impact pre-analysis for selective context-sensitive analysis based on abstract interpretation[1, 2, 3] and to check the correctness of the input for the generation. It costs a lot to design and implement impact pre-analysis for selective context-sensitive analysis because it consists of many algorithms. It is impossible to make general impact pre-analysis because the design of it depends on its target main analysis. The part depending on main analysis in impact pre-analysis is abstract semantic function. We can generate impact pre-analysis receiving a part of abstract semantic function as an input. We can make only impact pre-analysis generated by correct inputs be performed by checking the correctness of the inputs design. We can check the abstract semantic function given as an input using static analysis. This paper presents a core language describing an abstract semantic function given as an input and the analysis design for checking the correctness of the input.