قبل بضعة أيام ، تفوق فريق الهندسة على فيسبوك - حيث حصل على جائزة
POPL الأكثر نفوذاً . بين المتخصصين في التعلم الآلي ، هذا أمر مشرف جدًا. تم تقديم الجائزة لعمل
تحليل الشكل المركب من
قبل وسائل الاختطاف الثنائي ، والتي تكشف الفروق الدقيقة في مشروع Infer. تم تصميم المشروع نفسه للكشف عن الأخطاء وإزالتها في رمز تطبيق الهاتف المحمول قبل نشره.
الأخطاء في البرامج للأجهزة المحمولة غالية جدًا لكل من المطورين والمستخدمين. بالنسبة إلى الأول ، فإن اكتشاف مشكلة في تطبيق موجود بالفعل في الدلائل هو كابوس لأي متخصص. بالطبع ، يتم اختبار البرنامج ، ويتم فحص عمل البرامج وفقًا لقوالب معينة. ولكن في أغلب الأحيان ، لا يستطيع المطورون التنبؤ بكل شيء ، ويتم اكتشاف الأخطاء في التطبيق بعد النشر.
نذكرك: لجميع قراء "Habr" - خصم بقيمة 10،000 روبل عند التسجيل في أي دورة تدريبية في Skillbox باستخدام الرمز الترويجي "Habr".
توصي Skillbox بما يلي: دورة Python Data Analyst Online.
يقوم Project Infer بمسح رمز تطبيقات الأجهزة المحمولة ويسمح لك بالعثور على جميع أنواع المشكلات ، والتي يتم تخزين أنماطها في قاعدة البيانات (ويتم تحديثها طوال الوقت). تم تقديم المشروع نفسه قبل ثلاث سنوات. بعد الإعلان فورًا تقريبًا ، فتح Facebook الرمز ، وبعد ذلك بدأ استخدامه في شركات مثل Amazon Web Services و Spotify و Uber.
كيف يعمل؟
يستخدم Project Infer مجموعة متخصصة من الخوارزميات لتحليل تشغيل الكود. قد يكون هناك ملايين من التوليفات في الكود المصدري لأي تطبيق كبير قد يؤدي إلى حدوث أخطاء. لا يمكن أن تساعد إجراءات تحليل الشفرة التقليدية في اكتشاف كل شيء. إن Infer from Facebook ، التعلم الذاتي ، يقوم بتوسيع قاعدته ، لذلك يتيح لك المشروع اكتشاف الكثير من المشكلات في الكود.
بشكل عام ، يمكن تقسيم عملية Facebook Infer إلى مرحلتين: جمع البيانات وتحليلها. تنقسم دورة الحياة أيضًا إلى قسمين: عالمي وتفاضلي.
في مرحلة جمع البيانات ، يترجم Infer الكود المصدري إلى لغته الخاصة. يتم تخصيص مرحلة التحليل لدراسة أصغر تفاصيل بنية الكود ، والتي يمكن أن تؤدي إلى ظهور خطأ. إذا واجهت Infer مجموعة مألوفة بالفعل من العوامل المحددة كنمط خطأ ، فسيتوقف التحليل لطريقة أو وظيفة معينة ، ولكن يستمر تحليل الطرق والوظائف الأخرى. هنا مثال على Infer.
من وجهة نظر التنفيذ ، يمكن أن تعمل Infer بطريقتين - العالمية والتفاضلية ، كما ذكر أعلاه. في الحالة الأولى ، يحلل Infer جميع الملفات. بالنسبة لمشروع يجمع باستخدام Gradle ، يتم إطلاق Infer باستخدام الأمر
infer run -- gradle build
تُستخدم العملية التفاضلية في أنظمة الإنشاء التزايدي الخاصة بالتطبيقات المتنقلة. في هذه الحالة ، يجب أن تبدأ أولاً في جمع بيانات Infer للحصول على جميع أوامر التحويل البرمجي ، ثم تحليل التغييرات فقط. للقيام بذلك ، استخدم مجموعة الأوامر التالية:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
يمكن عرض تقارير Infer باستخدام أمر InferTraceBugs.
infer run -- gradle build inferTraceBugs
مشروع الاستنتاج
يعتمد Facebook Infer على طريقتين رياضيتين جديدتين:
منطق الانفصال والاختطاف الثنائي .
الميزة الرئيسية لمنطق الفصل هي إمكانية التفكير المحلي. يبدو بسبب وجود في الوصلات المكانية بين أجزاء الكومة. في هذه الحالة ، ليست هناك حاجة للنظر في حجم الذاكرة بالكامل في كل مرحلة.
العنصر الرئيسي لمنطق الفصل هو العامل * (وبشكل منفصل) ، والذي يسمى اتصال التقسيم. يمكن قراءة الصيغة X↦Y ∗ Y↦X كـ "X يشير إلى Y ، و Y يشير بشكل منفصل إلى X" ، وهو مشابه جدًا لكيفية عمل مؤشرات الذاكرة.
في سياق Infer Bi-abduction ، يمكن اعتباره طريقة استدلال منطقية تمكن النظام الأساسي من اكتشاف الخصائص المتعلقة بسلوك الأجزاء المستقلة من رمز التطبيق. يعرض الاختطاف الثنائي معًا إطارات مضادة (الأجزاء المفقودة من الحالة) وإطارات (الأجزاء التي لا تتأثر بالعملية). رياضيا ، يتم التعبير عن مشكلة ثنائية الاختطاف باستخدام بناء الجملة التالي: A ∗؟ Antiframe⊢B ∗؟ الإطار.
في Infer from Facebook ، تتيح الطريقة اشتقاق المواصفات المسبقة / المنشورة من الكود النظيف ، بشرط أن نعرف مواصفات المواد الأولية على مستوى أساسي من الكود.
أصبح إنشاء FI ممكنًا بفضل تحليل عمل أخصائيي التعلم الآلي ، والذي تم تنفيذه لسنوات عديدة. في سياق العمل على Infer ، تم نشر المقالات الرئيسية التالية للحقل بأكمله:
حتى الآن ، لا يمكن استخدام Infer إلا لتطبيقات الأجهزة المحمولة. لكن بعض مبادئه تنطبق على تطبيقات للأغراض العامة. ربما ستصبح إمكانيات Infer في المستقبل أكثر اتساعًا ، وسيتمكن مطورو البرامج من تحليل تطبيقات سطح المكتب أو الخادم.
توصي Skillbox بما يلي: