Lec13.Semantic Analysis (4) - 13주차 1강/2강

11월 25일, 27일 / 13주차 1강, 2강

* 개인 공부를 위해 정리한 것입니다. 정확한 내용은 꼭 본인이 공부하는 교재를 참고하시기 바랍니다.

• 고정점 계산
  • 반복문처럼 state의 변화가 있는 명령문에서 stable state를 찾기 위해 고정점 계산을 함
  • 고정점은 항상 종료되는가? 종료되기 위해서는 추상 도메인의 lattice가 finite height를 가져야 함
  • 그러나 실제 도메인은 infinite height를 가져, 고정점 계산이 끝나지 않을 수 있음
• Widening 연산자 - 고정점 계산이 종료하지 않는 문제를 해결하기 위해 도입
  • 상태 병합(join) 과정에서 빠르게 상위 상태로 approximation하여 반복 과정을 종료하도록 함
  • 무한 높이를 가진 lattice에서도 고정점 계산의 종료를 보장
  • 정확성을 약간 희생하고 safe approximation을 보장

• 구간 도메인의 정의
  • none: 추상값이 존재하지 않는 상태
  • [l,u]: 구간의 상한과 하한.
  • 구간 도메인은 무수히 많은 조합을 가지고 있어, 무한한 높이를 가짐
• invariant: 불변식, 프로그램의 특정 지점 p에서 x의 추상 값이 [l,u]라면 l<=x<=u라는 불변식이 보장됨

반복문이 종료되기 위해서는 x와 y의 추상값이 더 이상 변하지 않아야 하는데

x<10 조건은 걸려있지만, y에 대한 조건이 없어서 계속 범위가 늘어남

 

• widening: 고정점 계산을 빠르게 종료시키기 위해, 상태를 더 포괄적인 값으로 확장
• narrowing: widening으로 인해 발생할 수 있는 over-approximation을 보정. 다시 state를 좁혀서 정확한 값 계산

• widening으로 fixed point 계산하기
• 초기에는 x와 y 모두 범위 [0,0]으로 설정하기
• 첫 번째 반복 후
  • x와 y의 범위 [0,1]가 됨
  • 상태가 계속 확장되는 것을 막기 위해 widening을 적용하면, [0,+inf]로 범위가 확장됨
  • m1이 m0에 포함되지 않아 fixed point에 도달하지 못했기 때문에 2nd 반복을 실행함 ([0,0]은 [0,+inf]에 포함 안됨)

• 두 번째 반복
  • m2는 이전 x,y에 대해 값이 1씩 증가했으므로, 가능한 범위 값의 출발점이 0이 아니라 1이 됨
  • 그리고 x는 10보다 작다는 제한이 걸려있으니까 x의 경우 가능한 +inf에서 10으로 조정됨
  • m0랑 교집합을 구하면 x [0,10] y [+inf]
  • 근데 여기서 다시 widening을 적용해서 강제 수렴시켜버리면 [0,+inf] [0,+inf]이 됨
  • 그럼 m1이랑 비교하면 [0,+inf]는 [0,+inf]에 포함되므로 만족. 종료됨.

 

• 다시 narrowing으로 정확하게 축소가힉
• 초기 상태는 x와 y의 값이 각각 [0,+inf]로 추상화됨
• 첫번째 반복 후, x [0,10] y [0,+inf]가 됨
  • narrowing 적용하면, m1은 x [0,10] y [0,+inf]가 됨 m0는 m1에 포함되지 않음. fixed point가 아님
• 두번째 반복 후, x [0,10] y [0,+inf]가 됨
  • narrowing 적용하면 m2는 x [0,10], y는 [0,+inf]가 됨. m1은 m2에 포함됨. fixed point만남. 종료.

• interval domain의 요소
  • I, 빈구간과 정수 l과 u 사이의 값으로 표현되는 구간의 교집합으로 표현됨
  • partial order
    • 모든 구간 내 요소는 빈구간을 포함해야 하고, [-inf, inf] 범위 내에 모든 요소가 포함되어야 하며
    • [l1,u1]은 [l2,u2]에 포함되어야 함. 이때 l1은 l2보다 커야 하고, u1은 u2보다 작아야 함

연산 결과를 구간으로 표현함

모든 조합의 덧셈, 곱셉, 뺄셈을 포함하는 구간으로 계산함

 

연산 예시값들

none은 뭐랑 어떻게 해도 none으로 나옴

 

불리안 연산

명령어

if문에서 조건 b의 결과가 불확실한 경우(any가 되는 경우), 두 경로의 결과를 결합함.

while문에서 b가 참인 경우 c를 실행, 새로운 상태에서 다시 b를 평가, b가 거짓이 되면 종료.

간단한 확장, 축소 연산 결과

[a,b] [c,d]의 경우

widening 연산을 하면, c<a이면 -inf아니면 a, b<d이면 +inf 아니면 b를 채택해서 구간 산정

narrowing 연산을 하면, a=-inf이면 c 아니면 a, b=+inf이면 d 아니면 b