seahorn

عن

Seahorn هو إطار تحليل تلقائي للغات القائمة على LLVM. هذا الإصدار يجمع ضد LLVM 14.

بعض الميزات المدعومة

• تحليل ثابت قائم على التفسير التجريدي
• تحليل المؤشر الحساس للسياق القائم على التوحيد
• فحص النموذج المحدد المستند إلى SMT (أي التنفيذ الرمزي)
• فحص نموذج البرمجيات المستند إلى CHC (أي الاستدلال الثابت)
• أمثلة قابلة للتنفيذ (أي ، لا تقارير ، فقط الأخطاء!)

تم تطوير Seahorn في المقام الأول كإطار لإجراء البحوث في التحقق الآلي. توفر الأطر العديد من المكونات التي يمكن تجميعها بطرق متنوعة. ومع ذلك ، فهي ليست أداة تحليل ثابت "خارج الصندوق".

يتم توفير العديد من أدوات التحليل والأمثلة مع الإطار. نحن نبحث باستمرار عن تطبيقات جديدة ونقدم الدعم للمستخدمين الجدد. لمزيد من المعلومات حول ما يحدث ، تحقق من مدونةنا (المحدثة بشكل غير متكرر).

رخصة

يتم توزيع Seahorn تحت رخصة BSD معدلة. انظر الترخيص. txt للحصول على التفاصيل.

مقدمة

يوفر Seahorn نص Python يسمى sea للتفاعل مع المستخدمين. بالنظر إلى برنامج C مشروح مع التأكيدات ، يحتاج المستخدمون فقط إلى الكتابة: sea pf file.c

نتيجة sea-pf unsat إذا تمسك جميع التأكيدات ، sat إذا تم انتهاك أي من التأكيدات.

يخبر الخيار pf Seahorn بترجمة file.c إلى LLVM bitcode ، وإنشاء مجموعة من شروط التحقق (VCs) ، وأخيراً حلها. المحاليل الخلفية الرئيسية هو الفضاء.

يوفر الأمر pf ، من بين أمور أخرى ، الخيارات التالية:

• --show-invars : عرض الثوابات المحسوبة إذا كانت الإجابة unsat .

• --cex=FILE : يخزن مثال مضاد في FILE إذا تم sat الإجابة.

• -g : يجمع مع معلومات التصحيح لمزيد من الأمثلة المضادة للتتبع.

• --step=large : تشفير خطوة كبيرة. كل علاقة انتقالية تتوافق مع شظايا خالية من الحلقة.

• --step=small : ترميز خطوة صغيرة. كل علاقة انتقالية تتوافق مع كتلة أساسية.

• --track=reg : نموذج (عدد صحيح) يسجل فقط.

• --track=ptr : سجلات النماذج والمؤشرات (ولكن ليس محتوى الذاكرة)

• --track=mem : نموذج كل من العدادات والمؤشرات ومحتويات الذاكرة

• --inline : يحلّل البرنامج قبل التحقق

• --crab : حقن الثبات في spacer الناتجة عن الأداة القائمة على تفسير السلطعون. اقرأ هنا للحصول على تفاصيل حول جميع خيارات السلطعون (بادئة --crab ). يمكنك أن ترى أي ثنائيات يتم استنتاجها بواسطة Crab عن طريق كتابة خيار --log=crab .

• --bmc : استخدم محرك BMC.

sea pf هو خط أنابيب يدير أوامر متعددة. يمكن تشغيل الأجزاء الفردية من خط الأنابيب بشكل منفصل أيضًا:

1. sea fe file.c -o file.bc : يترجم Seahorn Frontend برنامج C إلى رمز LLVM المحسّن بما في ذلك التحول المختلط المختلط.

2. sea horn file.bc -o file.smt2 : Seahorn يولد شروط التحقق من file.bc ويخرجها إلى تنسيق SMT -LIB V2. يمكن للمستخدمين الاختيار بين أنماط الترميز المختلفة مع عدة مستويات من الدقة من خلال إضافة:

   • --step={small,large,fsmall,flarge} حيث يكون small الترميز خطوة صغيرة ، وترميز large في الحجم ، fsmall هو خطوة صغيرة تشفير الجمل التي تنتج قرن مسطح (أي ، أنها تولد نظام انتقال مع مسند واحد فقط) ، و flarge : تشفير large الشفرات المنتجة المنتجة.

   • --track={reg,ptr,mem} حيث reg فقط نماذج integer ، نماذج ptr reg و COONTER ، ونماذج mem ptr ومحتويات الذاكرة.

