Несколько дней назад команда инженеров Facebook отличилась — ее удостоили награды Most Influential POPL Paper Award. В среде специалистов по машинному обучению это весьма почетно. Награду вручили за работу Compositional Shape Analysis by Means of Bi-abduction, которая раскрывает нюансы Project Infer. Сам проект предназначен для обнаружения и ликвидации багов в коде мобильного приложения перед его деплоем.
Баги в программном обеспечении для мобильных устройств обходятся очень дорого как разработчикам, так и пользователям. Что касается первых, то обнаружение проблемы в уже размещенном в каталогах приложении — ночной кошмар для любого специалиста. Конечно, софт тестируется, работу программ проверяют по определенным шаблонам. Но чаще разработчики не могут предусмотреть всего, и баги в приложении обнаруживаются уже после деплоя.
Напоминаем: для всех читателей «Хабра» — скидка 10 000 рублей при записи на любой курс Skillbox по промокоду «Хабр».
Skillbox рекомендует: Онлайн-курс «Аналитик данных на Python».
Project Infer сканирует код мобильных приложений и позволяет найти разного рода проблемы, паттерны которых хранятся в базе (а она все время обновляется). Сам проект был представлен три года назад. Почти сразу после анонса Facebook открыл код, после чего его стали использовать в таких компаниях, как Amazon Web Services, Spotify и Uber.
Как это работает?
Project Infer использует специализированный набор алгоритмов для анализа работы кода. В исходном коде любого крупного приложения могут быть миллионы комбинаций, которые приводят к появлению ошибок. Традиционные процедуры анализа кода не могут помочь обнаружить все. Infer от Facebook, самообучаясь, расширяет свою базу, так проект позволяет обнаружить массу проблем в коде.
В общем смысле процесс работы Facebook Infer можно разделить на два этапа: сбор данных и их анализ. Жизненный цикл (lifecycle) также разделяется на две части: глобальную и дифференциальную.
На этапе сбора данных Infer переводит исходный код в собственный язык. Этап анализа посвящается изучению мельчайших деталей структуры кода, которые могут потенциально привести к появлению ошибки. Если Infer встречает уже знакомое сочетание факторов, идентифицируемое как паттерн ошибки, анализ останавливается для конкретного метода или функции, но остальные методы и функции продолжают анализироваться. Вот пример работы Infer.
C точки зрения исполнения Infer может работать в двух модальностях — Global и Differential, как и говорилось выше. В первом случае Infer анализирует все файлы. Для проекта, который компилируется с использованием Gradle, запуск Infer производится командой
infer run — gradle build.
Дифференциальный процесс используется в инкрементных системах сборки, характерных для мобильных приложений. В этом случае нужно сначала запустить сбор данных Infer, чтобы получить все команды компиляции, а затем провести анализ только изменений. Для этого используется такой набор команд:
gradle clean
infer capture — gradle build
edit some/File.java
# make some changes to some/File.java
infer run --reactive — gradle build.
Отчеты Infer можно просмотреть при помощи команды InferTraceBugs.
infer run — gradle build
inferTraceBugs
Основа Project Infer
Infer от Facebook основан на двух новых математических методах: логике разделения и Bi-abduction.
Ключевая особенность логики разделения — возможность локальных рассуждений (local reasoning). Она появилась благодаря наличию в утверждениях пространственных связок (англ. spatial connectives) между частями кучи. В этом случае нет необходимости учитывать весь объем памяти на каждом из этапов.
Основной элемент логики разделения — оператор * (и отдельно), который называется разделяющим соединением. Формула X↦Y ∗ Y↦X может быть прочитана как «X указывает на Y, а отдельно Y указывает на X», что очень похоже на то, как работают указатели памяти.
В контексте Infer Bi-abduction можно рассматривать как метод логического вывода, который дает платформе возможность обнаруживать свойства, касающиеся поведения независимых частей кода приложения. Bi-abduction совместно выводит антифреймы (отсутствующие части состояния) и фреймы (те части, которые не затронуты операцией). Математически проблема Bi-abduction выражается с использованием следующего синтаксиса: A ∗? Antiframe⊢B ∗? Frame.
В Infer от Facebook метод дает возможность вывести спецификации pre/post из чистого кода при условии, что мы знаем спецификации для примитивов на базовом уровне кода.
Создание FI стало возможно благодаря анализу работы специалистов по машинному обучению, который проводился много лет. В ходе работы над Infer были опубликованы такие ключевые для всей сферы статьи:
- Compositional Shape Analysis by means of Bi-abduction. Как раз за эту работу была получена премия, о которой говорится выше. Работа знакомит читателя с композиционным анализом формы. Это дополнение к традиционному анализу формы (shape analysis), дающее возможность применить метод для анализа исходного кода приложений.
- A Local Shape Analysis Based on Separation Logic: эта статья описывает логику разделения в качестве механизма анализа исходного кода приложений. Авторы показывают возможность изучения отдельных ячеек в куче памяти, без изучения всей кучи целиком. Таким образом, определенные ячейки составляют связанный список и без полного анализа.
- Smallfoot: Modular Automatic Assertion Checking with Separation Logic: в этой работе описывается предшественник Facebook Infer, который называется Smallfoot.
- AL: A new declarative language for detecting bugs with Infer: AL позволяет любому разработчику проектировать новые чекеры без полного понимания внутренней кухни Infer. AL — это декларативный язык.
- Moving Fast with Software Verification: Наконец, статья, которая раскрывает, как Facebook использует Project Infer для собственных нужд. В документе рассказывается о том, как разработчики Facebook интегрировали Infer в свой процесс разработки для обеспечения статического анализа для мобильных приложений, таких как Instagram, Facebook Messenger и приложения Facebook для Android и iOS.
Пока что Infer может использоваться лишь для мобильных приложений. Но некоторые его принципы применимы к приложениям общего назначения. Возможно, в будущем возможности Infer станут шире, и с его помощью разработчики смогут анализировать десктопные или серверные приложения.
Skillbox рекомендует:
- Практический курс «Мобильный разработчик PRO».
- Онлайн-курс «Профессия Frontend-разработчик».
- Практический годовой курс «PHP-разработчик с 0 до PRO».
Автор: Онлайн-университет Skillbox
