모양 분석을 사용한 소스 코드 검증 및 오류 추적

Abstract

프로그램을 실행시켜 보지 않고 프로그램의 성질을 유추하는 기법인 프로그램 분석 기법은 그 유용성으로 인해 많은 분야에서 적용되어 왔다. 그런데 이러한 프로그램 분석 기법은 포인터 및 힙 메모리를 다루는 프로그램에 대해서는 분석해야 할 정보의 복잡성으로 인해 적용이 쉽지 않았다. 그러나 최근, 모양 분석 및 분리 논리과 같은 독보적인 기술의 발전으로 프로그램 분석이 포인터 프로그램에 적용될 수 있는 길이 열리기 시작했다. 하지만 이러한 분석 기술을 적용한 대부분의 분석기는, 천여 줄의 프로그램을 분석하는 데에도 많은 시간이 걸리는 문제점을 안고 있다. 이러한 문제는 분석기가 복잡한 힙 메모리 구조도 정확하게 파악하기 위해 분석을 정교히 수행하는 데서 기인한다. 그러나 실제로는 복잡하지 않은 구조의 힙 메모리를 다루는 프로그램이 대부분이다. 본 논문에서는 이러한 사실을 고려하여 기존의 모양 분석에서 문제되어 왔던 비싼 비용 문제를 극복하고, 실제 현장에서 쓰이는 만여 줄 가량의 포인터 프로그램을 저렴한 비용에 분석하는 분석기를 기술한다. 또한 이러한 분석기가 내놓은 분석 결과를 가지고, 실제 오류가 발생하는 지점을 찾아내는 오류 추적기 또한 설명하고자 한다.; Shape analysis, which is a sort of static program analysis, can detect pointerrelated defects of the program. However, the cost of previous shape analysis is expensive due to trying to precisely analyze complicated data-structures. But many programs in real world handle simple data structure like lists or tree. Therefore, one reasonable approach to low-cost shape analysis is to consider only simple data-structures. In this thesis, we propose a low-cost shape analyzer for the program that handles only lists or tree-like data-structures. Also, we propose a error tracer to trace error path which heads to the error location found by the shape analyzer. As a case study, we use our shape analyzer to find pointer errors of some Linux device drivers. In result, we can analyze the examples with lower cost than previouse shape analyzer and find error path represents defects of the program.