crab

السلطعون: مكتبة C ++ لبناء التحليلات الثابتة

Crab هي مكتبة C ++ لبناء التحليلات الثابتة على أساس التفسير التجريدي. يوفر Crab مجموعة غنية من المجالات التجريدية ، وحلال FixPoint المستندة إلى Kleene ، بالإضافة إلى تحليلات مختلفة مثل تدفق البيانات ، بين الجسور والخلفية. يعد تصميم Crab معياريًا تمامًا بحيث يكون من السهل الإضافي مجالات وحلول مجردة جديدة أو بناء تحليلات جديدة.

يمكن لمجالات تجريد السلطعون أن تسبب محتويات الذاكرة ، والصفائف الشبيهة بالخصائص العددية. يستخدم Crab تطبيقات فعالة للمجالات العددية الشائعة مثل المناطق والأوكتاجونات والمجالات الجديدة ، على سبيل المثال ، حول المصطلحات الرمزية (المعروفة أيضًا باسم الوظائف غير المفترضة). يقوم CRAB أيضًا بتنفيذ المجالات غير العلائقية الشائعة مثل الفاصل الزمني أو التطابقات باستخدام خرائط بيئة فعالة ، ويسمح بمجموعة من المجالات التعسفية عبر إنشاءات المنتجات المنخفضة القياسية. يوفر Crab أيضًا مجالات غير محددة مثل فترات متخصصة متخصصة تسمى الصناديق القائمة على مخططات القرار الخطية واستراتيجية تقسيم القيمة الأكثر عمومية التي ترفع مجالًا تعسفيًا إلى القرب المفرط في الانتهاء من الانتهاء من الانفصال. بالإضافة إلى هذه المجالات ، التي تم تطويرها من قبل مؤلفي Crab ، تدمج مكتبة Crab Library المكتبات التجريدية الشهيرة مثل Apron و Elina و Pplite.

يوفر CRAB حلول FixPoint المحدد على أحدث طراز والذي يستخدم الترتيب الطوبولوجي الضعيف في Bourdoncle لتحديد مجموعة نقاط الاتساع. للتخفيف من الخسائر الدقيقة أثناء الاتساع ، يقوم Crab بتنفيذ بعض التقنيات الشائعة مثل الاتساع مع العتبات وتوسيع LookaHead.

يوفر CRAB تطبيقين مختلفين للتحليلات بين المباركين: من أعلى إلى أسفل مع تحليل مذكرات بين المذكرات مع دعم للمكالمات العودية ، ومجموعة من التحليل من أعلى إلى أعلى + من أعلى إلى أسفل. أخيرًا وليس آخرًا ، يقوم Crab أيضًا بتنفيذ تحليل متخلف أكثر تجريبية يمكن استخدامه لحساب الشروط المسبقة الضرورية و/أو تقليل عدد الإنذارات الخاطئة.

لا يقوم Crab بتحليل لغة البرمجة السائدة مباشرة ، ولكنه بدلاً من ذلك يحلل تمثيله الوسيط القائم على CFG يسمى Crabir. Crabir هو رمز ثلاثية الأضلاع ويتم كتابته بقوة. في Crabir ، يتم تعريف تدفق التحكم من خلال تعليمات GOTO غير المحددة. بصرف النظر عن العمليات المنطقية والحسابية القياسية ، يوفر Crabir بيانات خاصة وتأكيد. يمكن استخدام الأول لتحسين تدفق التحكم ويوفر الأخير ميكانيكيًا بسيطًا للتحقق من الخصائص المعرفة من قبل المستخدم. على الرغم من تصميمها البسيط ، فإن Crabir غني بما يكفي لتمثيل لغات مثل LLVM.

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

النوافذ	أوبونتو	OS X.	التغطية
TBD		TBD

عامل ميناء

يمكن الحصول على نسخة (ليلية) من السلطعون التي تعمل مسبقًا والتي تقوم بتشغيل جميع الاختبارات باستخدام Docker:

docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionic

متطلبات

Crab مكتوب في C ++ ويعتمد على مكتبة Boost. المتطلبات الرئيسية هي:

• C ++ 11 مترجم
• Boost> = 1.65
• GMP
• MPFR (if -DCRAB_USE_APRON=ON or -DCRAB_USE_ELINA=ON )
• فلينت (فقط إذا -DCRAB_USE_PPLITE=ON )

في 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

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

لتثبيت السلطعون ، اكتب:

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
 3. cmake --build . --target install 

يحتوي دليل tests على العديد من الأمثلة على كيفية بناء البرامج المكتوبة في Crabir وحساب الثوابات باستخدام تحليلات مختلفة ومجالات مجردة. لتجميع هذه الاختبارات ، أضف الخيار -DCRAB_ENABLE_TESTS=ON السطر 2.

ثم ، على سبيل المثال ، لتشغيل test1 :

 build/test-bin/test1

تضمين مكتبات المجال التجريدية الطرف الثالث

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

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

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

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

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

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

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

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
 3. cmake --build . --target ldd && cmake ..
 4. cmake --build . --target apron && cmake ..	
 5. cmake --build . --target install 	

ستقوم الخطوط 3 و 4 بتنزيل وتجميع وتثبيت المربعات ومجالات المئزر ، على التوالي. استبدل apron في السطر 4 مع elina أو pplite إذا كنت ترغب في استخدام Elina أو Pplite بدلاً من ذلك. إذا قمت بالفعل بتجميع هذه المكتبات وتثبيتها في جهازك ، فقم بتخطي الأوامر على السطر 3 و 4 وأضف الخيارات التالية في السطر 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

باستخدام مكتبة السلطعون في مشاريع C ++ الأخرى

لتضمين السلطعون في تطبيق C ++ الخاص بك ، تحتاج إلى:

• قم بتضمين ملفات رأس C ++ الموجودة في $INSTALL_DIR/crab/include ، و

• ربط التطبيق الخاص بك مع مكتبات السلطعون المثبتة في $INSTALL_DIR/crab/lib .

إذا قمت بالتجميع مع الصناديق/المئزر/elina/pplite ، فأنت بحاجة أيضًا إلى تضمين $INSTALL_DIR/EXT/include وربط $INSTALL_DIR/EXT/lib حيث EXT=apron|elina|ldd|pplite .

cmake

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

 add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})

ثم اربط قابلة للتنفيذ باستخدام ${CRAB_LIBS}

يصنع

إذا كان مشروعك يستخدم make ، فاقرأ هذه العينة Makefile.