Meta telah mengirimkan lebih dari 100.000 perbaikan bug yang tertangkap oleh static analyzer sebelum kode tersebut sampai ke pengguna. Tool tersebut bernama Infer, bersifat open source, dan tidak menjalankan kode Anda. Ia membacanya, membangun model matematis dari apa yang bisa dilakukan kode, dan membuktikan bahwa hal-hal buruk tertentu tidak bisa terjadi. Atau ia menemukan jalur di mana hal tersebut bisa terjadi.

Tekniknya adalah abstract interpretation. Terdengar akademis karena memang begitu. Patrick Cousot dan Radhia Cousot menemukannya pada tahun 1970-an sebagai cara untuk menalar tentang program tanpa mengeksekusinya. Tim Meta, yang dipimpin oleh Peter O’Hearn, mengambil teori tersebut dan membuatnya cukup cepat untuk menganalisis jutaan baris kode mobile dan server dalam hitungan menit. Hasilnya adalah tool yang menemukan null pointer dereference, memory leak, resource leak, dan race condition pada saat diff.

Masalahnya: dynamic testing tidak bisa mencakup apa yang tidak Anda pikirkan untuk dijalankan

Unit test memeriksa satu jalur melalui kode Anda. Integration test memeriksa beberapa jalur lagi. Tetapi fungsi dengan lima conditional dan dua loop memiliki ratusan jalur, dan sebagian besar tidak pernah dieksekusi dalam test suite.

Dynamic testing, menjalankan kode, hanya bisa menemukan bug pada jalur yang benar-benar Anda eksekusi. Static analysis menemukan bug pada jalur yang tidak pernah Anda pikirkan. Ini adalah perbedaan antara memeriksa rumah Anda dari penyusup dengan berjalan di ruangan menggunakan senter, dan memeriksanya dengan membuktikan bahwa semua pintu dan jendela terkunci.

Tantangannya adalah membuktikan hal-hal tentang program nyata itu sulit. Program nyata memiliki loop, rekursi, alokasi heap, dan concurrency. Anda tidak bisa menghitung setiap state. Abstract interpretation memecahkan ini dengan melakukan aproksimasi.

Apa yang sebenarnya dimaksud dengan abstract interpretation

Abstract interpretation bekerja dengan menjalankan program Anda pada nilai-nilai abstrak, bukan nilai-nilai konkret.

Dalam eksekusi normal, variabel x mungkin memiliki integer 42. Dalam abstract interpretation, x mungkin memiliki nilai abstrak “positif”. Analisis tidak tahu bahwa x adalah 42. Ia tahu bahwa x lebih besar dari nol. Itu cukup untuk membuktikan bahwa x / y tidak akan membagi dengan nol jika y juga positif. Itu tidak cukup untuk membuktikan bahwa x == 42. Abstract interpretation mempertukarkan presisi dengan computability.

Kumpulan nilai-nilai abstrak disebut abstract domain. Domain paling sederhana adalah sign domain: setiap variabel negatif, nol, positif, atau tidak diketahui. Domain yang lebih kompleks melacak ranges, pointer, atau apakah lokasi memori telah dibebaskan. Analisis mengulangi program, menerapkan versi abstrak dari setiap operasi, hingga state abstrak berhenti berubah. Pada saat itu, ia telah menemukan fixed point, sebuah aproksimasi dari setiap state konkret yang mungkin di setiap titik program.

Loop adalah bagian yang sulit. Sebuah loop mungkin berjalan nol kali, sekali, atau satu miliar kali. Analyzer tidak bisa meng-unroll-nya satu miliar kali. Sebaliknya, ia menerapkan widening operator yang melompat ke over-approximation. Jika sebuah variabel bertambah satu setiap iterasi, analyzer mungkin melebar nilai abstraknya dari “positif” menjadi “non-negatif” dan berhenti di sana. Ia kehilangan batas yang tepat, tetapi mempertahankan properti yang penting untuk pembuktian.

Bagaimana Infer menggunakan bi-abduction untuk menganalisis prosedur secara modular

