Beberapa hari yang lalu, tim teknik Facebook unggul - dianugerahi
Penghargaan Kertas Paling Berpengaruh . Di antara spesialis pembelajaran mesin, ini sangat terhormat. Penghargaan tersebut diberikan untuk karya
Analisis Bentuk Komposisi oleh Sarana Penculikan , yang mengungkapkan nuansa Project Infer. Proyek itu sendiri dirancang untuk mendeteksi dan menghilangkan bug dalam kode aplikasi seluler sebelum penerapannya.
Bug dalam perangkat lunak untuk perangkat seluler sangat mahal bagi pengembang dan pengguna. Adapun yang pertama, deteksi masalah dalam aplikasi yang sudah ada di direktori adalah mimpi buruk bagi spesialis. Tentu saja, perangkat lunak diuji, pekerjaan program diperiksa sesuai dengan templat tertentu. Tetapi lebih sering, pengembang tidak dapat memperkirakan segalanya, dan bug dalam aplikasi terdeteksi setelah penyebaran.
Kami mengingatkan Anda: untuk semua pembaca "Habr" - diskon 10.000 rubel saat mendaftar untuk kursus Skillbox apa pun menggunakan kode promo "Habr".
Skillbox merekomendasikan: Kursus Online Analis Data Python .
Project Infer memindai kode aplikasi seluler dan memungkinkan Anda menemukan semua jenis masalah, pola yang disimpan dalam basis data (dan diperbarui setiap saat). Proyek itu sendiri dipresentasikan tiga tahun lalu. Hampir segera setelah pengumuman, Facebook membuka kode, setelah itu mulai digunakan di perusahaan-perusahaan seperti Amazon Web Services, Spotify dan Uber.
Bagaimana cara kerjanya?
Project Infer menggunakan seperangkat algoritma khusus untuk menganalisis operasi kode. Mungkin ada jutaan kombinasi dalam kode sumber aplikasi besar apa pun yang dapat menyebabkan kesalahan. Prosedur analisis kode tradisional tidak dapat membantu mendeteksi semuanya. Infer dari Facebook, belajar mandiri, memperluas basisnya, sehingga proyek ini memungkinkan Anda untuk mendeteksi banyak masalah dalam kode.
Secara umum, proses Facebook Infer dapat dibagi menjadi dua tahap: pengumpulan dan analisis data. Siklus hidup juga dibagi menjadi dua bagian: global dan diferensial.
Dalam fase pengumpulan data, Infer menerjemahkan kode sumber ke dalam bahasanya sendiri. Fase analisis dikhususkan untuk mempelajari rincian terkecil dari struktur kode, yang berpotensi menyebabkan munculnya kesalahan. Jika Infer menemukan kombinasi faktor yang sudah dikenal yang diidentifikasi sebagai pola kesalahan, analisis berhenti untuk metode atau fungsi tertentu, tetapi metode dan fungsi lain terus dianalisis. Ini adalah contoh dari Infer.
Dari sudut pandang pelaksanaan, Infer dapat bekerja dalam dua modalitas - Global dan Diferensial, seperti yang disebutkan di atas. Dalam kasus pertama, Infer menganalisis semua file. Untuk proyek yang mengkompilasi menggunakan Gradle, Infer diluncurkan menggunakan perintah
infer run -- gradle build
Proses diferensial digunakan dalam sistem build tambahan yang khusus untuk aplikasi seluler. Dalam hal ini, Anda harus terlebih dahulu memulai pengumpulan data Infer untuk mendapatkan semua perintah kompilasi, dan kemudian hanya menganalisis perubahan. Untuk melakukan ini, gunakan serangkaian perintah berikut:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
Laporan infer dapat dilihat menggunakan perintah InferTraceBugs.
infer run -- gradle build inferTraceBugs
Yayasan Infer Proyek
Facebook's Infer didasarkan pada dua metode matematika baru:
pemisahan logika dan
penculikan dua .
Fitur utama dari logika pemisahan adalah kemungkinan penalaran lokal. Itu muncul karena adanya dalam pernyataan penghubung spasial antara bagian-bagian tumpukan. Dalam hal ini, tidak perlu mempertimbangkan seluruh jumlah memori pada setiap tahap.
Elemen utama dari logika pemisahan adalah operator * (dan secara terpisah), yang disebut koneksi pemisahan. Rumus X↦Y ∗ Y↦X dapat dibaca sebagai "X menunjuk ke Y, dan secara terpisah Y menunjuk ke X", yang sangat mirip dengan cara kerja pointer memori.
Dalam konteks Infer Bi-abduction, ini dapat dilihat sebagai metode inferensi logis yang memungkinkan platform untuk mendeteksi properti mengenai perilaku bagian independen dari kode aplikasi. Penculikan secara kolektif menampilkan antiframe (bagian yang hilang dari negara bagian) dan bingkai (bagian-bagian yang tidak terpengaruh oleh operasi). Secara matematis, masalah dua penculikan diekspresikan menggunakan sintaks berikut: A ∗? Antiframe⊢B ∗? Bingkai.
Di Infer dari Facebook, metode ini memungkinkan untuk memperoleh spesifikasi sebelum / sesudah dari kode bersih, asalkan kita tahu spesifikasi untuk primitif pada level kode dasar.
Penciptaan FI menjadi mungkin berkat analisis pekerjaan spesialis pembelajaran mesin, yang telah dilakukan selama bertahun-tahun. Dalam perjalanan kerja pada Infer, artikel-artikel kunci berikut diterbitkan untuk seluruh bidang:
- Analisis Bentuk Komposisi dengan Bi-abduksi . Hanya untuk pekerjaan ini hadiah telah diterima, yang disebutkan di atas. Karya memperkenalkan pembaca untuk analisis komposisi formulir. Ini merupakan tambahan untuk analisis bentuk tradisional, yang memungkinkan untuk menerapkan metode untuk menganalisis kode sumber aplikasi.
- Analisis Bentuk Lokal Berdasarkan Logika Pemisahan : Artikel ini menjelaskan logika pemisahan sebagai mekanisme untuk menganalisis kode sumber aplikasi. Para penulis menunjukkan kemungkinan mempelajari sel-sel individu dalam tumpukan memori, tanpa memeriksa seluruh tumpukan secara keseluruhan. Dengan demikian, sel-sel tertentu membuat daftar tertaut tanpa analisis penuh.
- Smallfoot: Pengecekan Pernyataan Otomatis Modular dengan Separation Logic : Makalah ini menjelaskan pendahulu Facebook Infer yang disebut Smallfoot.
- AL: Bahasa deklaratif baru untuk mendeteksi bug dengan Infer : AL memungkinkan pengembang untuk merancang catur baru tanpa pemahaman penuh tentang dapur bagian dalam Infer. AL adalah bahasa deklaratif.
- Bergerak Cepat dengan Verifikasi Perangkat Lunak : Terakhir, sebuah artikel yang mengungkapkan bagaimana Facebook menggunakan Project Infer untuk kebutuhannya sendiri. Dokumen tersebut berbicara tentang bagaimana pengembang Facebook mengintegrasikan Infer ke dalam proses pengembangan mereka untuk memberikan analisis statis untuk aplikasi seluler seperti Instagram, Facebook Messenger, dan aplikasi Facebook untuk Android dan iOS.
Sejauh ini, Infer hanya dapat digunakan untuk aplikasi seluler. Tetapi beberapa prinsipnya berlaku untuk aplikasi tujuan umum. Mungkin di masa depan kemungkinan Infer akan menjadi lebih luas, dan dengan bantuannya pengembang akan dapat menganalisis aplikasi desktop atau server.
Skillbox merekomendasikan: