Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

История [ править ]

Infer уходит корнями в академические исследования логики разделения , теории формальной проверки программного обеспечения. Работа над автоматической верификацией программ на основе Separation Logic привела к появлению ряда академических инструментов, включая Smallfoot и 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 также имеет специфический для предметной области язык для связывания абстрактного синтаксического дерева, основанный на идеях из Model Checking for Computing Tree Logic . [10] [11]

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

Награды [ править ]

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

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

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

Ссылки [ править ]

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

Внешние ссылки [ править ]

  • Официальный веб-сайт