charon

Patinir, E., 1515-1524, lansekap dengan Charon melintasi styx [minyak di atas kayu]. Museo del Prado, Madrid. Sumber

Charon

Charon bertindak sebagai antarmuka antara kompiler RustC dan proyek verifikasi program. Tujuannya adalah untuk memproses peti karat dan mengubahnya menjadi file yang mudah ditangani dengan verifikasi program. Ini diimplementasikan sebagai driver khusus untuk kompiler RustC.

Charon, dalam mitologi Yunani, seorang lelaki tua yang membawa jiwa -jiwa orang yang meninggal Accross the Styx, sebuah sungai yang memisahkan dunia orang yang hidup dari dunia orang mati. Dalam konteks saat ini, Charon memungkinkan kita untuk beralih dari dunia program karat ke dunia verifikasi formal.

Kami terbuka untuk kontribusi ! Silakan hubungi kami sehingga kami dapat mengoordinasikan diri kami, jika Anda bersedia berkontribusi. Untuk tujuan ini Anda dapat bergabung dengan Zulip.

Llbc

Charon mengkonversi kode miR ke ULLBC (kalkulus pinjaman tingkat rendah yang tidak terstruktur) kemudian ke LLBC. Kedua ASTS dapat di -output oleh Charon.

ULLBC adalah mir yang sedikit disederhanakan, di mana kami mencoba menghapus redudansi sebanyak mungkin. Misalnya, kami secara drastis menyederhanakan representasi konstanta yang berasal dari kompiler karat.

LLBC adalah ULLBC di mana kami merestrukturisasi aliran kontrol dengan loop, if ... then ... else ... , dll. Alih-alih gotos. Akibatnya, kami menggabungkan pernyataan MIR dan terminator menjadi satu jenis pernyataan LLBC. Kami juga melakukan beberapa modifikasi tambahan, beberapa di antaranya tercantum di bawah ini:

Komentar : Sebagian besar transformasi yang mengubah miR ke ULLBC kemudian LLBC diimplementasikan dengan menggunakan mikro-pass. Tergantung pada kebutuhan, kita bisa membuat mereka opsional dan mengendalikannya dengan bendera. Jika Anda ingin tahu lebih banyak tentang detailnya, lihat translate di src/driver.rs , yang menerapkan mikro-pass satu demi satu.

Komentar : Jika Anda ingin mengetahui detail lengkap (u) llbc, lihat: types.rs , values.rs , expressions.rs , ullbc_ast.rs dan llbc_ast.rs .

AST yang diekstraksi diekstraksi dalam file .ullbc dan .llbc (menggunakan format JSON). Kami mengekstrak seluruh peti dalam satu file.

Struktur proyek

• charon : Implementasi karat.
• charon-ml : Perpustakaan ML. Memberikan utilitas untuk mengambil dan memanipulasi AST di OCAML (deserialisasi, pencetakan, dll.).
• tests dan tests-polonius : Tes Direktori File. tests-polonius berisi kode yang membutuhkan pemeriksa pinjaman Polonius.

Instalasi & Bangun

Pertama -tama Anda harus menginstal rustup .

Saat Charon diatur dengan Cargo, Rustup akan secara otomatis mengunduh dan menginstal paket yang tepat saat membangun proyek. Jika Anda hanya ingin membangun proyek karat (di ./charon ), cukup jalankan make build-charon-rust di direktori teratas.

Jika Anda juga ingin membangun perpustakaan ML (di ./charon-ml ), Anda harus menginstal OCAML dan dependensi yang tepat.

Kami menyarankan Anda untuk mengikuti instruksi itu, dan menginstal OPAM di jalan (instruksi yang sama).

Untuk Charon-ML, kami menggunakan OCAML 4.13.1 : opam switch create 4.13.1+options

Ketergantungan dapat diinstal dengan perintah berikut:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

Anda kemudian dapat menjalankan make build-charon-ml untuk membangun perpustakaan ML, atau bahkan hanya make untuk membangun seluruh proyek (Rust dan OCAML). Akhirnya, Anda dapat menjalankan tes dengan make test .

Atau, Anda dapat menggunakan Nix dan melakukan nix develop (atau menggunakan https://direnv.net/ dan direnv allow ) dan semua dependensi harus tersedia.

Dokumentasi

Anda dapat mengakses dokumentasi karat secara online.

Anda juga dapat menjalankan make untuk menghasilkan dokumentasi secara lokal. Ini akan menghasilkan dokumentasi yang dapat diakses dari doc-rust.html (untuk proyek karat) dan doc-ml.html (untuk perpustakaan ML).

Penggunaan

Untuk menjalankan Charon, Anda harus menjalankan Binary Charon dari dalam peti yang ingin Anda kompilasi, seolah -olah Anda ingin membangun peti dengan cargo build . Charon Executable terletak di bin/charon .

Charon akan membangun peti dan ketergantungannya, lalu mengekstrak ast. Charon menyediakan berbagai opsi dan bendera untuk mengubah perilakunya: Anda dapat menampilkan dokumentasi terperinci dengan --help . Secara khusus, Anda dapat mencetak LLBC yang dihasilkan oleh Charon dengan --print-llbc .

Jika ada file Charon.toml di root proyek Anda, Charon juga akan mengambil opsi darinya. File mendukung opsi yang sama di antarmuka CLI, kecuali untuk opsi yang berhubungan dengan input/output seperti --print-llbc . Contoh Charon.toml :

[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ]

Komentar : Karena Charon dikompilasi dengan Rust Nigthly (ini adalah persyaratan untuk mengimplementasikan pengemudi RustC), itu akan membangun peti Anda dengan karat setiap malam. Anda dapat menemukan versi malam yang disematkan untuk Charon di rust-toolchain.template .