/
Поиск
RU
ENRU

Контракты, трапы и тесты

kola различает два вида сбоев и никогда их не смешивает. Ожидаемые сбои (плохой ввод, занятый порт, короткий кадр) — это значения: Result и Option, и обрабатывает их обычный код. Нарушенное допущение самой программы (переполнение, выход индекса за границы, ложный контракт) — это трап, детерминированная остановка. Исключений нет, null нет, раскрутки стека тоже нет (так называют механизм, которым исключения C++ и паники Rust выполняют код очистки в каждой функции на пути вверх по стеку вызовов).

Result, Option и оператор ?

enum ParseErr { Short }

fn rd16_manual[r](b: &r [u8]) -> Result[u16, ParseErr] !{} {
    if b.len < 2 { return Err(ParseErr::Short); }
    Ok((widen[u16](b[0]) << 8) | widen[u16](b[1]))
}

fn parse_pair[r](b: &r [u8]) -> Result[(u16, u16), ParseErr] !{} {
    if b.len < 4 { return Err(ParseErr::Short); }
    let x = rd16_manual(b[0..2])?;
    let y = rd16_manual(b[2..4])?;
    Ok((x, y))
}

e? смотрит на Result. При Ok(v) значение выражения равно v, при Err(e) текущая функция немедленно возвращает Err(e). Поэтому ? применим только к Result и только внутри функции, которая сама возвращает Result с совместимым типом ошибки:

error[card §3]: `?` applies to Result, found `u64`
  --> q.kl:2:13
   |
 2 |     let y = x?;
   |             ^

? — это досрочный возврат, поэтому ресурс, ещё живой в точке ?, означает ошибку компиляции: на пути Err он бы потерялся (см. Ресурсы и линейность). Израсходуйте его раньше или разберите результат явным match.

Проигнорировать Result тоже нельзя. Его обрабатывают через match, ? или .unwrap() либо сознательно отбрасывают: let _ = ...;. На Option это правило не распространяется: None — это ответ, а проигнорированный Err — сбой, на который никто не посмотрел.

unwrap: сознательное «здесь этого быть не может»

.unwrap() достаёт значение из Option или Result, а на None или Err срабатывает трап. Это утверждение, записанное в коде: автор заявляет, что другой случай невозможен, и согласен на громкую остановку, если ошибся. Как и любое использование по значению, unwrap перемещает свой получатель.

test unwrap_when_proven {
    let v: Option[u64] = narrow[u64](12u64 * 5);
    // 60 всегда помещается в u64, так что None здесь невозможен
    assert v.unwrap() == 60;
}

Если невозможное всё же случится, трап укажет место:

trap: error[card §3]: unwrap on `None`
  --> u.kl:3:13
   |
 3 |     let v = o.unwrap();
   |             ^^^^^^^^^^

Для внешних данных нужны match или ?. unwrap оставьте для случаев, невозможность которых доказуема (и объясните в комментарии почему), и для тестов, где сбой как раз и есть нужный сигнал.

Что такое трап и что он завершает

Трап срабатывает при арифметическом переполнении, делении на ноль, сдвиге на ширину операнда или больше, выходе за границы, нарушении контракта или инварианта, исчерпании бюджета памяти или при явном вызове trap("msg"). Программа, чьё допущение оказалось ложным, не продолжает работу с испорченными данными на руках.

trap: error[card §3]: explicit trap: n out of range
  --> t.kl:3:16
   |
 3 |     if n > 2 { trap("n out of range"); }
   |                ^^^^^^^^^^^^^^^^^^^^^^

То, что останавливается, называется доменом отказа; по умолчанию это весь процесс. Операционная система затем забирает всё, что держал процесс, например его файловые дескрипторы (небольшие целые числа, которыми ОС обозначает открытые файлы и сокеты). Это корректно, потому что линейность обещала расходование ресурсов только на нормальных путях. Под kola test трап проваливает лишь свой тест, и тот печатает FAILED (seed N). Программа может и сама сузить домен отказа.

domain и recover

