lart
1.0.0
LART = LLVM Abstraction & Refinement Tool เป้าหมายของเครื่องมือนี้คือการให้การแปลง LLVM-to-LLVM ที่ใช้ abstractions โปรแกรมต่างๆ ในแง่ของชุดคำสั่งโปรแกรมผลลัพธ์เป็นปกติโปรแกรม LLVM คอนกรีตที่สามารถดำเนินการและวิเคราะห์ได้ ข้อมูลเพิ่มเติมเกี่ยวกับสิ่งที่เป็นนามธรรมมีผลมากกว่าโปรแกรม (ชิ้นส่วน) ถูกแทรกโดยใช้ฟังก์ชั่น LLVM ที่แท้จริงพิเศษและโหนดข้อมูลเมตา LLVM LART ให้บริการทั้งเครื่องมือแบบสแตนด์อโลนที่ประมวลผลไฟล์ bitcode บนดิสก์รวมถึงเฟรมเวิร์กที่สามารถรวมเข้ากับเครื่องมือที่ใช้ LLVM ที่ซับซ้อน แรงจูงใจหลักที่อยู่เบื้องหลัง LART คือการจัดหา "ตัวประมวลผลล่วงหน้า" สำหรับตัวตรวจสอบโมเดลที่ใช้ LLVM และเครื่องมือวิเคราะห์อื่น ๆ ทำให้งานของพวกเขาง่ายขึ้นโดยการลดขนาดปัญหาโดยไม่ลดทอนความสมบูรณ์ของการวิเคราะห์ abstractions ที่ดำเนินการโดย LART มักจะได้รับการปรับปรุงตามคำแนะนำเฉพาะเกี่ยวกับ "ส่วน" ของนามธรรมนั้นหยาบเกินไป (สิ่งที่เป็นนามธรรมที่หยาบเกินไปจะสร้างข้อผิดพลาดปลอมที่มองเห็นได้จากการวิเคราะห์ที่ตามมา แต่ไม่ได้อยู่ในโปรแกรมดั้งเดิม)
จุดประสงค์ของการออกกำลังกายทั้งหมดคือการอธิบายข้อมูลจาก LLVM BitCode ทำให้การวิเคราะห์ที่ตามมามีประสิทธิภาพมากขึ้น (ด้วยค่าใช้จ่ายของความแม่นยำบางอย่าง) ด้วยเหตุนี้เราจึงจำเป็นต้องสามารถเข้ารหัสตัวเลือกที่ไม่ได้ตัดสินใจในโปรแกรม LLVM ซึ่งสามารถทำได้ง่ายๆผ่านฟังก์ชั่นวัตถุประสงค์พิเศษ (คล้ายกับ LLVM Intrinsics) ฟังก์ชั่นนี้มีชื่อว่า @lart.choice ใช้คู่ของขอบเขตเป็นอาร์กิวเมนต์และไม่ได้ส่งคืนค่าที่อยู่ระหว่างขอบเขตเหล่านั้น
ส่วนขยายนี้เป็นความหมาย LLVM นี้จะต้องได้รับการยอมรับจากเครื่องมือดาวน์สตรีม นี่เป็นเพียงการเบี่ยงเบนที่สำคัญเพียงอย่างเดียวจาก BitCode LLVM มาตรฐาน เครื่องมือวิเคราะห์หลายอย่างจะใช้กลไกที่คล้ายกันทั้งภายในหรือแม้กระทั่งกับอินเทอร์เฟซภายนอก การปรับเครื่องมือโดยไม่สนับสนุน @lart.choice ในการทำงานกับ Lart มักจะตรงไปตรงมามาก
มีฟังก์ชั่นวัตถุประสงค์พิเศษอื่น ๆ ที่จัดทำโดย LART คือ @lart.meta.* ครอบครัว แต่เท่าที่คำแนะนำเหล่านี้เกี่ยวข้องเครื่องมือส่วนใหญ่จะสามารถเพิกเฉยต่อการดำรงอยู่ของพวกเขาได้อย่างปลอดภัยเช่นเดียวกับ @llvm.dbg.* การแปลงโปรแกรมคาดว่าจะเก็บสายเหล่านั้นไว้ในกรณีที่ Lart ถูกเรียกเข้ามาเพื่อปรับแต่งสิ่งที่เป็นนามธรรม (แต่ละนามธรรมที่จัดทำโดย Lart มาพร้อมกับขั้นตอนการปรับแต่งที่สอดคล้องกันซึ่งมักจะต้องค้นหาการโทร @lart.meta ที่แทรกโดยนามธรรม)
ในขณะที่เอ็นจิ้นนามธรรมแบบดั้งเดิมส่วนใหญ่ทำงานเป็นล่ามบทคัดย่อสามารถ "รวบรวม" ลงในโปรแกรมได้ แทนที่จะเป็นคำแนะนำในการตีความ (ซ้ำ) สัญลักษณ์คำแนะนำเชิงสัญลักษณ์สามารถรวบรวมได้ ในกรณีที่เป็นนามธรรมของภาคแสดง BitCode ที่ได้จะจัดการโดยตรงและใช้การประเมินมูลค่าภาคแสดงแทนตัวแปรคอนกรีต ตามที่อธิบายไว้ข้างต้นความแตกต่างที่สำคัญคือ BitCode จำเป็นต้องเลือกตัวเลือกที่ไม่ได้กำหนดเนื่องจากบางภาคการศึกษาอาจมีการประเมินค่าที่ไม่แน่นอน (เป็นทั้งความจริงและเท็จ) ตัวแปรบางตัวอาจถูกแยกออกไปทั้งหมดและการทดสอบทั้งหมดในตัวแปรดังกล่าวจะให้ทั้งใช่และไม่มีคำตอบ
ใช้หรือทำซ้ำการตั้งค่าจาก ./devcontainer/Dockerfile dockerfile ในขณะนี้
จากนั้นใช้:
./scripts/build.sh
./build/bin/lartcc <domain> <compiler arguments> in.c
opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc
lit -v build/test
หมายเหตุ: build/lartcc/lartcc ต้องมีใบอนุญาต exacutabple
