컴파일러 정확성

Compiler correctness

컴퓨팅에서 컴파일러의 정확성컴파일러언어 사양에 따라 행동한다는 것을 보여주려는 시도를 다루는 컴퓨터 과학의 한 분야다.[citation needed]기법에는 형식적인 방법을 사용하여 컴파일러를 개발하고 기존 컴파일러에 대해 엄격한 테스트(종종 컴파일러 유효성 검사라고 함)를 사용하는 것이 포함된다.null

형식검증

컴파일의 정확성을 확립하기 위한 두 가지 주요 형식 검증 접근방식은 모든 입력에 대해 컴파일러의 정확성을 입증하고 특정 프로그램 컴파일의 정확성을 증명하고 있다(번역 유효성 검사).null

모든 입력 프로그램에 대한 컴파일러 정확성

형식적인 방법에 의한 컴파일러 검증은 긴 공식 연역논리의 사슬을 포함한다.[1]단, 증명(테레머 프로베서)을 찾는 툴은 소프트웨어에서 구현되고 복잡하기 때문에 오류를 포함할 가능성이 높다.한 가지 접근방식은 교정쇄기보다 훨씬 간단하기 때문에 오류를 포함할 가능성이 적은 교정쇄기(증거확인기)를 사용하는 것이었다.null

이 접근방식의 두드러진 예는 C99의 큰 부분집합에 대한 컴파일러 최적화를 공식적으로 검증한 CompCert이다.[2][3][4]null

또 다른 검증된 컴파일러는 KakeML 프로젝트에서 개발되었는데,[5] 이 프로젝트에서는 HOL(proof assistant)을 사용하여 표준 ML 프로그래밍 언어의 상당 부분 집합의 정확성을 확립한다.null

공식적으로 올바른 컴파일러를 얻기 위한 또 다른 접근법은 의미론적 방향 컴파일러 생성을 사용하는 것이다.[6]null

변환 유효성 검사: 주어진 프로그램에서 컴파일러 수정

컴파일러가 모든 유효한 입력 프로그램에 대해 올바르다는 것을 증명하려고 시도하는 것과 대조적으로, 변환 검증은 주어진 입력 프로그램이 올바르게 컴파일되는지 자동으로 설정하는 것을 목표로 한다.주어진 프로그램의 정확한 컴파일러를 증명하는 것은 잠재적으로 모든 프로그램에 대해 컴파일러가 옳다는 것을 증명하는 것보다 쉽지만, 여전히 상징적인 추론을 필요로 한다. 왜냐하면 고정된 프로그램은 여전히 임의로 큰 입력에 대해 작동하고 임의로 오랜 시간 동안 실행될 수 있기 때문이다.번역 유효성 검사는 주어진 컴파일에 대해 컴파일이 정확하다는 증거를 생성하여 기존 컴파일러 구현을 재사용할 수 있다.번역 유효성 검사는 때때로 잘못된 코드를 생성하는 컴파일러에서도 사용될 수 있다. 이 부정확한 코드가 특정 프로그램에 대해 그 자체를 나타내지 않는 한 말이다.입력 프로그램에 따라 번역 유효성 검사가 실패할 수 있다(생성된 코드가 잘못되었거나 번역 유효성 검사 기법이 너무 약해서 정확성이 보이지 않기 때문이다).그러나 번역 유효성 검사에 성공하면 컴파일러 프로그램이 모든 입력에 대해 정확함을 보장한다.null

테스트

시험은 컴파일러를 운송하는 노력의 상당한 부분을 차지하지만 표준 문헌에서는 비교적 적은 커버리지(coverage)를 받는다.1986년판 아호, 세티, 울만에는 컴파일러 테스트에 관한 한 페이지 섹션이 있으며, 명명된 예는 없다.[8]2006년 판은 시험에 관한 부분은 생략하지만, "컴파일러를 최적화하는 것은 너무 어려워서 우리는 감히 어떤 컴파일러 최적화도 오류가 전혀 없다고 말할 수 없다!따라서 컴파일러를 쓰는 데 있어서 가장 중요한 목표는 그것이 옳다는 것이다."[9]Fraser & Hanson 1995에는 회귀 테스트에 대한 간단한 섹션이 있다; 소스 코드를 사용할 수 있다.[10]Bailey & Davidson 2003 커버 테스트 절차 호출에[11] 대한 많은 기사들은 공개된 컴파일러들이 유의미한 코드 수정 버그를 가지고 있다는 것을 확인시켜 준다.[12]Sheridan 2007은 아마도 일반 컴파일러 시험에 관한 가장 최근의 저널일 것이다.[13]대부분의 경우 컴파일러 테스트에서 사용할 수 있는 가장 큰 정보는 Fortran[14] 및 Cobol[15] 유효성 검사 제품군이다.null