Напомним: регион — это блок со своим пулом памяти (ареной); всё, что в нём выделено, освобождается разом на закрывающей скобке. domain d { … } recover(t: Trap) { … } — это регион, который ещё и перехватывает трапы. Это регион в полном смысле главы Память: регионы и ссылки, с теми же правилами выхода ссылок и тем же from m. Именно поэтому перехват здесь корректен: снос арены и есть очистка, а раскрутки, которую можно прервать на полпути, просто нет.

use std::log;

// Обработчик запроса, домен отказа которого — один запрос, а не процесс.
pub fn serve(payload: &[u8]) -> u32 !{log} {
    let mut status: u32 = 200u32;
    domain d {
        // намеренная ошибка: вызывающий может прислать меньше байтов, чем здесь читается
        let b = payload[7];
        status = widen[u32](b);
    } recover(t: Trap) {
        status = 500u32;
        log::error(f"request died: {t.kind} at {t.site}");
    }
    status
}

test a_trap_kills_the_request_not_the_process {
    assert serve(&b"short") == 500u32;    // домен перехватил трап
    assert serve(&b"long enough.") == 111u32;
    // а процесс жив и выполняет эту строку
}

Под kola test --sim, который печатает журнал и прошедших тестов, первый вызов пишет:

log[error] request died: Bounds at serve.kl:8

Правила:

  • recover обязателен и выполняется только при трапе. return или break покидают блок, как обычный регион, и его не запускают.

  • Trap — простые данные. t.kind имеет тип TrapKind: Bounds, Arith, Req, Ens, Inv, Assert, Unwrap, Explicit, Budget или Capacity. Budget означает, что кончился бюджет памяти; Capacity — что достигнута фиксированная граница, например в Pool заняты все слоты. В первом случае нужно сбрасывать нагрузку, во втором — отказать именно этому элементу. t.site — строка вида module:line, например serve.kl:8, и никогда не путь в файловой системе машины, на которой шла сборка.

  • Трап внутри recover фатален. Его не перехватит ни один домен, даже внешний.

  • Линейный ресурс не может жить внутри домена (маркеры полномочия вроде Clock — исключение): трап оставил бы его без хозяина, а деструкторов нет. Домены вычисляют над данными.

error[card §3]: `m`: a linear resource may not live inside a `domain` — a trap would strand it
  --> dom.kl:3:9
   |
 3 |         let m: Mem = sys.mem.split(1024);
   |         ^^^
   = help: domains compute over data; move this resource outside the domain, or consume it before entering

Контракты: req и ens

Контракт — это проверяемое условие, записанное в сигнатуру. req — предусловие, обязанность вызывающего: «вызывай меня только так». ens — постусловие, обещание функции о результате, который в нём называется ret. Каждое ключевое слово принимает список условий через запятую:

fn sum_range(xs: &[u64], a: usize, b: usize) -> u64 !{}
    req a <= b, b <= xs.len
{
    let mut s: u64 = 0;
    let mut i = a;
    while i < b {
        s = s +% xs[i];
        i = i + 1;
    }
    s
}

fn clamp100(x: u64) -> u64 !{}
    ens ret <= 100
{
    if x > 100 { 100 } else { x }
}

Контракт соблюдается всегда. Если компилятор может его доказать, проверка исчезает из сгенерированного кода; если нет, остаётся проверка времени выполнения с трапом. Режима сборки, который отключает контракты, нет, и в этом их отличие от assert в C или debug_assert в Rust. Нарушенный req выглядит так:

trap: error[card §8]: req violated calling `sum_range`
  --> rq.kl:2:17
   |
 2 |     req a <= b, b <= xs.len
   |                 ^^^^^^^^^^^
   = help: contracts are always enforced: proven statically or trapped at runtime

Индексация xs[i] и срез xs[a..b] несут встроенные контракты req на границы, так что выход за границы — ещё один нарушенный контракт. Проверка выше по коду (if i < xs.len) снимает его статически. В sum_range условие цикла i < b вместе с req b <= xs.len доказывает i < xs.len, и в скомпилированном цикле проверки границ нет. В компиляторе есть небольшой прувер — компонент, который пытается по самому коду показать, что условие никогда не бывает ложным. Здесь работает именно доказательство, а не эвристика (см. Под капотом).

