crab

ปู: ห้องสมุด C ++ สำหรับการสร้างโปรแกรมการวิเคราะห์แบบคงที่

Crab เป็นห้องสมุด C ++ สำหรับการสร้างโปรแกรมการวิเคราะห์แบบคงที่ตามการตีความเชิงนามธรรม Crab ให้บริการโดเมนนามธรรมที่หลากหลายนักแก้ปัญหา FiverPoint-based Kleene รวมถึงการวิเคราะห์ที่แตกต่างกันเช่น dataflow, ระหว่างกระบวนการและย้อนหลัง การออกแบบปูค่อนข้างเป็นแบบแยกส่วนเพื่อให้ง่ายต่อการปลั๊กอินโดเมนนามธรรมและตัวแก้ปัญหาใหม่หรือสร้างการวิเคราะห์ใหม่

โดเมนบทคัดย่อปูสามารถให้เหตุผลเกี่ยวกับเนื้อหาหน่วยความจำอาร์เรย์เหมือน C และคุณสมบัติเชิงตัวเลข Crab ใช้การใช้งานที่มีประสิทธิภาพของโดเมนตัวเลขยอดนิยมเช่นโซนและ octagons และโดเมนนวนิยายเพื่อเหตุผลเช่นเกี่ยวกับคำที่เป็นสัญลักษณ์ (ฟังก์ชั่นที่ไม่ได้ตีความ) ปูยังใช้โดเมนที่ไม่สัมพันธ์ที่เป็นที่นิยมเช่นช่วงเวลาหรือความสอดคล้องโดยใช้แผนที่สภาพแวดล้อมที่มีประสิทธิภาพและช่วยให้การรวมกันของโดเมนโดยพลการผ่านการสร้างผลิตภัณฑ์ที่ลดลงมาตรฐาน ปูยังให้โดเมนที่ไม่ใช่ convex เช่นช่วงเวลาที่แยกออกจากกันโดยเฉพาะที่เรียกว่ากล่องขึ้นอยู่กับไดอะแกรมการตัดสินใจเชิงเส้นและกลยุทธ์การแบ่งพาร์ติชันมูลค่าทั่วไปมากขึ้น นอกเหนือจากโดเมนเหล่านี้ทั้งหมดที่พัฒนาโดยผู้เขียนปูไลบรารีปูยังรวมไลบรารีโดเมนนามธรรมยอดนิยมเช่นผ้ากันเปื้อน Elina และ Pplite

Crab จัดหาตัวแก้ปัญหาจุดแก้ไขที่ทันสมัยซึ่งใช้การสั่งซื้อทอพอโลยีที่อ่อนแอของ Bourdoncle เพื่อเลือกชุดจุดกว้าง เพื่อลดการสูญเสียที่แม่นยำในระหว่างการขยายตัวปูใช้เทคนิคที่ได้รับความนิยมบางอย่างเช่นการขยายด้วยเกณฑ์และการขยายรูปแบบ lookahead

Crab ให้การใช้งานที่แตกต่างกันสองประการของการวิเคราะห์ระหว่างกระบวนการ: จากบนลงล่างพร้อมการวิเคราะห์ระหว่างกระบวนการบันทึกการบันทึกด้วยการสนับสนุนการเรียกซ้ำและไฮบริดของการวิเคราะห์จากล่างขึ้นบน + จากบนลงล่าง สุดท้าย แต่ไม่ท้ายสุดปูยังใช้การวิเคราะห์ย้อนหลังทดลองมากขึ้นซึ่งสามารถใช้ในการคำนวณเงื่อนไขที่จำเป็นและ/หรือลดจำนวนการเตือนที่ผิดพลาด

