프로그램분석 어떻게하나 (quick/tiny) 이광근 서울대 프로그래밍연구실 kwang@ropas.snu.ac.kr

프로그램 분석 Static Program Analysis 실행전에 실행성질을 자동으로 안전하게 어림잡는 일반적인 방법

Value = Int U Real U Addr U Tree U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U Exception val(x) val(y) val(z) val(*p) val(p) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

Value = Int U Real U Addr U Tree U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U Exception val(x) val(*p) val(p) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 요약실행 V = I U R U A U T U E v(x) v(*p) v(p) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception v(x) v(y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 오류 검증 V = I U R U A U T U E v(x) v(*p) v(y) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception val(x) val(y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 늑대소년 V = I U R U A U T U E v(x) v(y) 프로그램 분석의 정확도 문제 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception val(x-y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 관계형분석 V = I U R U A U T U E v(x-y) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

프로그램 분석의 3-스텝 모든 프로그램 분석은 항상 다음의 세단계를 거친다 입력: 프로그램 단계1: “연립방정식”을 세운다 각 프로그램 지점에서 발생할 수 있는 모든 실제 프로그램 상태들을 어떻게 유한하게 요약할 지를 정한다 (abstract domain design) 각 프로그램 지점마다 그렇게 요약된 프로그램의 상태가 어떻게 흘러다니는 지를 정한다 (abstract execution flow) 단계2: 그 방정식을 푼다 각 프로그램 지점이 가질 수 있는 요약된 프로그램의 상태가 결정된다 단계3: 그 해를 가지고 분석의 결론을 내린다 (eg) 있는가 없는가? 같은가 다른가?

요약된 상태: 변수마다 변수가 가질 수 있는 정수값의 (min,max) s1 = {} 1: s2 = s1*{x:[1,1]} 2: y = 2; 3: if x 4: 5: then z=x+y; else w=y*-1 6: 7: 8: s2 = s1*{x:[1,1]} s3 = s2*{y:[2,2]} s4 = s3 s5 = s3*{x:[0,0]} s6 = s4*{z:s4(x)©s4(y)} s7 = s5*{w:s5(y)­[-1,-1] s8 = s6 U s7 s2 = {x:[1,1]} s3 = s4 = {x:[1,1], y:[2,2]} s5 = {x:[0,0],y:[2,2]} s6 = {x:[1,1],y:[2,2],z:[3,3]} s7 = {x:[0,0],y:[2,2],w:[-2,-2]} s8 = {x:[0,1],y:[2,2],z:[3,3],w:[-2,-2]}

요약된 상태: 변수마다 변수가 가질 수 있는 정수값의 (min,max) s1 = [-1,+1] 1: s2 = [1,1] s3 = (s2 U s4)Å[-1,9999] s4 = s3©[1,1] s5 = (s2 U s4)Å[10000,+1] 1: x = 1; 2: while x<10000 do 3: x = x+1; 4: od; 5: s1 = [-1,+1] s2 = [1,1] s3 = [1,9999] s4 = [2,10000] s5 = [10000,10000] 방정식의 해 구하는 방법: fixpoint iteration with widening

방정식의 해 구하기 S = F(S) S = limit of {?, F?, F(F?),} the sequence sometimes needs to be accelerated by special operation theory guides us how to make sure that the equation is correct how to make sure that the limit is computed in finite time