Infer , [1] a veces denominado "Facebook Infer", es una herramienta de análisis de código estático desarrollada por un equipo de ingeniería de Facebook junto con colaboradores de código abierto. Proporciona soporte para Java , C , C++ y Objective-C , y se implementa en Facebook en el análisis de sus aplicaciones de Android e iOS (incluidas las de WhatsApp, Instagram, Messenger y la aplicación principal de Facebook). [2]
Infer tiene sus raíces en la investigación académica sobre Lógica de Separación , una teoría para la verificación formal de software. El trabajo en la verificación automática de programas basado en Separation Logic dio lugar a una sucesión de herramientas académicas, incluidas Smallfoot y SpaceInvader. Sobre la base del trabajo académico, Cristiano Calcagno, Dino Distefano y Peter O'Hearn, tres investigadores del University College London y la Queen Mary University de Londres, cofundaron la startup de verificación Monoidics en 2009, y Monoidics desarrolló la primera versión de Infer. [3] [4] [2] Monoidics fue adquirida por Facebook en 2013, [5] y en 2015 el código de Infer fue de código abierto. [2] [6]
A partir de 2013, cuando Infer era de código abierto, se afirmaba que los desarrolladores de Facebook solucionaban cientos de errores por mes identificados por Infer antes de llegar a producción. [5] Para 2015, esto había aumentado a más de 1000 errores por mes. [7]
Spotify, Uber, Mozilla, Sky y Marks and Spencer se encuentran entre los usuarios reportados de Infer. [1]
Infer realiza comprobaciones de excepciones de puntero nulo, fugas de recursos, accesibilidad de anotaciones, protecciones de bloqueo faltantes y condiciones de carrera de concurrencia en código de Android y Java. Comprueba si hay problemas de puntero nulo, pérdidas de memoria, convenciones de codificación y API no disponibles en C, C++ y Objective C. [1]
Infer utiliza una técnica llamada bi-abducción [8] para realizar un análisis compositivo del programa que interpreta los procedimientos del programa independientemente de quienes lo llaman. Se afirma que esto permite a Infer escalar a grandes bases de código y ejecutar rápidamente cambios de código de manera incremental, sin dejar de realizar un análisis interprocedimental que razona a través de los límites de los procedimientos. [9]
Infer está conectado al sistema de revisión de código de Facebook. Su modelo de implementación consiste en comentar automáticamente las modificaciones del código a medida que se envían para su revisión, donde informa posibles regresiones. Lo hace analizando incrementalmente los cambios de código a través de un trabajo en el sistema de integración continua de Facebook que se ejecuta en sus centros de datos. [9]
Infer también tiene un lenguaje de dominio específico para el linting de árboles de sintaxis abstracta, basado en ideas de Model Checking for Computation Tree Logic . [10] [11]
Infer está escrito principalmente en el lenguaje de programación OCaml . [12]
Dino Distefano [it] recibió la medalla de plata de la Real Academia de Ingeniería en 2014 en reconocimiento a la adquisición de Monoidics. [13]
Cuatro miembros del equipo Infer, Josh Berdine, Cristiano Calcagno, Dino Distafano y Peter O'Hearn, recibieron el Premio de Verificación Asistida por Computadora 2016, un premio que compartieron con John C. Reynolds , Samin Ishtiaq y Hongseok Yang. [7] [14]
Peter O'Hearn fue elegido miembro de la Real Academia de Ingeniería en 2016, por su trabajo en Separation Logic and Infer. [15]