형상분석(프로그램분석)

Shape analysis (program analysis)

프로그램 분석에서 쉐이프 분석은 (보통 필수) 컴퓨터 프로그램에서 동적으로 할당된 링크된 데이터 구조의 속성을 발견하고 검증하는 정적 코드 분석 기법입니다.보통 컴파일 시 소프트웨어 버그를 찾거나 프로그램의 높은 수준의 정확성 속성을 확인하기 위해 사용됩니다.Java 프로그램에서는 정렬 메서드가 목록을 올바르게 정렬하는 데 사용할 수 있습니다.C 프로그램의 경우 메모리 블록이 제대로 해제되지 않은 곳을 찾을 수 있습니다.

적용들

형상 분석은 다양한 문제에 적용되어 왔습니다.

  • 메모리 안전성: 메모리 누수, 매달린 포인터의 폐기, 메모리 블록이 여러 [1][2]번 해방된 경우의 검출.
  • 어레이 Out-of-Bounds[citation needed] 오류 검색
  • type-state 속성 확인(예를 들어 파일이 다음 위치에 있는지 확인)open()그 전에read()） [citation needed]。
  • 링크된 목록을 되돌리는 방법이 목록에[2] 사이클을 도입하지 않도록 합니다.
  • 정렬 방법이 정렬된[citation needed] 순서대로 결과를 반환하는지 확인

예

형상 분석은 일반적인 포인터 분석보다 더 정밀하지만 포인터 분석의 한 형태입니다.포인터 분석은 포인터가 가리킬 수 있는 객체 세트(포인터의 포인트 투 세트라고 함)를 결정하려고 합니다.유감스럽게도 이러한 분석은 (완벽한 정밀한 정적 분석을 통해 정지 문제를 해결할 수 있기 때문에) 반드시 근사치입니다.형상 분석을 통해 더 작은(더 정확한) 점 대 집합을 결정할 수 있습니다.

다음과 같은 간단한 C++ 프로그램을 생각해 보십시오. 

