Хабрахабр

[Перевод] Как Project Infer от Facebook помогает искать баги в мобильных приложениях перед деплоем

В среде специалистов по машинному обучению это весьма почетно. Несколько дней назад команда инженеров 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, самообучаясь, расширяет свою базу, так проект позволяет обнаружить массу проблем в коде.

Жизненный цикл (lifecycle) также разделяется на две части: глобальную и дифференциальную. В общем смысле процесс работы Facebook Infer можно разделить на два этапа: сбор данных и их анализ.

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

В первом случае Infer анализирует все файлы. C точки зрения исполнения Infer может работать в двух модальностях — Global и Differential, как и говорилось выше. Для проекта, который компилируется с использованием 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», что очень похоже на то, как работают указатели памяти. Основной элемент логики разделения — оператор * (и отдельно), который называется разделяющим соединением.

Bi-abduction совместно выводит антифреймы (отсутствующие части состояния) и фреймы (те части, которые не затронуты операцией). В контексте Infer Bi-abduction можно рассматривать как метод логического вывода, который дает платформе возможность обнаруживать свойства, касающиеся поведения независимых частей кода приложения. Antiframe⊢B ∗? Математически проблема Bi-abduction выражается с использованием следующего синтаксиса: A ∗? Frame.

В Infer от Facebook метод дает возможность вывести спецификации pre/post из чистого кода при условии, что мы знаем спецификации для примитивов на базовом уровне кода.

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

  • 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 рекомендует:

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть