Dialyzer

Success typing, pembuatan PLT, dan cara membaca konflik dialyzer.

Daftar isi

Topik ini menjalankan dialyzer, alat analisis statis Erlang yang mencari kontradiksi nyata pada kode: spesifikasi yang tidak mungkin dipenuhi, cabang yang pasti gagal, dan pemanggilan dengan bentuk yang salah. Pembahasan mencakup cara kerja success typing, pembuatan PLT, dan cara membaca konfliknya dengan tenang.

Success typing dan sifatnya#

Dialyzer bekerja dengan teknik success typing: ia menghitung untuk setiap fungsi himpunan argumen dan hasil yang bisa terjadi sepanjang jalur eksekusi yang ada, lalu membandingkannya dengan spec dan pemanggilan antar fungsi. Temuan yang dilaporkan hanyalah kontradiksi yang pasti, yaitu kode yang tidak mungkin berjalan sesuai klaimnya. Akibatnya ada dua sisi. Sisi baiknya, hampir setiap temuan dialyzer adalah masalah nyata dan tidak ada alarm palsu. Sisi lainnya, dialyzer tidak mencantumkan pelanggaran yang mungkin saja tidak terjadi, sehingga laporan bersih bukan jaminan kode bebas bug. Dialyzer juga bekerja tanpa anotasi sama sekali, dan hasilnya semakin tajam bila typespec yang diberikan semakin lengkap.

Membangun PLT#

Analisis atas kode pengguna membutuhkan pemahaman atas pustaka bawaan, dan pemahaman itu disimpan dalam Persistent Lookup Table (PLT) yang dibangun sekali lalu dipakai berulang. Perintah berikut membangun PLT dari tiga aplikasi inti dan memakan waktu sekitar setengah menit pada mesin uji:

bash
# bangun PLT dari pustaka inti
dialyzer --build_plt --apps erts kernel stdlib
text Keluaran
done (warnings were emitted)
done in 0m39.08s

Baris warnings were emitted pada pembangunan PLT adalah catatan tentang pustaka bawaan itu sendiri dan bukan tentang kode pengguna. PLT tersimpan pada folder cache pengguna, diperiksa ulang setiap kali dialyzer dijalankan, dan diperbarui dengan --add_to_plt bila aplikasi lain ikut dianalisis. Modul yang dianalisis juga harus dikompilasi dengan informasi debug, yaitu opsi +debug_info yang sudah menjadi bawaan rebar3 melalui erl_opts.

Membaca konflik#

Modul berikut sengaja berisi satu pelanggaran: spec menjanjikan float, sedangkan operator div selalu menghasilkan bilangan bulat:

erlang Modul dengan spec yang tidak mungkin
-module(statistik_salah).
-export([rerata/1]).

-spec rerata([number()]) -> float().
rerata(Nilai) -> lists:sum(Nilai) div length(Nilai).

Hasil analisisnya terbaca sebagai berikut:

text Keluaran
statistik_salah.erl:4:2: Invalid type specification for function statistik_salah:rerata/1.
 The success typing is statistik_salah:rerata
          ([number()]) -> integer()
 But the spec is statistik_salah:rerata
          ([number()]) -> float()
 The return types do not overlap

Konfliknya dibedah tiga lapis: lokasi baris, success typing yang dihitung dialyzer, yaitu hasilnya pasti integer, dan spec yang menjanjikan float. Kalimat penutupnya menyatakan kedua himpunan tidak bertumpang tindih sama sekali, sehingga tidak ada pemanggilan yang bisa memenuhi klaim spec. Perbaikannya pun jelas, yaitu mengganti div dengan / agar hasilnya benar-benar float, dan modul statistik_tipe pada topik typespec lolos analisis yang sama tanpa temuan. Cara membaca ini berlaku untuk seluruh kelas temuan: pahami dulu apa yang dihitung dialyzer, bandingkan dengan klaim yang melanggar, lalu putuskan sisi mana yang salah.

Modul yang bersih mengembalikan kalimat yang jelas juga:

text Keluaran
  Proceeding with analysis... done in 0m0.10s
done (passed successfully)

PLT pada proyek rebar3#

Proyek rebar3 menyederhanakan seluruh urutan di atas menjadi satu perintah, yaitu rebar3 dialyzer. Plugin dialyzer bawaan rebar3 membangun PLT dari pustaka bawaan dan dependensi proyek secara otomatis, mengompilasi modul dengan debug_info, dan menjalankan analisis atas seluruh aplikasi proyek, dengan hasil tersimpan di cache agar berjalan berikutnya cepat. Opsi pada rebar.config seperti {dialyzer, [{plt_apps, ...}, {warnings, [...]}]} menyetel lingkup PLT dan daftar peringatan yang dianggap fatal, sehingga tim dapat menetapkan kontrak bersama bahwa dialyzer harus bersih sebelum kode bergabung. Tanpa rebar3, urutan manualnya tetap sama: bangun PLT, kompilasi dengan debug_info, dan jalankan dialyzer atas berkas beam yang dihasilkan.

Temuan di luar spec#

Spec hanyalah salah satu sumber temuan. Dialyzer juga melaporkan cabang pencocokan pola yang tidak mungkin dicapai, pemanggilan fungsi yang tidak ada, dan nilai kembalian yang selalu dibuang, dengan nama peringatan masing-masing yang dapat disetel lewat opsi baris perintah. Temuan tanpa spec pun tetap berguna, karena success typing menghitung dari kode itu sendiri. Spec hanya membuat klaim yang dibandingkan menjadi eksplisit. Kebiasaan yang sehat adalah menaikkan tingkat keparahan temuan secara bertahap: bersihkan spec yang keliru terlebih dahulu, lalu anggap temuan dialyzer sebagai pemecah build, karena kontradiksi yang pasti hampir selalu berarti masalah nyata.

Ringkasan#

  • Success typing menghitung argumen dan hasil yang mungkin, dan dialyzer hanya melaporkan kontradiksi yang pasti.
  • Tidak ada temuan bukan jaminan bersih, tetapi temuan yang ada nyaris selalu masalah nyata.
  • PLT menyimpan analisis pustaka bawaan, dibangun sekali dengan –build_plt dan dipakai berulang.
  • Konflik dibaca tiga lapis: success typing, spec yang melanggar, dan kalimat yang menyatakan hubungan keduanya.

Referensi#