컴파일러를 테스트할 때 더 일반적인 기법으로는[16] 솜털(컴파일러에서 버그를 찾기 위해 무작위 프로그램을 생성하는 것)과 테스트 케이스 축소(검색된 테스트 케이스를 최소화하여 이해하기 쉽게 하기 위해 노력하는 것)가 있다.[17]null

참고 항목

참조

  1. ^ De Millo, R. A.; Lipton, R. J.; Perlis, A. J. (1979). "Social processes and proofs of theorems and programs". Communications of the ACM. 22 (5): 271–280. doi:10.1145/359104.359106.
  2. ^ Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices. 41: 42–54. doi:10.1145/1111320.1111042.
  3. ^ Leroy, Xavier (2009-12-01). "A Formally Verified Compiler Back-end". Journal of Automated Reasoning. 43 (4): 363–446. arXiv:0902.2137. doi:10.1007/s10817-009-9155-4. ISSN 0168-7433.
  4. ^ "CompCert - The CompCert C compiler". compcert.inria.fr. Retrieved 2017-07-21.
  5. ^ "CakeML: A Verified Implementation of ML".
  6. ^ Stephan Diehl, 자연적 의미론적 생성 컴파일러 추상적 기계, 컴퓨팅의 형식적 측면, Vol. 12(2), Springer Verlag, 2000. doi:10.1007/PL00003929
  7. ^ Pnueli, Amir; Siegel, Michael; Singerman, Eli. Translation Validation. Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98.
  8. ^ 컴파일러: 원칙, 기술도구, infra 1986, 페이지 731.
  9. ^ ibid, 2006, 페이지 16.
  10. ^ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 978-0-8053-1670-4., 페이지 531–3.
  11. ^ Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls" (PDF). IEEE Transactions on Software Engineering. 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829. doi:10.1109/tse.2003.1245304. Archived from the original (PDF) on 2003-04-28. Retrieved 2009-03-24., 페이지 1040.
  12. ^ 예, 크리스티안 Lindig(2005년)."C의 예측할 시험 호출 규약"(PDF).제6회 국제 워크숍 자동 디버깅에 회보.ACM. 아이 에스비엔 1-59593-050-7.2011-07-11에 있는 원본(PDF)에서 Archived.., 에릭 Eide;JohnRegehr(2008년)2009-03-24 Retrieved."Volatiles 있게 하고 무엇이 그것에 대해 miscompiled"(PDF).임베디드 소프트웨어에 관한 7ACM국제 회의 회보.ACM. 아이 에스비엔 978-1-60558-468-3.2009-03-24 Retrieved.
  13. ^ Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. doi:10.1002/spe.812. Retrieved 2009-03-24. 참고 문헌 목록:{{cite web}} 누락되거나 비어 있음(도움말).
  14. ^ "Source of Fortran validation suite". Retrieved 2011-09-01.
  15. ^ "Source of Cobol validation suite". Retrieved 2011-09-01.
  16. ^ Chen, Yang; Groce, Alex; Zhang, Chaoqiang; Wong, Weng-Keen; Fern, Xiaoli; Eide, Eric; Regehr, John (2013). Taming Compiler Fuzzers. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '13. New York, NY, USA: ACM. pp. 197–208. CiteSeerX 10.1.1.308.5541. doi:10.1145/2491956.2462173. ISBN 9781450320146.
  17. ^ Regehr, John; Chen, Yang; Cuoq, Pascal; Eide, Eric; Ellison, Chucky; Yang, Xuejun (2012). Test-case Reduction for C Compiler Bugs. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '12. New York, NY, USA: ACM. pp. 335–346. doi:10.1145/2254064.2254104. ISBN 9781450312059.