lart

Lart: Alat abstraksi dan penyempurnaan LLVM

LART = Alat abstraksi & penyempurnaan LLVM. Tujuan dari alat ini adalah untuk memberikan transformasi LLVM-ke-LLVM yang menerapkan berbagai abstraksi program. Dalam hal set instruksi, program yang dihasilkan adalah program LLVM konkret normal yang dapat dieksekusi dan dianalisis. Informasi tambahan tentang abstraksi yang berlaku untuk program (fragmen) dimasukkan menggunakan fungsi intrinsik LLVM khusus dan node metadata LLVM. LART menyediakan kedua alat mandiri yang memproses file bitcode on-disk, serta kerangka kerja yang dapat diintegrasikan ke dalam alat berbasis LLVM yang kompleks. Motivasi utama di belakang LART adalah untuk menyediakan "preprosesor" untuk checker model berbasis LLVM dan alat analisis lainnya, menyederhanakan pekerjaan mereka dengan mengurangi ukuran masalah tanpa mengorbankan kesehatan analisis. Abstraksi yang diimplementasikan oleh LART biasanya disempurnakan berdasarkan instruksi spesifik tentang "bagian" abstraksi mana yang terlalu kasar (abstraksi yang terlalu kasar akan membuat kesalahan palsu yang terlihat untuk analisis selanjutnya tetapi tidak ada dalam program asli).

Abstraksi untuk bitcode LLVM

Tujuan dari seluruh latihan adalah untuk mengabstraksi informasi dari bitcode LLVM, membuat analisis selanjutnya lebih efisien (dengan mengorbankan beberapa presisi). Untuk tujuan ini, kita terutama harus dapat mengkodekan pilihan non-deterministik dalam program LLVM, yang dapat dilakukan hanya melalui fungsi tujuan khusus (mirip dengan intrinsik LLVM). Fungsi ini bernama @lart.choice , mengambil sepasang batas sebagai argumen dan non-deterministik mengembalikan nilai yang jatuh di antara batas-batas tersebut.

Ekstensi ini ke semantik LLVM perlu dikenali oleh alat hilir. Ini juga satu -satunya penyimpangan penting dari bitcode LLVM standar. Banyak alat analisis sudah akan menerapkan mekanisme yang sama, baik secara internal atau bahkan dengan antarmuka eksternal. Alat mengadaptasi tanpa dukungan untuk @lart.choice untuk bekerja dengan LART biasanya sangat mudah.

Ada fungsi tujuan khusus lainnya yang disediakan oleh LART, yaitu @lart.meta.* Keluarga, tetapi sejauh menyangkut instruksi ini, sebagian besar alat akan dapat dengan aman mengabaikan keberadaan mereka, seperti halnya dengan panggilan @llvm.dbg.* yang ada. Transformasi program diharapkan untuk mempertahankan panggilan tersebut jika LART dipanggil untuk memperbaiki abstraksi (setiap abstraksi yang disediakan oleh LART dilengkapi dengan prosedur penyempurnaan yang sesuai, yang sering perlu menemukan panggilan @lart.meta yang dimasukkan oleh abstraksi).

Sementara sebagian besar mesin abstraksi tradisional berfungsi sebagai penerjemah, abstraksi juga dapat "dikompilasi" menjadi program. Alih-alih (kembali) menafsirkan instruksi secara simbolis, instruksi simbolik dapat dikompilasi. Dalam hal abstraksi predikat, bitcode yang dihasilkan akan secara langsung memanipulasi dan menggunakan penilaian predikat alih -alih variabel beton. Seperti yang dijelaskan di atas, perbedaan penting adalah bahwa bitcode perlu membuat pilihan non-deterministik, karena beberapa predikat mungkin memiliki penilaian yang tidak ditentukan (keduanya benar dan salah). Beberapa variabel bahkan dapat diabstraksi sepenuhnya, dan semua tes pada variabel tersebut akan menghasilkan jawaban ya dan tidak.

Membangun

Gunakan atau ulangi pengaturan dari ./devcontainer/Dockerfile untuk saat ini.

Kemudian gunakan:

 ./scripts/build.sh

Jalankan kompiler

 ./build/bin/lartcc <domain> <compiler arguments> in.c

MEMILIH

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

Tes

 lit -v build/test

Catatan: build/lartcc/lartcc harus memiliki izin yang lebih besar.