Доказательство того, что мертвый код не может быть обнаружен компиляторами

Я планирую провести зимний курс по разному количеству тем, одной из которых будут составители. Теперь я столкнулся с этой проблемой, думая о заданиях, которые нужно давать на протяжении всего квартала, но это поставило меня в тупик, поэтому я мог бы вместо этого использовать его в качестве примера.

public class DeadCode {
  public static void main(String[] args) {
     return;
     System.out.println("This line won't print.");
  }
}

В приведенной выше программе очевидно, что оператор print никогда не будет выполнен из-за return. Компиляторы иногда выдают предупреждения или ошибки об мертвом коде. Например, приведенный выше код не будет компилироваться в Java. Однако компилятор javac не будет обнаруживать все случаи мертвого кода в каждой программе. Как мне доказать, что ни один компилятор не может это сделать?

Все это происходит из-за неразрешимости проблемы остановки. Предположим, у нас есть «идеальная» функция мертвого кода, некоторая машина Тьюринга M, некоторая входная строка x и процедура, которая выглядит примерно так:

Run M on input x;
print "Finished running input";

Если M выполняется вечно, мы удаляем оператор print, так как никогда не достигнем его. Если M не работает вечно, тогда нам нужно сохранить оператор print. Таким образом, если у нас есть средство для удаления мертвого кода, это также позволяет нам решить проблему остановки, поэтому мы знаем, что такого средства для удаления мертвого кода не может быть.

Мы можем обойти это путем «консервативного приближения». Итак, в моем примере с машиной Тьюринга, приведенном выше, мы можем предположить, что выполнение M на x может закончиться, поэтому мы проигнорируем его и не удаляем оператор print. В вашем примере мы знаем, что независимо от того, какие функции останавливаются или не останавливаются, мы никак не сможем достичь этого оператора print.

Обычно это делается путем построения «графа потока управления». Мы делаем упрощающие предположения, такие как «конец цикла while связан с началом и оператором после», даже если он выполняется вечно или выполняется только один раз и не посещает оба. Точно так же мы предполагаем, что оператор if может достичь всех своих ветвей, даже если в действительности некоторые из них никогда не используются. Подобные упрощения позволяют нам удалять «явно мертвый код», как в примере, который вы приводите, оставаясь разрешимым.

Чтобы уточнить некоторые путаницы из комментариев:

1. Nitpick: для фиксированного M это всегда решаемо. М должен быть вход

   Как говорит Рафаэль, в моем примере мы рассматриваем машину Тьюринга как исходную информацию. Идея состоит в том, что, если бы у нас был идеальный алгоритм DCE, мы могли бы создать фрагмент кода, который я даю для любой машины Тьюринга , и наличие DCE решило бы проблему остановки.

2. не убежден. Возврат как тупое утверждение в прямолинейном исполнении без ответвлений не трудно решить. (и мой компилятор говорит мне, что способен это выяснить)

   В связи с вопросом, который поднимает njzk2: вы абсолютно правы, в этом случае вы можете определить, что нет никакого способа сделать заявление после возврата. Это потому, что он достаточно прост, чтобы мы могли описать его недостижимость, используя ограничения графа потока управления (т. Е. Нет выходных ребер из оператора return). Но не существует идеального средства удаления мертвого кода, которое устраняет весь неиспользуемый код.

