From: Sergey Matveev <stargrave@stargrave.org>
Date: Mon, 9 Jan 2023 17:40:30 +0000 (+0300)
Subject: Тестирование корректности работы компилятора
X-Git-Url: http://www.git.stargrave.org/?a=commitdiff_plain;h=017b42e5b34d936e606298542b203e30890e8ad1;p=stargrave-blog.git

Тестирование корректности работы компилятора

https://bronevichok.ru/posts/highload-2022.html
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106523
В докладе упоминается баг в GNU GCC:

    unsigned char f7 (unsigned char x, unsigned int y)
    { return (x << y) | (x >> ((-y) & 7)) }

где программа будет по разному отрабатывать. Бага до сих пор не закрыта.

А вообще для меня там всё магией является (до подобного не дорос, не
факт что дорасту когда-либо), хотя про технологии и инструменты слышал.
Чтобы понять не сломала ли оптимизация компилятора чего, то берётся
получающийся на этапе JIT-а IR-код, преобразуется в SMT-формулу, затем
подаётся в SMT-решатель, который оценивает идентичны ли результаты до и
после оптимизации.
---