Il y a quelques jours, l'équipe d'ingénierie de Facebook a excellé - elle a reçu le prix du
papier POPL le
plus influent . Parmi les spécialistes de l'apprentissage automatique, c'est très honorable. Le prix a été décerné pour le travail d'
analyse de la forme compositionnelle par des moyens de bi-abduction , qui révèle les nuances du projet Infer. Le projet lui-même est conçu pour détecter et éliminer les bogues dans le code d'une application mobile avant son déploiement.
Les bogues dans les logiciels pour appareils mobiles sont très chers pour les développeurs et les utilisateurs. Quant au premier, la détection d'un problème dans une application déjà présente dans des répertoires est un cauchemar pour tout spécialiste. Bien sûr, les logiciels sont testés, le travail des programmes est vérifié selon certains modèles. Mais le plus souvent, les développeurs ne peuvent pas tout prévoir et les bogues de l'application sont détectés après le déploiement.
Nous vous rappelons: pour tous les lecteurs de «Habr» - une remise de 10 000 roubles lors de l'inscription à un cours Skillbox en utilisant le code promo «Habr».
Skillbox recommande: Le cours en ligne de Python Data Analyst .
Project Infer scanne le code des applications mobiles et vous permet de trouver toutes sortes de problèmes, dont les modèles sont stockés dans la base de données (et il est mis à jour tout le temps). Le projet lui-même a été présenté il y a trois ans. Presque immédiatement après l'annonce, Facebook a ouvert le code, après quoi il a commencé à être utilisé dans des sociétés telles que Amazon Web Services, Spotify et Uber.
Comment ça marche?
Project Infer utilise un ensemble d'algorithmes spécialisés pour analyser le fonctionnement du code. Il peut y avoir des millions de combinaisons dans le code source de toute grande application qui peuvent entraîner des erreurs. Les procédures traditionnelles d'analyse de code ne peuvent pas tout détecter. Déduire de Facebook, l'auto-apprentissage, élargit sa base, donc le projet vous permet de détecter beaucoup de problèmes dans le code.
D'une manière générale, le processus Facebook Infer peut être divisé en deux étapes: collecte et analyse des données. Le cycle de vie est également divisé en deux parties: global et différentiel.
Dans la phase de collecte des données, Infer traduit le code source dans sa propre langue. La phase d'analyse est consacrée à l'étude des moindres détails de la structure du code, ce qui peut potentiellement conduire à une erreur. Si Infer rencontre une combinaison déjà familière de facteurs identifiés comme un modèle d'erreur, l'analyse s'arrête pour une méthode ou une fonction particulière, mais d'autres méthodes et fonctions continuent d'être analysées. Voici un exemple d'Infer.
Du point de vue de l'exécution, Infer peut fonctionner selon deux modalités - globale et différentielle, comme mentionné ci-dessus. Dans le premier cas, Infer analyse tous les fichiers. Pour un projet qui se compile à l'aide de Gradle, Infer est lancé à l'aide de la commande
infer run -- gradle build
Le processus différentiel est utilisé dans les systèmes de construction incrémentielle spécifiques aux applications mobiles. Dans ce cas, vous devez d'abord démarrer la collecte de données Infer pour obtenir toutes les commandes de compilation, puis analyser uniquement les modifications. Pour ce faire, utilisez l'ensemble de commandes suivant:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
Les rapports Infer peuvent être affichés à l'aide de la commande InferTraceBugs.
infer run -- gradle build inferTraceBugs
Fondation Project Infer
Infer de Facebook est basé sur deux nouvelles méthodes mathématiques: la
logique de séparation et la
bi-abduction .
Une caractéristique clé de la logique de séparation est la possibilité d'un raisonnement local. Il est apparu en raison de la présence dans les déclarations de connecteurs spatiaux entre les parties du tas. Dans ce cas, il n'est pas nécessaire de considérer la totalité de la mémoire à chaque étape.
L'élément principal de la logique de séparation est l'opérateur * (et séparément), qui est appelé la connexion de séparation. La formule X↦Y ∗ Y↦X peut être lue comme «X pointe vers Y et séparément Y pointe vers X», ce qui est très similaire au fonctionnement des pointeurs de mémoire.
Dans le contexte d'Infer Bi-abduction, elle peut être considérée comme une méthode d'inférence logique qui permet à la plateforme de détecter des propriétés concernant le comportement de parties indépendantes du code d'application. La bi-abduction affiche collectivement les antiframes (parties manquantes de l'état) et les cadres (les parties qui ne sont pas affectées par l'opération). Mathématiquement, le problème de la bi-abduction est exprimé en utilisant la syntaxe suivante: A ∗? Antiframe⊢B ∗? Cadre.
Chez Infer de Facebook, la méthode permet de dériver les spécifications pré / post du code propre, à condition de connaître les spécifications des primitives à un niveau de code basique.
La création de FI a été rendue possible grâce à l'analyse du travail des spécialistes de l'apprentissage automatique, qui a été menée pendant de nombreuses années. Au cours des travaux sur Infer, les articles clés suivants ont été publiés pour l'ensemble du domaine:
Jusqu'à présent, Infer ne peut être utilisé que pour des applications mobiles. Mais certains de ses principes s'appliquent aux applications à usage général. Peut-être qu'à l'avenir, les possibilités d'Infer s'élargiront et, avec son aide, les développeurs pourront analyser les applications de bureau ou de serveur.
Skillbox recommande: