확정과제분석

Definite assignment analysis

컴퓨터 과학에서 확정 할당 분석은 변수 또는 위치가 사용되기 전에 항상 할당되도록 보수적으로 보장하기 위해 컴파일러에 의해 사용되는 데이터 흐름 분석입니다.

동기

C 및 C++ 프로그램에서는 특히 진단이 어려운 에러의 원인은 미초기화 변수를 읽어냄으로써 발생하는 비결정적인 동작입니다.이 동작은 플랫폼, 빌드, 실행 시마다 다를 수 있습니다.

이 문제를 해결하는 두 가지 일반적인 방법이 있습니다.하나는 읽기 전에 모든 위치를 확실히 쓰는 것입니다.라이스의 정리는 이 문제를 모든 프로그램에 대해 일반적으로 해결할 수 없다는 것을 증명하지만, 일부 올바른 프로그램을 거부하면서 이 제약을 충족하는 프로그램만 받아들이는 보수적(불확실한) 분석을 만들 수 있으며, 확실한 할당 분석은 그러한 분석이다.Java 및 C#[2] 프로그래밍 언어 사양에서는[1] 분석이 실패했을 경우 컴파일러가 컴파일 시 오류를 보고해야 합니다.두 언어 모두 상세하게 기술된 특정 형식의 분석이 필요합니다.Java에서 이 분석은 Stérk [3]등에 의해 공식화되었으며, 일부 올바른 프로그램은 거부되고 명시적인 불필요한 할당을 도입하기 위해 수정되어야 한다.C#에서는 이 분석은 Fruja에 의해 공식화되어 모든 제어 흐름 경로를 따라 할당된 모든 변수가 확실하게 할당된 [4]것으로 간주된다는 점에서 정확하고 소리도 정확합니다.또한 Cyclon 언어는 프로그램이 [5]명확한 할당 분석을 통과해야 하지만, 포인터 유형이 있는 변수에서만 C 프로그램의 이동을 용이하게 합니다.

이 문제를 해결하는 두 번째 방법은 정의된 시점에서 모든 위치를 일정한 예측 가능한 값으로 자동으로 초기화하는 것이지만, 이로 인해 새로운 할당이 발생하여 성능이 저하될 수 있습니다.이 경우 확실한 할당 분석을 통해 중복 할당(개입 가능한 읽기 없이 다른 할당만 이어지는 할당)을 제거할 수 있는 컴파일러 최적화가 가능합니다.이 경우 프로그램은 거부되지 않지만 분석이 명확한 할당을 인식하지 못한 프로그램에는 중복 초기화가 포함될 수 있습니다.공통 언어 인프라스트럭처는 이 [6]접근방식에 의존합니다.

용어.

변수 또는 위치는 프로그램의 특정 지점에서 다음 세 가지 상태 중 하나라고 할 수 있습니다.

  • 확실하게 할당됨:변수는 확실하게 할당되어야 합니다.
  • 완전 미할당:변수는 할당 해제될 것이 확실합니다.
  • 알 수 없음:변수를 할당할 수도 있고 할당 해제할 수도 있습니다. 분석이 정확하지 않아 어느 변수를 지정할 수 없습니다.

분석

다음은 Fruja가 C# 절차 내(단일 방식) 확정 할당 분석을 공식화한 것을 기반으로 합니다.이것은 모든 로컬 변수를 [4]사용하기 전에 할당하는 것을 책임집니다.명확한 할당 분석과 부울 값의 지속적인 전파를 동시에 수행합니다.5가지 정적 함수를 정의합니다.

이름. 도메인 묘사
전에 모든 문장과 표현 지정된 문 또는 식을 평가하기 전에 할당된 변수입니다.
끝나고 모든 문장과 표현 주어진 스테이트먼트 또는 식을 평가한 후 정상적으로 완료된다고 가정한 후 할당된 변수입니다.
변수 모든 문장과 표현 지정된 문 또는 식 범위에서 사용할 수 있는 모든 변수.
진실의 모든 부울식 표현식이 true로 평가된다고 가정할 때 지정된 표현식의 평가 후에 할당된 변수입니다.
거짓의 모든 부울식 표현식이 false로 평가된다고 가정할 때 지정된 표현식의 평가 후에 할당된 변수입니다.

