Статический анализ IntelliJ IDEA против человеческого разума

Не так давно я изучал вывод статического анализатора IntelliJ IDEA для Java-кода и наткнулся на интересный случай. Так как соответствующий фрагмент кода не является open source, я его анонимизировал и отвязал от внешних зависимостей. Будем считать, что он выглядел так:

private static List<Integer> process(Map<String, Integer> options, List<String> inputs) {
    List<Integer> res = new ArrayList<>();
    int cur = -1;
    for (String str : inputs) {
        if (str.startsWith("-"))
            if (options.containsKey(str)) {
                if (cur == -1) cur = options.get(str);
            }
            else if (options.containsKey("+" + str)) {
                if (cur == -1) cur = res.isEmpty() ? -1 :
                        res.remove(res.size() - 1);
                if (cur != -1) res.add(cur + str.length());
            }
    }
    return res;
}

Код как код, что-то преобразуется, что-то делается, но статическому анализатору он не понравился. Здесь мы видим целых два предупреждения:

На выражении res.isEmpty() IDE говорит, что условие всегда истинно, а на cur выдается, что присваивание бессмысленно, так как то же самое значение уже лежит в этой переменной. Нетрудно видеть, что проблема с присваиванием — прямое следствие первой проблемы. Если res.isEmpty() действительно всегда истинно, то строка редуцируется до

if (cur == -1) cur = -1;

Это и в самом деле излишне. Вот только почему выражение всегда истинно? Ведь res — это список, он заполняется в этом же цикле. Количество итераций цикла и то, в какие ветки мы зайдем, зависит от входных параметров, которых IDE знать не может. Мы же могли добавить элемент в res на предыдущей итерации, и тогда список не будет пустым.

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

Для начала пометим все строчки, где меняется состояние метода. Это изменение переменной cur или изменение списка res:

private static List<Integer> process(Map<String, Integer> options, List<String> inputs) {
    List<Integer> res = new ArrayList<>();
    int cur = -1;
    for (String str : inputs) {
        if (str.startsWith("-"))
            if (options.containsKey(str)) {
                if (cur == -1) cur = options.get(str); // A
            }
            else if (options.containsKey("+" + str)) {
                if (cur == -1) cur = res.isEmpty() ? -1 : // B 
                        res.remove(res.size() - 1); // C
                if (cur != -1) res.add(cur + str.length()); // D
            }
    }
    return res;
}

Строки 'A' и 'B' ('B' — это первая ветка условного оператора) изменяют переменную cur, 'D' изменяет список, а 'C' (вторая ветка условного оператора) изменяет и список, и переменную cur. Для нас существенно, лежит ли в cur -1 и является ли список пустым. То есть надо следить за четырьмя состояниями:

Строка 'A' меняет cur, если там до этого было -1. Причем мы не знаем, будет в результате -1 или нет. Поэтому возможны два варианта:

Строка 'B' тоже работает, только если cur равно -1. При этом, как мы уже заметили, она в принципе ничего не делает. Но отметим все-таки это ребро для полноты картины:

Строка 'C', как и предыдущие, работает при cur == -1 и меняет его произвольно (как и 'A'). Но при этом она еще может непустой список res превратить в пустой, или оставить непустым, если там было больше одного элемента.

Наконец, строка 'D' увеличивает размер списка: пустой она может превратить в непустой, либо непустой увеличить. Непустой в пустой она превратить не может:

Что это нам дает? Ровным счетом ничего. Совершенно непонятно, почему условие res.isEmpty() всегда истинно.

На самом деле, мы начали неправильно. В этом случае недостаточно отслеживать состояние каждой переменной отдельно. Тут играют важную роль коррелированные состояния. К счастью, в связи с тем, что 2+2 = 2*2, у нас их тоже только четыре:

Двойной рамкой я отметил начальное состояние, которое мы имеем при входе в метод. Что ж, пробуем все заново. 'A' меняет либо сохраняет cur при любом res, res при этом не меняется:

'B' работает только при cur == -1 && res.isEmpty() и ничего не делает. Добавляем:

'C' работает только при cur == -1 && !res.isEmpty(). При этом и cur, и res меняются произвольно: после 'C' мы попадаем в любое состояние:

Наконец, 'D' может начаться в cur != -1 && res.isEmpty() и сделать список непустым, либо начаться в cur != -1 && !res.isEmpty() и там же и остаться:

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

И тут обнаруживается весьма любопытная вещь. Мы не можем попасть в левый нижний угол. А раз мы в него попасть не можем, значит, мы не можем пройтись ни по одной стрелке 'C'. То есть строчка 'C' действительно недостижима, а 'B' при этом может выполняться. Это возможно, только если условие res.isEmpty() действительно всегда истинно! Анализатор IntelliJ IDEA полностью прав. Извини, анализатор, зря я думал, что ты глючный. Просто ты настолько умный, что мне, простому человеку, трудно за тобой успеть.

В нашем анализаторе нет никаких “хайповых” технологий искусственного интеллекта, а используются подходы control flow analysis и data flow analysis, которым уже не менее полувека. Тем не менее он действительно порой делает весьма нетривиальные выводы. Впрочем, это и понятно: строить графы и гулять по ним у машин давно получается лучше, чем у людей. Тут есть важная нерешенная задача: недостаточно просто сказать человеку, что у него в программе ошибка. Кремниевый мозг должен объяснить биологическому, почему он так решил, причем так чтобы биологический мозг понял. Если у кого-то есть гениальные идеи, как это сделать, я буду рад вас выслушать. Если же вы готовы сами реализовать ваши идеи, наша команда не откажется с вами посотрудничать!

Один из acceptance-тестов перед вами: для этого примера объяснение должно генерироваться автоматически. Это может быть текст, граф, дерево, картинка с котиками — все что угодно, лишь бы человеку было понятно.

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