Является ли поиск указателей в коде C / C ++ статически эквивалентным проблеме Halting?
Я не слишком глубоко укоренен в очень формальной стороне статического анализа кода, отсюда и этот вопрос.
Пару лет назад я прочитал, что различение кода от данных с использованием статического анализа кода эквивалентно Проблема остановки. (Требуется цитирование, но у меня его больше нет. В Stackoverflow есть потоки на этом Вот или же Вот.По крайней мере, для обычных компьютерных архитектур, основанных на Архитектура фон Неймана где код и данные совместно используют одну и ту же память, это, кажется, имеет смысл.
Сейчас я смотрю на статический анализ кода C / C ++ и анализ указателей; программа не выполняется. Почему-то у меня такое ощущение, что отслеживание всех созданий и использований значений указателя статически похоже на проблему остановки, потому что я не могу определить, является ли данное значение в памяти значением указателя, т.е. я не могу отслеживать поток значений значений указателя через объем памяти. Анализ псевдонимов может сузить проблему, но она кажется менее полезной перед лицом многопоточного кода.
(Можно даже рассмотреть отслеживание произвольных значений, а не только указателей: построение полного потока значений для любого данного «интересного» значения кажется эквивалентным проблеме останова.)
Поскольку это всего лишь догадка, мой вопрос таков: на какие формальные выводы я могу ссылаться? Я ошибаюсь?
Решение
Вы всегда можете написать это:
extern bool some_program_halts();
extern int* invalid_pointer();
#include <iostream>
int main()
{
using namespace std;
if( some_program_halts() ) { cout << *invalid_pointer() << endl; }
}
Проверка разыменования этой программой неверного указателя эквивалентна выяснению, является ли вызов some_program_halts()Останавливается
Другие решения
Это почти наверняка эквивалентно по модулю того факта, что C не является языком, эквивалентным тьюрингу (данная реализация C является гигантским конечным автоматом, а не машиной Тьюринга, из-за Представление типов). Указатели не должны храниться в своих исходных представлениях в объектах, эффективный тип которых является типом указателя; Вы можете проверить представление и выполнить произвольные операции с ним, например, зашифровав указатели и расшифровав их позже. Определение того, является ли произвольное вычисление обратимым, или два вычисления взаимно противоположны друг другу, является (необязательно) эквивалентным определению остановки.
Если я вас правильно понял: да, проверка того, получает ли программа на C или C ++ доступ к недопустимому указателю, эквивалентна проблеме остановки (в любом случае, программы C или C ++).
Предположим, у вас есть инструмент, который сообщает вам, обращалась ли программа к недействительному указателю, и программа, которую вы хотели проверить на предмет остановки. Добавляя дополнительную информацию к каждому указателю, вы можете проверить (во время выполнения), является ли указатель действительным или нет; добавить такие проверки, с бесконечным циклом при неудаче. Теперь у вас есть программа без доступа к недействительным указателям. Заменив все места, где программа может завершить доступ с недействительным указателем, вы получите программу, которая имеет доступ с недействительным указателем тогда и только тогда, когда исходная программа завершается.
Статический анализ — это почти всегда приближение, часто доказываемое сведением проблемы остановки к таким программам, как тот, в ответе Альфа. Тем не менее, аппроксимация может привести к ошибкам либо ложных срабатываний, либо ложных отрицаний.
- «Консервативный» статическая проверка будет иметь только ложные негативы. Он никогда не примет «плохую» программу, но неизбежно отвергнет некоторые «достаточно сложные» хорошие программы.
- «Либеральный» статическая проверка будет иметь ложные срабатывания. Иногда он принимает плохую программу по ошибке, но (как правило) он также принимает все хорошие программы.
Некоторые примеры:
- Система типов Java является консервативной: переменная с типом
Tвсегда будет содержать экземпляр типаT(или подтипTили ноль) во время выполнения, несмотря ни на что. - Опция GCC, предупреждающая о неинициализированных переменных, является либеральной: она не находит всех потенциальных применений неинициализированной переменной. Вот пример ложноположительной программы.
- Напротив, Java выполняет консервативную неинициализированную проверку переменных для локальных переменных. Он отказывается компилировать программу, если видит потенциальный путь выполнения с использованием потенциально неинициализированной переменной.
Либеральные проверки часто используются компиляторами для выдачи предупреждений и внешними инструменты статического анализа. Такие вещи, как системы типов и оптимизация компилятора, как правило, полагаются на консервативные проверки, чтобы быть правильными.
Многие задачи имеют несколько разумных консервативных и либеральных алгоритмов различной точности. Анализ псевдонимов безусловно, один из них.
Для получения дополнительной информации смотрите любой хороший учебник по компилятору, такой как книга дракона.