الصفحة الرئيسية>كود المصدر JSP>فئات أخرى
تنزيل

البطلينوس: LLVM الواجهة الأمامية لسرطان البحر

CLAM هو محلل ثابت قائم على التفسير التجريدي يحسب الثبات الاستقرائي لـ LLVM bitcode استنادًا إلى مكتبة السلطعون. هذا الفرع يدعم LLVM 14.

يمكن العثور على الوثائق المتاحة في كل من Clam Wiki و Crab Wiki.

عامل ميناء

يمكنك الحصول على البطلينوس من Docker Hub (مصممة ليلا) باستخدام الأمر: 

 docker pull seahorn/clam-llvm14:nightly

متطلبات

تم كتابة البطلينوس في C ++ ويستخدم مكتبة Boost بشدة. المتطلبات الرئيسية هي:

  • برنامج التحويل البرمجي C ++ الحديث يدعم C ++ 14
  • Boost> = 1.65
  • GMP
  • MPFR (فقط إذا -DCRAB_USE_APRON=ON أو -DCRAB_USE_ELINA=ON )
  • فلينت (فقط إذا -DCRAB_USE_PPLITE=ON )
  • بيثون> = 3.6

في Linux ، يمكنك تثبيت المتطلبات التي تكتب الأوامر: 

 sudo apt-get install libboost-all-dev libboost-program-options-dev
 sudo apt-get install libgmp-dev
 sudo apt-get install libmpfr-dev	
 sudo apt-get install libflint-dev

الاختبارات

يعتمد اختبار البنية التحتية على عدة حزم بيثون. لتشغيل الاختبارات ، تحتاج إلى تثبيت lit و OutputCheck : 

 pip3 install lit
 pip3 install OutputCheck

التجميع والتركيب

خطوات التجميع الأساسية هي: 

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..   
4. cmake --build . --target extra && cmake ..                  
5. cmake --build . --target install

سيحاول الأمر في السطر 2 العثور على LLVM 14 من المسارات القياسية. إذا قمت بتثبيت LLVM 14 في مسار غير قياسي ، فأضف الخيار -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm إلى السطر 2. سيقوم الأمر في السطر 3 بتنزيل السلطعون وتجميعه من المصادر. يستخدم Clam مكونين خارجيين مثبتان عبر الهدف extra في السطر 4. هذه المكونات هي:

  • Sea-DSA هو تحليل الكومة المستخدمة لترجمة تعليمات ذاكرة LLVM. يمكن العثور على التفاصيل هنا وهنا.

  • يوفر LLVM-Seahorn إصدارات متخصصة من مكونات LLVM لجعلها أكثر قابلية للتحقق. llvm-seahorn اختياري ولكنه موصى به.

تتطلب مجالات الصناديق/المئزر/Elina/Pplite مكتبات طرف ثالث. لتجنب العبء على المستخدمين الذين لا يهتمون بهذه المجالات ، يكون تثبيت المكتبات اختياريًا.

  • إذا كنت ترغب في استخدام مجال المربعات ، فأضف -DCRAB_USE_LDD=ON Option.

  • إذا كنت ترغب في استخدام مجالات مكتبة Apron ، فأضف -DCRAB_USE_APRON=ON Option.

  • إذا كنت ترغب في استخدام مجالات مكتبة Elina ، فأضف -DCRAB_USE_ELINA=ON Option.

  • إذا كنت ترغب في استخدام مجالات مكتبة PPLITE ، فأضف -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON الخيارات.

هام: Apron و Elina غير متوافقين حاليًا ، لذا لا يمكنك تمكين -DCRAB_USE_APRON=ON و -DCRAB_USE_ELINA=ON في نفس الوقت.

على سبيل المثال ، لتثبيت البطلينوس مع الصناديق والمئزر: 

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..                
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..             
7. cmake --build . --target install

على سبيل المثال ، ستقوم الخطوط 5 و 6 بتنزيل وتجميع وتثبيت المربعات ومكتبات المئزر ، على التوالي. إذا كنت قد قمت بالفعل بتجميع هذه المكتبات وتثبيتها في جهازك ، فقم بتخطي الأوامر في السطر 5 و 6 وأضف الخيارات التالية في السطر 2.

  • لـ APRON: -DAPRON_ROOT=$APRON_INSTALL_DIR
  • بالنسبة إلى Elina: -DELINA_ROOT=$ELINA_INSTALL_DIR
  • للمربعات: -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
  • لـ pplite: -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

التحقق من التثبيت

لتشغيل بعض اختبارات الانحدار: 

 cmake --build . --target test-simple

الاستخدام

يوفر Clam نصًا Python يسمى clam.py (الموجود في $DIR/bin حيث يكون $DIR هو الدليل الذي تم تثبيت البطلينوس) للتفاعل مع المستخدمين. أبسط أمر هو clam.py test.c اكتب clam.py --help لجميع الخيارات وقراءة wiki لدينا.

يوسع
معلومات إضافية
تطبيقات ذات صلة
نوصي لك
أخبار ذات صلة الكل