형식 안전 모델 #

SafeC의 안전 보장은 지향적인 목표가 아닙니다 — 이는 구문적 타입 안전성(progress + preservation)을 갖춘 타입 시스템으로 형식화되어 있으며, Oxide(Weiss 외)와 Cyclone(Grossman 외)의 선행 연구를 기반으로 합니다.

일곱 가지 안전 속성 #

1. 공간 안전성 #

범위를 벗어난 메모리 접근이 없습니다. 배열 첨자는 상수 인덱스의 경우 컴파일 타임에, 동적 인덱스의 경우 런타임에 경계 검사됩니다.

int arr[4];
arr[5] = 1;        // 컴파일 타임 오류: index 5 out of bounds for array of size 4

int i = get_index();
arr[i] = 1;        // 런타임 경계 검사가 삽입됨 (위반 시 abort)

런타임 경계 검사는 unsafe {} 블록 안에서 억제될 수 있습니다.

2. 시간 안전성 #

use-after-free가 없습니다: 리전 표기는 참조의 라이프타임을 할당 스코프에 묶습니다. 스택 메모리에 대한 참조는 함수를 벗어날 수 없고, arena에 대한 참조는 arena_reset<R>()/arena_destroy<R>()/arena_free_to<R>()에 의해 무효화되며, &heap T 참조는 std::dealloc()에 의해 무효화됩니다 — 이 세 가지 모두 단순히 런타임뿐 아니라 컴파일 타임에도 검사됩니다.

&stack int get_local() {
    int x = 42;
    return &x;      // 컴파일 타임 오류: stack reference escapes function
}

#include <std/mem.h>

void heap_example() {
    &heap int p = new int;
    std::dealloc(p);
    *p = 1;              // 컴파일 타임 오류: use of 'p' (&heap reference) after std::dealloc() freed it
    std::dealloc(p);      // 컴파일 타임 오류: double-free, same check
}

3. 별칭 안전성 #

가변 참조는 배타적입니다. 대여 검사기는 프로그램의 어느 시점에서든 값이 하나의 가변 참조를 갖거나 임의 개수의 불변 참조를 가질 수 있지만, 결코 둘 다는 가질 수 없도록 강제합니다.

int x = 10;
&stack int a = &x;          // 가변 대여
&stack const int b = &x;    // error: cannot borrow 'x' as immutable: already borrowed as mutable

const &stack int b는 &stack const int b와 같은 타입입니다. const는 리전 한정자의 앞과 뒤 어느 쪽에 써도 됩니다.

4. 리전 이스케이프 안전성 #

참조는 자신이 가리키는 리전보다 오래 살아남을 수 없습니다. 컴파일러는 리전 스코프 깊이를 추적하며, 참조를 더 얕은 스코프로 옮기는 할당이나 반환을 거부합니다.

region R { capacity: 1024 }
&arena<R> int outer_ptr;

void demo() {
    &arena<R> int p = new<R> int;
    outer_ptr = p;   // error: cannot assign '&arena<R> int' to variable in
                     //        outer scope: arena reference would escape
}

5. 데이터 레이스 자유 #

모든 타입은 구조에서 유도되는 Send 및/또는 Sync입니다(unsafe impl Send; / impl !Send;로 덮어쓸 수 있음). spawn은 스레드가 공유해도 되는 정적 데이터만 받고, spawn_scoped는 join될 때까지 지역 변수를 빌려주며, thread_spawn과 채널은 Send 값을 이동시키고, Mutex<T>는 가드를 통해서만 값에 닿습니다 — 따라서 안전한 코드는 동기화 없이 스레드 사이에 가변 상태를 공유할 수 없습니다. 스레드 안전성을 참고하세요.

6. Null 안전성 #

참조는 기본적으로 non-null입니다. 안전한 SafeC 코드에는 null 참조가 없습니다. Nullable 참조는 ?&T 구문을 사용합니다; 흐름 민감적인 null 좁히기(narrowing)를 가진 언어들과 달리, 단순한 != null 비교만으로는 이후의 역참조가 안전해지지 않습니다 — nullable 참조를 읽는 것은 오직 match, .is_null(), .default(fallback), 또는 명시적인 unsafe 블록을 통해서만 허용됩니다(안전성 참고).

7. 결정론 #

숨겨진 런타임 비용이 없습니다. SafeC는 가비지 컬렉션도, 참조 카운팅도, 암묵적 힙 할당도 삽입하지 않습니다. 모든 할당은 소스 코드에 명시적입니다. 성능 모델은 투명합니다 — 작성한 것이 곧 실행되는 것입니다.

C, C++, Rust, Zig와의 메모리 안전성 비교 #

비교에는 동일한 다섯 언어에 걸친 한 줄짜리 "메모리 안전성: Yes/No" 요약이 있습니다; 이 섹션은 그 단일 행을 위 속성들로 세분화합니다. "yes"와 "no"는 각 언어가 언제(컴파일 타임 vs. 런타임 vs. 전혀 하지 않음) 그리고 얼마나 완전하게(모든 안전 모드 프로그램 vs. 옵트인 빌드 모드 vs. 아무것도 없음) 검사하는지의 실제 차이를 가리기 때문입니다.

