. Вывод NotNull-аннотаций по байткоду Java
Вывод NotNull-аннотаций по байткоду Java

Вывод NotNull-аннотаций по байткоду Java

В большинстве наиболее распространенных языков программирования со статической типизацией (включая Java) есть нулевые ссылки (в Java это null), разыменование которых приводит к ошибкам времени выполнения. Автор нулевых ссылок Тони Хоар признал их существование "ошибкой на миллиард долларов" (Tony Hoare. Null References: The Billion Dollar Mistake http://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare).

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

В Java разыменование нулевой ссылки приводит к NullPointerException (NPE). Другой распространенной и близкой по духу ошибкой было ClassCastException, вызванное отсутствием типовых параметров – эта проблема была решена (по мнению многих, отнюдь не самым элегантным образом) в Java 1.5.

Расширение системы типов и проблемы интероперабельности

Интуитивно понятно, что вероятность того, что в будущем в Java проблема NPE будет решаться "из коробки" элегантным и надежным способом, невелика, – слишком тяжело наследие legacy-кода. Поэтому появляются альтернативные решения.

Основных решений два.

  • Расширение типов java с помощью аннотаций @NotNull/@Nullable и использование дополнительных инструментов для анализа кода.
  • Использование альтернативных языков программирования.

Детали и тонкости этих решений описаны в конце статьи. Однако высока вероятность, что рано или поздно, в большом проекте, возникнет необходимость использовать существующие библиотеки, написанные на старой доброй Java. И тогда проблема нулевых ссылок возникает на границе взаимодействия двух миров – вашего нового чистого кода и библиотек Java. В общем случае сделать использование библиотек java полностью безопасным элегантным способом (без введения дополнительных конструкций, сущностей и рутинной работы) практически невозможно. Однако можно сделать такое использование более безопасным автоматически, без усилий со стороны пользователя.

Постановка задачи

Будем аннотировать параметр как @NotNull, если при любых условиях при передаче нулевого аргумента в данный параметр метод не может нормально завершиться. С точки зрения использования, инструмент, работающий с такими аннотациями (а с такими аннотациями умеет работать IDEA), должен предупреждать пользователя об ошибках, если в такой параметр передается null или значение, которое может быть null (@Nullable значение).

Здесь существенна фраза "при любых условиях". Автоматически выведенные аннотации не должны угадывать намерения автора, – они должны помогать пользоваться библиотекой, но не запрещать пользоваться ей. Ситуация, когда аннотация может помешать пользоваться библиотекой - это сужение ее реальной области определений или области значений.

Рассмотрим некоторый метод с сигнатурой

Мы считаем, что null, переданный в параметр x, принадлежит области определения, если можно создать такое состояние системы и так подобрать остальные параметры, что метод завершится в нормальном режиме. Будем считать, что автоматически выведенная аннотация корректна, если она не сужает область определения метода. Поэтому естественное требование – пользователь не должен получать ложных предупреждений. Рассмотрим несколько простых примеров.

Интуитивно может показаться, что нужно проаннотировать view как @NotNull. Однако мы ничего не знаем о принципах устройства библиотеки с данным методом. Может быть, здесь действует негласное соглашение, что когда конфигурацию некуда сохранить, нормально освободить (обнулить) view еще до вызова этого метода. Если мы проаннотируем view как @NotNull, то мы сломаем один из вариантов потенциального правильного использования библиотеки – программист может либо получить ложный warning, либо потерять возможность вызвать метод с легальным null.

Далее мы будем называть аннотацию @NotNull на параметре некорректной, если метод может нормально завершиться при передаче null в данный параметр.

Задача: автоматически вывести как можно больше корректных @NotNull аннотаций на параметрах.

Подзадача распознавания проверок

Во многих реальных Java-библиотеках есть ранние проверки того, что параметр не равен null, в следующем виде:

Мы хотим обрабатывать, в том числе, и такие случаи.

Иногда эта проверка может иметь более скрытую форму:

В данном случае, если x = null, исполнение завершится аварийно.

Мы хотим, по возможности, обрабатывать и такие случаи.

Вывод гарантированно корректного подмножества @NotNull-аннотаций

В общем случае невозможно автоматически вывести все корректные аннотация. В двух словах, эта невозможность сводится к неразрешимости в общем случае проблемы останова.

Наш алгоритм выводит лишь подмножество всех корректных аннотаций. Мы сделаем простое упрощение, которое приведет к потере точности, но не приведет к потере корректности.

Байткод Java и интересующие нас инструкции

Байткод для каждого метода анализируется отдельно (технически, мы будем выполнять интерпроцедурный анализ). Рассматривается случай, когда библиотека уже частично проаннотирована – то есть для некоторых методов мы уже имеется набор @NotNull-аннотаций для параметров.

Вкратце объясним, как устроен байткод, и как работает JVM с точки зрения нашей задачи.

Более формальное описание можно прочесть здесь

  • http://en.wikipedia.org/wiki/Java_bytecode
  • http://en.wikipedia.org/wiki/Java_bytecode_instruction_listings
  • The Java® Virtual Machine Specification: http://docs.oracle.com/javase/specs/jvms/se8/html/

JVM – стековая виртуальная машина, для вызова процедур (методов) используется стек вызововов. С выполнением каждого метода связан фрейм, в котором хранятся локальные переменные, стек операндов и указатель на текущую инструкцию. При вызове метода текущий фрейм помещается в стек фреймов, запоминается "адрес возврата", создается новый фрейм, инициализируется в соответствии с аргументами вызова, и управление передается инструкциям вызываемого метода с новым фреймом в качестве текущего. При завершении метода предыдущий фрейм восстанавливается, возвращаемое значение помещается в стек операндов, и управление передается инструкции, сохраненной в адресе возврата.

В java bytecode более 200 инструкций для операций с целыми числами, числами с плавающей точной, с массивами, записи и чтения полей объектов, вызовов методов – статических и методов объектов и т.д.

В контексте решаемой задачи нас интересуют такие инструкции байткода, исполнение которых может привести к NPE. Вот полный список таких инструкций с описанием ситуаций, когда точно произойдет NPE.

  • GETFIELD, PUTFIELD – чтение/запись поля объекта. NPE, если ссылка на объект равна null.
  • ARRAYLENGTH - чтение длины массива. NPE, если ссылка на массив – null.
  • IALOAD, LALOAD, FALOAD, DALOAD, AALOAD, BALOAD, CALOAD, SALOAD - чтение элементов массива. NPE, если ссылка на массив – null.
  • IASTORE, LASTORE, FASTORE, DASTORE, AASTORE, BASTORE, CASTORE, SASTORE - запись в массив. NPE, если ссылка на массив – null.
  • MONITORENTER - синхронизация. NPE, если ссылка на объект, который используется для синхронизации, равна null.
  • INVOKESTATIC - вызов статического метода. NPE, если в параметр, проаннотированный как @NotNull, передается null.
  • INVOKEVIRTUAL, INVOKESPECIAL, INVOKEINTERFACE - вызов метода объекта. NPE, если ссылка на объект, метод которого вызывается, равна null, или null передается в параметр, проаннотированный как @NotNull.
  • ATHROW – генерация исключения. Нас интересуют исключения, генерируемые в результате проверки значения параметра на null.

Из перечисленного выше набора опасных ситуаций нас интересуют те, которые связаны с обрабатываемым параметром.

Описание алгоритма

В данном разделе описывается суть алгоритма. Детали реализации описываются в следующем разделе.

Для работы с байткодом мы используем библиотеку ASM (http://asm.ow2.org/). (Кстати, документация библиотеки ASM очень хороша для знакомства с принципами java bytecode.)

Суть алгоритма – рассмотреть все возможные пути исполнения байткода данного метода и, если каждый путь исполнения завершается NPE-ошибкой на данном параметре, пометить данный параметр как @NotNull.

Такой анализ проводится для каждого параметра независимо. То есть, если у метода, скажем, 3 параметра, анализ проводится 3 раза – для каждого параметра. Для решения поставленной задачи достаточно абстрагироваться от реальных значений, с которыми работает виртуальная машина Java, и разделить все значения на два класса абстрактных значений – ParamValue и BasicValue. ParamValue – это значение параметра, BasicValue – все остальные значения (необходимое нам org.objectweb.asm.tree.analysis.BasicValue уже реализовано в ASM). Таким образом, мы переходим от исполнения кода на конкретных значениях к исполнению (интерпретации) кода на абстрактных значениях.

С помощью библиотеки ASM легко строится граф потока управления для метода. Чтобы проанализировать все возможные пути исполнения байткода данного метода достаточно проследить все пути исполнения по графу потока управления данного метода. Естественно, что если в графе потока управления есть циклы, то в общем случае число путей в этом графе бесконечно. Однако, для наших целей все пути, в том числе и бесконечные, можно представить в конечном виде.

Построение дерева конфигураций

Будем строить дерево всех возможных путей в графе потока управления. В узлах такого дерева будут находиться конфигурации , однозначно описывающие интересующее нас состояние. Конфигурация представляется парой (insnIndex, frame), где insnIndex — номер текущей инструкции, а frame – массив из абстрактных значений переменных и операндов (для состояния фрейма нам подойдет org.objectweb.asm.tree.analysis.Frame). Будем называть такое дерево деревом конфигураций.

Дерево строится сверху вниз, в самом начале в корень дерева помещается конфигурация (0, startFrame), в startFrame все значения, кроме интересующего нас параметра – BasicValue, а интересующий нас параметр – ParamValue.

Начинаем достраивать это дерево конфигураций – по insnIndex получаем инструкцию байткода, исполняем ее над frame (над абстрактными значениями) и получаем обновленное состояние фрейма nextFrame. Если текущая инструкция приводит к завершению исполнения метода (return или throw), то конфигурация становится листом дерева конфигураций. Иначе рассматриваем все возможные переходы (из графа потока управления). Для каждого перехода к инструкции с номером nextInsnIndex конструируем новую конфигурацию (nextInsnIndex, nextFrame) и добавляем ее в качестве дочернего узла к текущему. Помимо прочего, будем отслеживать, происходит ли при исполнении инструкции разыменовывание ParamValue (возникает ли опасная ситуация, если в параметр передан null). Также будем отслеживать ветви в дереве конфигураций, на которые мы попадаем, если значение ParamValue – null.

Распознавание циклов – построение конечных деревьев конфигураций

В общем случае при наличии в методе циклов дерево конфигураций будет бесконечным. Приятным фактом является то, что количество всех возможных конфигураций нашего дерева конечно. Действительно, вариантов для первой компоненты конфигураций конечное число – число инструкций в данном методе ограничено. Количество же значений frame - тоже конечное число, 2^n, где n – размер массива значений во фрейме (локальные переменные и операнды).

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

Введем упорядочение ≤ на абстрактных значениях («быть частным случаем») следующим образом:

  • ParamValue ≤ ParamValue
  • ParamValue ≤ BasicValue
  • BasicValue ≤ BasicValue

Пусть frame[i] - значение в i-ом слоте фрейма. Будем считать, что фрейм frame2 является частным случаем фрейма frame1 (и записывать это как frame2 ≤ frame1), если для всех индексов слотов выполняется frame2[i] ≤ frame1[i]. Введем упорядочение "быть частным случаем" и на конфигурациях, конфигурация (insnIndex2, frame2) ≤ (insnIndex1, frame1) если:

  • insnIndex2 == insnIndex1 и
  • frame2 ≤ frame1.

Если при построении дерева конфигураций мы встречаем конфигурацию conf2 и на пути от данной конфигурации до корня дерева конфигураций есть conf1, такая, что conf2 ≤ conf1, то не будем достраивать поддерево для conf2, а превратим эту конфигурацию в лист со специальным значением CYCLE. Это значит, что мы просто переходим в начало некоторого цикла.

Дерево конфигураций, построенное таким образом, будет конечным всегда .

Аппроксимация поведения метода по дереву конфигураций и вывод аннотации

Пусть у нас есть полностью построенное дерево конфигураций. Проаннотируем листы дерева конфигураций метками со следующими значениями.

  • RETURN – возможен нормальный возврат, на пути от стартового узла до данного листа мы не смогли обнаружить разыменовывания параметра.
  • NPE – на пути от стартового узла до данного листа мы обнаружили разыменование параметра, или же в данном листе инициируется исключение, и мы обнаружили, что до данного листа мы можем дойти, только если наш параметр равен null.
  • ERROR – в данном листе инициируется исключение, но у нас нет информации о том, что до данного листа мы можем дойти, только если наш параметр равен null.
  • CYCLE – переход в начало цикла.

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

📎📎📎📎📎📎📎📎📎📎