>> Анализ кода. Как правило с целью найти потенциальные ошибки в коде. Или
>> даже не потенциальные, а самые натуральные ошибки.
> Опять задам парочку уточняющих вопросов, ибо не ясно, что значит "анализ кода",
> "потенциальные или натуральные ошибки", а за "ошибки" мы не раз обсуждалиif(a = b) {
бла-бла-бла
}
Это есть потенциальная ошибка. С точки зрения статического анализатора. Он не знает задумку программиста, он не знает, хотел ли программист сравнить a и b (и написать a == b), или он хотел выполнить присвоение, а полученное значение в a использовать как булевское значение.
Это, судя по интернетам, довольно распространённая ошибка в C, вызванная опечаткой. Но, я повторю, статический анализатор, не знает, ошибка ли это или нет. Я это назвал "потенциальной" ошибкой.
Что же касается "натуральной" ошибки -- я может неудачно слово подобрал, но я "натуральный" использовал в том контексте противопоставляя "потенциальной", наверное, лучше было бы назвать её "актуальной"?
И вот тебе пример, заодно к вопросам про проверки индексов на выход за границы внутри цикла:
Сначала без ошибки, но с лишней проверкой:
for(i = 0; i < arr.len(); i ++) {
if(i < arr.len()) {
sum += arr[i];
}
}
Проверка лишняя, это математически доказуемо, и оптимизаторы эту проверку легко устраняют. Статический же оптимизатор может кинуть варнинг о том, что проверка лишняя. Зачем он будет так делать -- это другой вопрос, отдельный большой и длинный.
Теперь с не лишней проверкой:
for(i = 0; i < arr.len() * 2; i ++) {
if(i < arr.len()) {
sum += arr[i];
}
}
Тут уже не удастся доказать, что проверка лишняя, то есть что устранение этой проверки не изменит результат выполнения кода. Более того, если мы проверку устраним, то статический анализатор сможет доказать, что i выходит за границу arr.len() и кинуть нам варнинг. Но это сработает, только если компилятор представляет себе инварианты массивов. Язык C не представляет: для него массив это просто указатель, ты можешь объявлять переменную как int arr[5], но C потом с радостью позволит тебе индексировать arr числом больше пяти или отрицательным числом. Даже если в коде будет написано arr[-1000], компилятор C не увидит в этом ничего странного. Но статический анализатор может возбудиться от такого. И если он сможет доказать, что индекс достигает 5 и превосходит его, он тоже может возбудиться.
> - это очень широкое понятие, что конкретно принимается за ошибку (то
> есть нужно определить это множество ошибок)?
Естественно это очень широкое понятие, и именно поэтому мы не будем его определять. Всё что ты в разговоре можешь назвать ошибкой, и всё что может быть детектировано как ошибка посредством разглядывания кода и размышлений -- это всё потенциальная цель поиска для статического анализатора.
Хотя, быть может, синтаксические ошибки стоит из этого списка выкинуть, статический анализатор всё ж заточен на работу с "синтаксически корректными" программами, которые компилируются.
>> Внешний по отношению к
>> компилятору статический анализатор может выискивать больше подозрительных мест.
> Только если он будет следовать каким-то заранее заданным шаблонам (паттернам логических
> ошибок), ибо не существует анализатора который бы разрешил бы проблему останова,
> так как это проблема банальный логический парадокс. Если человеческая логика впадает
> в ступор перед логическими парадоксами, думаете анализатор с ними справится (можно
> на это не отвечать)?
Я не видел ни одного статического анализатора, который бы обещал выполнять роль серебряной пули и находить вообще все проблемы. Теоретически мы можем нафантазировать такой, но практически таких нет. Они все решают вполне конкретные задачи, и да, наверное, посредством сопоставления с образцом... Не, не всё можно. И вообще можно зайти и с другой стороны. Можно объявлять инварианты -- логические утверждения, которые должны сохранять истинность на протяжении выполнения программы. Скажем, что индекс в массиве >=0 и меньше длины этого массива. А дальше статический анализатор ищет все индексации массивов, и пытается доказать это утверждение про индекс. Иногда он доказывает его, и всё ок. Иногда он опровергает его, и это можно рассматривать как ошибку. Иногда он не может ни доказать, ни опровергнуть -- тут можно вести себя по разному, можно выкидывать варнинг, ибо нехрен писать код, про который невозможно доказать инварианты.
> Выше описал это, ток в данном контексте надо отделать понятия профайлинга (Анализ
> кода с точки зрения оптимальности алгоритма)
Весь профайлинг, с которым мне приходилось сталкиваться был динамическим. Но если ты настаиваешь, давай разделять профайлинг на динамический и статический. Динамический требует запуска программы для измерения времени, мы не об этом говорим совершенно.
> Тут просто мне не ясно, как "статически" произвести профайлинг (без выполнения
> программы), то есть как оценить оптимальность без исполнения, и сравнения результата
> с ожидаемым?
Я не знаю, как оценить "оптимальность", я не понимаю, что ты имеешь в виду. А вот как провести профайлинг -- это, например, в случае ассемблера, можно попытаться делать так: берёшь мануал к процессору, выковыриваешь оттуда информацию о том, сколько времени занимает выполнение той или иной инструкции, после чего разбиваешь программу на линейные куски без ветвления, считаешь время для каждого куска, а потом начинаешь анализировать ориентированный граф ветвления, высчитывая сколько раз какая итерация цикла выполнится.
Этот последний этап будет, надо полагать, довольно сложным, но если позволить анализатору выводить асимптотическое время, в виде формулы с параметром, то я думаю можно. Другое дело, что формулы могут получиться слишком громоздкими для анализа глазами. Но их потом можно попытаться анализировать при помощи софтины, которая будет искать самые тормоза и пытаться угадать бутылочные горлышки.
> Смотрите, что такое тип ? - область (диапазон) допустимых значений, из примера
> выше переменная i имеет тип целочисленного значения (не важно пока со
> [...]
> находится в области допустимых целочисленных значений без знака. Но если мы
> обращаемся по индексу, который больше размера (длины) массива, то происходит аварийный
> останов, из-за выхода за границы массива.
Нет. Это зависит от языка. C не выполняет никаких аварийных остановов из-за такой мелочи, как выход за границы массива.
> когда размер (длина) массива заранее не известна, статический анализатор скажет (без
> исполнения), мол тут выход за границы массива?
Во-первых, длина может быть известна -- это зависит от языка. Во-вторых, если она не известна, то статический анализатор может исходить из самой общей идеи: неограниченные значения индекса -- это потенциальная ошибка. А здесь он не сможет наложить на значения индекса никаких ограничений, кроме ограничений типа.
> А выход из цикла
> разве не будет если допустим что аварийного останова нет и после
> переполнения инта он становится обратно в 0,
Он становится в INT_MIN, который при четырёхбайтовом инте равен -2^31. А это значит переполнение буфера вниз. Плюс, кстати, это переполнение целого, что в случае C есть UB.
> то по условию это уже освобожденный файловый дескриптор и выполниться exit().
Не, во-первых, про освобождёные фд анализатор будет знать только если ему каким-то образом сообщили про инварианты. Если не сообщили, он вообще никаких допущений о содержимом fds делать не может. Во-вторых, в цикле не зануляются значения fds. Они остаются прежними. Их можно назвать "dangling file descriptors". Повторный проход по массиву повторно вызовет все close.
> А не легче сильно статически это определять? Вспомним язык паскаль, и мнение
> Кернигана о нем (Почему Паскаль не является моим любимым языком программирования).
> Помните, мы обсуждали строки сишные и паскалевы их плюсы и минусы,
> тоже самое и с анализаторами Вывод мой таков, статический анализатор применим
> в основном в сильно статических (система типов) ЯП, а для "динамических"
> - динамический анализатор. Не вижу смысла статическим анализатором пытаться анализировать
> код динамического ЯП.
Да, динамический сложнее анализировать. Но потенциально можно извлечь больше, если анализировать не только функции отдельно, и забывать этот анализ, переходя к другой функции, а строить общую блоксхему выполнения программы, и отслеживать какая функция откуда вызывается, какого типа аргументы туда передаются, и соответственно _доказать_, что например в локальной переменной a функции foo может быть только четырёхбайтовое целочисленное значение, потому что a заполняется из аргумента arg1 строчкой a = arg1 + 3; а все вызовы функции foo кладут в arg1 целочисленное значение.
То есть, можно статически восстановить информацию о типах, и... А дальше можно взять и сказать, что если foo почти всегда вызывается с целочисленным аргументом, лишь один раз туда передаётся строковый, то это подозрительно похоже на ошибку программиста, который задумал foo с целочисленным аргументом, но один раз нечаянно сунул туда строку.
> Кстати про no-return функции, что нам предоставляет паскаль?
Ничего.
> - процедуры (которые ничего не возвращают) и собственно функции. Статический анализатор
> способен в таком случае распознать no-return "функцию"?
Нет.
> А в С что? оператор return. А если его нет?
Если в сишной функции нет оператора return, то возвращаемое значение функции неопределено, то есть это UB. Функция без return'а в C -- это не no-return функция. По-крайней мере в том определении "no-return", которое мы используем в данном разговоре. И паскалевская процедура -- это тоже не no-return функция в этом смысле. no-return функция -- это функция которая не возвращает управление в код, вызвавший её. В стандарте C нет ничего такого, так же как и в pascal'е. Но в gcc, если мне не изменяет память, есть атрибут noreturn или типа того, который можно повесить на функцию, сообщив компилятору, что она noreturn.
>> А где там проблема останова вылезет? Как я это вижу, если компилятор
>> может проследить пути выполнения таким образом, чтобы разложить код в линейную
>> последовательность ассемблерных инструкций, или операций интерпретатора, то значит он
>> может определить моменты, где происходит возврат из функции, а возвращаемое значение
>> не предоставлено, так? А если компилятор может, то и статический анализатор
>> сможет. Особенно если он -- часть компилятора.
> Стоп, стоп, тут не надо путать понятия компиляции с понятием исполнения, компилятор
> не исполняет!
> Ибо как вы представляете себе компиляцию такой программы?
В смысле? Ты ждёшь, что я разложу эту функцию здесь в линейную последовательность команд ассемблера? Ты можешь сделать это без моей помощи: gcc/clang вызванные с аргументом -S выдадут тебе ассемблерный дамп, то есть линейную последовательность ассемблерных команд.
> Тоже самое с unused кодом, во многих случаях ни компилятор ни статический
> анализатор не сможет принять решение является ли код не используемым, исключая
> некоторые частные случаи, как отметил выше, паттерны заложенные в анализатор или
> компилятор.
Да. Есть три варианта:
1. анализатор доказал, что код used
2. анализатор доказал, что код unused
3. анализатор не смог доказать ни того, ни другого.
Первые два случая тривиальны, с точки зрения того, что анализатору делать столкнувшись с ними. Третий случай сложнее, и анализатор может вести себя по-разному. Это зависит от языка, от целей анализатора, возможно от опций запуска анализатора.
>> Да, именно так он и делает, он кидает варнинги. Но для того,
>> чтобы решить, что здесь нужно кинуть варнинг, он сначала должен детектировать
>> код, который не будет выполняться никогда. А для этого ему надо
>> знать, что exit -- это no-return функция.
> И детектирует только по заранее известному паттерну, то есть вы должны создать
> статический анализатор все-возможного говно-кода (грубо говоря).
Скорее всего да. Но если мы будем рассматривать систему доказывающую соответствие кода спецификации, которая задана в виде логических утверждений о коде, то тут ситуация обратна: мы задаём все правильные состояния, а статистический анализатор находит отклонения. Такие программы, правда, не называют статическими анализаторами, но я не вижу качественной разницы, только количественную.
Ведь инварианты можно задавать спорадически, допустим комментариями специального вида. В принципе, даже объявления типов переменных -- это своего рода инварианты, типа "эта переменная хранит только значения типа int". Можно задавать инварианты чаще, и, скажем, для структуры динамического массива с полями buf, size, len, писать инвариант len <= size, а статический анализатор потом будет обращать внимание на все изменения len и size, и пытаться доказать или опровергнуть инвариант, с опорой на код меняющий их. Получать один из трёх вариантов доказано/опровергнуто/хз, и выдавать реакцию вида кинуть варнинг, ошибку, или ничего не кидать.
Можно писать инварианты ещё чаще -- на каждую функцию. Можно вообще на каждый чих: каждый раз, когда можно написать простой инвариант (когда не надо две страницы покрывать математической вязью, когда достаточно простого условия). Ну и, наконец, можно полную спецификацию кода задать. То есть, разница между ubsan и проверкой спецификации скорее количественная, чем качественная.
> Статический анализатор
> это не симулятор исполнения, тогда ему необходимы входные данные, а если
> ему эти данные дать, то это динамический анализатор.
Нет, есть такая штука, как символьные вычисления. Алгебра, короче. Зная какие-то истинные утверждения о значениях переменных, можно доказывать другие. Например, можно сказать, что sqrt(a) <= a, для любого a>=0. А это значит, что, например:
for(i = 0; i < sqrt(arr.len()); i ++) {
arr[i] = 0;
}
никогда не выйдет за границы массива, вне зависимости от значения arr и arr.len().
Можно взять баблсорт:
for(i = 1; i < arr.len(); i++) {
for(j = i; j > 0; j --) {
make_them_ascending(&arr[j-1], &arr[j]);
}
}
И доказать, что здесь не случится выхода за границы массива, хотя нигде нет непосредственного сравнения j с arr.len(). С одной из границ он сравнивается, а с другой нет, но статический анализ, применив немного логического вывода, может доказать, что всё ок. И для этого вовсе не обязательно выполнять.
Да, вот логический вывод, как раз, сталкивается с проблемой останова, но это будет означать лишь то, что статический анализатор иногда будет долго думать, прерывать свои размышления по таймеру (или по используемой памяти, или ещё по чему), и выводить варнинг "я не могу доказать X в строке N сорца SOURCE_NAME, но, допустим, я доказал, и вот я дальше разбираю остальной код". Или может мы запустим его в sloppy режиме, и он будет нам сообщать только о тех местах, где ему удалось опровергнуть какой-нибудь инвариант. Или может ещё как-нибудь выкрутимся: сделав отрицательный результат поиска багов ненадёжным; или заставив программистов принять такой стиль написания кода, чтобы всё доказывалось...
Вариант для распечатки