핵심 요지: C와 C++는 이들 대부분을 전혀 검사하지 않습니다(정의되지 않은 동작이 대부분의 시간 동안 "검사된" 상태입니다). Zig는 이들 중 여럿을 검사하지만, 빌드 모드 선택으로서 그렇게 합니다 — 같은 소스가 검사를 갖거나 갖지 않으며, 줄 단위가 아니라 바이너리 전체에 대해 한 번 결정됩니다. Rust와 SafeC는 둘 다 기본적으로 컴파일 타임에 검사하며, 특정 코드 블록에 대해 검사를 끄려면 명시적이고 어휘적으로 스코프가 지정된 옵트아웃(unsafe {})이 필요합니다 — 이것이 바로 이 페이지 자신의 unsafe 탈출구 섹션이 설명하는 속성입니다. Rust와 SafeC가 다른 지점은 시간 안전성을 어떻게 증명하는가(소유권/대여 vs. 리전 소속 — 그 트레이드오프에 대한 자세한 내용은 Rust와 비교 참고)와 그 증명이 얼마나 완전한가입니다: Rust의 대여 검사기는 자신이 받아들이는 패턴에 대해 건전하고 완전한 정적 증명입니다(유효한 프로그램을 거부할 수는 있지만, 결코 안전하지 않은 프로그램을 받아들이지 않습니다); SafeC의 리전 및 수명 검사는 명시된 신뢰 경계(함수 포인터를 통한 호출과 본문이 없는 extern 함수 호출, unsafe {} 안에서 원시 포인터로 도달한 메모리) 안에서 건전하지만, 몇 가지 유효한 형태(서로 반대되는 조건으로 보호된 해제와 사용, 연결 구조를 노드 단위로 해제하는 루프 — 시간 안전성 참고)는 여전히 거부할 수 있으며, 더 단순하고 더 C 호환적인 사고 모델을 위해 일부 정밀함을 희생합니다.

안전 분석 단계 #

컴파일러는 의미 분석 중 일련의 분석 패스를 통해 이러한 속성들을 강제합니다:

모든 검사는 컴파일 타임에 실행됩니다. 유일한 런타임 삽입은 동적 배열·슬라이스 인덱스에 대한 경계·범위 검사이며, 이는 생성된 IR에서 눈에 보입니다.

unsafe 탈출구 #

모든 안전 검사는 unsafe {} 블록 안에서 지역적으로 억제될 수 있습니다:

unsafe {
    int* raw = (int*)some_addr;
    *raw = 42;       // no bounds check, no borrow check, no region check
}

unsafe는 어휘적으로 스코프가 지정됩니다. 호출된 함수로 전파되지 않습니다. 수동 감사가 필요한 코드를 위한 검색 가능한(grep-able) 마커 역할을 합니다.

FFI 경계 규칙 #

외부 함수 호출(C 상호운용)은 특정 안전 규칙을 따릅니다:

• extern 선언은 원시 C 타입을 사용합니다 — 리전 한정자 없음
• &static T에서 T*로의 강제 변환은 unsafe {} 없이 안전합니다
• &T/?&T(리전 한정자가 전혀 없는, "outliving reference" — 메모리와 리전 참고)도 양방향으로 T*/void*와의 강제 변환이 unsafe {} 없이 안전합니다 — 호출이 반환된 이후에도 C 쪽에서 보유할 수 있는 포인터를 위한 타입입니다
• 정적이지 않고 리전이 없지도 않은 참조를 C에 전달하려면 unsafe {}가 필요합니다
• C로부터 받은 원시 포인터는 &T/?&T 타입 변수로 직접 받는 경우가 아니라면 unsafe {} 안에서 처리해야 합니다

이러한 규칙들은 안전한 SafeC 코드와 안전하지 않은 C 코드 사이의 경계가 항상 명시적임을 보장합니다.

형식적 토대 #

안전 모델은 확립된 타입 이론에 기반합니다:

• Oxide(Weiss 외, 2019) — place와 provenance를 가진 타입 있는 계산법으로서 Rust의 소유권과 대여를 형식화
• Cyclone(Grossman 외, 2002) — C와 비슷한 언어를 위한 정적 안전 보장을 갖춘 리전 기반 메모리 관리

SafeC는 이러한 형식주의들을 리전을 주요 메모리 안전 메커니즘으로 삼는 C 호환 언어에 맞게 조정합니다.

Progress와 Preservation #

타입 시스템은 표준적인 구문적 안전성 속성을 만족합니다:

• Progress: 타입이 올바른 프로그램은 값이거나, 한 단계를 진행할 수 있거나, 승인된 런타임 오류(abort를 동반한 경계 검사 실패)입니다
• Preservation: 타입이 올바른 프로그램이 한 단계를 진행하면, 결과 프로그램도 타입이 올바릅니다

이 두 속성이 함께, 타입이 올바른 SafeC 프로그램이 unsafe {} 블록 밖에서는 정의되지 않은 동작을 보이지 않음을 보장합니다.