WikiDer > Статический анализатор Infer

Infer Static Analyzer

Сделать вывод,[1] иногда называемый «Facebook Infer», является статический анализ кода инструмент, разработанный командой инженеров Facebook вместе с участниками открытого кода. Он обеспечивает поддержку Ява, C, C ++, и Цель-C, и развертывается в Facebook при анализе приложений для Android и iOS (в том числе для WhatsApp, Instagram, Messenger и основного приложения Facebook).[2]

Infer уходит корнями в академические исследования Логика разделения, теория для формальная проверка программного обеспечения. Работа над автоматической верификацией программ на основе логики разделения привела к появлению ряда академических инструментов (включая Смолфут и SpaceInvader). Основываясь на академической работе, Кристиано Кальканьо, Дино Дистефано и Питер О'Хирн, трое исследователей из Лондона, в 2009 году соучредили стартап по верификации Monoidics, а Monoidics разработала первую версию Infer.[3][4][2] Monoidics была приобретена Facebook в 2013 году.[5] а в 2015 году исходный код Infer был открыт.[2][6]

По состоянию на 2013 год, когда Infer был открыт с открытым исходным кодом, утверждалось, что сотни ошибок в месяц, выявленных Infer, были исправлены разработчиками Facebook до того, как они попали в производство.[5] К 2015 году это количество увеличилось до 1000 ошибок в месяц.[7]

Spotify, Uber, Mozilla, Sky и Marks and Spencer входят в число зарегистрированных пользователей Infer.[1]

Технологии

Infer выполняет проверки исключений нулевого указателя, утечек ресурсов, доступности аннотаций, отсутствия средств защиты блокировок и условий конкуренции в коде Android и Java. Он проверяет наличие проблем с нулевым указателем, утечек памяти, соглашений о кодировании и недоступных API в C, C ++ и Objective C.[1]

Infer использует технику под названием bi-abduction.[8] выполнить композиционный программный анализ который интерпретирует программные процедуры независимо от их вызывающих. Утверждается, что это позволяет Infer масштабироваться до больших кодовых баз и быстро запускать изменения кода инкрементным способом, при этом выполняя межпроцедурный анализ, выходящий за границы процедур.[9]

Infer подключен к системе проверки кода в Facebook. Его модель развертывания заключается в автоматическом комментировании изменений кода при их отправке на рассмотрение, где он сообщает о потенциальных регрессиях. Это достигается путем постепенного анализа изменений кода с помощью задания на Facebook непрерывная интеграция система, которая работает в ее центрах обработки данных.[9]

Infer также имеет предметно-ориентированный язык для связывания абстрактного синтаксического дерева, основанный на идеях из Проверка модели для Логика дерева вычислений.[10][11]

Infer в основном написан в OCaml язык программирования.[12]

Награды

Дино Дистефано получил Королевская инженерная академия серебряная медаль в 2014 году в знак признания приобретения Monoidics.[13]

Четыре члена команды Infer, Джош Бердин, Криштиану Кальканьо, Дино Дистафано и Питер О'Хирн, получили в 2016 году премию Computer Aided Verification Award, которую они разделили. Джон С. Рейнольдс, Самин Иштиак и Хонгсок Ян.[7][14]

Питер О'Хирн был избран Член Королевской инженерной академии в 2016 году за работу над Separation Logic and Infer.[15]

использованная литература

  1. ^ а б c «Сделать вывод статического анализатора». Интернет сайт.
  2. ^ а б c Кальканьо, Криштиану; Дистефано, Дино; О'Хирн, Питер. «Вывод Facebook с открытым исходным кодом: выявление ошибок перед отправкой».
  3. ^ Кальканьо, Криштиану; Дистефано, Дино; О? Хирн, Питер В .; Ян, Хонгсок (1 декабря 2011 г.). «Анализ формы композиции с помощью би-абдукции». Журнал ACM. 58 (6): 1–66. CiteSeerX 10.1.1.420.2150. Дои:10.1145/2049697.2049700.
  4. ^ Кальканьо, Криштиану; Дистефано, Дино (18 апреля 2011 г.). Infer: автоматический верификатор программ для безопасности памяти программ на C. Формальные методы НАСА. Конспект лекций по информатике. 6617. Шпрингер, Берлин, Гейдельберг. С. 459–465. CiteSeerX 10.1.1.421.9629. Дои:10.1007/978-3-642-20398-5_33. ISBN 978-3-642-20397-8.
  5. ^ а б Константин, Джош. "Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics | TechCrunch". Techcrunch.
  6. ^ Финли, Клинт. "AI-инструмент Facebook для устранения ошибок теперь открыт для всех | WIRED". www.wired.com.
  7. ^ а б О'Салливан, Брайан. «Четыре сотрудника Facebook выиграли престижную награду CAV». Facebook исследования.
  8. ^ Логика разделения и двойное похищение, стр., Вывести сайт проекта.
  9. ^ а б Кальканьо, Криштиану; Дистефано, Дино; Dubreil, Джереми; Габи, Доминик; Hooimeijer, Pieter; Лука, Мартино; О'Хирн, Питер; Папаконстантину, Ирен; Пурбрик, Джим; Родригес, Дулма (27 апреля 2015 г.). Быстрые шаги с проверкой программного обеспечения. Формальные методы НАСА. Конспект лекций по информатике. 9058. Спрингер, Чам. С. 3–11. Дои:10.1007/978-3-319-17524-9_1. ISBN 978-3-319-17523-2.
  10. ^ Черчилль, Дульма; Дистефано, Дино; Лука, Мартино; Ри, Райан; Виллар, Жюль. «AL: новый декларативный язык для обнаружения ошибок с помощью Infer». Сообщение в блоге с кодом Facebook.
  11. ^ Серхио, де Симоне. «Новый язык AL от Facebook призван упростить анализ статических программ». InfoQ.
  12. ^ "Вывести страницу Github".
  13. ^ «Серебряные медали для самых ярких и перспективных предпринимателей Великобритании». Королевская инженерная академия. Архивировано из оригинал в 2014-10-26. Получено 2017-07-05.
  14. ^ комитет, Премия CAV. «Премия за компьютерную проверку 2016». PRLog.
  15. ^ «Новые стипендиаты RAEng 2016, Питер О'Хирн». Королевская инженерная академия.

внешние ссылки