หน้าแรก>ซอร์สโค้ด JSP>หมวดหมู่อื่นๆ
ดาวน์โหลด

หอย: LLVM front-end สำหรับปู

หอยเป็นเครื่องวิเคราะห์แบบคงที่การตีความแบบนามธรรมที่คำนวณค่าคงที่อุปนัยสำหรับ BitCode LLVM ตามไลบรารีปู สาขานี้รองรับ LLVM 14

เอกสารที่มีอยู่สามารถพบได้ทั้งในหอยวิกิและวิกิปู

นักเทียบท่า

คุณสามารถรับหอยจาก 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 )
  • Flint (เฉพาะถ้า -DCRAB_USE_PPLITE=ON )
  • Python> = 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

การทดสอบ

การทดสอบโครงสร้างพื้นฐานขึ้นอยู่กับแพ็คเกจ Python หลายแห่ง ในการเรียกใช้การทดสอบคุณต้องติดตั้ง 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 จะดาวน์โหลดปูและรวบรวมจากแหล่งที่มา หอยใช้ส่วนประกอบภายนอกสองส่วนที่ติดตั้งผ่านเป้าหมาย extra ที่บรรทัด 4 ส่วนประกอบเหล่านี้คือ:

  • SEA-DSA เป็นการวิเคราะห์กองที่ใช้ในการแปลคำแนะนำหน่วยความจำ LLVM รายละเอียดสามารถดูได้ที่นี่และที่นี่

  • LLVM-Seahorn ให้บริการส่วนประกอบ LLVM รุ่นพิเศษเพื่อให้สามารถตอบสนองได้มากขึ้นสำหรับการตรวจสอบ llvm-seahorn เป็นตัวเลือก แต่แนะนำอย่างหนัก

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

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

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

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

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

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

  • สำหรับผ้ากันเปื้อน: -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 สำหรับตัวเลือกทั้งหมดและอ่านวิกิของเรา

ขยาย
ข้อมูลเพิ่มเติม
แอปที่เกี่ยวข้อง
แนะนำสำหรับคุณ
ข้อมูลที่เกี่ยวข้อง ทั้งหมด