추상 해석

컴퓨터 과학에서 **추상 해석**(abstract interpretation)은 순서 집합, 특히 격자에 대한 단조함수를 기반으로 하는 컴퓨터 프로그램의 의미론의 건전한 근사 이론이다. 이는 모든 계산을 수행하지 않고도 컴퓨터 프로그램의 의미론(예: 제어 흐름, 데이터 흐름)에 대한 정보를 얻는 부분적인 실행으로 볼 수 있다. 주요 구체적인 적용 분야는 정적 분석, 즉 컴퓨터 프로그램의 가능한 실행에 대한 정보를 자동으로 추출하는 것이다. 이러한 분석에는 두 가지 주요 용도가 있다. * 컴파일러 내에서 프로그램을 분석하여 특정 최적화 또는 변환이 적용 가능한지 결정 * 디버그 또는 버그 클래스에 대한 프로그램 인증 추상 해석은 1970년대 후반 프랑스 컴퓨터 과학자 부부인 파트릭 쿠소와 라디아 쿠소에 의해 형식화되었다.s2cid=207614632s2cid=1547466
# 직관
이 섹션에서는 현실 세계의 비-컴퓨팅 예시를 통해 추상 해석을 설명한다. 회의실에 있는 사람들을 생각해 보자. 미국 사회 보장 번호와 같이 방에 있는 각 사람에 대한 고유 식별자가 있다고 가정한다. 누군가가 참석하지 않았음을 증명하려면 해당 사회 보장 번호가 목록에 없는지 확인하기만 하면 된다. 두 명의 다른 사람이 같은 번호를 가질 수 없으므로 단순히 번호를 찾아봄으로써 참가자의 존재 여부를 증명하거나 반증할 수 있다. 그러나 참석자의 이름만 등록되었을 수도 있다. 만약 목록에서 사람의 이름이 발견되지 않으면, 그 사람이 참석하지 않았다고 안전하게 결론내릴 수 있지만, 만약 발견된다면 동형동음이의어의 가능성(예: 존 스미스라는 두 사람) 때문에 추가 조사 없이 확실히 결론내릴 수는 없다. 이 부정확한 정보는 실제로는 동형동음이의어가 드물기 때문에 대부분의 목적에 여전히 적절할 것이다. 그러나 엄격하게 말하면, 우리는 누군가가 방에 있었다고 확실히 말할 수 없다. 우리가 말할 수 있는 것은 그들이 여기에 있었을 수도 있다는 것뿐이다. 우리가 찾고 있는 사람이 범죄자라면 우리는 경보를 발령할 것이다. 그러나 물론 오경보를 발령할 가능성도 있다. 유사한 현상이 프로그램 분석에서도 발생할 것이다. 만약 우리가 "방에 n세인 사람이 있었는가?"와 같은 특정 정보에만 관심이 있다면, 모든 이름과 생년월일 목록을 유지할 필요는 없다. 우리는 참가자들의 나이 목록을 유지하는 것으로 안전하게 그리고 정확도 손실 없이 제한할 수 있다. 만약 이것도 처리하기에 너무 많다면, 가장 어린 사람의 나이 m과 가장 나이 많은 사람의 나이 M만 유지할 수도 있다. 질문이 m보다 엄격히 낮거나 M보다 엄격히 높은 나이에 관한 것이라면, 그러한 참가자는 참석하지 않았다고 안전하게 답변할 수 있다. 그렇지 않으면, 우리는 모른다고만 말할 수 있을 것이다. 컴퓨팅의 경우, 구체적이고 정밀한 정보는 일반적으로 유한한 시간과 메모리 내에서 계산할 수 없다(라이스의 정리 및 정지 문제 참조). 추상은 질문에 대한 일반화된 답변을 허용하는 데 사용된다(예: 예/아니오 질문에 "아마도"라고 답변하는 것은 "예 또는 아니오"를 의미하며, 이는 (추상 해석 알고리즘이) 정확한 답변을 확실하게 계산할 수 없을 때 사용된다). 이것은 문제를 단순화하여 자동 솔루션에 적합하게 만든다. 한 가지 중요한 요구 사항은 문제를 관리 가능하게 만들면서도 중요한 질문("프로그램이 충돌할 수 있는가?")에 답변하기에 충분한 정밀도를 유지할 만큼 충분한 모호성을 추가하는 것이다.
# 컴퓨터 프로그램의 추상 해석
프로그래밍 또는 명세 언어가 주어지면, 추상 해석은 추상화 관계로 연결된 여러 의미론을 제공하는 것으로 구성된다. 의미론은 프로그램의 가능한 동작에 대한 수학적 특성이다. 프로그램의 실제 실행을 매우 밀접하게 설명하는 가장 정밀한 의미론을 구체적 의미론이라고 한다. 예를 들어, 명령형 프로그래밍 언어의 구체적 의미론은 각 프로그램에 대해 생성할 수 있는 실행 추적 집합을 연관시킬 수 있다. 실행 추적은 프로그램 실행의 가능한 연속 상태의 시퀀스이며, 상태는 일반적으로 프로그램 카운터와 메모리 위치(전역 변수, 스택 및 힙)의 값으로 구성된다. 그런 다음 더 추상적인 의미론이 파생된다. 예를 들어, 실행에서 도달 가능한 상태의 집합(유한 추적의 마지막 상태를 고려하는 것과 같다)만 고려할 수 있다. 정적 분석의 목표는 어떤 시점에서 계산 가능한 의미론적 해석을 도출하는 것이다. 예를 들어, 정수 변수를 조작하는 프로그램의 상태를 변수의 실제 값을 잊고 부호(+, − 또는 0)만 유지함으로써 표현할 수 있다. 곱셈과 같은 일부 기본 연산의 경우 이러한 추상화는 정밀도를 잃지 않는다. 곱의 부호를 얻으려면 피연산자의 부호를 아는 것으로 충분하다. 다른 일부 연산의 경우 추상화는 정밀도를 잃을 수 있다. 예를 들어, 피연산자가 각각 양수와 음수인 합의 부호를 아는 것은 불가능하다. 때로는 의미론을 결정 가능하게 만들기 위해 정밀도 손실이 필요하다(라이스의 정리 및 정지 문제 참조). 일반적으로 분석의 정밀도와 결정 가능성(계산 가능성) 또는 다루기 쉬움(계산 비용) 사이에는 절충이 필요하다. 실제로 정의된 추상화는 분석하고자 하는 프로그램 속성과 대상 프로그램 집합 모두에 맞춰진다. 추상 해석을 사용한 컴퓨터 프로그램의 첫 대규모 자동화된 분석은 1996년 아리안 5호 로켓의 첫 비행을 파괴한 사고로 인해 동기가 부여되었다.access-date=3 October 2010
# 형식화
예: 정수 집합(빨간색)을 부호 집합(녹색)으로 추상화 구체적 집합이라고 불리는 순서 집합 L과 추상 집합이라고 불리는 또 다른 순서 집합 L'이 있다고 하자. 이 두 집합은 한 집합에서 다른 집합으로 요소를 매핑하는 전사 함수를 정의하여 서로 관련된다. 함수 \alpha는 구체적 집합 L의 요소 x를 추상 집합 L'의 요소 \alpha(x)로 매핑하는 경우 추상화 함수라고 불린다. 즉, L'의 요소 \alpha(x)는 L의 x의 추상화이다. 함수 \gamma는 추상 집합 L'의 요소 x'를 구체적 집합 L의 요소 \gamma(x')로 매핑하는 경우 구체화 함수라고 불린다. 즉, L의 요소 \gamma(x')는 L'의 x'의 구체화이다. L_1, L_2, L'_{1}, L'_2를 순서 집합이라고 하자. 구체적 의미론 f는 L_1에서 L_2로의 단조함수이다. L'_{1}에서 L'_2로의 함수 f'는 L'_{1}의 모든 x'에 대해 (f \circ \gamma)(x') \leq (\gamma \circ f')(x')가 성립하면 f의 유효한 추상화라고 불린다. 프로그램 의미론은 일반적으로 루프 또는 재귀 프로시저가 있을 때 고정점을 사용하여 설명된다. L이 완비 격자이고 f가 L에서 L로의 단조함수라고 가정하자. 그러면 f(x') \leq x'를 만족하는 모든 x'는 타르스키 고정점 정리에 따라 존재하는 f의 최소 고정점의 추상화이다. 이제 이러한 x'를 얻는 것이 어렵다. 만약 L'이 유한 높이를 가지거나, 적어도 사슬 조건을 만족한다면(모든 오름차순 시퀀스가 궁극적으로 정지한다면), 이러한 x'는 x'_{0} = \bot ( L'의 최소 요소)와 x'_{n+1} = f'(x'_{n})로 귀납적으로 정의된 오름차순 수열 x'_{n}의 정지 한계로 얻을 수 있다. 다른 경우에는 확장 연산자(series=Lecture Notes in Computer Science)를 통해 그러한 x'를 얻는 것이 여전히 가능하다. 이 연산자는 이진 연산자 \nabla\colon L\times L\to L로 정의되며 다음 조건을 만족한다. # 모든 x와 y에 대해 x \leq x \mathbin{\nabla} y와 y \leq x \mathbin{\nabla} y가 성립한다. # 모든 오름차순 수열 (y'_{n})_{n\geq 0}에 대해, x'_{0} := \bot와 x'_{n+1} := x'_{n} \mathbin{\nabla} y'_{n}으로 정의된 수열은 궁극적으로 정지한다. 이때 y'_{n}=f'(x'_{n})로 둘 수 있다. 어떤 경우에는 갈루아 연결 (\alpha, \gamma)를 사용하여 추상화를 정의할 수 있다. 여기서 \alpha는 L에서 L'로의 함수이고 \gamma는 L'에서 L로의 함수이다. 이는 최상의 추상화의 존재를 가정하지만, 항상 그런 것은 아니다. 예를 들어, 실수 쌍 (x, y)의 집합을 둘러싸는 볼록 다면체로 추상화한다면, x^2 + y^2 \leq 1로 정의된 원반에 대한 최적의 추상화는 없다.
# 추상 도메인의 예시

## 수치 추상 도메인
주어진 프로그램 지점에서 사용 가능한 각 변수 x에 대해 구간 [L_{x}, H_{x}]를 할당할 수 있다. 변수 x에 값 v(x)를 할당하는 상태는 모든 x에 대해 v(x) \in [L_{x}, H_{x}]인 경우 이러한 구간의 구체화가 된다. 변수 x와 y에 대한 구간 [L_{x}, H_{x}]와 [L_{y}, H_{y}]로부터 x + y(즉, [L_{x}+L_{y}, H_{x}+H_{y}])와 x - y(즉, [L_{x} - H_{y}, H_{x} - L_{y}])에 대한 구간을 쉽게 얻을 수 있다. 이들은 정확한 추상화인데, 예를 들어 x+y에 대한 가능한 결과 집합은 정확히 구간 [L_{x}+L_{y}, H_{x}+H_{y}]이기 때문이다. 곱셈, 나눗셈 등에 대한 더 복잡한 공식도 도출될 수 있으며, 이를 구간연산이라고 한다.contribution-url=https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf 이제 다음의 매우 간단한 프로그램을 고려해 보자.

y = x;
z = x - y;

{| | C 코드의 간단한 조각을 분석한다(빨간색: 런타임에 가능한 값의 구체적 집합). 합동 정보(0=짝수, 1=홀수)를 사용하면 0으로 나누기를 제외할 수 있다. (하나의 변수만 관련되므로 관계형 도메인과 비관계형 도메인 문제는 여기서 문제가 되지 않는다.)]] |} {| | 어떤 프로그램 지점에서 3개 변수의 가능한 값을 설명하는 3차원 볼록 예시 다면체. 각 변수는 0일 수 있지만, 3개 모두 동시에 0일 수는 없다. 후자의 속성은 구간 연산 도메인에서는 설명할 수 없다. |} 합리적인 산술 유형을 사용하면 z의 결과는 0이어야 한다. 그러나 x를 [0, 1]에서 시작하여 구간 산술을 수행하면 z는 [−1, +1]이 된다. 개별적으로 수행된 각 연산은 정확하게 추상화되었지만, 이들의 합성은 그렇지 않다. 문제는 명백하다. 우리는 x와 y 사이의 동등 관계를 추적하지 않았다. 실제로 이 구간 도메인은 변수들 사이의 어떠한 관계도 고려하지 않으므로 비관계형 도메인이다. 비관계형 도메인은 빠르고 구현하기 쉽지만 정밀도가 떨어진다. 관계형 수치 추상 도메인의 몇 가지 예시는 다음과 같다. * 정수에 대한 합동 관계doi=10.1080/00207168908803778year=1991 * 볼록 다면체date=January 1978 (왼쪽 그림 참조) – 높은 계산 비용이 든다. * 차이 경계 행렬arxiv=cs/0703073 * "팔각형"date=Dec 2004arxiv=cs/0703084hdl-access=free * 선형 등식s2cid=376574 그리고 이들의 조합(예: 축소곱, 오른쪽 그림 참조). 추상 도메인을 선택할 때 일반적으로 미세한 관계 유지와 높은 계산 비용 사이에서 균형을 맞춰야 한다.
## 기계어 추상 도메인
파이썬이나 하스켈과 같은 고급 언어는 기본적으로 무한대 정수를 사용하지만, C나 어셈블리어와 같은 저수준 프로그래밍 언어는 일반적으로 유한 크기의 기계어 워드에서 작동하며, 이는 2^n을 법으로 하는 정수 (여기서 n은 기계어 워드의 비트 너비)를 사용하여 더 적절하게 모델링된다. 이러한 변수들의 다양한 분석에 적합한 여러 추상 도메인이 있다. 비트필드 도메인은 기계어 워드의 각 비트를 개별적으로 처리한다. 즉, 너비 n의 워드는 n개의 추상 값 배열로 처리된다. 추상 값은 집합 \\{0,1,\bot\\}에서 가져오며, 추상화 및 구체화 함수는 다음과 같다.pages=16s2cid=13221224 \gamma(0) = \\{0\\}, \gamma(1) = \\{1\\}, \gamma(\bot) = \\{0,1\\}, \alpha(\\{0\\}) = 0, \alpha(\\{1\\}) = 1, \alpha(\\{0, 1\\}) = \bot, \alpha(\\{\\}) = \bot. 이러한 추상 값에 대한 비트 단위 연산은 일부 3치 논리의 해당 논리 연산과 동일하다.s2cid=8451238 {| | colspan="3" | |- valign="bottom" | {| class="wikitable" |+ NOT(A) ! width="25" | A ! width="25" | ¬A |- ! scope="row" 0 | 1 |- ! scope="row" | ⊥ | ⊥ |- ! scope="row" 1 | 0 |} | {| class="wikitable" |+ AND(A, B) ! rowspan="2" colspan="2" | A ∧ B ! colspan="3" | B |- ! width="25" 0 ! width="25" | ⊥ ! width="25" 1 |- ! scope="row" rowspan="3" width="25" | A ! scope="row" width="25" 0 | 0 | 0 | 0 |- ! scope="row" | ⊥ | 0 | ⊥ | ⊥ |- ! scope="row" 1 | 0 | ⊥ | 1 |} | {| class="wikitable" |+ OR(A, B) ! rowspan="2" colspan="2" | A ∨ B ! colspan="3" | B |- ! width="25" 0 ! width="25" | ⊥ ! width="25" 1 |- ! scope="row" rowspan="3" width="25" | A ! scope="row" width="25" 0 | 0 | ⊥ | 1 |- ! scope="row" | ⊥ | ⊥ | ⊥ | 1 |- ! scope="row" 1 | 1 | 1 | 1 |} |} 추가 도메인으로는 부호 있는 구간 도메인과 부호 없는 구간 도메인이 있다. 이 세 도메인 모두 덧셈, 시프트, XOR, 곱셈과 같은 일반적인 연산을 위한 전향 및 역향 추상 연산자를 지원한다. 이러한 도메인은 축소곱을 사용하여 결합할 수 있다.arxiv=2304.10768