Abstract interpretation adalah istilah yang membuat insinyur menutup tab. Terdengar seperti sesuatu yang membutuhkan satu semester teori kisi untuk dipahami. Sebagian besar pengembang mengasumsikannya hidup di makalah penelitian, bukan di pull request.

Asumsi itu mahal. Abstract interpretation hanyalah cara untuk membuktikan hal-hal tentang kode Anda tanpa menjalankannya. Alat yang dibangun di atasnya dapat menangkap null dereference, kebocoran memori, dan race condition yang terlewat oleh pemeriksa tipe dan linter. Kabar baiknya: Anda tidak perlu memahami koneksi Galois untuk menggunakannya. Anda memerlukan konfigurasi CI yang berfungsi dan sekitar dua puluh menit.

Apa yang sebenarnya dilakukan abstract interpretation

Intinya, abstract interpretation adalah teknik pembuktian otomatis. Ini menjalankan program Anda, tetapi alih-alih menggunakan nilai nyata, ia menggunakan perkiraan.

Pertimbangkan variabel x. Dalam eksekusi normal, x mungkin memegang 42. Dalam abstract interpretation, x mungkin memegang “integer positif”. Analisis melacak nilai-nilai abstrak ini melalui setiap jalur kode yang mungkin. Jika dapat membuktikan bahwa tidak ada jalur yang mengarah ke null dereference, Anda aman. Jika menemukan jalur di mana x bisa menjadi null di situs dereferensi, ia melaporkan bug potensial.

Keajaibannya adalah ini berfungsi untuk loop dan kondisional. Analisis menghitung fixed point atas keadaan abstrak sehingga dapat menalar tentang iterasi tak terbatas tanpa benar-benar beriterasi selamanya. Inilah yang membedakan abstract interpretation dari alat eksekusi simbolik yang lebih sederhana yang kesulitan dengan loop.

Infer dari Facebook adalah alat produksi yang paling mudah diakses yang menggunakan teknik ini. Ini menganalisis Java, C, C++, dan Objective-C dengan mengompilasi kode Anda menjadi representasi perantara dan menjalankan abstract interpretation komposisional pada setiap fungsi. Infer menyimpan hasil per fungsi dalam cache, sehingga build inkremental cepat. Itulah rahasia yang membuatnya layak di CI.

Mengapa linter Anda tidak cukup

Linter melihat sintaks. Pemeriksa tipe melihat tipe. Abstract interpretation melihat perilaku lintas jalur.

Linter dapat menandai bahwa Anda lupa memeriksa null. Pemeriksa tipe dapat menegakkan bahwa fungsi mengembalikan Optional<T>. Tetapi tidak satu pun yang dapat secara andal menangkap bahwa Anda mendereferensikan pointer di baris 47 setelah serangkaian cabang kompleks di mana satu jalur membuatnya tidak diinisialisasi. Abstract interpretation melacak kemungkinan status pointer tersebut melalui setiap titik cabang dan penggabungan.

Trade-off-nya adalah noise. Abstract interpretation menghasilkan false positive. Ini dapat melaporkan null dereference yang logika bisnis Anda jamin tidak akan pernah terjadi. Analisis tidak mengetahui invarian Anda. Ia hanya tahu apa yang kode secara harfiah izinkan.

Pemeriksa default Infer disetel untuk menjaga tingkat false positive tetap rendah, sekitar 10-15% untuk sebagian besar codebase. Itu lebih tinggi dari pemeriksa tipe, tetapi bug yang ditemukannya sering kali adalah yang lolos dari tinjauan kode dan pengujian.

Menambahkan Infer ke pipeline CI Anda

Anda tidak perlu membangun Infer dari sumber. Facebook menerbitkan image Docker. Berikut adalah alur kerja GitHub Actions yang berfungsi yang menganalisis proyek Java:

# .github/workflows/infer.yml
name: Abstract Interpretation

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Run Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "mvn compile"
            --
            mvn compile

      - name: Upload report
        uses: actions/upload-artifact@v4
        with:
          name: infer-report
          path: infer-out/report.json

Untuk proyek Node.js atau Python, tukar perintah build. Infer tidak menganalisis JavaScript atau Python secara native, tetapi Anda dapat menjalankannya pada ekstensi C/C++ yang sering bergantung pada proyek tersebut. Jika Anda berada di lingkungan bahasa yang dikelola murni, Anda masih dapat mendapatkan analisis yang sensitif terhadap jalur dari alat seperti CodeQL atau SonarQube, meskipun mesin yang mendasarinya berbeda.

Untuk proyek C atau C++, pengaturannya bahkan lebih sederhana:

# .github/workflows/infer-cpp.yml
name: Infer C++ Analysis

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Build with Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "make"
            --
            make

Pola infer run --make-command mencegat panggilan compiler selama proses build normal Anda. Infer mengekstrak representasi perantara, menganalisanya, dan menulis hasil ke infer-out/. Artefak build aktual Anda tidak terpengaruh.

Membaca output dan menyesuaikan false positive

Infer menghasilkan temuan ke infer-out/report.json dan infer-out/report.txt yang dapat dibaca manusia. Temuan tipikal terlihat seperti ini:

src/parser.c:142: error: NULL_DEREFERENCE
  pointer `node` last assigned on line 138 could be null and is dereferenced at line 142, column 5

Pesan tersebut memberi tahu Anda variabelnya, di mana ditetapkan, dan di mana dereferensi terjadi. Anda dapat melacak jalur di editor Anda.

Jika Infer terlalu berisik, Anda dapat menekan pemeriksa tertentu atau menganotasi kode untuk melewati analisis:

// src/parser.c
// infer-ignore: the parent check guarantees node is non-null here
node->value = parsed;

Atau nonaktifkan pemeriksa tertentu secara global:

infer run --make-command "make" --no-bufferoverrun --

Pemeriksa buffer overrun sangat rentan terhadap false positive pada kode dengan aritmatika pointer yang kompleks. Saya biasanya menonaktifkannya pada codebase C warisan dan membiarkan pemeriksa null dereference dan kebocoran memori tetap aktif. Kedua pemeriksa tersebut menemukan bug nyata dengan tingkat yang membenarkan waktu peninjauan.

Trade-off waktu build

Abstract interpretation tidak gratis. Run Infer penuh pada proyek C++ berukuran menengah dapat memakan waktu 2-4x lebih lama dari build normal. Analisis inkremental membantu: pada run berikutnya, Infer hanya menganalisis ulang fungsi yang berubah dan dependencynya. Dalam praktiknya, ini berarti build 10 menit mungkin menjadi 15-20 menit pada run CI bersih, tetapi 3-5 menit pada run inkremental.

Jika anggaran CI Anda ketat, jalankan Infer pada pull request tetapi tidak pada setiap push ke main. Atau jalankan setiap malam. Bug yang ditemukannya biasanya sepadan dengan latensi, tetapi frekuensi yang tepat bergantung pada toleransi tim Anda terhadap waktu CI.

Pilihan lain adalah menjalankan Infer secara lokal sebelum push. Image Docker yang sama berfungsi di mesin apa pun dengan Docker yang terinstal:

docker run --rm -v $(pwd):/workspace -w /workspace \
  ghcr.io/facebook/infer:main \
  infer run --make-command "make" --

Apa yang tidak ditangkap Infer

Infer bersifat komposisional. Ini menganalisis fungsi secara terisolasi dan menggunakan ringkasan untuk memodelkan caller dan callee. Ini membuatnya scalable, tetapi berarti bug lintas fungsi yang sensitif terhadap jalur yang memerlukan analisis grafik panggilan lengkap dapat lolos.

Ini juga tidak menemukan bug logika. Jika kode Anda mendereferensikan pointer dengan aman tetapi menggunakan nilai yang salah, Infer diam. Ini adalah pemeriksa keamanan, bukan oracle kebenaran.

Bug concurrency terbatas. Infer memiliki pemeriksa race condition, tetapi ini bersifat eksperimental dan menghasilkan cukup banyak false positive sehingga sebagian besar tim mematikannya.

Apa yang harus dilakukan selanjutnya

Mulailah dari yang kecil. Pilih satu proyek dengan bahasa yang dikompilasi dan tambahkan alur kerja GitHub Actions di atas. Biarkan berjalan pada beberapa pull request berikutnya. Tinjau temuan dengan tim Anda dan bangun daftar penekanan untuk noise.

Setelah seminggu, Anda akan merasakan apakah sinyalnya sepadan dengan waktu CI. Menurut pengalaman saya, run pertama pada codebase C atau Java yang ada selalu menemukan setidaknya satu null dereference yang terlewat oleh tinjauan kode. Itu biasanya cukup untuk membenarkan mempertahankannya.

Jika Anda ingin menyelami lebih dalam, dokumentasi Infer mencakup penulisan pemeriksa kustom dalam OCaml. Di situlah gelar PhD berguna. Untuk segala sesuatu yang lain, pemeriksa default dan image Docker sudah cukup.

FAQ

Apa itu abstract interpretation dalam istilah sederhana? Ini adalah teknik analisis statis yang memperkirakan bagaimana program Anda berperilaku untuk membuktikan properti seperti “pointer ini tidak pernah null” tanpa benar-benar mengeksekusi kode.

Apakah Infer gratis digunakan? Ya. Infer adalah open source di bawah lisensi MIT dan dikelola oleh Meta.

Bagaimana Infer dibandingkan dengan SonarQube? SonarQube menggunakan campuran pattern matching, taint analysis, dan beberapa analisis yang lebih dalam tergantung pada bahasa. Infer secara khusus dibangun di atas abstract interpretation dan sensitif terhadap jalur dengan cara yang biasanya tidak dilakukan SonarQube untuk C, C++, Java, dan Objective-C.

Bisakah saya menjalankan Infer pada JavaScript atau Python? Tidak secara langsung. Infer menganalisis bahasa yang dikompilasi. Untuk JavaScript dan Python, pertimbangkan CodeQL atau linter yang sadar tipe seperti ESLint dengan aturan ketat atau Pyright.

Apakah Infer memperlambat CI secara signifikan? Analisis lengkap memakan waktu 2-4x waktu build. Analisis inkremental pada pull request jauh lebih cepat, biasanya menambahkan beberapa menit.