report checks: что осталось на время выполнения

«Доказано или трап» полезно, только если видно, что именно получилось. kola report checks перечисляет каждое обязательство в файле и то, чем оно закрыто. Вот отчёт для двух функций выше:

$ kola report checks contracts.kl
fn sum_range
  proven   xs[i]  [proved i < xs.len from req+guards]
  proven   i + 1usize  [sum bounded by width]
fn clamp100
  proven   ens at tail  [ens discharged at this exit]

1 index site(s): 1 proven at compile time, 0 runtime
1 arith site(s): 1 proven at compile time, 0 runtime
1 ens exit(s): 1 proven at compile time, 0 runtime

(Заголовок и две заключительные строки настоящего вывода здесь опущены.) Теперь уберите строку req и спросите снова. Программа по-прежнему работает и по-прежнему безопасна по памяти, но доказательства больше нет, и проверка границ выполняется на каждой итерации:

$ kola report checks unguarded.kl
fn sum_range_weak
  RUNTIME  xs[i]
  proven   i + 1usize  [sum bounded by width]

1 index site(s): 0 proven at compile time, 1 runtime
1 arith site(s): 1 proven at compile time, 0 runtime

Так и работают с горячими путями: усиливают req и добавляют проверки, пока в столбце runtime не окажется 0. Тогда проверок границ в сгенерированном коде нет вовсе, потому что компилятор доказал, что они никогда не сработают. Так ускоряют путь данных в ядре или внутренний цикл шифра: не отключая проверки, а заслуживая их удаление.

assert и почему он должен быть повторяемым

assert EXPR; — проверяемое утверждение посреди кода с тем же правилом, что и у контракта: доказано и удалено либо проверяется с трапом. Инварианты resource struct (inv) разобраны в главе Ресурсы и линейность.

Правило, на котором спотыкаются: выражение ничего не должно изменять. Сначала свяжите результат с именем: let ok = q.push(1); assert ok;. Это похоже на правило об эффектах, но им не является, и диагностика прямо об этом говорит:

error[card §8]: assert expression mutates state (calls `bump`, which writes through `g.level`)
  --> as.kl:5:5
   |
 5 |     assert bump(&mut v);
   |     ^^^^^^
   = help: `mutates` is not the effect row's sense — a write through a `&mut` param is effect-PURE (§6) and this rule still refuses it. A PROVEN assert is ELIDED, so its expression must be repeatable and must mean the same thing in the build where it never runs. Bind first — let ok = x.f(); assert ok;

С точки зрения ряда эффектов запись через параметр &mut чиста: вызывающий видит её в сигнатуре (см. Эффекты и капабилити). Но assert, закрытый прувером, удаляется, и изменяющий assert сделал бы смысл программы зависимым от того, сколько сумел доказать прувер. Правило смотрит на то, что делает тело вызываемой функции, а не на то, как объявлены её параметры.

untrusted: контракт не может зависеть от байтов атакующего

req превращается в трап, поэтому req, который атакующий может нарушить, — это удалённый выключатель. Возьмём декодер пакетов с req packet.len >= 32, где packet — полезная нагрузка UDP. Специально собранная 20-байтовая датаграмма нарушает контракт, срабатывает трап, и в freestanding-сборке (программе, работающей без операционной системы, например на пути пакетов маршрутизатора) один пакет останавливает весь маршрутизатор ещё до всякой аутентификации.

req — это утверждение о вызывающем, а у байтов из сети вызывающего нет. Пометьте такой параметр как untrusted, и чекер обеспечит это различие сам:

// Пакет из сети. Это не компилируется.
pub fn decap(untrusted packet: &[u8]) -> Option[u64] !{}
    req packet.len >= 32
{
    Some(widen[u64](packet[0]))
}
error[card §8]: `req` depends on untrusted input `packet`
  --> un.kl:2:9
   |
 2 |     req packet.len >= 32
   |         ^^^^^^^^^^^^^^^^
   = help: this `req` depends on untrusted input `packet`; return `Result`/`Option` and check at runtime, or remove the `untrusted` marker if this param is not attacker-controlled