3. Я не принимаю зависящее от ввода доказательство для доказательства. Если существует такой вид пользовательского ввода, который может позволить коду быть конечным, то для компилятора будет правильным предположить, что следующая ветвь не мертва. Я не могу понять, для чего все эти возражения, это и очевидно (например, бесконечный стандарт) и неправильно.

   Для TomášZato: это не доказательство, зависящее от ввода. Скорее, интерпретируйте это как «обман». Он работает следующим образом: предположим, у нас есть идеальный алгоритм DCE. Если вы дадите мне произвольную машину Тьюринга M и введете x, я могу использовать мой алгоритм DCE, чтобы определить, останавливается ли M, создав приведенный выше фрагмент кода и посмотрев, удален ли оператор print. Этот метод, позволяющий оставить параметр произвольным для доказательства утверждения, является обычным в математике и логике.

   Я не совсем понимаю точку зрения ТомашаЗато о конечном коде. Конечно, код конечен, но идеальный алгоритм DCE должен применяться ко всему коду, который является бесконечным множеством. Точно так же, хотя сам код конечен, потенциальные наборы входных данных бесконечны, как и потенциальное время выполнения кода.

   Что касается того, что последняя ветвь не умерла: она безопасна с точки зрения «консервативного приближения», о котором я говорю, но недостаточно для обнаружения всех случаев мертвого кода, как запрашивает OP.

Рассмотрим код, подобный следующему:

while (true)
  print "Hello"
print "goodbye"

Понятно, что мы можем удалить print "goodbye"без изменения поведения программы. Таким образом, это мертвый код. Но если есть другой вызов функции вместо (true)в whileсостоянии, то мы не знаем , если мы можем удалить его или нет, что приводит к неразрешимости.

