ikos
Public release 3.4
IKOS (เคอร์เนลการอนุมานสำหรับตัววิเคราะห์แบบคงที่) เป็นเครื่องวิเคราะห์แบบคงที่สำหรับ C/C ++ ตามทฤษฎีของการตีความนามธรรม
IKOS เริ่มต้นจากห้องสมุด C ++ ที่ออกแบบมาเพื่ออำนวยความสะดวกในการพัฒนาเครื่องวิเคราะห์เสียงแบบสแตติกที่ใช้การตีความเชิงนามธรรม ความเชี่ยวชาญของเครื่องวิเคราะห์แบบคงที่สำหรับแอปพลิเคชันหรือตระกูลแอปพลิเคชันเป็นสิ่งสำคัญสำหรับการบรรลุทั้งความแม่นยำและความสามารถในการปรับขนาด การพัฒนาเครื่องวิเคราะห์ดังกล่าวนั้นลำบากและต้องการความเชี่ยวชาญที่สำคัญในการตีความนามธรรม
IKOS ให้การใช้งานโครงสร้างข้อมูลและอัลกอริทึมที่ล้ำสมัยและมีประสิทธิภาพเช่นกราฟการควบคุมการไหลของฟมิวท์พอยต์ทรีสเตอร์โดเมนนามธรรมเชิงตัวเลข ฯลฯ IKOS เป็นอิสระจากภาษาการเขียนโปรแกรมเฉพาะ
IKOS ยังมีเครื่องวิเคราะห์แบบคงที่ C และ C ++ ตาม LLVM มันใช้การวิเคราะห์ที่ปรับขนาดได้สำหรับการตรวจจับและพิสูจน์การขาดข้อผิดพลาดรันไทม์ในโปรแกรม C และ C ++
IKOS ได้รับการปล่อยตัวภายใต้ข้อตกลงของ NASA Open Source เวอร์ชัน 1.3 ดู license.pdf
ดูรุ่น
ดู troubleshooting.md
ในการติดตั้ง IKOS บน Linux หรือ MacOS เราขอแนะนำให้ใช้ Homebrew
ขั้นแรกให้ติดตั้ง Homebrew โดยทำตามคำแนะนำเหล่านี้
จากนั้นเพียงแค่เรียกใช้:
$ brew install nasa-sw-vnv/core/ikos
สำหรับ Windows ให้พิจารณาใช้ระบบย่อย Windows สำหรับ Linux
สมมติว่าเราต้องการวิเคราะห์โปรแกรม C ต่อไปนี้ในไฟล์ที่เรียกว่า loop.c :
1 : #include <stdio.h>
2 : int a [ 10 ];
3 : int main ( int argc , char * argv []) {
4 : size_t i = 0 ;
5 : for (; i < 10 ; i ++ ) {
6 : a [ i ] = i ;
7 : }
8 : a [ i ] = i ;
9 : printf ( "%i" , a [ i ]);
10 : }ในการวิเคราะห์โปรแกรมนี้ด้วย IKOS เพียงแค่เรียกใช้:
$ ikos loop.c
คุณจะเห็นผลลัพธ์ต่อไปนี้ IKOS รายงานการล้นบัฟเฟอร์สองครั้งที่บรรทัดที่ 8 และ 9
[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
คำสั่ง ikos ใช้ไฟล์ต้นฉบับ ( .c , .cpp ) หรือไฟล์ LLVM BitCode ( .bc ) เป็นอินพุตวิเคราะห์เพื่อค้นหาข้อผิดพลาดรันไทม์ (เรียกอีกอย่างว่าพฤติกรรมที่ไม่ได้กำหนด) สร้าง output.db ในไดเรกทอรีการทำงานปัจจุบันและพิมพ์รายงาน
ในรายงานแต่ละบรรทัดมีหนึ่งในสถานะต่อไปนี้:
โดยค่าเริ่มต้น IKOS แสดงคำเตือนและข้อผิดพลาดโดยตรงในเทอร์มินัลของคุณเช่นคอมไพเลอร์จะทำ
หากรายงานการวิเคราะห์มีขนาดใหญ่เกินไปคุณจะใช้:
ikos-report output.db เพื่อตรวจสอบรายงานในเทอร์มินัลของคุณikos-view output.db เพื่อตรวจสอบรายงานในเว็บอินเตอร์เฟสข้อมูลเพิ่มเติม:
ด้านล่างนี้เป็นคำแนะนำในการสร้าง IKO จากแหล่งที่มา นี่เป็นเพียงสำหรับผู้ใช้ขั้นสูงที่ต้องการแพ็คเกจ IKO สำหรับระบบปฏิบัติการหรือทดสอบกับ codebase มิฉะนั้นโปรดทำตามคำแนะนำด้านบน
ในการสร้างและเรียกใช้เครื่องวิเคราะห์คุณจะต้องมีการอ้างอิงต่อไปนี้:
ส่วนใหญ่สามารถติดตั้งได้โดยใช้ตัวจัดการแพ็คเกจของคุณ
หมายเหตุ: หากคุณสร้าง LLVM จากแหล่งที่มาคุณต้องเปิดใช้งานข้อมูลประเภทรันไทม์ (RTTI)
ตอนนี้คุณมีการพึ่งพาทั้งหมดในระบบของคุณคุณสามารถสร้างและติดตั้ง IKOS
ในขณะที่คุณเปิดการกระจาย IKOS คุณจะเห็นโครงสร้างไดเรกทอรีต่อไปนี้:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IKOS ใช้ระบบ CMake Build คุณจะต้องระบุไดเรกทอรีการติดตั้งที่จะมีไบนารีไลบรารีและส่วนหัวทั้งหมดหลังจากการติดตั้ง หากคุณไม่ได้ระบุไดเรกทอรีนี้ CMake จะติดตั้งทุกอย่างภายใต้ install ในไดเรกทอรีรูทของการแจกแจง ในขั้นตอนต่อไปนี้เราจะติดตั้ง IKOS ภายใต้ /path/to/ikos-install-directory
นี่คือขั้นตอนในการสร้างและติดตั้ง IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
จากนั้นเพิ่ม ikos ในเส้นทางของคุณ (พิจารณาเพิ่มสิ่งนี้ใน. bashrc):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
ในการสร้างและเรียกใช้การทดสอบเพียงพิมพ์:
$ make check
ดูผู้ร่วมให้ข้อมูล
Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur การคำนวณจุดแก้ไขแบบคู่ขนานที่กำหนดขึ้น ใน หลักการของภาษาการเขียนโปรแกรม (Popl 2020) , New Orleans, Louisiana (PDF)
Guillaume Brat, Jorge Navas, Nija Shi และ Arnaud Venet IKOS: กรอบสำหรับการวิเคราะห์แบบคงที่บนพื้นฐานของการตีความนามธรรม ใน การประชุมนานาชาติเกี่ยวกับวิศวกรรมซอฟต์แวร์และวิธีการอย่างเป็นทางการ (SEFM 2014) , Grenoble, ฝรั่งเศส (PDF)
Arnaud Venet โดเมนมาตรวัด: การวิเคราะห์ที่ปรับขนาดได้ของค่าคงที่ความไม่เท่าเทียมกันเชิงเส้น ใน การดำเนินการตรวจสอบความช่วยเหลือจากคอมพิวเตอร์ (CAV 2012) , Berkeley, California, USA 2012 บันทึกการบรรยายในวิทยาศาสตร์คอมพิวเตอร์, หน้า 139-154, เล่ม 7358, Springer 2012 (PDF)
ดู doc/coding_standards.md
ดู doc/overview.md