// Исправление: проверить длину во время выполнения и ответить значением.
pub fn decap(untrusted packet: &[u8]) -> Option[u64] !{} {
    if packet.len < 32 { return None; }
    Some(widen[u64](packet[0]))
}

test a_short_packet_is_refused_not_fatal {
    assert decap(&b"too short").is_none();
}

Исправление ничего не ослабляет: длина по-прежнему проверяется до чтения первого байта, только функция отвечает значением, а не убивает процесс. untrusted стоит в одном ряду с Secret[T] и ct (см. Константное время): всё это способы kola указать, насколько данным можно доверять. Для кода, который ещё не размечен, kola report tainted-reqs перечисляет каждый req, ограничивающий разделяемый срез или массив. Это список для разбора, а не приговор: по одному типу компилятор не отличит входящий пакет от вашего собственного исходящего буфера.

Тесты

enum ParseErr { Short }

fn rd16_manual(b: &[u8]) -> Result[u16, ParseErr] !{} {
    if b.len < 2 { return Err(ParseErr::Short); }
    Ok((widen[u16](b[0]) << 8) | widen[u16](b[1]))
}

test parse_short_frame {
    region r {
        let b = alloc in r [1u8];
        assert rd16_manual(b) == Err(ParseErr::Short);
    }
}

// капабилити с зерном: sim.rng, sim.clock, sim.fs, ...
test seeded_rng(mut sim: Sim) {
    let a = sim.rng.weak_u64();
    let b = sim.rng.weak_u64();
    assert a != b;
}

Тесты живут рядом с кодом и запускаются командой kola test file.kl (каталог обходится рекурсивно). --test <substring> выбирает тесты по имени; подстрока, которой ничего не соответствует, — ошибка со списком имеющихся имён. Тест, которому нужны капабилити, объявляет (mut sim: Sim) и получает набор с зерном и теми же полями, что у Sys: виртуальные часы, детерминированный источник случайности, симулированную файловую систему. Упавший тест печатает своё зерно, и --seed N в точности воспроизводит сбой. Вместо этого тест может объявить (mut sys: Sys): тогда он «живой», с настоящими сокетами и настоящими часами, и только sys.rng по-прежнему идёт от зерна.

--sim добавляет внедрение сбоев и отчёт о пиковом потреблении памяти каждым регионом:

$ kola test --interp --sim --seed 7 tests.kl
tests.kl: test parse_short_frame ... ok
    region r: 1 bytes region-charged high-water (arena-faithful)
tests.kl: test seeded_rng ... ok

2 passed, 0 failed (interpreted, JIT backend)

Выполнить программу kola можно двумя способами. Интерпретатор исполняет исходный код напрямую и служит эталоном того, что программа означает. C-бэкенд переводит программу на C и компилирует её компилятором C — так собирается то, что вы поставляете. По умолчанию kola test прогоняет каждый тест обоими способами, сравнивает результаты по файлам и завершается с кодом 3, если они расходятся. --interp запускает только интерпретатор и не требует компилятора C: это быстрый цикл во время работы. --native запускает только C-сборку, каждый тест в отдельном процессе.

Тест без единого assert проходит независимо от того, выполнилось ли что-нибудь, поэтому kola check о нём предупреждает; если всё утверждение сводится к «трап не срабатывает», напишите expects 0. В общем случае test name expects N { … } требует, чтобы выполнилось ровно N утверждений (включая те, что в вызываемых функциях), и проверка, пропущенная из-за пустого ввода, делает тест красным:

test three_claims expects 3 {
    let xs = [1u64, 2u64, 3u64];
    assert xs[0] == 1;
    assert xs[1] == 2;
    assert xs.len == 3;
}

Нормативный источник — SPEC-CARD §3, §8 и §10 (kola help spec-card).