Постусловие о длине, прошедшее сетку, всё ещё может быть ложным — ловит фаззинг напечатанного кода

Утверждение «переворот строки сохраняет длину» ядро приняло на сетке: ни один из примеров функции его не нарушил. Фаззинг напечатанного JavaScript нашёл контрпример за секунды. Длина в flang считается в кодовых точках, а переворот идёт по кодовым точкам — и если во входе есть непарный суррогат, два непарных при перевороте могут встать в порядок правильной пары и слиться в одну кодовую точку (длина падает), а правильная пара — разойтись на два непарных (длина растёт). Ни равен, ни не больше, ни не меньше не держатся.

Отсюда правило того же класса, что «минус ноль»: любое утверждение о длине строки проверяется фаззингом на строках с суррогатами до попадания в библиотеку. Сетка примеров этот класс входов не порождает — литералов с непарным суррогатом в примерах никто не пишет.

Чем подтверждено. Ветка work/biblioteka, коммит «Запросы и ответы: 17 постусловий там, где их не было ни одного». Модуль напечатан в JavaScript (flang emit --target js) и прогнан на 4000 случайных строк длиной 0…12 из алфавита с астральным символом и переводами строк: у «Перевернуть» 5 нарушений из 4000, у остальных семи утверждений о длине («Обрезать края», «Обрезать слева», «Обрезать справа», «Закодировать проценты», «Раскодировать проценты», «Плюсы в пробелы», «Путь цели», «Строка запроса цели») — 0 из 4000. На тех же 4000 строках, порождённых только правильными кодовыми точками, у «Перевернуть» тоже 0 — то есть ломает именно непарный суррогат, а не астральный символ.

Чем ограничено. Способ работает только там, где модуль печатается в язык, на котором есть чем фаззить. Он ничего не говорит о функциях, у которых длина результата не выражается через длину входа.

Связано: minus-zero-is-a-class, claims-about-length-are-two-thirds-of-what-the-kernel-refuses