intAbs

readme

พื้นที่เก็บข้อมูลนี้เกี่ยวกับการตีความนามธรรมแบบแยกส่วนของเธรด (โดยใช้ไลบรารีผ้ากันเปื้อน) สำหรับโปรแกรมที่ขับเคลื่อนด้วยการขัดจังหวะโดยใช้ข้อมูลลำดับความสำคัญ

ซอร์สโค้ดเป็นเวอร์ชันที่แก้ไขจาก https://github.com/markus-kusano/watts

ตอนนี้ไฟล์ทั้งหมดไม่ได้ทำความสะอาดรวมถึงไฟล์ทดสอบ

อย่างไรก็ตามชุดย่อยของตารางผลลัพธ์สามารถพิมพ์ได้เนื่องจากอัปโหลดไฟล์เอาต์พุตบางไฟล์

อ้างถึง intabs

 @inproceedings{DBLP:conf/kbse/SungKW17,
  author    = {Chungha Sung and
               Markus Kusano and
               Chao Wang},
  title     = {Modular verification of interrupt-driven software},
  booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated
               Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November
               03, 2017},
  pages     = {206--216},
  year      = {2017},
  crossref  = {DBLP:conf/kbse/2017},
  url       = {https://doi.org/10.1109/ASE.2017.8115634},
  doi       = {10.1109/ASE.2017.8115634},
  timestamp = {Fri, 01 Dec 2017 22:44:10 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/kbse/SungKW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

อาคาร

โปรแกรมคือ LLVM Opt Pass มันถูกสร้างขึ้นโดยใช้ cmake เนื่องจากเราใช้ CMake สิ่งนี้น่าจะต้องใช้ LLVM เวอร์ชัน 3.6.0

แก้ไขตัวแปรไฟล์ cmakelists apron_prefix เป็นตำแหน่งที่ติดตั้งผ้ากันเปื้อน

สมมติว่าไฟล์ไลบรารี LLVM ของคุณอยู่ในตำแหน่งมาตรฐาน (เพิ่มเติมในด้านล่างนี้) เพียง:

 mkdir build
cd build
cmake ../
make

ผลลัพธ์ของกระบวนการสร้างคือไฟล์. so, libworklistai.so

หากคุณต้องการบอก CMake ว่า LLVM อาศัยอยู่ที่ไหนคุณจะต้องเพิ่มตัวเลือก -dllvm_dir, เช่น

cmake -dllvm_dir =/home/chungha/src/share/llvm/cmake ../

ไดเรกทอรีที่ส่งผ่านไปยัง LLVM_DIR ควรเป็นตำแหน่งที่ไฟล์ LLVM CMake คือ (เช่น LLVM-config.cmake)

คุณอาจต้องตั้งค่า -DZ3_INC และ -DZ3_LIB เป็นไดเรกทอรีรวมและไฟล์ไลบรารีสำหรับ Z3 ตามลำดับ

เส้นทางทดสอบ

คุณต้องแก้ไขเส้นทาง LLVM และสร้างเส้นทางในไฟล์ SRC/Test/Export.SH เพื่อทดสอบโปรแกรมเช่น LLVM_PREFIX, WORDLIST_SO, Z3_BIN

ยืนยันการใช้งาน

หากคุณต้องการตรวจสอบค่าคงที่ของโปรแกรมโดยใช้ Assert คุณต้องใช้ด้วยวิธีนี้

แทนที่จะใช้ assert(a==1) คุณต้องเขียนลง if (a != 1) { assert(0); } .

เนื่องจากความสัมพันธ์ของโพสต์ Dominator ฉันต้องใช้เครื่องมือของฉันเพื่อสนับสนุนเฉพาะกรณีนี้ (ยืนยันทำให้โปรแกรมไม่สามารถเข้าถึงได้ดังนั้นความสัมพันธ์โพสต์ Dominator บางอย่างจะหายไป)

คำอธิบายไดเรกทอรี

• ICBMC: นี่คือไดเรกทอรีที่ฉันทดสอบไฟล์ไบนารี ICBMC จากกระดาษวันที่ 15 ด้วยเกณฑ์มาตรฐานของฉัน

• SRC: มันมีการใช้งานหลัก (worlist-ai, utils, cmakelists.txt) และไดเรกทอรีทดสอบ (ทดสอบ)

• SRC/TEST: มันมีไฟล์สคริปต์เพื่อเรียกใช้โปรแกรมทดสอบและเกณฑ์มาตรฐาน นอกจากนี้ไฟล์ผลลัพธ์จะรวมอยู่ในแต่ละไดเรกทอรี