Crab ไม่ได้วิเคราะห์ภาษาการเขียนโปรแกรมกระแสหลักโดยตรง แต่แทนที่จะวิเคราะห์การเป็นตัวแทนระดับกลางที่ใช้ CFG ของตัวเองที่เรียกว่า Crabir Crabir เป็นรหัสสามที่อยู่และพิมพ์อย่างมาก ใน Crabir การไหลของการควบคุมจะถูกกำหนดผ่านคำแนะนำที่ไม่ได้กำหนด นอกเหนือจากการดำเนินการบูลีนมาตรฐานและการคำนวณทางคณิตศาสตร์ Crabir ยังให้บริการพิเศษและยืนยันงบ อดีตสามารถใช้เพื่อปรับแต่งกระแสการควบคุมและหลังมีกลไกง่ายๆเพื่อตรวจสอบคุณสมบัติที่ผู้ใช้กำหนด แม้จะมีการออกแบบที่เรียบง่าย Crabir ก็อุดมสมบูรณ์พอที่จะเป็นตัวแทนของภาษาเช่น LLVM

ปูอยู่ระหว่างการพัฒนาอย่างแข็งขัน หากคุณพบข้อผิดพลาดโปรดเปิดปัญหา GitHub คำขอดึงที่มีคุณสมบัติใหม่ยินดีต้อนรับมาก เอกสารที่มีอยู่สามารถพบได้ในวิกิของเรา หากคุณใช้ห้องสมุดนี้โปรดอ้างอิงบทความนี้

หน้าต่าง	Ubuntu	OS X	ความครอบคลุม
TBD		TBD

นักเทียบท่า

A (ทุกคืน) ของปูที่สร้างไว้ล่วงหน้าที่เรียกใช้การทดสอบทั้งหมดสามารถรับได้โดยใช้ Docker:

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

ความต้องการ

ปูถูกเขียนใน C ++ และอาศัยห้องสมุด Boost ข้อกำหนดหลักคือ:

• คอมไพเลอร์ C ++ 11
• boost> = 1.65
• GMP
• mpfr (ถ้า -DCRAB_USE_APRON=ON หรือ -DCRAB_USE_ELINA=ON )
• Flint (เฉพาะถ้า -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 TO LINE 2

จากนั้นตัวอย่างเช่นการเรียกใช้ test1 :

 build/test-bin/test1

รวมไลบรารีโดเมนนามธรรมของบุคคลที่สาม

Boxes/Apron/Elina/Pplite ต้องใช้ห้องสมุดบุคคลที่สาม เพื่อหลีกเลี่ยงภาระให้กับผู้ใช้ที่ไม่สนใจโดเมนเหล่านั้นการติดตั้งไลบรารีเป็นทางเลือก

• หากคุณต้องการใช้โดเมนกล่องให้เพิ่ม -DCRAB_USE_LDD=ON ตัวเลือก

• หากคุณต้องการใช้โดเมน Apron Library จากนั้นเพิ่ม -DCRAB_USE_APRON=ON ตัวเลือก

• หากคุณต้องการใช้โดเมน Elina Library จากนั้นเพิ่ม -DCRAB_USE_ELINA=ON ตัวเลือก

• หากคุณต้องการใช้โดเมนไลบรารี pplite ให้เพิ่ม -DCRAB_USE_PPLITE=ON ตัวเลือก

สำคัญ: ผ้ากันเปื้อนและ 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

• สำหรับผ้ากันเปื้อน: -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

หากคุณรวบรวมด้วย Boxes/Apron/Elina/Pplite คุณต้องรวม $INSTALL_DIR/EXT/include และลิงก์ด้วย $INSTALL_DIR/EXT/lib โดยที่ EXT=apron|elina|ldd|pplite

cmake

หากโครงการของคุณใช้ cmake คุณเพียงแค่ต้องเพิ่มใน CMakeLists.txt ของโครงการของคุณ txt:

 add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})

จากนั้นเชื่อมโยงการดำเนินการของคุณด้วย ${CRAB_LIBS}

ทำ

หากโครงการของคุณใช้ make อ่านตัวอย่าง MakeFile นี้