cpachecker

เริ่มต้นใช้งาน cpachecker

• คำแนะนำการติดตั้ง
• แนวทางการบริจาค
• คำแนะนำการพัฒนา

เอกสารเพิ่มเติมสามารถพบได้ใน doc/ Directory

ใบอนุญาตและลิขสิทธิ์

CPACHECKER ได้รับใบอนุญาตภายใต้ใบอนุญาต Apache 2.0 พร้อมลิขสิทธิ์โดย Dirk Beyer และอื่น ๆ (cf. Authors.md สำหรับรายชื่อผู้มีส่วนร่วมทั้งหมด) ห้องสมุดบุคคลที่สามอยู่ภายใต้ใบอนุญาตและลิขสิทธิ์อื่น ๆ อีกมากมาย ไฟล์ในใบ LICENSES ไดเรกทอรีสำหรับข้อความใบอนุญาตเต็มรูปแบบ โดยเฉพาะอย่างยิ่ง Mathsat มีให้เพื่อวัตถุประสงค์ในการวิจัยและประเมินผลเท่านั้น (cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ) ดังนั้นอย่าลืมใช้ตัวแก้ SMT ที่แตกต่างกันหากจำเป็น โปรดทราบว่าแม้ว่าโปรแกรม GPL จะถูกแจกจ่ายร่วมกับ CPACHECKER แต่ CPACHECKER นั้นแยกจากโปรแกรมนั้นและไม่อยู่ภายใต้เงื่อนไขของ GPL

เตรียมโปรแกรมสำหรับการตรวจสอบโดย cpachecker

โปรแกรมทั้งหมดจำเป็นต้องประมวลผลล่วงหน้าด้วยตัวประมวลผลก่อน C คือพวกเขาอาจไม่มีคำสั่ง #define และ #include คุณสามารถเปิดใช้งานการประมวลผลล่วงหน้าภายใน CPACHECKER โดยการระบุ --preprocess บนบรรทัดคำสั่ง สามารถให้ไฟล์ C หลายไฟล์และจะเชื่อมโยงเข้าด้วยกันและตรวจสอบว่าเป็นโปรแกรมเดียว (คุณสมบัติการทดลอง)

Cpachecker สามารถแยกวิเคราะห์และวิเคราะห์ชุดย่อยขนาดใหญ่ของ (GNU) c หากการแยกวิเคราะห์ล้มเหลวสำหรับโปรแกรมของคุณโปรดส่งรายงานไปที่ [email protected]

การตรวจสอบโปรแกรมด้วย cpachecker

1. เลือกไฟล์ซอร์สโค้ดที่คุณต้องการตรวจสอบ หากคุณใช้โปรแกรมของคุณเองอย่าลืมประมวลผลล่วงหน้าตามที่กล่าวไว้ข้างต้น ตัวอย่าง: doc/examples/example.c หรือ doc/examples/example_bug.c แหล่งข้อมูลที่ดีสำหรับโปรแกรมตัวอย่างเพิ่มเติมคือพื้นที่เก็บข้อมูล SV-benchmarks ที่ใช้โดยการแข่งขันระหว่างประเทศเกี่ยวกับการตรวจสอบซอฟต์แวร์

2. ทางเลือก: หากคุณต้องการเลือกการวิเคราะห์บางอย่างเช่นการวิเคราะห์ภาคแสดงให้ระบุไฟล์การกำหนดค่า ไฟล์นี้กำหนดตัวอย่างเช่น CPA ที่ใช้ ไฟล์การกำหนดค่ามาตรฐานสามารถพบได้ใน config/ หากคุณไม่ต้องการการวิเคราะห์เฉพาะเราขอแนะนำการกำหนดค่าเริ่มต้นของ CPACHECKER อย่างไรก็ตามโปรดทราบว่าหากคุณอยู่ใน MACOS คุณต้องจัดเตรียมไบนารีคณิตศาสตร์ที่รวบรวมโดยเฉพาะสำหรับการกำหนดค่าเริ่มต้นในการทำงาน (หรือใช้ Docker เพื่อเรียกใช้ CPACHECKER เวอร์ชัน Linux) การกำหนดค่าของ cpachecker อธิบายไว้ใน doc/Configuration.md

3. เลือกไฟล์สเปค (คุณอาจไม่จำเป็นต้องใช้สำหรับการกำหนดค่าบางอย่าง) การกำหนดค่ามาตรฐานใช้ config/specification/default.spc เป็นข้อกำหนดเริ่มต้น ด้วยอันนี้ CPACHECKER จะค้นหาป้ายกำกับชื่อ ERROR (case insensitive) และการยืนยันในไฟล์ซอร์สโค้ด ตัวอย่างอื่น ๆ สำหรับข้อมูลจำเพาะสามารถพบได้ใน config/specification/ ในไดเรกทอรี cpachecker

