Утечки регионов: отчёт, бюджет и чего отчёт не видит
Регион освобождает свою память на закрывающей скобке, и ни мгновением раньше. В этом и состоит вся модель памяти из главы Память: регионы и ссылки, и у неё есть один способ отказа. За каждым регионом стоит арена: блок памяти, который выдаёт место под выделения одно за другим и не умеет вернуть отдельный кусок. Поэтому если цикл на каждом проходе выделяет память в регионе, открытом не в теле цикла, все эти выделения доживают до закрытия внешнего региона. Программа растёт всё время, пока живёт регион.
Это не теоретическая ошибка. HTTP-сервер на kola стартовал с 2 МБ резидентной памяти (RSS — память, которую ОС действительно отобразила для процесса) и после 573 000 запросов дошёл до 799 МБ: буферы каждого запроса выделялись в регионе соединения, а он живёт столько же, сколько соединение. При этом код всё время оставался безопасным по памяти: каждая ссылка указывала на живую память правильного типа. Проблема была в размещении, а не в безопасности.
Форму такой ошибки kola видит, не запуская программу. Каждое выделение называет свой регион (alloc in r, эффект !{alloc(r)}), а верифицированное промежуточное представление компилятора (IR, внутренняя форма, с которой работает прувер) сохраняет структуру циклов. kola report leaks FILE.kl обходит этот IR и перечисляет подозрительные места.
Отчёт
Вот та же ошибка в нескольких строках: обработчик соединения, регион r которого принадлежит соединению, и по буферу на каждый запрос.
// `hello` живёт в регионе соединения `r`, и все буферы запросов тоже.
fn serve[r](hello: &r [u8], n: u64) -> usize !{alloc(r)} {
let mut total: usize = 0;
for i in 0..n {
let buf: &r mut Vec[u8] = alloc in r mut Vec::new();
buf.push(hello[0]);
total = total + buf.len;
}
total
}
test serves_every_request {
region conn {
let hello = alloc in conn [7u8, 8u8];
assert serve(hello, 3) == 3;
}
}Тест проходит, kola check молчит. Ни одно правило, за которым следит чекер, здесь не нарушено: r принадлежит вызывающему, поэтому каждый буфер жив и каждая ссылка &r действительна всё время, пока ею пользуются. Отчёт об утечках задаёт другой вопрос:
$ kola report leaks serve.kl
kola report leaks — candidate region-leak sites inside loops
(a preamble explaining each class, and the rule that a site count must be
read together with the DE-ANALYZED list)
fn serve
fresh Vec::new [the fn's own region (bound before this loop)] — repair: open a per-iteration region: `region rq { .. }`
not analyzed `test serves_every_request`: test items run on the interpreter — any allocation inside it (loop or not) is invisible to this report
1 candidate leak site(s): 1 fresh, 0 grow, 0 mintКаждая находка называет функцию, класс (здесь fresh), место в том виде, в каком его видит компилятор, причину подозрения (регион был привязан до этого цикла) и исправление. Помнить о запуске отчёта не обязательно: если есть что посмотреть, kola test сам напечатает подсказку.
$ kola test --interp serve.kl
serve.kl: test serves_every_request ... ok
1 passed, 0 failed (interpreted, JIT backend)
note: 1 candidate region-leak site(s) inside loops — run `kola report leaks serve.kl` (see `kola help ai`)Исправление
Откройте регион внутри цикла и выделяйте память в нём. Он освобождается в конце каждого прохода, а именно такое время жизни буферу и было нужно:
// Тот же цикл, исправленный: буфер живёт в регионе, открытом внутри цикла.
fn serve[r](hello: &r [u8], n: u64) -> usize !{alloc(r)} {
let mut total: usize = 0;
for i in 0..n {
region rq {
let buf: &rq mut Vec[u8] = alloc in rq mut Vec::new();
buf.push(hello[0]);
total = total + buf.len;
}
}
total
}
test serves_every_request {
region conn {
let hello = alloc in conn [7u8, 8u8];
assert serve(hello, 3) == 3;
}
}0 candidate leak site(s): 0 fresh, 0 grow, 0 mintСигнатура, вызывающий код, тест и результат не изменились. Вся правка — в том, где лежат байты. В языке с регионами ошибка роста памяти — это ошибка размещения, а размещение локально и видно на ревью.
Регион на каждую итерацию исправляет класс fresh, но не все классы. Отчёт печатает исправление, подходящее к найденному: например, сбрасывать растущий буфер или дать каждому рекурсивному вызову собственный регион. Поэтому читайте строку отчёта, а не применяйте везде один и тот же приём.
Четыре формы
Класс | Что означает | Насколько вероятна настоящая утечка |
|---|---|---|
| на каждой итерации создаётся новое значение: выделение в цикле или вызов функции, которая выделяет память и возвращает значение | почти наверняка |
|
| стоит посмотреть |
| интерполированная строка ( | почти наверняка |
рекурсия | функция в цикле вызовов, которая выделяет память в регионе, открытом не ею: цикл без цикла в исходном коде | почти наверняка |
Строка f"...", переданная прямо в параметр типа &str, собирается во временном буфере и ничего не выделяет, поэтому log::info(f"req={i}") в цикле в отчёт не попадает. А привязанная к переменной попадает: let s: &r str = f"req={i}"; внутри цикла — место класса mint.
fresh, в том числе через вызов
В примере выше alloc стоял прямо в теле цикла, и его можно было найти чтением. У HTTP-сервера ошибка выглядела иначе: в его цикле не было ни одного выделения, они были во вспомогательных функциях. Отчёт следует за вызовами:
fn enc_msg[r](conn: &r [u8], n: u64) -> &r Vec[u8] !{alloc(r)} {
let v: &r mut Vec[u8] = alloc in r mut Vec::new();
v.push(wrap[u8](n));
v
}
fn push64le[r](out: &r mut Vec[u8], v: u64) !{alloc(r)} {
for i in 0..8u64 {
out.push(wrap[u8](v >> (i * 8)));
}
}
// собственных `alloc` здесь нет
fn frames[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
let mut total: usize = 0;
for i in 0..n {
let msg = enc_msg(conn, i);
total = total + msg.len;
}
total
}
fn stream[r](sink: &r mut Vec[u8], n: u64) -> usize !{alloc(r)} {
for i in 0..n {
push64le(sink, i);
}
sink.len
}
test both expects 2 {
region r {
let conn = alloc in r [0u8; 4];
assert frames(conn, 3) == 3;
let s: &r mut Vec[u8] = alloc in r mut Vec::new();
let n = stream(s, 2);
assert n == 16;
}
}fn frames
fresh enc_msg(conn, i) [the fn's own region (bound before this loop) via call to `enc_msg`] — repair: open a per-iteration region: `region rq { .. }`
fn stream
grow push64le(sink, i) [the fn's own region (bound before this loop) via call to `push64le`] — repair: open a per-iteration region: `region rq { .. }`
2 candidate leak site(s): 1 fresh, 1 grow, 0 mintОбе вызываемые функции классифицированы по сигнатурам, тела отчёт не читает. enc_msg возвращает значение в регионе, значит, каждый вызов создаёт что-то новое: fresh. push64le принимает Vec и может его удлинить: grow. (stream сначала привязывает результат к переменной и только потом проверяет его, потому что выражение в assert не может вызывать то, что пишет через &mut.)
grow, класс потише
Накапливать данные в одном буфере — часто именно то, чего код и добивается, поэтому этот класс скорее вопрос, чем обвинение. Помечается прямой .push в Vec, который функция сама выделила во внешнем регионе, если нигде в цикле на этом дескрипторе нет .clear() или .truncate(). Добавьте сброс, и отчёт замолчит:
// `grow`: Vec, выделенный этой функцией в регионе соединения, растёт на каждом проходе.
fn collect[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
let acc: &r mut Vec[u8] = alloc in r mut Vec::new();
for i in 0..n {
acc.push(conn[0]);
}
acc.len
}
// Та же форма со сбросом того же дескриптора: ёмкость используется повторно,
// и отчёт молчит.
fn batched[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
let acc: &r mut Vec[u8] = alloc in r mut Vec::new();
let mut total: usize = 0;
for i in 0..n {
acc.push(conn[0]);
total = total + acc.len;
acc.clear();
}
total
}
test both_count_the_same expects 2 {
region r {
let conn = alloc in r [1u8];
let a = collect(conn, 4);
let b = batched(conn, 4);
assert a == 4;
assert b == 4;
}
}fn collect
grow acc.push(conn[0usize] [checked]) [grows a handle bound before this loop, never cleared/truncated] — repair: reset the handle each pass (`.clear()`/`.truncate()`) or bound its size
1 candidate leak site(s): 0 fresh, 1 grow, 0 mintbatched не просто не помечена, она корректна. clear() обнуляет длину и сохраняет ёмкость, то есть место, которое Vec уже зарезервировал, поэтому повторное заполнение ничего не стоит региону. Тот же учёт показывает отчёт о пике потребления kola test --sim, описанный в главе о памяти. Если функция возвращает заполненный Vec, значение уходит вместе с результатом, и такое место тоже не помечается.
рекурсия
В рекурсивном обходе отчёту нечего найти по части циклов, а память он накапливает так же быстро. Поэтому отчёт сообщает о функции в цикле вызовов, которая выделяет память в регионе, открытом не ею, в том же блоке, где делает рекурсивный вызов:
// Рекурсия — это цикл без узла цикла.
fn scan[r](depth: u64, out: &r mut Vec[u8]) !{alloc(r)} {
if depth == 0 {
return;
}
let scratch: &r mut Vec[u8] = alloc in r mut Vec::new();
scratch.push(1u8);
out.push(2u8);
scan(depth - 1, out);
}
test scan_walks {
region r {
let out: &r mut Vec[u8] = alloc in r mut Vec::new();
scan(3, out);
assert out.len == 3;
}
}fn scan
fresh Vec::new [recursion cycle through `scan` — allocates into a region it did not open] — repair: give each call its OWN region (`region rq { .. }`) or return the value
1 candidate leak site(s): 1 fresh, 0 grow, 0 mintПравило намеренно осторожное. Рекурсивный построитель дерева, например парсер, чьи узлы уходят в возвращаемое синтаксическое дерево, выделяет память в регионе вызывающего сознательно и не помечается, потому что значение покидает функцию. Не помечается и region rq { .. } на каждый вызов. Остаётся черновая память, которую заполнили, бросили и рекурсивно прошли дальше: настоящее накопление.
Чего отчёт не видит
Обход идёт по верифицированному IR, а попадает туда не каждая функция. У некоторых конструкций пока нет представления в IR; одна из них — блок domain, и функция, которая его использует, остаётся вне анализа. Молча такая функция никогда не выпадает: она перечисляется с указанием причины, и этот список — часть результата.
Функция, вызывающая непроанализированную, тоже лишается анализа. Отчёт называет её de-analysed (снятой с анализа), а итоговая строка не позволяет нулю выглядеть чистым результатом:
use std::trap;
// Из-за блока `domain` эта функция не попадает в верифицированный IR.
fn guarded[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
let mut total: usize = 0;
for i in 0..n {
let buf: &r mut Vec[u8] = alloc in r mut Vec::new();
buf.push(conn[0]);
domain d {
total = total + buf.len;
} recover(t: Trap) {
total = 0;
}
}
total
}
fn serve[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
guarded(conn, n)
}$ kola report leaks dom.kl
...
de-analyzed `guarded`: `domain`/`recover` has no KIR lowering, so the prover cannot see inside it — ... — its leak sites are UNCHECKED (a reachable body left the IR-v0 subset); NOT counted below
de-analyzed `serve`: call to `guarded` which is outside IR-v0 — its leak sites are UNCHECKED (a reachable body left the IR-v0 subset); NOT counted below
0 candidate leak site(s): 0 fresh, 0 grow, 0 mint — ⛔ 2 fn(s) DE-ANALYZED, their leak sites UNCHECKED, so this count is NOT a clean bill of healthВ guarded та же утечка, что в первом примере, а счётчик равен нулю. Отчёт не ошибается: он говорит, что функцию никто не проверял. Ноль рядом с непустым списком снятых с анализа или непроанализированных функций означает «ничего не проверено», а не «ничего не найдено». Если сборка зависит от этого отчёта, проверяйте счётчик и список снятых с анализа вместе.
Остальные ограничения:
Если пропущена
fn main, отчёт сообщает об этом на видном месте. Циклы приёма и обслуживания соединений у сервера обычно живут вmain, и отчёт, который её не видит, слеп ровно там, где этот класс ошибок причиняет больше всего вреда.Элементы
testвсегда числятся непроанализированными. Они выполняются в интерпретаторе, и выделения внутри них здесь не видны.Находка
growназывает регион, видимый в месте вызова. Это эвристика: как только появился дескрипторVec, IR уже не помнит, из какого региона пришла его память..pushв буфер, переданный параметром, не помечается никогда. Дописывать в буфер вызывающего — обычная работа любого кодировщика, а ложные тревоги приучили бы рецензентов пролистывать вывод инструмента.
Машиночитаемая форма
--format json (или --json) печатает тот же обход для скрипта или агента. Текст и JSON получаются из одного обхода, поэтому расходиться не могут.
$ kola report leaks --format json grow.kl
{"file":"grow.kl","report":"leaks","main_unchecked":null,
"fns":[{"fn":"collect","sites":[{"class":"grow","site":"acc.push(conn[0usize] [checked])",
"why":"grows a handle bound before this loop, never cleared/truncated",
"repair":"reset the handle each pass (`.clear()`/`.truncate()`) or bound its size"}]}],
"syntactic":[],"de_analyzed":[],
"not_analyzed":[{"name":"test both_count_the_same","why":"test items run on the interpreter"}],
"totals":{"fresh":0,"grow":1,"syntactic_loop_alloc":0,"syntactic_aliased_region":0,"mint":0}}Читайте de_analyzed и not_analyzed раньше totals. Скрипт, который смотрит только на итоги, воспроизводит в точности то ложное «всё чисто», против которого отчёт и работает.
Закрепляем: бюджет [leaks] в kola.pack
Отчёт запускают, а бюджет валит сборку. Пакет включает его, добавив в свой kola.pack секцию [leaks] (см. Пакеты). После этого kola audit прогоняет тот же анализ по исходникам самого пакета, предварительно дав пруверу полностью снять проверки границ, и завершается с кодом 1 при любом неподтверждённом месте. На большом пакете полное снятие проверок может занять минуты, и аудит предупреждает об этом при старте. Без секции [leaks] строки об утечках носят справочный характер и сборку не валят.
Проверяйте каталог пакета, а не отдельный файл. kola audit <file> печатает те же строки для замыкания этого файла, но сообщает, что бюджет не применялся: бюджет — утверждение о пакете целиком.
[pack]
name = "leakdemo"
version = "0.1.0"
src = "src"
[caps]
allowed = []
[leaks]
acknowledged = []Положите первую функцию serve из этой главы в src/lib.kl, и аудит откажет, выдав точный ключ, который нужно вставить:
$ kola audit leakdemo
audit: leaks — proving 1 file(s) under full prover discharge ...
audit: caps within budget — pack `leakdemo` (used=[] ⊆ allowed=[])
...
error[pack leaks budget]: 1 candidate leak site(s) not in [leaks] acknowledged — review EACH (acking a site never covers a new one): fix the code, open a per-iteration region (`region rq { .. }`), or copy the exact key(s) into [leaks] acknowledged: {"serve::fresh::Vec::new"}
audit: FAILED (1 violation(s)) — see the `error[...]` line(s) above; `kola audit` exits 1Законных путей дальше два, и аудиту всё равно, какой вы выберете: исправить код или осознанно принять это место.
[leaks]
acknowledged = ["serve::fresh::Vec::new"]
not_analyzed_pct_cap = 0$ kola audit leakdemo
...
audit: leaks within budget (1 fresh, 0 grow acknowledged, 0/1 own non-`test` item(s) not analyzed = 0.0%, cap 0%) — computed under full prover discharge
audit ok: 0 violation(s) — every budget checked in this run is within its declared limitsКлюч — это место, а не функция
Ключ подтверждения имеет вид fn::class::text и обозначает одно конкретное место. Подтверждённое место никогда не покрывает новое в той же функции, а любое изменение кода меняет ключ. Переименуйте serve в handle, и ревью откроется снова:
audit: leaks — 1 acknowledged key(s) match NO candidate site: {"serve::fresh::Vec::new"}. Either those sites were FIXED (remove the keys — ...) or their fn LEFT THE ANALYSIS, which is why the de-analyzed count is worth reading beside this: 0 fn(s) de-analyzed here
error[pack leaks budget]: 1 candidate leak site(s) not in [leaks] acknowledged — ...: {"handle::fresh::Vec::new"}Пометки прувера внутри текста места (например, [checked] в примере с grow выше) перед сравнением отбрасываются. Они могут измениться, когда прувер научится лучше справляться с какой-то посторонней проверкой границ, а подтверждение должно переживать то, что компилятор поумнел, и не переживать изменение кода.
Функция вне анализа, в которой есть цикл и эффект alloc, — ровно то место, где может спрятаться утечка, поэтому аудит просит подтвердить и её по имени, ключом вида "leakdemo::lib::guarded::unchecked-loop". Такой ключ устаревает (и об этом сообщается) в тот день, когда функция становится доступной для анализа.
not_analyzed_pct_cap: граница слепой зоны
Второй ключ ограничивает, какая часть библиотеки может оставаться вне анализа: процент собственных элементов пакета, кроме test, которых нет в верифицированном IR. Он нужен для того, чтобы покрытие могло уменьшиться только намеренно. Это доля, поэтому пакет может расти, не задевая предела, пока покрытие сохраняется. Старый ключ с абсолютным числом, not_analyzed_cap, отвергается с объяснением.
Это число ограничивает слепоту анализатора, а не указывает на то, что надо исправить. Рядом с ним аудит печатает разбивку по классам. param-type и return-type означают сигнатуру, которую IR пока не умеет выразить: это обычный код, а не долг. body означает функцию, тело которой вышло за анализируемое подмножество, и вот там утечка спрятаться может. Элементы test считаются отдельно и в предел никогда не входят, чтобы новые тесты не мешали уложиться в бюджет.
Закреплять число нужно правильно. Пакет без секции [leaks] считается быстрым структурным проходом, пакет с ней — при полном снятии проверок прувером, и проценты могут различаться. Чтобы ввести предел, добавьте секцию [leaks] без него, запустите kola audit и закрепите число, которое напечатает этот прогон. Строку для вставки аудит напечатает сам.
Вердикт не может пережить своё покрытие
Пакет может нести бюджет [leaks], проходить аудит и печатать audit ok, хотя ни одна из функций, попавших в верифицированный IR, вообще не выделяет память. Такой бюджет никогда не сработает, но на ревью выглядит как защита, поэтому аудит его отвергает:
error[pack leaks budget]: pack `leakdemo` declares a [leaks] budget, and NOT ONE of the 1 fn(s) that reached the verified IR ALLOCATES, so no region leak this pack could contain is reachable by the analysis and the budget cannot fire (1 further fn(s) are outside the IR-v0 subset). A budget that cannot fire is worse than none: it reads as protection on a review surface. Repair: bring at least one ALLOCATING fn into the IR-v0 subset (`kola report leaks <file>` names why each is outside it), or delete the [leaks] section so the pack claims what is true — nothingОба исправления законны. Пакет, который не выделяет память в анализируемом коде, должен сообщать об этом отсутствием бюджета утечек, а не бюджетом, который зелёный по причине, которую никто не проверял.
Что покрывает бюджет
Собственные исходники пакета, его библиотечный код. Элементы
testвыводятся отдельной строкой и в предел никогда не входят.Не примеры. Для
examples/*.klв выводе аудита есть своя подписанная разбивка: о них сообщается, но бюджетом они не ограничиваются, так же как раздельны[caps]и[caps.examples].Не зависимости. Бюджет каждого пакета применяется к его собственным файлам. Бюджет зависимости проверяется, когда аудит проходит она сама, и к числам импортирующего пакета никогда не прибавляется.