charon

Patinir, E. , 1515-1524, ภูมิทัศน์กับ Charon ข้าม Styx [Oil on Wood] Museo del Prado, มาดริด แหล่งที่มา

ชรา

Charon ทำหน้าที่เป็นส่วนต่อประสานระหว่าง RustC Compiler และโครงการตรวจสอบโปรแกรม วัตถุประสงค์ของมันคือการประมวลผลลังสนิมและแปลงเป็นไฟล์ง่ายต่อการจัดการโดยโปรแกรมตรวจสอบโปรแกรม มันถูกนำไปใช้เป็นไดรเวอร์ที่กำหนดเองสำหรับคอมไพเลอร์ RustC

ชารอนอยู่ในตำนานเทพเจ้ากรีกชายชราที่ถือวิญญาณของผู้เสียชีวิตสะสม Styx แม่น้ำที่แยกโลกแห่งชีวิตจากโลกแห่งความตาย ในบริบทปัจจุบัน Charon ช่วยให้เราไปจากโลกแห่งโปรแกรมสนิมสู่โลกแห่งการตรวจสอบอย่างเป็นทางการ

เรา เปิดรับการบริจาค ! โปรดติดต่อเราเพื่อให้เราสามารถประสานงานตัวเองได้หากคุณเต็มใจที่จะมีส่วนร่วม เพื่อจุดประสงค์นี้คุณสามารถเข้าร่วม Zulip

LLBC

Charon แปลงรหัส MIR เป็น ULLBC (แคลคูลัสยืมระดับต่ำที่ไม่มีโครงสร้าง) จากนั้นเป็น LLBC AST ทั้งสองสามารถส่งออกโดย Charon

UllBC เป็น MIR ที่ง่ายขึ้นเล็กน้อยซึ่งเราพยายามลบความซ้ำซ้อนให้มากที่สุดเท่าที่จะทำได้ ตัวอย่างเช่นเราทำให้การเป็นตัวแทนของค่าคงที่ที่มาจากคอมไพเลอร์สนิมง่ายขึ้นอย่างมาก

LLBC คือ UllBc ที่เราปรับโครงสร้างการควบคุมด้วยลูป if ... then ... else ... ฯลฯ แทนที่จะเป็น gotos ดังนั้นเราจึงรวมคำสั่ง MIR และ TERMINATORS เข้ากับประเภทคำสั่ง LLBC เดียว นอกจากนี้เรายังทำการปรับเปลี่ยนเพิ่มเติมบางส่วนซึ่งบางรายการอยู่ในรายการด้านล่าง:

หมายเหตุ : การเปลี่ยนแปลงส่วนใหญ่ที่เปลี่ยน miR เป็น UllBC จากนั้น LLBC จะถูกนำไปใช้โดยใช้วิธีไมโครพาส ขึ้นอยู่กับความต้องการเราสามารถทำให้พวกเขาเป็นตัวเลือกและควบคุมพวกเขาด้วยธง หากคุณต้องการทราบข้อมูลเพิ่มเติมเกี่ยวกับรายละเอียดดู translate ใน src/driver.rs ซึ่งใช้ micro-passes หนึ่งหลังจากอื่น ๆ

หมายเหตุ : หากคุณต้องการทราบรายละเอียดทั้งหมดของ (U) LLBC ให้ดูที่: types.rs , values.rs , expressions.rs , ullbc_ast.rs และ llbc_ast.rs

AST ที่แยกออกมาจะถูกทำให้เป็นอนุกรมในไฟล์ .ullbc และ .llbc (ใช้รูปแบบ JSON) เราแยกลังทั้งหมดในไฟล์เดียว

โครงสร้างโครงการ

• charon : การใช้งานสนิม
• charon-ml : ห้องสมุด ML จัดเตรียมยูทิลิตี้เพื่อดึงและจัดการ AST ใน OCAML (deserialization, การพิมพ์ ฯลฯ )
• tests และ tests-polonius : ไดเรกทอรีไฟล์ทดสอบ tests-polonius มีรหัสที่ต้องใช้ตัวตรวจสอบ Polonius ยืม

การติดตั้งและสร้าง

ก่อนอื่นคุณต้องติดตั้ง rustup

เมื่อ Charon ถูกตั้งค่าด้วยสินค้า Rustup จะดาวน์โหลดและติดตั้งแพ็คเกจที่เหมาะสมโดยอัตโนมัติเมื่อสร้างโครงการ หากคุณต้องการสร้างโครงการสนิม (ใน ./charon ) เพียงแค่เรียกใช้ make build-charon-rust ในไดเรกทอรีด้านบน

หากคุณต้องการสร้างไลบรารี ML (ใน ./charon-ml ) คุณจะต้องติดตั้ง OCAML และการพึ่งพาที่เหมาะสม

เราขอแนะนำให้คุณทำตามคำแนะนำเหล่านั้นและติดตั้ง OPAM ระหว่างทาง (คำแนะนำเดียวกัน)

สำหรับ Charon-ML เราใช้ OCAML 4.13.1 : opam switch create 4.13.1+options

การพึ่งพาสามารถติดตั้งได้ด้วยคำสั่งต่อไปนี้:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

จากนั้นคุณสามารถเรียกใช้ make build-charon-ml เพื่อสร้างห้องสมุด ML หรือแม้แต่ make โครงการทั้งหมด (Rust และ Ocaml) ในที่สุดคุณสามารถเรียกใช้การทดสอบด้วย make test

หรือคุณสามารถใช้ nix และ do nix develop (หรือใช้ https://direnv.net/ และ direnv allow ) และควรมีการพึ่งพาทั้งหมด

เอกสาร

คุณสามารถเข้าถึงเอกสารสนิมออนไลน์

นอกจากนี้คุณยังสามารถเรียกใช้ make เพื่อสร้างเอกสารในพื้นที่ มันจะสร้างเอกสารที่สามารถเข้าถึงได้จาก doc-rust.html (สำหรับโครงการสนิม) และ doc-ml.html (สำหรับไลบรารี ML)

การใช้งาน

ในการเรียกใช้ Charon คุณควรเรียกใช้ Charon Binary จาก ภายใน ลังที่คุณต้องการรวบรวมราวกับว่าคุณต้องการสร้างลังด้วย cargo build Executable Charon ตั้งอยู่ที่ bin/charon

Charon จะสร้างลังและการพึ่งพาของมันจากนั้นแยก AST Charon มีตัวเลือกและธงต่าง ๆ เพื่อปรับแต่งพฤติกรรม: คุณสามารถแสดงเอกสารรายละเอียดด้วย --help โดยเฉพาะอย่างยิ่งคุณสามารถพิมพ์ LLBC ที่สร้างโดย Charon ด้วย --print-llbc

หากมีไฟล์ Charon.toml ที่รูทของโครงการของคุณ Charon จะใช้ตัวเลือกจากมันด้วย ไฟล์รองรับตัวเลือกเดียวกันที่อินเทอร์เฟซ CLI ยกเว้นตัวเลือกที่เกี่ยวข้องกับอินพุต/เอาต์พุตเช่น --print-llbc ตัวอย่าง Charon.toml :

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

หมายเหตุ : เนื่องจาก Charon ถูกรวบรวมด้วย Rust Nigthly (นี่เป็นข้อกำหนดในการใช้ไดรเวอร์ RustC) มันจะสร้างลังของคุณด้วยสนิมทุกคืน คุณสามารถค้นหาเวอร์ชันทุกคืนที่ตรึงไว้สำหรับ Charon ใน rust-toolchain.template