4. ดำเนินการ bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> อาร์กิวเมนต์บรรทัดคำสั่งเพิ่มเติมอธิบายไว้ใน doc/Configuration.md หากต้องการใช้การกำหนดค่าเริ่มต้นของ CPACHECKER ให้ส่งเฉพาะไฟล์ต้นฉบับ: bin/cpachecker doc/examples/example.c C การวิเคราะห์ที่เฉพาะเจาะจง (เช่น K-INDUCTION) สามารถเลือกได้เช่นกับ bin/cpachecker --config/kInduction.properties doc/examples/example.c หรือตัวย่อที่เทียบเท่า bin/cpachecker --kInduction doc/examples/example.c Java 17 หรือใหม่กว่าเป็นสิ่งจำเป็น หากไม่ได้อยู่ในเส้นทางของคุณคุณต้องระบุในตัวแปรสภาพแวดล้อม Java ตัวอย่าง: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java สำหรับ 64 บิต openjdk 17 บน Ubuntu

   โปรดทราบว่าไม่มีการกำหนดค่าการวิเคราะห์ทั้งหมดสำหรับ MacOS เพราะเราไม่ได้จัดส่งไบนารีสำหรับนักแก้ปัญหา SMT สำหรับแพลตฟอร์มนี้ คุณจำเป็นต้องสร้างไบนารีที่เหมาะสมด้วยตัวเองหรือใช้การวิเคราะห์ที่ทรงพลังน้อยกว่าที่ทำงานกับนักแก้ปัญหาที่ใช้ Java เช่นอันนี้แทนที่จะกำหนดค่าเริ่มต้นของ Cpachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol แน่นอน

   หากคุณติดตั้ง cpachecker โดยใช้ Docker บรรทัดคำสั่งตัวอย่างด้านบนจะมีลักษณะเช่นนี้: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c cpachecker ไฟล์เอาต์พุตของ CPACHECKER จะถูกวางไว้ใน ./output/ OUTPUT/

5. นอกจากนี้ยังมีการสร้างเอาต์พุตคอนโซลรายงาน HTML แบบโต้ตอบถูกสร้างขึ้นใน output/ ทั้งชื่อ Report.html (สำหรับผลลัพธ์ที่เป็นจริง) หรือ Counterexample.*.html (สำหรับผลลัพธ์ที่เป็นเท็จ) เปิดไฟล์เหล่านี้ในเบราว์เซอร์เพื่อดูผลการวิเคราะห์ CPACHECKER (cf. doc/Report.md )

นอกจากนี้ยังมีไฟล์เอาต์พุตเพิ่มเติมใน output/ ::

• ARG.dot : การสร้างภาพของแผนผังความสามารถในการเข้าถึงบทคัดย่อ (รูปแบบ graphviz)
• cfa*.dot : การสร้างภาพของโฟลว์โฟลว์ออโต้ตัน (รูปแบบ graphviz)
• reached.dot : การสร้างภาพของโฟลว์โฟลว์ออโตเมตตันด้วยสถานะนามธรรมที่มองเห็นอยู่ด้านบน (รูปแบบ graphviz)
• coverage.info : ข้อมูลความครอบคลุม (คล้ายกับเครื่องมือทดสอบ) ในรูปแบบ Gcov ใช้บรรทัดคำสั่งต่อไปนี้เพื่อสร้างรายงาน HTML เป็น output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : เส้นทางผ่านโปรแกรมที่นำไปสู่ข้อผิดพลาด
• Counterexample.*.assignment.txt : การกำหนดสำหรับตัวแปรทั้งหมดบนเส้นทางข้อผิดพลาด
• Counterexample.*.harness.c : ชุดทดสอบที่สามารถทำซ้ำเส้นทางข้อผิดพลาดผ่านการทดสอบ ดู Doc/Tutorials/Test-Harness.md สำหรับการใช้ตัวอย่าง
• predmap.txt : เพรดิเคตที่ใช้โดยการวิเคราะห์เพรดิเคตเพื่อพิสูจน์ความปลอดภัยของโปรแกรม
• reached.txt : การถ่ายโอนข้อมูลทั้งหมดที่มาถึงนามธรรม
• Statistics.txt : สถิติเวลา (สามารถพิมพ์ไปยังคอนโซลด้วย --stats )

โปรดทราบว่าไฟล์เหล่านี้ทั้งหมดจะไม่พร้อมใช้งานสำหรับการกำหนดค่าทั้งหมด นอกจากนี้ไฟล์เหล่านี้บางไฟล์จะถูกสร้างขึ้นหากพบข้อผิดพลาด (หรือในทางกลับกัน) CPACHECKER จะเขียนทับไฟล์ในไดเรกทอรีนี้!

การตรวจสอบโปรแกรมด้วย CPA-WITness2test

คุณสามารถตรวจสอบการละเมิดพยานด้วย CPA-WITness2test ซึ่งเป็นส่วนหนึ่งของ CPACHECKER

1. ในการทำเช่นนั้นคุณต้องมีพยานละเมิดไฟล์ข้อกำหนดที่เหมาะกับพยานการละเมิดและไฟล์ซอร์สโค้ดที่เหมาะกับพยานการละเมิด

2. เพื่อตรวจสอบพยานให้ดำเนินการคำสั่งต่อไปนี้:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   อาร์กิวเมนต์บรรทัดคำสั่ง addtional จะถูกดูด้วย bin/cpa-witness2test -h

3. เมื่อเสร็จแล้วและหากพยานการละเมิดได้รับการตรวจสอบความสำเร็จแล้วผลลัพธ์ของคอนโซลจะแสดง Verification result: FALSE นอกจากนี้ยังมีเอาต์พุตคอนโซล CPA-WITness2test ยังสร้างไฟล์ output/*.harness.c ไฟล์นี้สามารถรวบรวมกับไฟล์ต้นฉบับเพื่อสร้างการทดสอบแบบปฏิบัติการที่สะท้อนถึงพยานการละเมิด

โปรดทราบว่าหากพยานการละเมิดไม่มีข้อมูลเพียงพอที่จะสร้างการทดสอบที่เรียกใช้งานได้ผลการตรวจสอบความถูกต้องจะเป็น ERROR และเอาต์พุตคอนโซลจะมีบรรทัดต่อไปนี้: Could not export a test harness, some test-vector values are missing.