Meta представила новый статический анализатор для Android
В Meta разработали статический анализатор, который фиксирует взаимоблокировки в Java-коде для Android, даже не запуская сам код. Он способен проводить ревизии в кодовых базах с сотнями миллионов строк.
Анализатор развернули в системе непрерывной интеграции Meta, где он сканирует каждую фиксацию в семействе приложений Android. За последние два года разработчики внесли более 200 исправлений в ответ на отчеты о взаимоблокировках, что составляет около 54% всех исправлений.
Анализатор Meta имеет открытый исходный код и является частью системы статического анализа Infer.
Разработчики использовали методы абстрактной интерпретации. Для каждого метода анализатор вычисляет сводную информацию о том, как он поведет себя с точки зрения получения и снятия блокировки, а также о том, будет ли метод выполняться в основном потоке или в фоновом. Это делается композиционным образом: каждый метод резюмируется максимум один раз, а сводка используется при суммировании вызывающих объектов, что обеспечивает предсказуемую высокую производительность.
Центральной частью метода является набор критических пар. Критическая пара (A, B) фиксирует следующий факт: метод пытается получить блокировку B, и в это время он уже удерживает ровно столько блокировок в наборе A. Этих данных, вычисленных по всем методам, достаточно, чтобы ответить на вопрос о том, возможна ли взаимоблокировка между двумя параллельными методами.
Инструмент не анализирует все исходные файлы в приложении. Вместо этого он сначала обрабатывает все методы в измененных файлах ревизии. Затем на основе этих данных он применяет эвристику, чтобы находить за пределами ревизии методы, которые потенциально могут заблокировать один из них в ревизии.
Разработчики утверждают, что их подход делает анализатор достаточно масштабируемым, чтобы его можно было развернуть на больших кодовых базах в Meta.