3. sea smt file.c -o file.smt2 : إنشاء CHC بتنسيق SMT -LIB2. هو الاسم المستعار للبحر sea fe يليه sea horn . sea pf هو الاسم المستعار ل sea smt --prove .

4. sea clp file.c -o file.clp : ينشئ CHC بتنسيق CLP.

5. sea lfe file.c -o file.ll : تشغيل الواجهة الأمامية القديمة

لرؤية جميع الأوامر ، اكتب sea --help . للاطلاع على خيارات لكل أمر فردي CMD (على سبيل المثال ، horn ) ، اكتب sea CMD --help (على سبيل المثال ، sea horn --help ).

تحليل ثابت مع التفسير التجريدي

استنتاج الثوابات الاستقرائية باستخدام السلطعون

Seahorn لا يستخدم السلطعون بشكل افتراضي. لتمكين السلطعون ، أضف الخيار --crab إلى أمر sea .

المترجم المجردة هو افتراضيًا داخل الجمعية ويستخدم مجال المناطق كمجال تجريدي رقمي. يجب أن تكون هذه الخيارات الافتراضية كافية للمستخدمين العاديين. للمطورين ، إذا كنت ترغب في استخدام مجالات مجردة أخرى ، فأنت بحاجة إلى:

1. ترجمة مع خيارات cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
2. قم بتشغيل sea مع الخيار- --crab-dom=DOM حيث يمكن أن يكون DOM :
   • int للفترات
   • term-int الفواصل مع وظائف غير مفهومة
   • boxes : لفترات فاصلة
   • oct للأوكتاجون
   • pk ل polyhedra

لاستخدام تحليل السلطعون بين المشكلات التي تحتاجها لتشغيل sea مع خيار- --crab-inter

بشكل افتراضي ، المترجم المجرد فقط أسباب حول متغيرات العددية (IE ، LLVM Regists). قم بتشغيل sea مع الخيارات- --crab-track=mem --crab-singleton-aliases=true للعقل حول محتويات الذاكرة.

كيفية استخدام الثبات الناتج عن السلطعون في الفاصل

السلطعون في الغالب غير حساس للمسار في حين أن الفضاء ، حلقة القرن لدينا ، حساسة للمسار. على الرغم من أن التحليلات غير الحساسة للمسار أكثر كفاءة ، إلا أن الحساسية المسار مطلوبة عادةً لإثبات خاصية الاهتمام. هذا يحفز قرارنا بتشغيل السلطعون الأول (إذا كان الخيار --crab ) ثم تمرير الثبات الذي تم إنشاؤه إلى الفضاء. يوجد حاليًا طريقتان لـ Spacer لاستخدام الثوابات التي تم إنشاؤها بواسطة Crab. خيار sea --horn-use-invs=VAL يخبر spacer كيفية استخدام تلك الثوابيات:

• إذا كان VAL مساوياً لـ bg ، فسيتم استخدام الثوابات فقط للمساعدة spacer في إثبات أن Lemma استقرائي.
• إذا كان VAL مساوياً always ، فإن السلوك يشبه bg ولكن بالإضافة إلى ذلك ، يتم استخدام الثبات أيضًا للمساعدة في spacer لمنع مثال مضاد.

القيمة الافتراضية هي bg . بالطبع ، إذا كان Crab يمكن أن يثبت أن البرنامج آمن ، فلا يتحمل الفاصل في أي تكلفة إضافية.

مواصفات الممتلكات

