charon

Patinir ، E. ، 1515-1524 ، المناظر الطبيعية مع Charon عبور styx [زيت على الخشب]. متحف ديل برادو ، مدريد. مصدر

تشارون

يعمل Charon كواجهة بين برنامج التحويل البرمجي Rustc ومشاريع التحقق من البرنامج. الغرض منه هو معالجة الصناديق الصدأ وتحويلها إلى ملفات سهلة التعامل مع التحقق من البرنامج. يتم تنفيذه كبرنامج سائق مخصص لمرجم Rustc.

تشارون هو ، في الأساطير اليونانية ، رجل عجوز يحمل أرواح المتوفى يتراكم على Styx ، وهو نهر يفصل عالم الأحياء عن عالم الموتى. في السياق الحالي ، يسمح لنا Charon بالانتقال من عالم برامج الصدأ إلى عالم التحقق الرسمي.

نحن منفتحون على المساهمات ! يرجى الاتصال بنا حتى نتمكن من تنسيق أنفسنا ، إذا كنت على استعداد للمساهمة. لهذا الغرض ، يمكنك الانضمام إلى Zulip.

LLBC

يقوم Charon بتحويل رمز MIR إلى ULLBC (حساب حساب الاقتراض منخفض المستوى غير منظم) ثم إلى LLBC. يمكن أن يكون كل من ASTS الإخراج بواسطة Charon.

ULLBC هو مير مبسط قليلاً ، حيث نحاول إزالة أكبر قدر ممكن من التكرار. على سبيل المثال ، نقوم بتبسيط تمثيل الثوابت القادم بشكل كبير من برنامج التحويل البرمجي للصدأ.

LLBC هو ULLBC حيث قمنا بإعادة هيكلة تدفق التحكم بالحلقات ، if ... then ... else ... ، إلخ. بدلاً من GOTOS. وبالتالي ، فإننا ندمج عبارات MIR والمحترفين في نوع بيان LLBC واحد. نقوم أيضًا بإجراء بعض التعديلات الإضافية ، بعضها مدرج أدناه:

ملاحظة : يتم تنفيذ معظم التحولات التي تحول miR إلى ULLBC ثم LLBC عن طريق المسارات الصغيرة. اعتمادًا على الحاجة ، يمكننا أن نجعلها اختياريًا والتحكم فيها مع الأعلام. إذا كنت ترغب في معرفة المزيد عن التفاصيل ، راجع translate في src/driver.rs ، والتي تطبق المسارات الصغيرة واحدة تلو الأخرى.

ملاحظة : إذا كنت ترغب في معرفة التفاصيل الكاملة لـ (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 Borrow Checker.

التثبيت والبناء

تحتاج أولاً إلى تثبيت rustup .

نظرًا لأن Charon تم إعداده باستخدام Cargo ، فسيقوم Rustup بتنزيل وتثبيت الحزم المناسبة تلقائيًا عند إنشاء المشروع. إذا كنت ترغب فقط في إنشاء مشروع Rust (في ./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 والقيام nix develop (أو استخدام https://direnv.net/ direnv allow ) ويجب توفير جميع التبعيات.

الوثائق

يمكنك الوصول إلى وثائق الصدأ عبر الإنترنت.

يمكنك أيضًا تشغيل make لإنشاء الوثائق محليًا. ستقوم بإنشاء وثائق يمكن الوصول إليها من doc-rust.html (لمشروع Rust) و doc-ml.html (لمكتبة ML).

الاستخدام

لتشغيل Charon ، يجب عليك تشغيل The Charon Binary من داخل الصندوق الذي تريد تجميعه ، كما لو كنت تريد بناء الصندوق باستخدام cargo build . يقع Charon Adlextible في bin/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) ، فسيقوم ببناء قفصك مع الصدأ الليلي. يمكنك العثور على النسخة الليلية المثبتة لشارون في rust-toolchain.template .