Analizador estático de inferencia

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. Ofrece soporte para Java , C , C++ y Objective-C , y se implementa en Facebook para 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 sobre verificación automática de programas basada en lógica de separación condujo a una sucesión de herramientas académicas, incluyendo Smallfoot y SpaceInvader . Partiendo del trabajo académico, Cristiano Calcagno, Dino Distefano y Peter O'Hearn , tres investigadores del University College London y la Queen Mary University of London , 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 se publicó como código abierto. ^{[ 2 ] [ 6 ]}

En 2013, cuando Infer se convirtió en código abierto, se afirmó que los desarrolladores de Facebook corregían cientos de errores al mes identificados por Infer antes de que llegaran a producción. ^{[ 5 ]} Para 2015, esta cifra había aumentado a más de 1000 errores al 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, falta de protecciones de bloqueo y condiciones de carrera de concurrencia en código Android y Java. Comprueba problemas de puntero nulo, fugas de memoria, convenciones de codificación y API no disponibles en C, C++ y Objective C. ^{[ 1 ]}

Infer utiliza una técnica denominada biabducción ^{[ 8 ]} para realizar un análisis compositivo de programas que interpreta los procedimientos del programa independientemente de quienes los llaman. Se afirma que esto permite a Infer escalar a grandes bases de código y ejecutarse rápidamente en cambios de código de forma incremental, al tiempo que realiza un análisis interprocedimental que razona más allá 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 de código a medida que se envían para su revisión, donde informa sobre posibles regresiones. Para ello, analiza incrementalmente los cambios de código mediante un proceso en el sistema de integración continua de Facebook , que se ejecuta en sus centros de datos. ^{[ 9 ]}

Infer también tiene un lenguaje específico de dominio para el análisis de árboles de sintaxis abstracta , basado en ideas de la verificación de modelos para la lógica de árboles de computación . ^{[ 10 ] [ 11 ]}

Infer está escrito principalmente en el lenguaje de programación OCaml . ^{[ 12 ]}

Dino Distefano 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 sobre lógica de separación e Infer. ^{[ 15 ]}

• Sitio web oficial