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