Lec11. Semantic Analysis (2) - 11주차 2강, 12주차 2강

11주차 2강, 12주차 2강 11/13, 11/20

11/18은 휴강

 

lec10에서 언급한 내용임

• Abstract Interperetation의 주요 단계
  • abstract domain: 변수는 구체적인 값 대신 추상화된 값으로 표현 됨
  • 변수의 값이 가질 수 있는 범위 또는 특성을 정의, 구간 / 옥타곤, 짝홀 등
  • 구체적인 의미로는 7에 2를 더하면 9가 되지만, 추상적인 의미로는 홀수에 2를 더하면 홀수이다

연산, 불리안 판별, command 처리에 대한 simple language 만드는 과정

• 추상 도메인 개요
  
  • 새로운 기호들이 등장하는데, 본문 슬라이드 내용과 같고
  • 이상하게 생긴 육각형은 맨위의 any부터 시작해서 아래로 뻗어나오는 tree처럼 생각하면 됨
  • any: 모든 값 포함
  • non-pos: 0 또는 음의 정수, non-zero: 음의 정수 또는 양의 정수: non-neg: 0 또는 양의 정수
  • neg: 음의 정수, zero: 0, pos: 양의 정수
  • none: 아무 값도 포함하지 않음
• 부분순서
  • Pos⊑Non−Zero: 양수 집합은 0이 아닌 값들의 부분 집합
  • Zero⊑Non−Pos 및 Zero⊑Non−Neg은 비양수 및 비음수에 속함.
  • a⊑b는 b가 a보다 더 많은 정보를 포함하고 있음을 나타냄

• 추상 도메인 D는 반드시 complete lattice여야 함
• 모든 부분집합 Y에 대해 최소상한이 D 안에 존재해야 함
  • 여러 분기에서 safe approximation을 보장하기 위함
  • if(...) {x:=Neg} else {x:=Zero} 예시에서
  • x의 가능한 값은 Neg 또는 Zero
  • 두 값을 결합한 최소상한인 Non-Pos를 정의해야 안전한 추론 가능
  • Neg와 Zero의 상한이 정의되지 않았다면, over-approximation 발생 가능

join - 두 원소 사이에 최소 상한을 계산하는 연산자

• State = Var -> Sign 각 변수가 기호로 매핑되는 함수 형태

• b1이 b2보다 같거나 더 구체적이거나, b1이 none 또는 b2가 any일 때 참이다

• 상수 n을 추상화된 부호로 표현함, 변수 x를 추상화된 부호로 표현함ㅁ -> Neg Zero Pos
• 추상 도메인에서 +,*,- 연산을 실시함. 그 결과 역시 추상화된 부호로 표현됨

 

• 추상적 부호 사이의 연산에 대한 결과(시계 방향으로 덧셈, 곱셈, 뺄셈에 대한 결과)
  • Any: 결과가 불확실하거나 모든 가능성을 포함할 수 있는 경우 사용됨. 양수나 음수 모두 가능
  • None: 결과가 정의되지 않거나 의미가 없는 경우 사용됨
  • Non-Neg, Non-Zero: 0또는 양수 포함. 0이 아닌 모든 값 포함

• boolean 연산에 대한 결과

 

command에 대한 처리

• 반복문: 진입상태를 over-approximation하여 fixed point(상태 변화 없을 때까지)에 도달
  • entry: 반복문 진입
  • b: 반복 조건, true: 반복문 본체 실행, false: 반복문 종료
  • c: 반복문 본체 body. 반복문 내부에서 상태를 갱신.
• 반복 횟수가 유한하든 무한하든 프로그램의 안정성이나 오류 가능성을 검증할 수 있도록 설계

• 부호분석을 통해 프로그램의 안정성을 증명.
• 종료 후에 x>=0임을 증명해야 함.
  • 초기화 단게에서 x=Zero
  • 모든 반복 과정에서 x는 Non-Neg 상태 유지
  • 반복문 종료 후에도 x>=0 조건이 항상 만족됨