Hace unos días, el equipo de ingeniería de Facebook se destacó: recibió el Premio
POPL Paper más influyente . Entre los especialistas en aprendizaje automático, esto es muy honorable. El premio fue presentado por el trabajo de
Análisis de forma compositiva por medios de bi-abducción , que revela los matices del Proyecto Infer. El proyecto en sí está diseñado para detectar y eliminar errores en el código de una aplicación móvil antes de su implementación.
Los errores en el software para dispositivos móviles son muy caros tanto para los desarrolladores como para los usuarios. En cuanto al primero, la detección de un problema en una aplicación que ya está en directorios es una pesadilla para cualquier especialista. Por supuesto, el software se prueba, el trabajo de los programas se verifica de acuerdo con ciertas plantillas. Pero con mayor frecuencia, los desarrolladores no pueden prever todo, y se detectan errores en la aplicación después de la implementación.
Le recordamos: para todos los lectores de "Habr": un descuento de 10.000 rublos al registrarse en cualquier curso de Skillbox con el código de promoción "Habr".
Skillbox recomienda: El curso en línea de Python Data Analyst .
Project Infer escanea el código de las aplicaciones móviles y le permite encontrar todo tipo de problemas, cuyos patrones se almacenan en la base de datos (y se actualiza todo el tiempo). El proyecto en sí fue presentado hace tres años. Casi inmediatamente después del anuncio, Facebook abrió el código, después de lo cual comenzó a usarse en empresas como Amazon Web Services, Spotify y Uber.
Como funciona
Project Infer utiliza un conjunto especializado de algoritmos para analizar el funcionamiento del código. Puede haber millones de combinaciones en el código fuente de cualquier aplicación grande que pueda conducir a errores. Los procedimientos tradicionales de análisis de código no pueden ayudar a detectar todo. Inferir desde Facebook, el autoaprendizaje, está expandiendo su base, por lo que el proyecto le permite detectar muchos problemas en el código.
En un sentido general, el proceso de Inferencia de Facebook se puede dividir en dos etapas: recopilación y análisis de datos. El ciclo de vida también se divide en dos partes: global y diferencial.
En la fase de recopilación de datos, Infer traduce el código fuente a su propio idioma. La fase de análisis se dedica al estudio de los detalles más pequeños de la estructura del código, lo que puede conducir a la aparición de un error. Si Infer encuentra una combinación ya familiar de factores identificados como un patrón de error, el análisis se detiene para un método o función en particular, pero otros métodos y funciones continúan siendo analizados. Aquí hay un ejemplo de Infer.
Desde el punto de vista de la ejecución, Infer puede trabajar en dos modalidades: Global y Diferencial, como se mencionó anteriormente. En el primer caso, Infer analiza todos los archivos. Para un proyecto que se compila con Gradle, Infer se inicia con el comando
infer run -- gradle build
El proceso diferencial se utiliza en sistemas de compilación incrementales específicos para aplicaciones móviles. En este caso, primero debe iniciar la recopilación de datos de Inferir para obtener todos los comandos de compilación y luego analizar solo los cambios. Para hacer esto, use el siguiente conjunto de comandos:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
Los informes inferidos se pueden ver con el comando InferTraceBugs.
infer run -- gradle build inferTraceBugs
Proyecto Infer Foundation
Infer de Facebook se basa en dos nuevos métodos matemáticos:
lógica de separación y
bi-abducción .
Una característica clave de la lógica de separación es la posibilidad de razonamiento local. Apareció debido a la presencia en las declaraciones de conectivos espaciales entre las partes del montón. En este caso, no es necesario considerar la cantidad total de memoria en cada etapa.
El elemento principal de la lógica de separación es el operador * (y por separado), que se denomina conexión de división. La fórmula X↦Y ∗ Y↦X puede leerse como "X apunta a Y, y por separado Y apunta a X", que es muy similar a cómo funcionan los punteros de memoria.
En el contexto de Infer Bi-abduction, puede verse como un método de inferencia lógica que permite a la plataforma detectar propiedades con respecto al comportamiento de partes independientes del código de la aplicación. Bi-abduction juntos muestra antiframes (partes faltantes del estado) y marcos (aquellas partes que no se ven afectadas por la operación). Matemáticamente, el problema de la bi-abducción se expresa usando la siguiente sintaxis: A ∗? Antiframe⊢B ∗? Marco.
En Infer from Facebook, el método permite derivar las especificaciones previas / posteriores del código limpio, siempre que conozcamos las especificaciones para primitivas en un nivel básico de código.
La creación de FI fue posible gracias al análisis del trabajo de especialistas en aprendizaje automático, que se llevó a cabo durante muchos años. En el curso del trabajo en Infer, se publicaron los siguientes artículos clave para todo el campo:
Hasta ahora, Infer solo se puede utilizar para aplicaciones móviles. Pero algunos de sus principios se aplican a aplicaciones de propósito general. Quizás en el futuro las posibilidades de Infer se amplíen, y con su ayuda los desarrolladores podrán analizar aplicaciones de escritorio o de servidor.
Skillbox recomienda: