Vor einigen Tagen hat sich das Facebook-Engineering-Team hervorgetan - es wurde mit dem
einflussreichsten POPL-Papierpreis ausgezeichnet . Unter Spezialisten für maschinelles Lernen ist dies sehr ehrenwert. Der Preis wurde für die Arbeit der
Analyse der
kompositorischen Form mittels Bi-Abduktion verliehen , die die Nuancen von Project Infer enthüllt. Das Projekt selbst wurde entwickelt, um Fehler im Code einer mobilen Anwendung vor ihrer Bereitstellung zu erkennen und zu beseitigen.
Fehler in der Software für mobile Geräte sind sowohl für Entwickler als auch für Benutzer sehr teuer. Zum einen ist die Erkennung eines Problems in einer Anwendung, die sich bereits in Verzeichnissen befindet, für jeden Spezialisten ein Albtraum. Natürlich wird Software getestet, die Arbeit von Programmen wird nach bestimmten Vorlagen überprüft. In den meisten Fällen können Entwickler jedoch nicht alles vorhersehen, und nach der Bereitstellung werden Fehler in der Anwendung erkannt.
Wir erinnern Sie daran: Für alle Leser von „Habr“ - ein Rabatt von 10.000 Rubel bei der Anmeldung für einen Skillbox-Kurs mit dem Promo-Code „Habr“.
Skillbox empfiehlt: Der Python Data Analyst Online-Kurs.
Project Infer scannt den Code mobiler Anwendungen und ermöglicht es Ihnen, alle Arten von Problemen zu finden, deren Muster in der Datenbank gespeichert sind (und die ständig aktualisiert werden). Das Projekt selbst wurde vor drei Jahren vorgestellt. Fast unmittelbar nach der Ankündigung öffnete Facebook den Code, wonach er in Unternehmen wie Amazon Web Services, Spotify und Uber verwendet wurde.
Wie funktioniert es
Project Infer verwendet einen speziellen Satz von Algorithmen, um die Funktionsweise des Codes zu analysieren. Der Quellcode einer großen Anwendung kann Millionen von Kombinationen enthalten, die zu Fehlern führen können. Herkömmliche Code-Analyseverfahren können nicht dazu beitragen, alles zu erkennen. Inferable from Facebook, Self-Learning, erweitert seine Basis, sodass Sie mit dem Projekt viele Probleme im Code erkennen können.
Im Allgemeinen kann der Facebook-Infer-Prozess in zwei Phasen unterteilt werden: Datenerfassung und -analyse. Der Lebenszyklus ist ebenfalls in zwei Teile unterteilt: global und differentiell.
In der Datenerfassungsphase übersetzt Infer den Quellcode in seine eigene Sprache. Die Analysephase ist der Untersuchung der kleinsten Details der Codestruktur gewidmet, die möglicherweise zum Auftreten eines Fehlers führen können. Wenn Infer auf eine bereits bekannte Kombination von Faktoren stößt, die als Fehlermuster identifiziert wurden, wird die Analyse für eine bestimmte Methode oder Funktion gestoppt, andere Methoden und Funktionen werden jedoch weiterhin analysiert. Hier ist ein Beispiel für Infer.
Unter dem Gesichtspunkt der Ausführung kann Infer in zwei Modalitäten arbeiten - Global und Differential, wie oben erwähnt. Im ersten Fall analysiert Infer alle Dateien. Für ein Projekt, das mit Gradle kompiliert wird, wird Infer mit dem Befehl gestartet
infer run -- gradle build
Der differenzielle Prozess wird in inkrementellen Build-Systemen verwendet, die für mobile Anwendungen spezifisch sind. In diesem Fall müssen Sie zuerst die Erfassung von Infer-Daten starten, um alle Kompilierungsbefehle abzurufen, und dann nur die Änderungen analysieren. Verwenden Sie dazu die folgenden Befehle:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
Infer-Berichte können mit dem Befehl InferTraceBugs angezeigt werden.
infer run -- gradle build inferTraceBugs
Project Infer Foundation
Facebooks Infer basiert auf zwei neuen mathematischen Methoden:
Trennungslogik und
Bi-Abduktion .
Ein Schlüsselmerkmal der Trennungslogik ist die Möglichkeit des lokalen Denkens. Es erschien aufgrund des Vorhandenseins von räumlichen Verbindungen zwischen den Teilen des Haufens in den Aussagen. In diesem Fall muss nicht in jeder Phase die gesamte Speichermenge berücksichtigt werden.
Das Hauptelement der Trennungslogik ist der Operator * (und separat), der als Aufteilungsverbindung bezeichnet wird. Die Formel X↦Y ∗ Y↦X kann als „X zeigt auf Y und separat zeigt Y auf X“ gelesen werden, was der Funktionsweise von Speicherzeigern sehr ähnlich ist.
Im Kontext der Infer Bi-Abduktion kann dies als logische Inferenzmethode angesehen werden, mit der die Plattform Eigenschaften hinsichtlich des Verhaltens unabhängiger Teile des Anwendungscodes erkennen kann. Bei der Bi-Abduktion werden zusammen Antiframes (fehlende Teile des Zustands) und Frames (Teile, die von der Operation nicht betroffen sind) angezeigt. Mathematisch wird das Bi-Abduktionsproblem mit der folgenden Syntax ausgedrückt: A ∗? Antiframe⊢B ∗? Rahmen.
Bei Infer from Facebook ermöglicht die Methode, die Pre / Post-Spezifikationen aus sauberem Code abzuleiten, vorausgesetzt, wir kennen die Spezifikationen für Grundelemente auf einer grundlegenden Codeebene.
Die Schaffung von FI wurde durch die langjährige Analyse der Arbeit von Spezialisten für maschinelles Lernen ermöglicht. Im Rahmen der Arbeit an Infer wurden folgende Schlüsselartikel für das gesamte Gebiet veröffentlicht:
- Analyse der Zusammensetzungsform mittels Bi-Abduktion . Nur für diese Arbeit wurde ein Preis erhalten, der oben erwähnt wurde. Die Arbeit führt den Leser in die kompositorische Analyse der Form ein. Dies ist eine Ergänzung zur herkömmlichen Formanalyse, die es ermöglicht, die Methode zur Analyse des Anwendungsquellcodes anzuwenden.
- Eine lokale Formanalyse basierend auf der Trennungslogik : In diesem Artikel wird die Trennungslogik als Mechanismus zur Analyse des Anwendungsquellcodes beschrieben. Die Autoren zeigen die Möglichkeit, einzelne Zellen in einem Speicherhaufen zu untersuchen, ohne den gesamten Haufen als Ganzes zu untersuchen. Daher bilden bestimmte Zellen eine verknüpfte Liste ohne vollständige Analyse.
- Smallfoot: Modulare automatische Überprüfung der Behauptung mit Trennungslogik : In diesem Dokument wird der Facebook Infer-Vorgänger Smallfoot beschrieben.
- AL: Eine neue deklarative Sprache zum Erkennen von Fehlern mit Infer : AL ermöglicht es jedem Entwickler, neue Prüfer zu entwerfen, ohne die innere Küche von Infer vollständig zu verstehen. AL ist eine deklarative Sprache.
- Schnelle Fortschritte bei der Softwareüberprüfung : Schließlich ein Artikel, der zeigt, wie Facebook Project Infer für seine eigenen Anforderungen verwendet. Das Dokument beschreibt, wie Facebook-Entwickler Infer in ihren Entwicklungsprozess integriert haben, um statische Analysen für mobile Apps wie Instagram, Facebook Messenger und Facebook-Apps für Android und iOS bereitzustellen.
Bisher kann Infer nur für mobile Anwendungen verwendet werden. Einige seiner Grundsätze gelten jedoch für Allzweckanwendungen. Vielleicht werden die Möglichkeiten von Infer in Zukunft größer und mit seiner Hilfe können Entwickler Desktop- oder Serveranwendungen analysieren.
Skillbox empfiehlt: