Никто не знает, работает ли оно или нет. У разработчиков нет этого оборудования (его трудно найти, нового нет). Правки в код этих систем не вносили уже 5 лет. Люди, ответственные за поддержку этого кода самоустранились (потеряли интерес, сменили работу, и т.д.).
Код останется в прошлых версиях ядер и будет поддерживаться в LTS релизах.
2. Любой новый код по идее вообще никак не должен влиять на старый.
В ядре сильно влияет. Внешние интерфейсы сохраняют совместимость, внутренний API — нет.
Хочу на всякий случай отметить, что разовые запуски анализатора не являются правильным способом его применения. Нерегулярные ненастроенные прогоны неэффективны.
Абсолютно с вами согласен. К сожалению, собственными силами в свободное время для всего ядра linux этого не осилить, поэтому мой комментарий имеет смысл только для тех, кто хочет за вечер запустить и что-то посмотреть.
Во-вторых, многие ошибки найдены и исправлены к этому моменту более дорогими способами.
$ git log --pretty=format:'%h %aN %ad %gs' --no-merges --grep 'PVS-Studio'
7c6082b903ac Oleh Kravchenko Wed Oct 16 10:24:30 2019 +0300 leds: mlxreg: Fix possible buffer overflow
4016ba85880b Oleh Kravchenko Wed Sep 4 00:18:19 2019 +0300 led: triggers: Fix dereferencing of null pointer
6a258f7d0fbd Colin Ian King Sat Apr 8 00:22:03 2017 +0100 ubifs: Fix cut and paste erroron sb type comparisons
6eeabd8b2b8a Colin Ian King Fri Apr 14 15:25:40 2017 +0100 staging: media: atomisp: fix range checking on clk_num
e56efe9322c5 Colin Ian King Sat Apr 8 18:09:59 2017 +0100 lockd: remove redundant check on block
7ecaeaffd72a Colin Ian King Sat Apr 8 18:28:42 2017 +0100 scsi: aic7xxx: fix order of arguments in function prototype
eea422709fd8 Colin Ian King Fri Apr 14 14:58:02 2017 +0100 scsi: fc: remove redundant check of an unsigned long being less than zero
ba508685d90f Colin Ian King Sat Apr 8 00:44:03 2017 +0100 staging: wilc1000: fix incorrect strncasecmp length
5bf1f439c89d Denis Efremov Fri Oct 25 15:53:25 2013 +0400 xfs:xfs_dir2_node.c: pointer use before check for null
Ядра регулярно анализируется Coverity (https://scan.coverity.com/projects/linux), Klever/LDV (http://linuxtesting.org/results/ldv). К тому же есть специальные инструменты для анализа кода ядра типа sparse, smatch, куча правил для coccinelle. Скоро будет добавлен удобный запуск Clang-Tidy (https://lkml.org/lkml/2020/7/24/1079). Но всё это меркнет, по сравнению с динамическим syzkaller и количеством реальных и пока не исправленных багов, выявленных им (https://syzkaller.appspot.com/upstream).
Анализируя /usb/bin/, вы не увидите системных инструкций. Их надо искать в ядре, в несжатом образе. Если вы сидите не на gentoo, собираемой gcc+graphite или clang+polly с какими-нибудь флагами -march=native -Ofast -ftree-vectorize и т.д. с последним процессором, так там и не будет ничего. Потому что дистрибутивы собирают программы с тем, чтобы они работали на как можно большем количестве процессоров. И лишь в очень небольшом количестве программ есть runtime определение доступных процессорных команд. И скорее всего там они ассемблером закодированы, а не компилятором порождаются. Вообще, мне кажется что надежнее грепом пройтись по исходникам компилятора, а не в бинарниках смотреть.
В подходе «давайте сделаем программу по тем же принципам, на которых математики создают уравнение» нет ничего нового.
Посмотреть, как сегодня выглядят на практике идеи «безошибочного кода» на примере доказательств функций на языке Си можно, например, в книжке ACSL By Example либо у меня в github репозитории verker. Там доказывается корректность реализаций библиотечных функций ядра Linux, их соответствие формальным спецификациям на языке ACSL. Там же можно скачать виртуальную машину с установленными инструментами и попробовать что-то самостоятельно.
Никто не знает, работает ли оно или нет. У разработчиков нет этого оборудования (его трудно найти, нового нет). Правки в код этих систем не вносили уже 5 лет. Люди, ответственные за поддержку этого кода самоустранились (потеряли интерес, сменили работу, и т.д.).
Код останется в прошлых версиях ядер и будет поддерживаться в LTS релизах.
2. Любой новый код по идее вообще никак не должен влиять на старый.
В ядре сильно влияет. Внешние интерфейсы сохраняют совместимость, внутренний API — нет.
Абсолютно с вами согласен. К сожалению, собственными силами в свободное время для всего ядра linux этого не осилить, поэтому мой комментарий имеет смысл только для тех, кто хочет за вечер запустить и что-то посмотреть.
Более того, я заметил что другие анализаторы и компиляторы берут к себе диагностики, которые ранее я только у вас видел. Лично написал простой шаблон для для coccinelle (он, конечно, дал очень много ложных срабатыванию, но мне так было проще) по образу вашей диагностики и исправил несколько реальных багов (
drm/radeon: fix fb_div check in ni_init_smc_spll_table(), staging: rtl8188eu: fix HighestRate check in odm_ARFBRefresh_8188E())
$ git log --pretty=format:'%h %aN %ad %gs' --no-merges --grep 'PVS-Studio'
7c6082b903ac Oleh Kravchenko Wed Oct 16 10:24:30 2019 +0300 leds: mlxreg: Fix possible buffer overflow
4016ba85880b Oleh Kravchenko Wed Sep 4 00:18:19 2019 +0300 led: triggers: Fix dereferencing of null pointer
6a258f7d0fbd Colin Ian King Sat Apr 8 00:22:03 2017 +0100 ubifs: Fix cut and paste erroron sb type comparisons
6eeabd8b2b8a Colin Ian King Fri Apr 14 15:25:40 2017 +0100 staging: media: atomisp: fix range checking on clk_num
e56efe9322c5 Colin Ian King Sat Apr 8 18:09:59 2017 +0100 lockd: remove redundant check on block
7ecaeaffd72a Colin Ian King Sat Apr 8 18:28:42 2017 +0100 scsi: aic7xxx: fix order of arguments in function prototype
eea422709fd8 Colin Ian King Fri Apr 14 14:58:02 2017 +0100 scsi: fc: remove redundant check of an unsigned long being less than zero
ba508685d90f Colin Ian King Sat Apr 8 00:44:03 2017 +0100 staging: wilc1000: fix incorrect strncasecmp length
5bf1f439c89d Denis Efremov Fri Oct 25 15:53:25 2013 +0400 xfs:xfs_dir2_node.c: pointer use before check for null
Ядра регулярно анализируется Coverity (https://scan.coverity.com/projects/linux), Klever/LDV (http://linuxtesting.org/results/ldv). К тому же есть специальные инструменты для анализа кода ядра типа sparse, smatch, куча правил для coccinelle. Скоро будет добавлен удобный запуск Clang-Tidy (https://lkml.org/lkml/2020/7/24/1079). Но всё это меркнет, по сравнению с динамическим syzkaller и количеством реальных и пока не исправленных багов, выявленных им (https://syzkaller.appspot.com/upstream).
Посмотреть, как сегодня выглядят на практике идеи «безошибочного кода» на примере доказательств функций на языке Си можно, например, в книжке ACSL By Example либо у меня в github репозитории verker. Там доказывается корректность реализаций библиотечных функций ядра Linux, их соответствие формальным спецификациям на языке ACSL. Там же можно скачать виртуальную машину с установленными инструментами и попробовать что-то самостоятельно.