Обратите внимание, что я не придумаю это самостоятельно. Это хорошо известный результат в теории компиляторов. Это обсуждается в книге тигров . (Возможно, вы сможете увидеть, о чем они говорят в книгах Google .

Это поворот в ответе jmite, который обходит потенциальную путаницу по поводу не прекращения. Я дам программу, которая всегда останавливает себя, может иметь мертвый код, но мы не можем (всегда) алгоритмически решить, есть ли она.

Рассмотрим следующий класс входных данных для идентификатора мертвого кода:

simulateMx(n) {
  simulate TM M on input x for n steps
  if M did halt
    return 0
  else
    return 1
}

Так как Mи xисправлены, simulateMsимеет мертвый код с return 0тогда и только тогда, когда Mне останавливается на x.

$M$x$M$$M$

Следовательно, проверка мертвого кода не вычислима.

В случае, если вы не знакомы с сокращением в качестве проверочного метода в этом контексте, я рекомендую наш справочный материал .

Простой способ продемонстрировать этот тип свойства, не увязая в деталях, - это использовать следующую лемму:

Лемма: Для любого компилятора C для языка, полного по Тьюрингу, существует функция, undecidable_but_true()которая не принимает аргументов и возвращает логическое значение true, так что C не может предсказать, undecidable_but_true()вернет ли значение true или false.

Обратите внимание, что функция зависит от компилятора. Для undecidable_but_true1()данной функции компилятор всегда можно дополнить информацией о том, возвращает ли эта функция значение true или false; но всегда есть какая-то другая функция undecidable_but_true2(), которая не будет охвачена.

Доказательство: по теореме Райс свойство «эта функция возвращает истину» неразрешимо. Поэтому любой алгоритм статического анализа не может определить это свойство для всех возможных функций.

Следствие: учитывая компилятор C, следующая программа содержит мертвый код, который не может быть обнаружен:

if (!undecidable_but_true()) {
    do_stuff();
}

Примечание о Java: язык Java предписывает, чтобы компиляторы отклоняли определенные программы, которые содержат недоступный код, в то время как разумный мандат этого кода предоставляется во всех достижимых точках (например, поток управления в функции non-void должен заканчиваться returnоператором). Язык определяет, как именно выполняется анализ недоступного кода; если бы этого не произошло, то было бы невозможно писать переносимые программы. Дана программа вида

some_method () {
    <code whose continuation is unreachable>
    // is throw InternalError() needed here?
}

необходимо указать, в каких случаях за недостижимым кодом должен следовать какой-то другой код, а в каких случаях за ним не должен следовать какой-либо код. Пример Java-программы, которая содержит код, который недоступен, но не так, как это разрешено компиляторам Java, появляется в Java 101:

String day_of_week(int n) {
    switch (n % 7) {
    case 0: return "Sunday";
    case 1: case -6: return "Monday";
    …
    case 6: case -1: return "Saturday";
    }
    // return or throw is required here, even though this point is unreachable
}

Ответ jmite относится к тому, выйдет ли когда-нибудь программа из вычислений - просто потому, что она бесконечна, я бы не стал называть код после его смерти.

Однако есть и другой подход: проблема, на которую есть ответ, но он неизвестен:

public void Demo()
{
  if (Chess.Evaluate(new Chessboard(), int.MaxValue) != 0)
    MessageBox.Show("Chess is unfair!");
  else
    MessageBox.Show("Chess is fair!");
}

public class chess
{
  public Int64 Evaluate(Chessboard Board, int SearchDepth)
  {
  ...
  }
}

Эта процедура, без сомнения , содержит мертвый код - функция вернет ответ, который выполняет один путь, но не другой. Удачи в поиске! Моя память не теоретическая компьютер может решить эту проблему в течение жизни Вселенной.

Более детально:

В Evaluate()функции вычисляет , какая сторона выигрывает игры в шахматы , если обе стороны играют отлично (с максимальной глубиной поиска).

Шахматные оценщики обычно смотрят в будущее на каждое возможное движение определенной глубины, а затем пытаются забить доску в этой точке (иногда расширение некоторых ветвей дальше, если смотреть на полпути или что-то подобное, может привести к очень искаженному восприятию.) Поскольку фактическая максимальная глубина 17695 наполовину ходов, поиск исчерпывающий, он пересекает все возможные шахматы. Поскольку все игры заканчиваются, нет проблем с попыткой определить, насколько хороши позиции на каждой доске (и, следовательно, нет причин смотреть на логику оценки доски - она ​​никогда не будет названа), результатом является либо выигрыш, либо проигрыш, либо ничья. Если результат - ничья, игра будет честной, если результат - не ничьей, это нечестная игра. Чтобы немного его расширить, мы получим:

public Int64 Evaluate(Chessboard Board, int SearchDepth)
{
  foreach (ChessMove Move in Board.GetPossibleMoves())
    {
      Chessboard NewBoard = Board.MakeMove(Move);
      if (NewBoard.Checkmate()) return int.MaxValue;
      if (NewBoard.Draw()) return 0;
      if (SearchDepth == 0) return NewBoard.Score();
      return -Evaluate(NewBoard, SearchDepth - 1);
    }
}

Также обратите внимание, что компилятору будет практически невозможно понять, что Chessboard.Score () является мертвым кодом. Знание правил игры в шахматы позволяет нам, людям, понять это, но чтобы понять это, вы должны знать, что MakeMove никогда не сможет увеличить количество фигур и что Chessboard.Draw () вернет true, если количество фигур остается неизменным в течение слишком долгого времени. ,

Обратите внимание, что глубина поиска составляет полшага, а не целые ходы. Это нормально для такого рода подпрограмм ИИ, так как это подпрограмма O (x ^ n) - добавление еще одного поискового слоя оказывает значительное влияние на продолжительность выполнения.

Я думаю, что в вычислительном курсе понятие мертвого кода интересно в контексте понимания разницы между временем компиляции и временем выполнения!

Компилятор может определить, когда у вас есть код, который ни в одном из сценариев времени компиляции не может быть пройден, но он не может сделать это во время выполнения. это показывает простой цикл while с пользовательским вводом для теста на разрыв цикла.

Если компилятор действительно может определить мертвый код во время выполнения (т. Е. Распознать завершение Тьюринга), то есть аргумент, что код никогда не нужно запускать, потому что работа уже выполнена!

Если ничто иное, существование кода, который проходит проверки мертвого кода во время компиляции, иллюстрирует необходимость прагматической проверки границ входных данных и общей гигиены кода (в реальном мире реальных проектов).