Abstract interpretation tradisional menganalisis seluruh program sebagai satu kesatuan. Itu tidak scalable untuk aplikasi mobile dengan satu juta baris kode. Infer memecahkan ini dengan teknik yang disebut bi-abduction.

Bi-abduction memungkinkan Infer menganalisis satu fungsi pada satu waktu. Ketika Infer menganalisis sebuah fungsi, ia menemukan dua hal: preconditions yang harus berlaku agar fungsi tersebut aman, dan postconditions yang dijamin oleh fungsi tersebut. Ini diinfer secara otomatis, tidak ditulis oleh programmer.

Berikut adalah contoh konkret. Misalkan Infer melihat fungsi C ini:

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

Infer menginfer bahwa greet memerlukan p untuk non-null. Itu adalah precondition. Ia juga menginfer bahwa greet tidak membebaskan p atau memodifikasi state yang terlihat. Itu adalah postcondition. Ketika fungsi lain memanggil greet, Infer memeriksa caller terhadap precondition yang diinfer. Jika caller mungkin melewatkan null, Infer melaporkan bug.

Mesin bi-abduction bekerja melalui symbolic execution atas separation logic. Separation logic memungkinkan Infer menalar tentang kepemilikan heap: fungsi mana yang memiliki memori mana, dan apakah memori tersebut telah dibebaskan. Inilah yang membuat Infer baik dalam menemukan null dereference dan memory leak di C, C++, Objective-C, dan Java.

Apa yang ditangkap Infer dan apa yang terlewat

Infer bukanlah linter tujuan umum. Ia menargetkan kelas bug tertentu yang mahal untuk ditemukan secara dinamis dan berbahaya di produksi.

Null pointer dereference. Infer melacak apakah setiap pointer pasti null, pasti non-null, atau mungkin null. Dereferensi pointer yang mungkin-null memicu laporan. Di Java dan Objective-C, ini menangkap tipe crash yang paling umum.

Memory leak. Infer menggunakan separation logic untuk melacak kepemilikan heap. Jika fungsi mengalokasikan memori dan tidak membebaskannya atau mengembalikannya ke caller, Infer melaporkan kebocoran. Ini sangat berharga di codebase C dan C++ di mana kebocoran menumpuk selama minggu uptime.

Resource leak. File descriptor, socket, dan lock dilacak secara serupa. Jika fungsi membuka file dan kembali tanpa menutupnya di setiap jalur, Infer melaporkan kebocoran.

Race condition. Module RacerD dari Infer menganalisis concurrency di Java. Ia melacak thread mana yang mengakses field mana dan apakah akses tersebut dilindungi oleh lock. Dua thread mengakses field yang sama tanpa sinkronisasi merupakan race.

Infer tidak menangkap semuanya. Ia melewatkan bug yang memerlukan penalaran tentang presisi numerik, konten string, atau pola aliasing yang kompleks. Ia juga secara desain unsound: ia mungkin melewatkan bug untuk menjaga false positive tetap rendah. Static analyzer yang menangis serigala di setiap diff akan dinonaktifkan. Deployment internal Meta menjaga tingkat false positive Infer di bawah 10%, itulah sebabnya developer benar-benar bertindak berdasarkan laporannya.

Menjalankan Infer di kode Anda sendiri

Infer bersifat open source dan mendukung C, C++, Objective-C, Java, dan (secara eksperimental) Rust dan Swift. Cara termudah untuk mencobanya adalah pada proyek Java atau C.

Instal Infer melalui Homebrew atau Docker:

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

Untuk proyek Java menggunakan Maven:

infer run -- mvn compile

Untuk proyek C menggunakan Make:

infer run -- make

Infer mengompilasi kode Anda, membangun control-flow graph, dan menjalankan analisis. Outputnya adalah kumpulan laporan bug dengan nama file, nomor baris, dan precondition yang diinfer yang dilanggar.

Berikut adalah contoh minimal C yang akan ditandai oleh Infer:

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