من المفترض أن تكون الخصائص تأكيدات. يوفر Seahorn sassert تأكيد ثابتة ، كما هو موضح في المثال التالي

 /* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();

int main ( void ) {
    int k = 1 ;
    int i = 1 ;
    int j = 0 ;
    int n = nd ();
    while ( i < n ) {
        j = 0 ;
        while ( j < i ) {
            k += ( i - j );
            j ++ ;
        }
        i ++ ;
    }
    sassert ( k >= n );
}

داخليًا ، يتبع Seahorn اتفاقية SV-Comp لمواقع الأخطاء الترميز عن طريق استدعاء إلى وظيفة الخطأ المعينة __VERIFIER_error() . يعود Seahorn unsat __VERIFIER_error() غير قابل للوصول ، ويعتبر البرنامج آمنًا. sat Seahorn عندما يمكن الوصول إلى __VERIFIER_error() والبرنامج غير آمن. يتم تعريف طريقة sassert() في seahorn/seahorn.h .

فحص الكود

بصرف النظر عن إثبات الخصائص أو إنتاج أمثلة مضادة ، يكون من المفيد في بعض الأحيان فحص الكود قيد التحليل للحصول على فكرة عن تعقيدها. لهذا ، يوفر Seahorn sea inspect القيادة. على سبيل المثال ، بالنظر إلى برنامج C ex.c نوع:

 sea inspect ex.c --sea-dsa=cs+t --mem-dot 

يتيح الخيار- --sea-dsa=cs+t تحليل SEA-DSA السياق الجديد ، الذي تم وصفه في FMCAD19. يقوم هذا الأمر بإنشاء ملف FUN.mem.dot لكل وظيفة FUN في برنامج الإدخال. لتصور الرسم البياني للوظيفة الرئيسية ، استخدم واجهة Web Graphivz ، أو الأوامر التالية:

$ dot -Tpdf main.mem.dot -o main.mem.pdf

مزيد من التفاصيل حول الرسوم البيانية للذاكرة موجودة في مستودع Seadsa: هنا.

استخدم sea inspect --help لرؤية جميع الخيارات. حاليا ، الخيارات المتاحة هي:

• sea inspect --profiler الظهر عدد الوظائف ، والكتل الأساسية ، والحلقات ، إلخ.
• sea inspect --mem-callgraph-dot يطبع لتنسيق الرسم dot للمكالمات الذي تم إنشاؤه بواسطة Seadsa.
• sea inspect --mem-callgraph-stats يطبع إلى الإخراج القياسي بعض الإحصائيات حول بناء الرسم البياني للمكالمات التي قام بها Seadsa.
• sea inspect --mem-smc-stats يطبع عدد الوصول إلى الذاكرة التي يمكن إثباتها من قبل Seadsa.

تثبيت

أسهل طريقة للبدء مع Seahorn هي عن طريق توزيع Docker.

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

ابدأ باستكشاف ما يمكن أن تفعله قيادة sea :

$ sea --help
$ sea pf --help

يتم تحديث العلامة nightly تلقائيًا يوميًا وتحتوي على أحدث إصدار تطوير. نحافظ على جميع العلامات الأخرى (التي تتطلب تحديثًا يدويًا) بشكل غير منتظم. تحقق من تواريخ DockerHub وقم بتسجيل مشكلة على Github إذا كانت قديمة جدًا.

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

يمكنك أيضًا التثبيت يدويًا بواسطة:

بعد الإرشادات الواردة في ملف Docker Dockerfile: docker/seahorn-builder.Dockerfile .

إذا لم ينجح هذا ، فتشغيل:

$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *

سيتم تثبيت الأوامر الثلاثة الأولى LLVM 14 ، وسيقوم الرابع بتثبيت Libpolly الذي تم حذفه بشكل خاطئ من LLVM 14 (ولكن مدرج في الإصدارات اللاحقة)

بعد ذلك ، اتبع التعليمات في ملف Docker أعلاه

منطقة المطور

المعلومات من هذه النقطة على المطورين فقط. إذا كنت ترغب في المساهمة في Seahorn ، فقم ببناء أدواتك الخاصة بناءً على ذلك ، أو مهتمًا فقط بكيفية عملها في الداخل ، أو الاستمرار في القراءة.

تعليمات التجميع

Seahorn يتطلب LLVM و Z3 و BOOST. تستمر الإصدارات الدقيقة للمكتبات في التغيير ، ولكن يتم استخدام Cmake Craft للتحقق من أن الإصدار الصحيح متاح.

لتحديد نسخة محددة من أي من التبعيات ، استخدم <PackageName>_ROOT و/أو <PackageName>_DIR (انظر Find_Package () للحصول على تفاصيل) Cmake Variables.

يتم تقسيم Seahorn إلى مكونات متعددة تعيش في مستودعات مختلفة (تحت منظمة Seahorn). تقوم عملية الإنشاء تلقائيًا بالتحقق من كل شيء عند الضرورة. للحصول على تعليمات البناء الحالية ، تحقق من نصوص CI.

هذه هي الخطوات العامة. لا تستخدمها. تابع القراءة للحصول على طريقة أفضل:

1. cd seahorn ; mkdir build ; cd build (يمكن أن يكون دليل الإنشاء أيضًا خارج دليل المصدر.)
2. cmake -DCMAKE_INSTALL_PREFIX=run ../ (التثبيت مطلوب! )
3. cmake --build . --target extra && cmake .. (مكونات Clones التي تعيش في مكان آخر)
4. cmake --build . --target crab && cmake .. (مكتبة Clones Crab)
5. cmake --build . --target install (بناء وتثبيت كل شيء تحت run )
6. cmake --build . --target test-all (اختبارات التشغيل)

ملاحظة : التثبيت الهدف مطلوب للاختبارات للعمل!

تعليمات تجميع أفضل

لتجربة التنمية المعززة:

1. استخدم clang
2. على Linux ، استخدم lld Linker
3. تشمل رموز التصحيح في بنيات الإصدار
4. استخدم النينجا
5. التصدير compile_commands.json

على Linux ، نقترح تكوين cmake التالي:

 $ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run 
      -DCMAKE_BUILD_TYPE=RelWithDebInfo 
      -DCMAKE_CXX_COMPILER="clang++-14" 
      -DCMAKE_C_COMPILER="clang-14" 
      -DSEA_ENABLE_LLD=ON  
      -DCMAKE_EXPORT_COMPILE_COMMANDS=1 
      ../ 
      -DZ3_ROOT=<Z3_ROOT> 
      -DLLVM_DIR=<LLMV_CMAKE_DIR> 
      -GNinja
$ (cd .. && ln -sf build/compile_commands.json .)

حيث <Z3_ROOT هو دليل يحتوي على توزيع ثنائي Z3 ، و LLMV_CMAKE_DIR هو دليل يحتوي على LLVMConfig.cmake .

الخيارات القانونية الأخرى لـ CMAKE_BUILD_TYPE هي Debug Coverage . لاحظ أن CMAKE_BUILD_TYPE يجب أن تكون متوافقة مع تلك المستخدمة لتجميع LLVM . على وجه الخصوص ، ستحتاج إلى بناء Debug من LLVM لتجميع SeaHorn في وضع Debug **. تأكد من أن لديك الكثير من الصبر ، ومساحة القرص ، والوقت إذا قررت السير في هذا الطريق.

بدلاً من ذلك ، يمكن تكوين المشروع باستخدام مسبقات CMake. للقيام بذلك ، ما عليك سوى تشغيل الأمر التالي:

$ cmake --preset < BUILD_TYPE > - < PRESET_NAME >

لتكوين cmake ، حيث يكون <BUILD_TYPE> واحد من: Debug ، RelWithDebInfo أو Coverage و <PRESET_NAME> هو الإعداد المسبق الذي ترغب في استخدامه. الإعدادات المسبقة المتوفرة حاليًا هي: jammy . تفترض هذه الإعدادات المسبقة أنك قمت بتثبيت Z3 في /opt/z3-4.8.9 وتثبيت Yices في /opt/yices-2.6.1 .

سيسمح ذلك أيضًا بتكوين المشروع وتجميعه ضمن كود VS باستخدام ملحق CMAKE Tools.

إذا كنت ترغب في استخدام إعدادات التجميع المختلفة أو إذا كان لديك Z3 أو Yices مثبتة في أي دليل آخر ، فستحتاج إلى جعل ملف CMakeUserPresets.json الخاص بك مع الإعدادات المسبقة الخاصة بك.

تجميع على جهاز Mac

لا تتضمن -DSEA_ENABLE_LLD=ON . المترجم الافتراضي هو clang ، لذلك قد لا تحتاج إلى تعيينه بشكل صريح.

الهدف الإضافي

يوفر Seahorn العديد من المكونات التي يتم استنساخها وتثبيتها تلقائيًا عبر الهدف extra . يمكن استخدام هذه المكونات من قبل مشاريع أخرى خارج Seahorn.

• Sea-Dsa: git clone https://github.com/seahorn/sea-dsa.git

  sea-dsa هو تحليل جديد للكومة على قائم على DSA. على عكس llvm-dsa ، فإن sea-dsa حساس للسياق ، وبالتالي ، يمكن إنشاء قسم أدق الحبيبات من الكومة في وجود مكالمات الوظائف.

• CLAM: git clone https://github.com/seahorn/crab-llvm.git

  يوفر clam ثباتًا استقرائيًا باستخدام تقنيات التفسير المجردة لبقية خلفية Seahorn.

• llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git

  يوفر llvm-seahorn إصدارات مصممة لتحويلها من تمريرات InstCombine و IndVarSimplify LLVM بالإضافة إلى تمريرة LLVM لتحويل القيم غير المحددة إلى مكالمات غير محددة ، من بين أمور أخرى.

لا يأتي Seahorn مع نسخته الخاصة من Clang ويتوقع العثور عليه إما في دليل البناء ( run/bin ) أو في المسار. تأكد من أن إصدار Clang يطابق إصدار LLVM الذي تم استخدامه لتجميع Seahorn (حاليًا LLVM14). أسهل طريقة لتوفير الإصدار المناسب من Clang هي تنزيله من LLVM.org ، وإلغاء تنظيمها في مكان ما وإنشاء رابط رمزي لـ clang و clang++ في run/bin .

$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++

حيث <CLANG_ROOT> هو الموقع الذي تم فيه تفريغ Clang.

الاختبارات

يعتمد اختبار البنية التحتية على عدة حزم بيثون. هذه لها تبعيات خاصة بهم. إذا لم تتمكن من اكتشافها ، فاستخدم Docker بدلاً من ذلك.

$ pip install lit OutputCheck networkx pygraphviz

التغطية

يمكننا استخدام gcov و lcov لإنشاء معلومات تغطية الاختبار لـ Seahorn. للبناء مع تمكين التغطية ، نحتاج إلى تشغيل البناء تحت دليل مختلف وتعيين CMAKE_BUILD_TYPE Coverage أثناء تكوين CMake.

مثال على خطوات توليد تقرير التغطية لهدف test-opsem :

1. mkdir coverage; cd coverage قم بإنشاء وأدخل دليل بناء التغطية
2. cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../
3. أكمل البناء كالمعتاد
4. cmake --build . --target test-opsem Run Test-Test .gcno CMakeFiles .gcda
5. lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info جمع بيانات التغطية من الوحدة النمطية المطلوبة ، إذا تم استخدام clang كمترجم بدلاً من gcc ، قم بإنشاء نص BASH llvm-gcov.sh :

 #! /bin/bash
exec llvm-cov gcov " $@ " 

$ chmod +x llvm-gcov.sh

ثم إلحاق- --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh to the lcov -c ... command. 6. استخراج البيانات من الدلائل المطلوبة وإنشاء تقرير HTML:

lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report

ثم فتح coverage_report/index.html في المتصفح لعرض تقرير التغطية

انظر أيضًا scripts/coverage للنصوص التي تستخدمها CI. تقرير التغطية للبناء الليلي متاح في Codecov

فهرسة الكود

يتم إنشاء قاعدة بيانات التجميع لمشروع Seahorn وجميع المشروعات الفرعية الخاصة به باستخدام -DCMAKE_EXPORT_COMPILE_COMMANDS=ON ONT cmake .

تتمثل إحدى الطرق السهلة للحصول على فهرسة التعليمات البرمجية مع دعم قاعدة بيانات التجميع في ربط ملف compilation_database.json في دليل المشروع الرئيسي واتبع الإرشادات المحددة لمحررك.

• CLION-https://www.jetbrains.com/help/clion/compilation-database.html
• VIM (youcompleteme) - تعليمات
• Emacs-استخدم lsp-ui مع clangd المتوفرة في SpacemAcs تطوير فرع

التكوين البعيد ل CLION

للحصول على دليل مفصل لسير عمل عن بُعد مع تكوين Clion Check Clion.

التكوين عن بُعد لـ EMACs (وغيرهم من المحررين)

استخدم شوكة لدينا من Mainframer. لا تفوت تكوين المثال.

المساهمين

• آري غورفينكل
• خورخي نافاس
• Temesghen Kahsai
• جاكوب كودرسكي
• نام لو
• تشارلز لي
• شيانغ تشو
• سيدهارث بريا
• إيزابيل جارسيا-السيطرة
• يوزن سو
• أرسل لي إذا كان اسمك هنا