아이템 *항목들[10]; 위해서 (인트 i = 0; i < > 10; ++i) {     항목들[i] = 신규 아이템(...); // 행 [1] } 프로세스_개요(항목들); // 행 [2] 위해서 (인트 i = 0; i < > 10; ++i) {     삭제하다 항목들[i]; // 행 [3] }

이 프로그램은 오브젝트의 배열을 작성하고 임의의 방법으로 처리한 후 삭제합니다.이 경우,process_items이 함수는 오류가 없고 프로그램이 안전한 것이 분명합니다.이 함수는 해방된 메모리를 참조하지 않으며 작성한 모든 오브젝트를 삭제합니다.

아쉽게도 대부분의 포인터 분석에서는 이 프로그램을 정확하게 분석하는 데 어려움이 있습니다.포인트 투 세트를 결정하려면 포인터 분석이 프로그램 객체의 이름을 지정할 수 있어야 합니다.일반적으로 프로그램은 무한한 수의 개체를 할당할 수 있지만 종료하기 위해 포인터 분석에서는 한정된 이름 집합만 사용할 수 있습니다.일반적인 근사치는 프로그램의 특정 행에 할당된 모든 객체에 동일한 이름을 부여하는 것입니다.위의 예에서는 [1] 행에 작성된 모든 객체의 이름이 동일합니다.그 때문에, 다음의 경우에,delete문이 처음으로 분석되고 분석 결과 [1]이라는 이름의 개체 중 하나가 삭제되고 있는 것으로 판단됩니다.문이 두 번째로 분석될 때(루프 상태이므로), 분석 결과 오류 가능성이 경고됩니다.배열 내의 오브젝트를 구별할 수 없기 때문에 두 번째가 될 수 있습니다.delete첫 번째 오브젝트와 동일한 오브젝트를 삭제하고 있습니다.delete. 이 경고는 거짓이며, 형상 분석의 목적은 이러한 경고를 피하는 것입니다.

요약 및 구체화

형상 분석은 객체에 대해 보다 유연한 명명 시스템을 사용하여 포인터 분석의 문제를 해결합니다.프로그램 전체에서 오브젝트에 동일한 이름을 붙이는 대신 오브젝트는 프로그램의 동작에 따라 이름을 변경할 수 있습니다.이름이 다른 여러 개의 개별 객체가 요약되거나 병합되어 동일한 이름을 가질 수 있습니다.그런 다음 프로그램에서 요약 개체를 사용하려고 할 때, 요약 개체를 구체화할 수 있습니다. 즉, 요약 개체는 단일 개체를 나타내고 다른 요약 개체는 나머지 요약 개체를 나타냅니다.도형분석의 기본 휴리스틱은 프로그램에 의해 사용되는 오브젝트는 고유한 구체화된 오브젝트를 사용하여 표현되는 반면 사용되지 않는 오브젝트는 요약되는 것입니다.

위의 예에서 개체 배열은 [1], [2] 및 [3] 행에 별도의 방법으로 요약되어 있습니다.[1] 행에서는 어레이가 부분적으로만 구성되어 있습니다.배열 요소 0..i-1에는 구성된 개체가 포함됩니다.어레이 요소 i가 생성될 예정이고 다음 요소가 초기화되지 않았습니다.형상 분석에서는 다음과 같이 첫 번째 요소 세트에 대한 요약, 요소 i에 대한 구체화된 메모리 위치 및 나머지 초기화되지 않은 위치에 대한 요약을 사용하여 이 상황을 근사할 수 있습니다.

0 .. i-1 i i+1 .. 9
생성된 객체에 대한 포인터(프로세서) 초기화되어 있지 않다 미초기화(비초기화)

루프가 종료된 후 회선 [2]에서는 아무것도 실현된 상태로 둘 필요가 없습니다.이 시점에서 모든 배열 요소가 초기화되었는지 확인합니다.

0 .. 9
생성된 객체에 대한 포인터(프로세서)

단, [3]행에서는 어레이 요소가i가 다시 사용되고 있습니다.따라서 분석에서는 [1] 행과 같이 어레이를 3개의 세그먼트로 분할합니다.근데 이번에 첫 번째 코너가i이 삭제되어 나머지 요소는 아직 유효합니다(예:delete문이 아직 실행되지 않았습니다).

0 .. i-1 i i+1 .. 9
프리(필수) 생성된 객체에 대한 포인터 생성된 객체에 대한 포인터(프로세서)

이 경우 분석은 인덱스의 포인터가i아직 삭제되지 않았습니다.따라서 중복 삭제를 경고하지 않습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Rinetzky, Noam; Sagiv, Mooly (2001). "Interprocedural Shape Analysis for Recursive Programs" (PDF). Compiler Construction. Lecture Notes in Computer Science. Vol. 2027. pp. 133–149. doi:10.1007/3-540-45306-7_10. ISBN 978-3-540-41861-0.
  2. ^ a b Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; o'Hearn, Peter W.; Wies, Thomas; Yang, Hongseok (2007). "Shape Analysis for Composite Data Structures" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 4590. pp. 178–192. doi:10.1007/978-3-540-73368-3_22. ISBN 978-3-540-73367-6.

참고 문헌

  • Neil D. Jones; Steven S. Muchnick (1982). "A flexible approach to interprocedural data flow analysis and programs with recursive data structures". POPL '82 Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM: 66–74. doi:10.1145/582153.582161. ISBN 0897910656.
  • Wilhelm, Reinhard; Sagiv, Mooly; Reps, Thomas (2007). "Chapter 12: Shape Analysis and Applications". In Srikant, Y. N.; Shankar, Priti (eds.). The Compiler Design Handbook: Optimizations and Machine Code Generation, Second Edition. CRC Press. pp. 12–1–12–44. ISBN 978-1-4200-4382-2.