Facebooks statischer Analyzer vereinfacht frühzeitiges Erkennen von Bugs

Facebook Infer goes Open Source
Kommentare

Gerade bei Mobile Code ist es wichtig, mögliche Bugs möglichst früh auszumerzen – am besten, bevor der Code überhaupt geshipped wird. Denn während im Web Bug-Fixes sofort an den Server ausgegeben werden können, dauert der Vorgang auf Mobile seine Zeit und setzt voraus, dass User ihre Apps updaten.

Facebook nutzt darum seinen statischen Programm-Analyser Facebook Infer, um Bugs zu identifizieren, bevor Mobile Code veröffentlicht wird – und hat ihn nun Open Source zugänglich gemacht. In einem Blogpost erklären Christiano Calcagno, Dino Distefano und Peter O’Hearn, was hinter Infer steckt und welche Zukunftspläne man im Bereich Programm-Verifizierung bei Facebook hat.

Facebook Infer – ein statischer Programm-Analyzer zur besseren Erkennung von Bugs

Facebook Infer ist ein statischer Programm-Analyzer – also ein automatisiertes Tool, das Bugs in Quellcode ausfindig macht, indem es Programme scannt, ohne sie auch auszuführen. Damit komplimentieren sie vor allem das dynamische Testing, bei dem Software-Teile individuell auf ihre Richtigkeit überprüft werden. Der besondere Vorteil eines statischen Programm-Analyzers ist dabei, dass mehrere – und manchmal sogar alle – Flows gleichzeitig geprüft werden können.

Das Facebook-Team nutzt Facebook Infer so beispielsweise zur internen Analyse der Facebook-Apps für iOS und Android, dem Facebook Messenger und Instagram. Dabei benachrichtigt der Analyzer derzeit vor allem bei Problemen, die von Null-Pointer-Zugriffen sowie Ressourcen- und Memory-Leaks verursacht werden. Momentan wird Infer auf dem Android- und Objective-C-Code für die Facebook-Apps ausgeführt, allerdings kann das Tool auch C-Projekte und Java-Code außerhalb von Android analysieren; zudem sollen die Fähigkeiten künftig noch erweitert werden.

Facebook Infer nutzt mathematische Logik

Facebook Infer macht sich mathematische Logik zu Nutze, mit der das Tool Schlussfolgerungen zur Ausführung eines Programms anstellt, was gerade bei umfangreichen Apps nicht unproblematisch ist. Dazu kommt, dass der Code ständig weiterentwickelt wird, während trotzdem erwartet wird, dass das genutzte Tool innerhalb kurzer Zeit Code-Modifikationen erkennt. Um dieses Problem zu lösen, nutzt Facebook Infer zwei mathematische Techniken: Separationslogik und Bi-Abduction. Durch deren Kombination kann der Analyzer komplizierte Probleme in der Modifikation lösen – und das in wenigen Minuten!

Damit wird Entwicklern die Arbeit deutlich vereinfacht, weil sich das Tool problemlos in den Workflow einfügen lässt. Durch das Open Sourcing des Analyzers profitieren sicher viele Entwickler und können zuverlässig funktionieren Code schneller entwickeln. Mehr Informationen zu Facebook Infer bieten der zugehörige Blogpost sowie die Projektseite. Dort steht das Tool auch zum Download zur Verfügung.
Aufmacherbild: Environmental health workers are fogging to control dengue during sunset von Shutterstock / Urheberrecht: mrfiza

Unsere Redaktion empfiehlt:

Relevante Beiträge

Meinungen zu diesem Beitrag

X
- Gib Deinen Standort ein -
- or -