구문 하위 표현식의 함수 값 측면에서 다양한 표현식 및 문장에서 이러한 함수의 값을 정의하는 데이터 흐름 방정식을 제공합니다.현재 goto, break, continue, return 또는 exception handling 문이 없다고 가정합니다.다음은 이들 방정식의 몇 가지 예입니다.

  • 할당된 변수 집합에 확실히 영향을 미치지 않는 표현식 또는 문장 e: after(e) = before(e)
  • e를 할당식 loc = v로 합니다.그런 다음 이전(v) = 이전(e) 및 이후(e) = 이후(v) U {loc}입니다.
  • e가 참이라는 표현으로 하자.그런 다음 true(e) = before(e) 및 false(e) = vars(e)입니다.즉, e가 false로 평가될 경우 e는 false로 평가되지 않기 때문에 모든 변수가 (공백하게)
  • 메서드 인수는 왼쪽에서 오른쪽으로 평가되므로 이전(예i + 1) = 이후(예i)입니다.메서드가 완료되면 out 파라미터가 확실하게 할당됩니다.
  • (e)가1 다른2 경우 조건문이 되도록 하자.그런 다음 이전(e) = 이전(e), 이전(s1) = 참(e), 이전(s2) = 거짓(e) 및 이후(s) = 이후(s1)가2 교차합니다.
  • while loop 스테이트먼트(e)를1 s로 합니다.그런 다음 이전(e) = 이전(s), 이전(s1) = 참(e), 이후(s) = 거짓(e)입니다.
  • 기타 등등.

메서드의 시작 부분에서는 로컬 변수가 확실하게 할당되지 않습니다.검증자는 추상 구문 트리에서 반복하여 데이터 흐름 방정식을 사용하여 고정점에 도달할 때까지 집합 간에 정보를 마이그레이션합니다.그런 다음 검증자는 로컬 변수를 사용하는 모든 식의 이전 세트를 검사하여 해당 변수가 포함되어 있는지 확인합니다.

이 알고리즘은 goto, break, continue, return 및 exception 처리와 같은 제어 흐름 점프의 도입으로 복잡해집니다.이러한 점프 중 하나의 대상이 될 수 있는 문장은 점프 소스에서 명확하게 할당된 변수 집합과 사전에 교차해야 한다.이러한 요소가 도입되면 다음 예시와 같이 결과 데이터 흐름에 여러 고정점이 있을 수 있습니다.

 인트 i = 1;  L:  에 가다 L;

레이블 L은 두 위치에서 도달할 수 있으므로, goto에 대한 제어 흐름 방정식은 (2) 이전 = (1) 이후가 (3) 이전과 교차하도록 지시합니다.그러나 (3) 이전 = (2) 이전이므로, 이전 (2) = 이후 (1)은 (2) 이전과 교차한다.여기에는 before(2), {i} 및 빈 집합에 대한 두 개의 고정 지점이 있습니다.그러나 데이터 흐름 방정식의 단조로운 형식 때문에 확실하게 할당된 변수에 대해 가장 가능한 정보를 제공하는 고유한 최대 고정점(가장 큰 크기의 고정점)이 있음을 알 수 있습니다.이러한 최대(또는 최대) 고정점은 표준 기법으로 계산할 수 있습니다. 데이터 흐름 분석을 참조하십시오.

또 다른 문제는 컨트롤 플로우점프가 특정 컨트롤 플로우를 실행할 수 없게 할 수 있다는 것입니다.예를 들어 이 코드프래그먼트에서는 변수 i가 사용 전에 확실하게 할당되어 있습니다.

 인트 i;  한다면 (j < > 0) 돌아가다; 또 다른 i = j;  인쇄물(i);

if에 대한 데이터 흐름 방정식은 after(2) = after(반환)가 after(i = j) 뒤에 교차한다고 말합니다.이 문제를 정확하게 해결하기 위해 모든 제어 흐름 점프에 대해 after(e) = vars(e)를 정의한다. 이는 제어 흐름 점프 직후에 제어가 불가능하기 때문에 false(true) = vars(e) 등식이 유효한 것과 동일한 의미에서 공허하게 유효하다.

레퍼런스

  1. ^ J. Gosling; B. Joy; G. Steele; G. Bracha. "The Java Language Specification, 3rd Edition". pp. Chapter 16 (pp.527–552). Retrieved December 2, 2008.
  2. ^ "Standard ECMA-334, C# Language Specification". ECMA International. pp. Section 12.3 (pp.122–133). Retrieved December 2, 2008.
  3. ^ Stärk, Robert F.; E. Borger; Joachim Schmid (2001). Java and the Java Virtual Machine: Definition, Verification, Validation. Secaucus, NJ, USA: Springer-Verlag New York, Inc. pp. Section 8.3. ISBN 3-540-42088-6.
  4. ^ a b Fruja, Nicu G. (October 2004). "The Correctness of the Definite Assignment Analysis in C#". Journal of Object Technology. 3 (9): 29–52. CiteSeerX 10.1.1.165.6696. doi:10.5381/jot.2004.3.9.a2. Retrieved 2008-12-02. We actually prove more than correctness: we show that the solution of the analysis is a perfect solution (and not only a safe approximation).
  5. ^ "Cyclone: Definite Assignment". Cyclone User's Manual. Retrieved December 16, 2008.
  6. ^ "Standard ECMA-335, Common Language Infrastructure (CLI)". ECMA International. pp. Section 1.8.1.1 (Partition III, pg. 19). Retrieved December 2, 2008.