Menjalankan infer run -- cc leak.c menghasilkan:

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer juga menangkap null dereference dalam contoh ini:

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

Tunggu, sebenarnya Infer tidak akan melaporkan yang di atas. Fungsi print_length menangani argumen null dengan aman. Infer hanya melaporkan ketika dereferensi terjadi pada pointer yang mungkin null tanpa pemeriksaan. Berikut adalah yang akan memicu:

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

Infer melacak jalur dari call_unsafe melalui unsafe_print dan melaporkan bahwa s adalah null ketika s[0] dievaluasi.

Trade-off: kecepatan versus presisi

Desain modular Infer membuatnya cukup cepat untuk berjalan di setiap pull request di Meta. Tetapi modularitas memperkenalkan aproksimasi. Ketika Infer menganalisis fungsi, ia tidak mengetahui calling context yang tepat. Ia menginfer preconditions yang konservatif, artinya mungkin lebih kuat dari yang diperlukan. Precondition yang lebih kuat berarti lebih sedikit bug yang dilaporkan di call site, tetapi juga lebih sedikit false positive.

Ini adalah ketegangan sentral dalam static analysis. Analyzer yang sound melaporkan setiap bug, tetapi menenggelamkan Anda dalam false positive. Analyzer yang unsound seperti Infer membuat developer senang dengan hanya melaporkan bug yang ia yakini. Bug yang terlewat adalah biaya adopsi.

Mesin bi-abduction Infer juga kesulitan dengan global state dan callback yang kompleks. Jika kode Java Anda melewatkan inner class anonim ke executor, Infer mungkin kehilangan jejak thread mana yang menjalankan metode mana. RacerD menangani pola umum tetapi melewatkan race yang halus melibatkan condition variables atau atomic fields.

Kapan mengadopsi static analysis dan kapan melewatkannya

Anda harus mempertimbangkan Infer jika Anda mengirimkan kode native, aplikasi mobile, atau kode server dalam bahasa keluarga C atau Java. Bug yang ditemukannya — null dereference, leak, race — adalah yang tepat menyebabkan crash produksi dan kerentanan keamanan.

Anda tidak boleh mengharapkan Infer untuk menggantikan test suite Anda. Static analysis dan dynamic testing saling melengkapi. Test memverifikasi bahwa kode Anda melakukan apa yang Anda maksudkan dengan input yang Anda pilih. Static analysis memverifikasi bahwa kode Anda tidak melakukan apa yang Anda larang dengan input apa pun.

Jika codebase Anda berada di Python, Ruby, atau JavaScript, Infer bukan tool yang tepat. Bahasa-bahasa ini kekurangan informasi tipe statis yang Infer gunakan untuk membangun model abstraknya. Untuk bahasa dinamis, type checker seperti mypy atau pyright menangkap kelas kesalahan yang berbeda.

Kesimpulan

100.000 perbaikan bug Meta bukanlah angka pemasaran. Mereka adalah output dari tool yang berjalan di setiap diff, menganalisis kode tanpa mengeksekusinya, dan melaporkan bug yang tidak akan tertangkap oleh test apa pun. Teknik yang mendasarinya, abstract interpretation, sudah berusia beberapa dekade. Pencapaian rekayasa adalah membuatnya cukup cepat dan presisi sehingga developer tidak mematikannya.

Anda tidak memerlukan infrastruktur Meta untuk mendapat manfaat. Instal Infer, arahkan ke sistem build Anda, dan jalankan pada module yang membuat Anda takut. Module manajemen memori, lapisan concurrency, batas interop C. Perbaiki kebocoran dan null dereference yang ditemukannya. Kemudian tambahkan ke CI dan jaga agar jumlah bug tidak bertambah.

Abstract interpretation bukanlah sihir. Ini adalah matematika yang diterapkan pada kode, dengan semua aproksimasi dan trade-off yang menyertainya. Tetapi ini adalah matematika yang menemukan bug nyata di codebase nyata, dan itu membuatnya layak untuk diketahui.