Polonius의 핵심인 Loan 분석을 소개하고, 입력 관계, origin 간 부분집합 전파, origin 내 loan 전파, liveness를 이용한 불법 접근 오류 및 placeholder 간 부분집합 오류를 계산하는 방법을 설명합니다. 또한 Naive, LocationInsensitive, Opt, Hybrid 변형의 개념과 용도를 개괄합니다.
Loan 분석은 borrow checker의 핵심이며 다음을 계산합니다:
이는 성능, 가독성, 테스트 및 검증 등 서로 다른 목표를 가진 여러 변형으로 수행됩니다.
대략적으로, 분석의 목표는 1) loan을 추적하는 것입니다:
subset 관계를 통해 origin에서 origin으로 흐름그리고 2) 선언되지 않은 placeholder origin 사이의 관계를 추적하는 것입니다.
live 상태의 loan이 무효화되면 불법 접근 오류가 되며, placeholder가 예기치 않게 다른 placeholder로 흘러들어가면 불법 부분집합 관계 오류가 됩니다.
입력 관계는 아래에서 설명하지만, 전용 페이지에서 더 많은 정보를 볼 수 있습니다.
// Indicates that the `loan` was "issued" at the given `point`, creating a
// reference with the `origin`. Effectively, `origin` may refer to data from
// `loan` starting at `point` (this is usually the point *after* a borrow rvalue).
.decl loan_issued_at(Origin:origin, Loan:loan, Point:point)
.input loan_issued_at
// When some prefix of the path borrowed at `loan` is assigned at `point`.
// Indicates that the path borrowed by the `loan` has changed in some way that the
// loan no longer needs to be tracked. (In particular, mutations to the path that
// was borrowed no longer invalidate the loan)
.decl loan_killed_at(Loan:loan, Point:point)
.input loan_killed_at
// Indicates that the `loan` is invalidated by some action
// taking place at `point`; if any origin that references this loan is live,
// this is an error.
.decl loan_invalidated_at(Loan:loan, Point:point)
.input loan_invalidated_at
// When we require `origin1@point: origin2@point`.
// Indicates that `origin1 <= origin2` -- i.e., the set of loans in `origin1`
// are a subset of those in `origin2`.
.decl subset_base(Origin1:origin, Origin2:origin, Point:point)
.input subset_base
// Describes a placeholder `origin`, with its associated placeholder `loan`.
.decl placeholder(Origin:origin, Loan:loan)
.input placeholder
// These reflect the `'a: 'b` relations that are either declared by the user on
// function declarations or which are inferred via implied bounds.
// For example: `fn foo<'a, 'b: 'a, 'c>(x: &'c &'a u32)` would have two entries:
// - one for the user-supplied subset `'b: 'a`
// - and one for the `'a: 'c` implied bound from the `x` parameter,
// (note that the transitive relation `'b: 'c` is not necessarily included
// explicitly, but rather inferred by polonius).
.decl known_placeholder_subset(Origin1:origin, Origin2:origin)
.input known_placeholder_subset
아래의 datalog 규칙은 부분집합 관계의 전체 추이 폐쇄를 계산하므로 "naive" 구현으로 간주되지만, 설명하고 이해하기 쉽습니다. 이는 Naive 변형에서 datafrog 엔진을 사용해 구현되어 있습니다.
구현과의 사소한 차이점이 있습니다:
; 대안 연산자의 사용아래 규칙은 origin 사이의 부분집합 완전 그래프를 계산합니다. 비추이적 부분집합에서 시작하여, CFG의 주어진 지점에서 이 관계에 대한 폐쇄를 수행합니다(활성 여부에 관계없이). 그런 다음 liveness를 고려하여 CFG를 따라 이러한 추이적 부분집합을 전파합니다. 즉, 어떤 지점에서 한 origin이 다른 origin으로 흐르고, 두 origin이 모두 후속 지점에서 live라면(참고: placeholder origin은 모든 지점에서 live로 간주됨) 그 관계를 후속 지점으로 전파합니다.
.decl subset(Origin1:origin, Origin2:origin, Point:point)
// R1: the initial subsets are the non-transitive `subset_base` static input
subset(Origin1, Origin2, Point) :-
subset_base(Origin1, Origin2, Point).
// R2: compute the subset transitive closure, at a given point
subset(Origin1, Origin3, Point) :-
subset(Origin1, Origin2, Point),
subset(Origin2, Origin3, Point).
// R3: propagate subsets along the CFG, according to liveness
subset(Origin1, Origin2, TargetPoint) :-
subset(Origin1, Origin2, SourcePoint),
cfg_edge(SourcePoint, TargetPoint),
(origin_live_on_entry(Origin1, TargetPoint); placeholder(Origin1, _)),
(origin_live_on_entry(Origin2, TargetPoint); placeholder(Origin2, _)).
아래 규칙은 CFG의 주어진 지점에서 어떤 origin이 어떤 loan을 포함하는지를 계산합니다. "발급 시점과 origin"에서 시작하여, loan은 위에서 계산한 부분집합을 통해 CFG의 해당 지점에서 전파됩니다. 그런 다음 liveness를 고려하여 CFG를 따라 이러한 loan을 전파합니다. 즉, 어떤 지점에서 loan이 어떤 origin에 포함되어 있고, 그 origin이 후속 지점에서 live라면 loan을 후속 지점으로 전파합니다. 여기에는 미묘한 점이 있는데, CFG에는 loan이 kill될 수 있는 지점이 있으며, 그 지점에서 전파가 중단됩니다. 규칙 6은 liveness와 kill 지점을 모두 사용하여 loan을 CFG에서 더 전파할지 여부를 결정합니다.
.decl origin_contains_loan_on_entry(Origin:origin, Loan:loan, Point:point)
// R4: the issuing origins are the ones initially containing loans
origin_contains_loan_on_entry(Origin, Loan, Point) :-
loan_issued_at(Origin, Loan, Point).
// R5: propagate loans within origins, at a given point, according to subsets
origin_contains_loan_on_entry(Origin2, Loan, Point) :-
origin_contains_loan_on_entry(Origin1, Loan, Point),
subset(Origin1, Origin2, Point).
// R6: propagate loans along the CFG, according to liveness
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
!loan_killed_at(Loan, SourcePoint),
cfg_edge(SourcePoint, TargetPoint),
(origin_live_on_entry(Origin, TargetPoint); placeholder(Origin, _)).
위에서 계산한 정보를 이용해 불법 접근 오류를 계산할 수 있습니다. 특정 지점에서 live한 loan을 무효화하는 것은 오류입니다. 어떤 지점에서 loan이 live하다는 것은, 그 지점에서 live한 origin에 그 loan이 포함되어 있다는 뜻입니다.
.decl loan_live_at(Loan:loan, Point:point)
// R7: compute whether a loan is live at a given point, i.e. whether it is
// contained in a live origin at this point
loan_live_at(Loan, Point) :-
origin_contains_loan_on_entry(Origin, Loan, Point),
(origin_live_on_entry(Origin, Point); placeholder(Origin, _)).
.decl errors(Loan:loan, Point:point)
// R8: compute illegal access errors, i.e. an invalidation of a live loan
errors(Loan, Point) :-
loan_invalidated_at(Loan, Point),
loan_live_at(Loan, Point).
이 오류는 변형에 따라 다르게 계산될 수 있지만, 목표는 동일합니다. 분석이 어떤 placeholder origin이 궁극적으로 다른 placeholder origin으로 흘러들어간다고 감지하면, 그 관계는 선언되어 있어야 하며, 그렇지 않으면 오류입니다.
Naive 규칙 변형은 완전한 부분집합 추이 폐쇄를 계산하므로, 이 사실이 두 placeholder origin을 연결하는지 더 쉽게 감지할 수 있습니다. LocationInsensitive 규칙 변형은 전혀 추이적 부분집합을 계산하지 않고, loan 전파를 사용해 이러한 오류를 감지합니다(placeholder loan이 placeholder origin으로 흘러드는 경우). Opt 최적화 규칙 변형은 liveness와 잠재적 오류 기여도에 따라 일부 origin의 추이 폐쇄만 계산하고(주로 엣지를 따라 소멸하는 origin들과 그들이 도달할 수 있는 origin), placeholder의 추이적 부분집합을 명시적으로 추적합니다.
.decl subset_errors(Origin1:origin, Origin2:origin, Point:point)
// R9: compute illegal subset relations errors, i.e. the undeclared subsets
// between two placeholder origins.
subset_errors(Origin1, Origin2, Point) :-
subset(Origin1, Origin2, Point),
placeholder_origin(Origin1),
placeholder_origin(Origin2),
!known_placeholder_subset(Origin1, Origin2).
위 규칙은 Polonius 모델이 계산하는 모든 중요한 부분을 개념적으로 단순하게 설명하는 Naive 변형의 loan 분석을 문서화합니다. 이 변형은 명료함을 위해 규칙이 엄밀히 필요한 것보다 더 많은 것을 계산한다는 점에서 "naive"입니다. 특히 모든 origin의 완전한 추이적 부분집합과 CFG의 모든 지점에서 각 origin이 포함한 loan을 계산합니다.
실제 사용에서는, 서로 다른 정밀도와 계산 복잡도 요구사항을 갖는 여러 "등급"의 borrow-checking이 유용할 수 있습니다. 그중 가장 낮은 등급인 LocationInsensitive 변형은 부분집합이 발생하는 위치와 CFG 지점에서의 origin 내용 둘 다를 무시하여 정밀도를 성능과 맞바꿉니다. 아이디어는 다음과 같습니다: 경로 및 흐름 민감도를 무시했을 때도 오류가 없다면, 전체 분석에서도 오류가 없을 것이다. 반대로 잠재적 오류를 찾는다면, 전체 분석은 이러한 위치 비민감 오류의 부분집합을 찾게 된다.
이는 빠른 사전 패스로 사용할 수 있습니다. 오류가 없다면 비싼 전체 분석을 수행할 필요가 없고, 그렇지 않다면 잠재적 오류가 발생한 loan만 완전히 검사하여 오탐을 제거하면 됩니다.
입력은 Naive 변형과 같지만, subset에서 CFG 지점을 무시합니다. 부분집합은 추적하지 않고, origin_contains_loan에서 origin 내부의 loan 전파를 근사하는 데 사용됩니다(liveness와 위치 민감도를 무시).
.decl subset(Origin1:origin, Origin2:origin)
// R1: the subsets are the non-transitive `subset_base` static input,
// with their location stripped.
subset(Origin1, Origin2) :-
subset_base(Origin1, Origin2, _).
.decl origin_contains_loan(Origin:origin, Loan:loan)
// R2: the issuing origins are the ones initially containing loans.
origin_contains_loan(Origin, Loan) :-
loan_issued_at(Origin, Loan, _).
// R3: the placeholder origins also contain their placeholder loan.
origin_contains_loan(Origin, Loan) :-
placeholder_loan(Origin, Loan).
// R4: propagate the loans from the origins to their subsets.
origin_contains_loan(Origin2, Loan) :-
origin_contains_loan(Origin1, Loan),
subset(Origin1, Origin2).
.decl loan_live_at(Loan:loan, Point:point)
// R5a: Approximate loan liveness. If an origin is live at a given
// point, and it contains a loan *anywhere* in the CFG, that loan is
// considered live at that point.
loan_live_at(Loan, Point) :-
origin_contains_loan(Origin, Loan),
(origin_live_on_entry(Origin, Point); placeholder_origin(Origin)).
.decl potential_errors(Loan:loan, Point:point)
// R5b: Compute potential illegal access errors, i.e. invalidations
// of live loans.
potential_errors(Loan, Point) :-
loan_invalidated_at(Loan, Point),
loan_live_at(Loan, Point).
참고: 위의 "5a"와 "5b" 규칙 이름은 구현과 맞추기 위한 것으로, 구현에서는 loan_live_at 중간 관계를 물질화하지 않고 단일 "규칙 5"로 potential_errors를 계산합니다.
불법 부분집합 관계 오류(정의상 "부분집합"에 관한 오류)는 placeholder loan을 전파하고, 그것이 예기치 않게 다른 placeholder origin으로 흘러드는 경우(두 placeholder 사이의 특정 관계가 선언되어 있지 않은 경우)를 감지함으로써 여전히 계산할 수 있습니다.
.decl potential_subset_errors(Origin1:origin, Origin2:origin)
// R6: compute potential illegal subset relations errors, i.e. the
// placeholder loans which ultimately flowed into another placeholder
// origin unexpectedly.
potential_subset_errors(Origin1, Origin2) :-
placeholder(Origin1, Loan1),
placeholder(Origin2, _),
origin_contains_loan(Origin2, Loan1),
!placeholder_known_to_contain(Origin2, Loan1).
이를 위해 known_placeholder_subset의 추이 폐쇄에 해당하는 간단한 입력이 필요하며, 대신 주어진 placeholder origin이 포함하는 것으로 알려진 placeholder loan을 추적합니다. 계산은 다음과 같습니다:
.decl placeholder_known_to_contain(Origin:origin, Loan:loan)
placeholder_known_to_contain(Origin, Loan) :-
placeholder(Origin, Loan).
placeholder_known_to_contain(Origin2, Loan1) :-
placeholder_known_to_contain(Origin1, Loan1),
known_placeholder_subset(Origin1, Origin2).
현재 구현에서는 이 빠른 LocationInsensitive 필터를 또 다른 최적화 변형의 사전 패스로 사용하며, 이는 Hybrid 알고리즘의 일부입니다.
이 Opt 변형의 규칙에 대한 더 자세한 설명은 추후 추가될 예정이지만, 위에서 설명한 Naive 변형과 동일한 데이터를 더 효율적으로 계산합니다. 즉, 부분집합 추이 폐쇄를 계산하는 위치를 제한합니다. 일부 origin은 수명이 짧거나, 어떤 loan도 결코 흘러들지 않는 부분집합 그래프의 하위 구간에 속하므로, 오류나 loan 전파에 기여하지 않습니다. 이러한 특정 경우를 추적할 필요는 없습니다.
그동안에는, 구현이 계산에 사용하는 관계와 규칙을 문서화하고 있습니다.