nathan-luevano/silicaالتحقق التفاضلي الشامل لجميع ترميزات تعليمات AArch64 البالغ عددها 4.3 مليار.
خريطة كاملة لمواضع اختلاف مفككات ترميز AArch64 مع المعمارية.
يمرّ Silica على كل كلمة تعليمة A64 ممكنة من أصل 4,294,967,296 كلمة، ويقارن Capstone وLLVM وUnicorn مع مواصفة Arm القابلة للقراءة آليًا، ويحوّل الفروقات إلى أدلة قابلة لإعادة الإنتاج.
أن يقول مفكك التجميع "صالح" أمر سهل. أما معرفة ما إذا كان محقًّا فأمر أصعب. معظم الاختبارات التفاضلية يمكنها أن تكشف أن الأدوات تختلف، لكنها لا تستطيع تحديد الإجابة الصحيحة دون مرجع مستقل. يستخدم Silica إصدار Arm بصيغة XML كذلك المرجع.
يتيح A64 تجربة بالغة الشمول: فالتعليمات بعرض 32 بت بالضبط، ما يجعل فضاء الترميز بأكمله منتهيًا وعمليًّا للتعداد. يستفيد Silica من هذه الخاصية. نتائج الصلاحية أدناه ليست تقديرًا ولا حملة اختبار عشوائي؛ بل تم فحص كل كلمة ممكنة.
تستخدم هذه النتائج ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). قُسِّم
المسح إلى 256 شريحة مُتحقَّقًا منها بشكل مستقل تغطي كامل ترميزات 2³².
| النتيجة | العدد | النسبة من الفضاء الكامل |
|---|---|---|
| مُخصَّصة وفق مواصفة Arm | 1,799,435,776 | 41.9% |
| غير مُخصَّصة وفق مواصفة Arm | 2,495,531,520 | 58.1% |
| اختلافات الصلاحية المكتشفة | 723,801,678 | 16.9% |
| حالات إعادة إنتاج دنيا جاهزة للمنبع الأصلي | 10 | — |
التوافق مع المواصفة بشأن ما إذا كان الترميز صالحًا:
| مفكك الترميز | التوافق | تمثيل بصري |
|---|---|---|
| Capstone | 84.8% | █████████████████████████░░░░░ |
| LLVM | 87.6% | ██████████████████████████░░░░ |
| Unicorn | 88.3% | ██████████████████████████░░░░ |
لفجوة الصلاحية الكبيرة أسباب قابلة للتحديد. يختبر Unicorn الصلاحية عبر
تنفيذ التعليمة ومراقبة المصائد، بينما تفكّك المراجع الأخرى الترميز دون
تنفيذ. كما تتأثر مناطق قليلة بشروط UNDEFINED وقت فك الترميز لا يقيّمها
مرجع المواصفة المُصرَّف. يسجّل Silica هذه القيود بدلًا من تنعيمها من النتيجة.
مقارنة أسماء التعليمات والمعاملات المُصيَّرة أغلى بكثير من تسجيل بت صلاحية. لذلك يقيّم Silica النص على عيّنة حتمية من 1,000,000 كلمة مسحوبة من 1,266,064,016 مرشحًا تعتبرها المراجع الأربعة جميعًا ترميزًا صالحًا. هذه نتيجة معتمدة على عيّنة، وتُبقى عمدًا منفصلة عن أرقام الصلاحية الشاملة.
| التصنيف داخل العيّنة | السجلات | النسبة |
|---|---|---|
| اختلاف في تصيير المعاملات | 862,648 | 86.3% |
| تطبيع يحتاج مراجعة | 137,352 | 13.7% |
العيّنة مفيدة لتحديد أعمال التطبيع والعرض؛ وهي لا تدّعي تغطية شاملة لكل تصيير نصي.
ينتج محرك المسح مجموعة بيانات بحثية ضخمة. silica-scope هو تطبيق الطرفية المرافق لجعل هذه المجموعة في متناول المستخدم. يفتح دليل مخرجات Silica مكتملًا ويتيح لك تصفح المقاييس الرئيسية، وفحص خريطة الترميز ذات الشرائح الـ256، وتصفية الاختلافات، والبحث عن أي كلمة 32 بت، وقراءة حالات إعادة الإنتاج الجاهزة للتقديم.
ثبّته من PyPI باستخدام Python 3.11 أو أحدث:
pipx install silica-scope
ثم شغّله من نسخة Silica محلية أو وجّهه إلى دليل مخرجات:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope قارئ بلغة Python خالصة دون تبعيات مفككات ترميز أصلية. وهو لا
يشغّل المسح الشامل، ويتعامل مع مجموعة المخرجات المنشورة الأصغر في المستودع
بسلاسة. راجع دليل قارئ الطرفية للاطلاع على الألواح ومفاتيح
التحكم وخيارات اكتشاف المخرجات.
flowchart LR
XML["Arm XML specification"] --> SPEC["compiled spec oracle"]
SPEC --> SWEEP["parallel 32-bit sweep"]
CAP["Capstone"] --> SWEEP
LLVM["LLVM"] --> SWEEP
UNI["Unicorn"] --> SWEEP
SWEEP --> MAP["validity bitmaps"]
MAP --> DIFF["exhaustive XOR comparison"]
DIFF --> CORPUS["classified disagreement corpus"]
CORPUS --> OUT["metrics · reproducers · result hash"]المسار عالي الحجم مكتوب بلغة Rust ويستدعي كل مفكك ترميز داخل العملية نفسها. يخزّن بتًّا واحدًا لكل ترميز لكل مرجع، ما يبقي المقارنة الشاملة مدمجة ويجعل الاختلاف عملية مباشرة على الخرائط النقطية. تُنسب الأعطال بالتنصيف إلى كلمة التعليمة الدقيقة.
تتولى Python تصريف المواصفة والتطبيع وإعداد التقارير وطبقة التحقق المستقلة. مخططات المخرجات وقواعد أخذ العيّنات والقيود المعروفة موثّقة في docs/formats.md.
أنشئ البيئة المثبّتة وتحقّق من توفر المدخلات المحلية المطلوبة:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
لا تُضمَّن مواصفة Arm بصيغة XML بسبب ترخيصها. يبلّغ silica doctor عن المكان
الذي يتوقع Silica العثور عليها فيه وعن أي متطلبات أساسية أخرى مفقودة.
لتشغيل خط الأنابيب الكامل من نسخة محلية مُهيّأة:
make all
هذا مسح كامل لـ2³²، وليس اختبارًا سريعًا. ينتج المرجع المُصرَّف وسجلات الشرائح وخرائط الصلاحية النقطية ومجموعة الاختلافات والمقاييس المنشورة وحالات إعادة الإنتاج وبصمة نتيجة SHA-256 مستقرة.
يعيد سبعة مُتحقِّقين مستقلين حساب ادعاءات المشروع من المخرجات الخام. وهم لا يثقون بملخص مُولَّد، ولكل مُتحقِّق حالة اختبار تُثبت أنه يكشف العيب الذي يحمي منه. لا توجد حالة متخطّاة أو مؤقتة.
micromamba run -p ./.venv silica verify
إصدارات مفككات الترميز المثبّتة وبصمة نتيجة مُعاد حسابها حديثًا تجعل التشغيلات المنفصلة قابلة للمقارنة. أهداف التحقق وحالتها الحالية مسجّلة في GOALS.yml.
يغطي Silica حاليًا فك ترميز A64 الأساسي وAdvanced SIMD. أما SVE وSVE2 وSME وA32/T32 وRISC-V ورحلات ذهاب وإياب عبر المُجمِّع واختبار التنفيذ العام فخارج دراسة الإصدار الأول.
أقرب مصدر إلهام هو Sandsifter، الذي يستكشف فضاء التعليمات متغيرة الطول في x86. يطبّق Silica الروح ذاتها من التشكيك المنهجي على AArch64، حيث تتيح الترميزات ثابتة العرض ومواصفة مستقلة مقارنة كاملة ومُحكَّمة.
Apache 2.0 — راجع LICENSE