Miri เป็นเครื่องมือตรวจจับพฤติกรรมที่ไม่ได้กำหนดสำหรับ Rust สามารถรันไบนารีและชุดทดสอบของโครงการขนส่งสินค้า และตรวจจับโค้ดที่ไม่ปลอดภัยซึ่งไม่เป็นไปตามข้อกำหนดด้านความปลอดภัย ตัวอย่างเช่น:
unreachable_unchecked เรียก copy_nonoverlapping ด้วยช่วงที่ทับซ้อนกัน ... )bool ที่ไม่ใช่ 0 หรือ 1 หรือการแบ่งแยกแจงนับที่ไม่ถูกต้อง) ยิ่งไปกว่านั้น Miri ยังจะแจ้งให้คุณทราบเกี่ยวกับหน่วยความจำรั่ว: เมื่อมีหน่วยความจำยังคงจัดสรรอยู่เมื่อสิ้นสุดการดำเนินการ และหน่วยความจำนั้นไม่สามารถเข้าถึงได้จาก Global static Miri จะแจ้งข้อผิดพลาด
คุณสามารถใช้ Miri เพื่อจำลองโปรแกรมบนเป้าหมายอื่นๆ ได้ เช่น เพื่อให้แน่ใจว่าการจัดการข้อมูลระดับไบต์ทำงานได้อย่างถูกต้องทั้งบนระบบ little-endian และ big-endian ดูการตีความข้ามด้านล่าง
มิริได้ค้นพบข้อบกพร่องในโลกแห่งความเป็นจริงมากมายแล้ว หากคุณพบข้อบกพร่องกับ Miri เราจะยินดีอย่างยิ่งหากคุณแจ้งให้เราทราบ แล้วเราจะเพิ่มมันเข้าไปในรายการ!
ตามค่าเริ่มต้น Miri จะรับรองการดำเนินการตามที่กำหนดโดยสมบูรณ์ และแยกโปรแกรมออกจากระบบโฮสต์ API บางตัวที่ปกติแล้วจะเข้าถึงโฮสต์ เช่น การรวบรวมเอนโทรปีสำหรับตัวสร้างตัวเลขสุ่ม ตัวแปรสภาพแวดล้อม และนาฬิกา จะถูกแทนที่ด้วยการใช้งาน "ปลอม" ที่กำหนดขึ้นเอง ตั้งค่า MIRIFLAGS="-Zmiri-disable-isolation" เพื่อเข้าถึง API ของระบบจริงแทน (โดยเฉพาะอย่างยิ่ง RNG API ของระบบ "ปลอม" ทำให้ Miri ไม่เหมาะกับการใช้การเข้ารหัส ! อย่าสร้างคีย์โดยใช้ Miri)
ทั้งหมดที่กล่าวมา โปรดทราบว่า Miri ไม่ได้ตรวจพบการละเมิดข้อกำหนด Rust ในโปรแกรมของคุณทุกครั้ง ไม่น้อยเพราะไม่มีข้อกำหนดดังกล่าว มิริใช้การประมาณค่าของตัวเองเกี่ยวกับสิ่งที่เป็นและไม่ใช่พฤติกรรมที่ไม่ได้กำหนดในสนิม เท่าที่เราทราบ Miri (ข้อบกพร่องแบบโมดูโล) ตรวจ พบพฤติกรรมที่ไม่ได้กำหนดทั้งหมดที่อาจส่งผลต่อความถูกต้องของโปรแกรม แต่คุณควรศึกษาข้อมูลอ้างอิงเพื่อดูคำจำกัดความอย่างเป็นทางการของพฤติกรรมที่ไม่ได้กำหนด Miri จะได้รับการอัปเดตด้วยคอมไพเลอร์ Rust เพื่อป้องกัน UB ตามที่คอมไพเลอร์ปัจจุบันเข้าใจ แต่ไม่มีคำมั่นสัญญาเกี่ยวกับสนิมเวอร์ชันในอนาคต
คำเตือนเพิ่มเติมที่ผู้ใช้ Miri ควรทราบ:
-Zrandomize-layout เพื่อตรวจหาบางกรณีเหล่านี้)-Zmiri-seed แต่นั่นจะยังไม่สำรวจการดำเนินการที่เป็นไปได้ทั้งหมด--target x86_64-unknown-linux-gnu เพื่อรับการสนับสนุนที่ดีขึ้นSeqCst ที่ไม่ได้รับอนุญาตจริง ๆ โดยโมเดลหน่วยความจำ Rust และไม่สามารถสร้างลักษณะการทำงานทั้งหมดที่อาจสังเกตได้บนฮาร์ดแวร์จริงยิ่งไปกว่านั้น Miri ไม่สามารถรับประกันได้ว่าโค้ดของคุณ มีเสียง ความสมบูรณ์เป็นคุณสมบัติของการไม่ก่อให้เกิดพฤติกรรมที่ไม่ได้กำหนดไว้เมื่อถูกเรียกใช้จากรหัสปลอดภัยที่กำหนดเอง แม้ว่าจะใช้ร่วมกับรหัสเสียงอื่นๆ ก็ตาม ในทางตรงกันข้าม Miri สามารถบอกคุณได้ว่า วิธีการโต้ตอบกับโค้ดของคุณด้วยวิธีใดวิธีหนึ่ง (เช่น ชุดทดสอบ) ทำให้เกิดพฤติกรรมที่ไม่ได้กำหนดไว้ ในการดำเนินการเฉพาะ หรือไม่ (ซึ่งอาจมีหลายอย่าง เช่น เมื่อเกิดการทำงานพร้อมกันหรือรูปแบบอื่นๆ ที่ไม่สามารถกำหนดได้ มีส่วนเกี่ยวข้อง) เมื่อ Miri พบ UB แสดงว่าโค้ดของคุณไม่มั่นคง แต่เมื่อ Miri ไม่พบ UB คุณอาจต้องทดสอบอินพุตเพิ่มเติมหรือตัวเลือกที่ไม่สามารถกำหนดได้ที่เป็นไปได้มากขึ้น
ติดตั้ง Miri บน Rust ทุกคืนผ่าน rustup :
rustup +nightly component add miri คำสั่งต่อไปนี้ทั้งหมดถือว่า toolchain ทุกคืนถูกปักหมุดผ่านการ rustup override set nightly หรือใช้ cargo +nightly สำหรับแต่ละคำสั่งต่อไปนี้
ตอนนี้คุณสามารถดำเนินโครงการของคุณใน Miri:
cargo miri testcargo miri runครั้งแรกที่คุณเรียกใช้ Miri เครื่องจะทำการตั้งค่าเพิ่มเติมและติดตั้งการขึ้นต่อกันบางอย่าง มันจะขอให้คุณยืนยันก่อนที่จะติดตั้งอะไร
cargo miri run/test รองรับแฟล็กเดียวกันกับ cargo run/test ตัวอย่างเช่น cargo miri test filter จะดำเนินการเฉพาะการทดสอบที่มี filter ในชื่อเท่านั้น
คุณสามารถส่งธงไปยังมิริผ่านทาง MIRIFLAGS ตัวอย่างเช่น MIRIFLAGS="-Zmiri-disable-stacked-borrows" cargo miri run รันโปรแกรมโดยไม่ตรวจสอบนามแฝงของการอ้างอิง
เมื่อคอมไพล์โค้ดผ่าน cargo miri ค่าสถานะการกำหนดค่า cfg(miri) จะถูกตั้งค่าสำหรับโค้ดที่จะถูกตีความภายใต้ Miri คุณสามารถใช้สิ่งนี้เพื่อละเว้นกรณีทดสอบที่ล้มเหลวภายใต้ Miri เนื่องจากกรณีเหล่านี้ทำสิ่งที่ Miri ไม่รองรับ:
# [ test ]
# [ cfg_attr ( miri , ignore ) ]
fn does_not_work_on_miri ( ) {
tokio :: run ( futures :: future :: ok :: < _ , ( ) > ( ( ) ) ) ;
}ไม่มีทางที่จะแสดงรายการสิ่งที่ไม่มีที่สิ้นสุดทั้งหมดที่มิริทำไม่ได้ แต่ล่ามจะบอกคุณอย่างชัดเจนเมื่อพบสิ่งที่ไม่รองรับ:
error: unsupported operation: can't call foreign function: bind
...
= help: this is likely not a bug in the program; it indicates that the program
performed an operation that Miri does not support
Miri ไม่เพียงแต่สามารถรันไบนารี่หรือชุดทดสอบสำหรับเป้าหมายโฮสต์ของคุณเท่านั้น แต่ยังสามารถทำการตีความข้ามสำหรับเป้าหมายต่างประเทศโดยพลการได้: cargo miri run --target x86_64-unknown-linux-gnu จะรันโปรแกรมของคุณเหมือนกับว่าเป็น Linux โปรแกรมไม่ว่าระบบปฏิบัติการโฮสต์ของคุณจะเป็นอย่างไร สิ่งนี้มีประโยชน์อย่างยิ่งหากคุณใช้ Windows เนื่องจากเป้าหมายของ Linux ได้รับการรองรับดีกว่าเป้าหมายของ Windows มาก
คุณยังสามารถใช้สิ่งนี้เพื่อทดสอบแพลตฟอร์มที่มีคุณสมบัติแตกต่างจากแพลตฟอร์มโฮสต์ของคุณ ตัวอย่างเช่น cargo miri test --target s390x-unknown-linux-gnu จะรันชุดการทดสอบของคุณบนเป้าหมาย big-endian ซึ่งมีประโยชน์สำหรับการทดสอบโค้ดที่ละเอียดอ่อนของ endian
บางส่วนของการดำเนินการจะถูกเลือกแบบสุ่มโดย Miri เช่น การจัดสรรที่อยู่ฐานที่แน่นอนจะถูกเก็บไว้ที่และการสลับเธรดที่ดำเนินการพร้อมกัน บางครั้ง อาจมีประโยชน์ในการสำรวจการดำเนินการต่างๆ หลายๆ แบบ เช่น เพื่อให้แน่ใจว่าโค้ดของคุณไม่ได้ขึ้นอยู่กับ "การวางตำแหน่งขั้นสูง" ของการจัดสรรใหม่โดยบังเอิญ และเพื่อทดสอบการสลับเธรดที่แตกต่างกัน ซึ่งสามารถทำได้ด้วยแฟล็ก --many-seeds :
cargo miri test --many-seeds # tries the seeds in 0..64
cargo miri test --many-seeds=0..16
ค่าเริ่มต้นของเมล็ดที่แตกต่างกัน 64 รายการค่อนข้างช้า ดังนั้นคุณอาจต้องการระบุช่วงที่เล็กลง
เมื่อรัน Miri บน CI ให้ใช้ตัวอย่างต่อไปนี้เพื่อติดตั้ง toolchain ทุกคืนด้วยส่วนประกอบ Miri:
rustup toolchain install nightly --component miri
rustup override set nightly
cargo miri testนี่คืองานตัวอย่างสำหรับ GitHub Actions:
miri :
name : " Miri "
runs-on : ubuntu-latest
steps :
- uses : actions/checkout@v4
- name : Install Miri
run : |
rustup toolchain install nightly --component miri
rustup override set nightly
cargo miri setup
- name : Test with Miri
run : cargo miri test cargo miri setup ที่ชัดเจนช่วยรักษาผลลัพธ์ของขั้นตอนการทดสอบจริงให้สะอาดอยู่เสมอ
Miri ไม่รองรับเป้าหมายทั้งหมดที่ Rust รองรับ อย่างไรก็ตาม ข่าวดีก็คือ ไม่ว่าระบบปฏิบัติการ/แพลตฟอร์มโฮสต์ของคุณจะเป็นอย่างไร การรันโค้ดสำหรับเป้าหมาย ใดๆ ที่ใช้ --target ก็เป็นเรื่องง่าย!
เป้าหมายต่อไปนี้ได้รับการทดสอบบน CI และควรใช้งานได้เสมอ (ตามระดับที่บันทึกไว้ด้านล่าง):
s390x-unknown-linux-gnu ได้รับการรองรับเป็น "เป้าหมายหลักที่เราเลือก"linux , macos หรือ windows โดยทั่วไปแล้ว Miri ควรใช้งานได้ แต่เราไม่ให้คำมั่นสัญญาและจะไม่ทำการทดสอบสำหรับเป้าหมายดังกล่าวsolaris / illumos : ดูแลโดย @devnexen รองรับ std::{env, thread, sync} แต่ไม่รองรับ std::fsfreebsd : ต้องการผู้ดูแล รองรับ std::env และบางส่วนของ std::{thread, fs} แต่ไม่ std::syncandroid : ต้องการผู้ดูแล การสนับสนุนไม่สมบูรณ์มาก แต่ "สวัสดีชาวโลก" ขั้นพื้นฐานใช้งานได้wasi : ต้องการคนดูแล รองรับการทำงานที่ไม่สมบูรณ์มาก แม้แต่เอาต์พุตมาตรฐานก็ใช้งานได้ แต่ฟังก์ชัน main ที่ว่างเปล่าก็ใช้งานได้main ด้วยซ้ำอย่างไรก็ตาม แม้แต่เป้าหมายที่เรารองรับ ระดับการรองรับในการเข้าถึง API ของแพลตฟอร์ม (เช่น ระบบไฟล์) ก็แตกต่างกันไปในแต่ละเป้าหมาย โดยทั่วไป เป้าหมายของ Linux จะได้รับการรองรับที่ดีที่สุด และเป้าหมายของ macOS มักจะพอๆ กัน Windows ได้รับการรองรับไม่ดีนัก
แม้ว่าจะใช้เธรดแบบ Rust แต่ Miri เองก็เป็นล่ามแบบเธรดเดียว ซึ่งหมายความว่าเมื่อรัน cargo miri test คุณอาจเห็นการเพิ่มขึ้นอย่างมากในระยะเวลาที่ใช้ในการรันชุดการทดสอบทั้งหมดของคุณ เนื่องจากการชะลอตัวของล่ามโดยธรรมชาติและการสูญเสียความขนาน
คุณสามารถรับความขนานของชุดทดสอบของคุณกลับมาได้โดยการรัน cargo miri nextest run -jN (โปรดทราบว่าคุณจะต้องติดตั้ง cargo-nextest ) วิธีนี้ได้ผลเนื่องจาก cargo-nextest รวบรวมรายการการทดสอบทั้งหมด จากนั้นจึงเริ่ม cargo miri run แยกกันสำหรับการทดสอบแต่ละครั้ง คุณจะต้องระบุ -j หรือ --test-threads ; โดยค่าเริ่มต้น cargo miri nextest run จะทำการทดสอบทีละรายการ สำหรับรายละเอียดเพิ่มเติม โปรดดูเอกสาร cargo-nextest ของ Miri
หมายเหตุ: โมเดลการทดสอบหนึ่งรายการต่อกระบวนการนี้หมายความว่า cargo miri test สามารถตรวจจับการแข่งขันของข้อมูลที่การทดสอบสองครั้งแข่งขันกันบนทรัพยากรที่ใช้ร่วมกัน แต่ cargo miri nextest run จะไม่ตรวจพบการแข่งขันดังกล่าว
หมายเหตุ: cargo-nextest ไม่รองรับ doctests โปรดดู nextest-rs/nextest#16
เมื่อใช้คำแนะนำข้างต้น คุณอาจพบข้อผิดพลาดของคอมไพเลอร์ที่ทำให้สับสนหลายประการ
RUST_BACKTRACE=1 เพื่อแสดง backtrace" คุณอาจเห็นสิ่งนี้เมื่อพยายามให้ Miri แสดงร่องรอยย้อนกลับ ตามค่าเริ่มต้น Miri จะไม่เปิดเผยสภาพแวดล้อมใดๆ ให้กับโปรแกรม ดังนั้นการรัน RUST_BACKTRACE=1 cargo miri test จะไม่เป็นไปตามที่คุณคาดหวัง
ในการรับ backtrace คุณต้องปิดการใช้งานการแยกโดยใช้ -Zmiri-disable-isolation :
RUST_BACKTRACE=1 MIRIFLAGS= " -Zmiri-disable-isolation " cargo miri test std ที่คอมไพล์โดยrustc เวอร์ชันที่เข้ากันไม่ได้" คุณอาจใช้งาน cargo miri ด้วยเวอร์ชันคอมไพเลอร์ที่แตกต่างจากเวอร์ชันที่ใช้สร้าง libstd แบบกำหนดเองที่ Miri ใช้ และ Miri ตรวจไม่พบสิ่งนั้น ลองรัน cargo miri clean ดูครับ
-Z และตัวแปรสภาพแวดล้อม Miri เพิ่มชุดแฟล็ก -Z ของตัวเอง ซึ่งโดยปกติจะตั้งค่าผ่านตัวแปรสภาพแวดล้อม MIRIFLAGS ก่อนอื่นเราจะจัดทำเอกสารแฟล็กที่เกี่ยวข้องและใช้บ่อยที่สุด:
-Zmiri-address-reuse-rate= เปลี่ยนความน่าจะเป็นที่การจัดสรร แบบ non-stack ที่ว่างจะถูกเพิ่มลงในพูลสำหรับการใช้ที่อยู่ซ้ำ และความน่าจะเป็นที่การจัดสรรแบบ non-stack ใหม่จะถูกพรากไปจากพูล การจัดสรรสแต็กจะไม่ถูกเพิ่มหรือนำออกจากพูล ค่าเริ่มต้นคือ 0.5-Zmiri-address-reuse-cross-thread-rate= เปลี่ยนความน่าจะเป็นที่การจัดสรรซึ่งพยายามนำบล็อกหน่วยความจำที่ว่างก่อนหน้านี้กลับมาใช้ใหม่จะพิจารณาบล็อกที่ว่างโดย เธรดอื่น ด้วย ค่าเริ่มต้นคือ 0.1 ซึ่งหมายความว่าโดยค่าเริ่มต้น ใน 90% ของกรณีที่พยายามใช้ที่อยู่ซ้ำ จะพิจารณาเฉพาะที่อยู่จากเธรดเดียวกันเท่านั้น การใช้ที่อยู่จากเธรดอื่นซ้ำจะทำให้เกิดการซิงโครไนซ์ระหว่างเธรดเหล่านั้น ซึ่งสามารถปกปิดการแข่งขันของข้อมูลและข้อบกพร่องของหน่วยความจำที่อ่อนแอได้-Zmiri-compare-exchange-weak-failure-rate= เปลี่ยนอัตราความล้มเหลวของการดำเนินการ compare_exchange_weak ค่าเริ่มต้นคือ 0.8 (ดังนั้น 4 ใน 5 การดำเนินการที่อ่อนแอจะล้มเหลว) คุณสามารถเปลี่ยนเป็นค่าใดก็ได้ระหว่าง 0.0 ถึง 1.0 โดยที่ 1.0 หมายความว่าจะล้มเหลวเสมอ และ 0.0 หมายความว่าจะไม่มีวันล้มเหลว โปรดทราบว่าการตั้งค่าเป็น 1.0 อาจทำให้แฮงค์ เนื่องจากหมายความว่าโปรแกรมที่ใช้ compare_exchange_weak ไม่สามารถดำเนินการได้-Zmiri-disable-isolation ปิดใช้งานการแยกโฮสต์ เป็นผลให้โปรแกรมสามารถเข้าถึงทรัพยากรโฮสต์ เช่น ตัวแปรสภาพแวดล้อม ระบบไฟล์ และการสุ่ม-Zmiri-disable-leak-backtraces ปิดใช้งานรายงาน backtraces สำหรับหน่วยความจำรั่ว ตามค่าเริ่มต้น Backtrace จะถูกบันทึกทุกครั้งที่มีการจัดสรรเมื่อมีการสร้าง เผื่อในกรณีที่ข้อมูลรั่วไหล ทำให้ต้องใช้หน่วยความจำบางส่วนในการจัดเก็บข้อมูลที่แทบไม่เคยใช้งาน การตั้งค่าสถานะนี้มีความหมายโดย -Zmiri-ignore-leaks-Zmiri-env-forward= ส่งต่อตัวแปรสภาพแวดล้อม var ไปยังโปรแกรมที่ตีความ สามารถนำมาใช้หลายครั้งเพื่อส่งต่อตัวแปรหลายตัว การดำเนินการจะยังคงถูกกำหนดไว้หากค่าของตัวแปรที่ส่งต่อยังคงเหมือนเดิม ไม่มีผลหากตั้งค่า -Zmiri-disable-isolation-Zmiri-env-set== ตั้งค่าตัวแปรสภาพแวดล้อม var ให้เป็น value ในโปรแกรมที่ตีความ สามารถใช้เพื่อส่งผ่านตัวแปรสภาพแวดล้อมโดยไม่จำเป็นต้องเปลี่ยนสภาพแวดล้อมของโฮสต์ สามารถใช้หลายครั้งเพื่อตั้งค่าตัวแปรหลายตัว หากตั้งค่า -Zmiri-disable-isolation หรือ -Zmiri-env-forward ค่าที่ตั้งค่าด้วยตัวเลือกนี้จะมีลำดับความสำคัญมากกว่าค่าจากสภาพแวดล้อมโฮสต์-Zmiri-ignore-leaks ปิดการใช้งานตัวตรวจสอบการรั่วไหลของหน่วยความจำ และยังอนุญาตให้มีเธรดที่เหลืออยู่บางส่วนอยู่เมื่อเธรดหลักออก-Zmiri-isolation-error= กำหนดค่าการตอบสนองของ Miri ต่อการดำเนินการที่ต้องการการเข้าถึงโฮสต์ในขณะที่เปิดใช้งานการแยก abort , hide , warn และ warn-nobacktrace เป็นการดำเนินการที่สนับสนุน ค่าเริ่มต้นคือ abort ซึ่งจะทำให้เครื่องหยุดทำงาน การดำเนินการบางอย่าง (แต่ไม่ใช่ทั้งหมด) ยังสนับสนุนการดำเนินการต่อเนื่องโดยมีข้อผิดพลาด "สิทธิ์ถูกปฏิเสธ" ถูกส่งกลับไปยังโปรแกรม warn จะพิมพ์ backtrace แบบเต็มทุกครั้งที่เกิดขึ้น warn-nobacktrace มีรายละเอียดน้อยกว่าและแสดงได้มากที่สุดหนึ่งครั้งต่อการดำเนินการ hide ซ่อนคำเตือนทั้งหมด-Zmiri-num-cpus ระบุจำนวน CPU ที่มีอยู่ที่จะรายงานโดย miri ตามค่าเริ่มต้น จำนวน CPU ที่มีอยู่คือ 1 โปรดทราบว่าแฟล็กนี้ไม่ส่งผลต่อวิธีที่ miri จัดการเธรด แต่อย่างใด-Zmiri-permissive-provenance ปิดการใช้งานคำเตือนสำหรับการแคสต์จำนวนเต็มถึงตัวชี้และ ptr::with_exposed_provenance สิ่งนี้จำเป็นต้องพลาดข้อบกพร่องบางอย่างเนื่องจากการดำเนินการเหล่านั้นไม่สามารถนำไปใช้ในน้ำยาฆ่าเชื้อได้อย่างมีประสิทธิภาพและแม่นยำ แต่จะพลาดเฉพาะข้อบกพร่องที่เกี่ยวข้องกับหน่วยความจำ/พอยน์เตอร์ที่อยู่ภายใต้การดำเนินการเหล่านี้-Zmiri-preemption-rate กำหนดค่าความน่าจะเป็นที่เมื่อสิ้นสุดบล็อกพื้นฐาน เธรดที่ใช้งานอยู่จะถูกจองล่วงหน้า ค่าเริ่มต้นคือ 0.01 (เช่น 1%) การตั้งค่านี้เป็น 0 จะปิดใช้การจอง-Zmiri-report-progress ทำให้ Miri พิมพ์ stacktrace ปัจจุบันเป็นระยะๆ เพื่อให้คุณสามารถบอกได้ว่ากำลังทำอะไรอยู่เมื่อโปรแกรมยังคงทำงานต่อไป คุณสามารถปรับแต่งความถี่ในการพิมพ์รายงานผ่าน -Zmiri-report-progress= ซึ่งจะพิมพ์รายงานทุกๆ N บล็อกพื้นฐาน-Zmiri-seed= กำหนดค่า seed ของ RNG ที่ Miri ใช้เพื่อแก้ไขสิ่งที่ไม่กำหนด RNG นี้ใช้เพื่อเลือกที่อยู่พื้นฐานสำหรับการจัดสรร เพื่อกำหนดการสำรองและความล้มเหลวของ compare_exchange_weak และเพื่อควบคุมการบัฟเฟอร์ของร้านค้าสำหรับการจำลองหน่วยความจำที่อ่อนแอ เมื่อเปิดใช้งานการแยก (ค่าเริ่มต้น) สิ่งนี้จะถูกใช้เพื่อจำลองเอนโทรปีของระบบด้วย ค่าเริ่มต้นคือ 0 คุณสามารถเพิ่มความครอบคลุมของการทดสอบได้โดยการเรียกใช้ Miri หลายครั้งโดยใช้ค่าเริ่มต้นที่แตกต่างกัน-Zmiri-strict-provenance มาช่วยให้การตรวจสอบแหล่งที่มาอย่างเข้มงวดใน Miri ซึ่งหมายความว่าการส่งจำนวนเต็มไปยังพอยน์เตอร์จะให้ผลลัพธ์ที่มีที่มาที่ 'ไม่ถูกต้อง' กล่าวคือ ด้วยที่มาที่ไม่สามารถใช้สำหรับการเข้าถึงหน่วยความจำใดๆ-Zmiri-symbolic-alignment-check ทำให้การตรวจสอบการจัดตำแหน่งเข้มงวดมากขึ้น ตามค่าเริ่มต้น การจัดตำแหน่งจะถูกตรวจสอบโดยการชี้ตัวชี้ไปที่จำนวนเต็ม และตรวจสอบให้แน่ใจว่าเป็นการจัดตำแหน่งแบบทวีคูณ สิ่งนี้สามารถนำไปสู่กรณีที่โปรแกรมผ่านการตรวจสอบการจัดตำแหน่งโดยบังเอิญ เนื่องจากสิ่งต่าง ๆ "เกิดขึ้น" สอดคล้องกันอย่างเพียงพอ - ไม่มี UB ในการดำเนินการนี้ แต่จะมี UB ในการดำเนินการอื่น เพื่อหลีกเลี่ยงกรณีดังกล่าว การตรวจสอบการจัดตำแหน่งเชิงสัญลักษณ์จะพิจารณาเฉพาะการจัดตำแหน่งที่ร้องขอของการจัดสรรที่เกี่ยวข้อง และออฟเซ็ตในการจัดสรรนั้น วิธีนี้จะหลีกเลี่ยงไม่ให้ข้อบกพร่องดังกล่าวหายไป แต่ยังทำให้เกิดผลบวกลวงเมื่อโค้ดคำนวณเลขจำนวนเต็มด้วยตนเองเพื่อให้แน่ใจว่ามีการจัดตำแหน่ง (เมธอดไลบรารีมาตรฐาน align_to ทำงานได้ดีในทั้งสองโหมด ภายใต้การจัดตำแหน่งเชิงสัญลักษณ์ จะเติมเฉพาะส่วนตรงกลางเมื่อการจัดสรรรับประกันการจัดตำแหน่งที่เพียงพอ)ธงที่เหลือมีไว้สำหรับการใช้งานขั้นสูงเท่านั้น และมีแนวโน้มที่จะเปลี่ยนแปลงหรือถูกลบออก สิ่งเหล่านี้บางส่วน ไม่ปลอดภัย ซึ่งหมายความว่าอาจทำให้ Miri ล้มเหลวในการตรวจจับกรณีของพฤติกรรมที่ไม่ได้กำหนดในโปรแกรม
-Zmiri-disable-alignment-check ปิดใช้งานการตรวจสอบการจัดตำแหน่งตัวชี้ ดังนั้นคุณจึงสามารถมุ่งเน้นไปที่ความล้มเหลวอื่นๆ ได้ แต่นั่นหมายความว่า Miri อาจพลาดจุดบกพร่องในโปรแกรมของคุณ การใช้ธงนี้ถือว่า ไม่ปลอดภัย-Zmiri-disable-data-race-detector ปิดใช้งานการตรวจสอบการแข่งขันข้อมูล การใช้ธงนี้ถือว่า ไม่ปลอดภัย -Zmiri-disable-weak-memory-emulation นี่หมายถึง-Zmiri-disable-stacked-borrows ปิดการใช้งานการตรวจสอบกฎนามแฝงทดลองเพื่อติดตามการยืม (Stacked Borrows และ Tree Borrows) สิ่งนี้สามารถทำให้ Miri ทำงานเร็วขึ้น แต่ก็หมายความว่าจะไม่มีการตรวจพบการละเมิดนามแฝงด้วย การใช้แฟล็กนี้ ไม่ปลอดภัย (แต่กฎความสมบูรณ์ที่ได้รับผลกระทบยังอยู่ในช่วงทดลอง) ธงในภายหลังจะมีความสำคัญกว่า: การติดตามการยืมสามารถเปิดใช้งานอีกครั้งได้โดย -Zmiri-tree-borrows-Zmiri-disable-validation ปิดใช้งานการบังคับใช้ค่าคงที่ความถูกต้อง ซึ่งถูกบังคับใช้ตามค่าเริ่มต้น สิ่งนี้มีประโยชน์เป็นส่วนใหญ่ในการมุ่งเน้นไปที่ความล้มเหลวอื่นๆ (เช่น การเข้าถึงนอกขอบเขต) ก่อน การตั้งค่าสถานะนี้หมายความว่า Miri สามารถพลาดจุดบกพร่องในโปรแกรมของคุณได้ อย่างไรก็ตาม สิ่งนี้สามารถช่วยให้มิริวิ่งเร็วขึ้นได้เช่นกัน การใช้ธงนี้ถือว่า ไม่ปลอดภัย-Zmiri-disable-weak-memory-emulation ปิดการใช้งานการจำลองเอฟเฟกต์หน่วยความจำที่อ่อนแอของ C ++ 11-Zmiri-native-lib= เป็นแฟล็กทดลองสำหรับการให้การสนับสนุนสำหรับการเรียกใช้ฟังก์ชันเนทิฟจากภายในล่ามผ่าน FFI ฟังก์ชั่นที่ไม่ได้มาจากไฟล์นั้นยังคงดำเนินการผ่าน Miri shims ตามปกติ คำเตือน : หากมีการระบุไฟล์ .so ที่ไม่ถูกต้อง/ไม่ถูกต้อง สิ่งนี้อาจทำให้เกิดพฤติกรรมที่ไม่ได้กำหนดในตัว Miri ได้! และแน่นอนว่า Miri ไม่สามารถตรวจสอบการทำงานของโค้ดเนทีฟได้ โปรดทราบว่า Miri มีการจัดการ file descriptor เป็นของตัวเอง ดังนั้น หากคุณต้องการแทนที่ฟังก์ชัน บางอย่าง ที่ทำงานบน file descriptor คุณจะต้องแทนที่ ทั้งหมด ไม่เช่นนั้น file descriptors ทั้งสองประเภทจะปะปนกัน นี้เป็น งานระหว่างดำเนินการ ; ในปัจจุบัน รองรับเฉพาะอาร์กิวเมนต์จำนวนเต็มและค่าส่งคืนเท่านั้น (และไม่ การใช้ตัวชี้/จำนวนเต็มเพื่อแก้ไขข้อ จำกัด นี้จะไม่ทำงาน พวกเขาจะล้มเหลวอย่างน่ากลัว) ขณะนี้ยังใช้ได้กับโฮสต์ Unix เท่านั้น-Zmiri-measureme= เปิดใช้งานการสร้างโปรไฟล์ measureme สำหรับโปรแกรมที่แปล สามารถใช้ค้นหาว่าส่วนใดของโปรแกรมของคุณที่ทำงานช้าภายใต้ Miri โปรไฟล์ถูกเขียนลงในไฟล์ภายในไดเร็กทอรีชื่อ -Zmiri-mute-stdout-stderr จะเพิกเฉยต่อการเขียนทั้งหมดไปยัง stdout และ stderr แต่จะรายงานไปยังโปรแกรมว่าเขียนจริงหรือไม่ สิ่งนี้มีประโยชน์เมื่อคุณไม่สนใจเอาต์พุตของโปรแกรมจริง แต่ต้องการดูข้อผิดพลาดและคำเตือนของ Miri เท่านั้น-Zmiri-recursive-validation เป็นแฟล็ก ทดลองขั้นสูง ที่ทำให้การตรวจสอบความถูกต้องถูกเรียกซ้ำด้านล่างการอ้างอิง-Zmiri-retag-fields[=] ควบคุมเมื่อ Stacked Borrows การติดแท็กซ้ำลงในฟิลด์ all หมายถึงการเรียกซ้ำเสมอ (ค่าเริ่มต้นและเทียบเท่ากับ -Zmiri-retag-fields โดยไม่มีค่าที่ชัดเจน) none หมายความว่าจะไม่เรียกซ้ำ ส scalar หมายความว่าเรียกซ้ำเฉพาะประเภทที่เราจะปล่อยคำอธิบายประกอบ noalias ใน LLVM IR ที่สร้างขึ้นด้วย ( ชนิดที่ส่งผ่านเป็นสเกลาร์เดี่ยวหรือสเกลาร์คู่) การตั้งค่านี้เป็น none ถือว่า ไม่ปลอดภัย-Zmiri-provenance-gc= กำหนดค่าความถี่ที่ตัวรวบรวมขยะแหล่งที่มาของตัวชี้ทำงาน ค่าเริ่มต้นคือการค้นหาและลบแหล่งที่มาที่ไม่สามารถเข้าถึงได้ทุกๆ 10000 บล็อกพื้นฐาน การตั้งค่านี้เป็น 0 จะปิดใช้งานตัวรวบรวมขยะ ซึ่งทำให้บางโปรแกรมมีการใช้หน่วยความจำแบบระเบิดและ/หรือรันไทม์แบบซูเปอร์ลิเนียร์-Zmiri-track-alloc-accesses ไม่เพียงแสดงการจัดสรรและกิจกรรมฟรีสำหรับการจัดสรรแบบติดตาม แต่ยังอ่านและเขียนอีกด้วย-Zmiri-track-alloc-id=,,... แสดงการติดตามย้อนกลับเมื่อมีการจัดสรรหรือปล่อยการจัดสรรที่กำหนด ซึ่งจะช่วยในการแก้ไขจุดบกพร่องหน่วยความจำรั่วและใช้งานหลังจากจุดบกพร่องฟรี การระบุอาร์กิวเมนต์นี้หลายครั้งไม่ได้เขียนทับค่าก่อนหน้า แต่จะผนวกค่าเข้ากับรายการแทน การแสดง ID หลายครั้งไม่มีผล-Zmiri-track-pointer-tag=,,... แสดง backtrace เมื่อแท็กตัวชี้ที่กำหนดถูกสร้างขึ้น และเมื่อ (ถ้าเคย) มันถูกดึงออกมาจากสแต็กยืม (ซึ่งเป็นที่ที่แท็กจะกลายเป็น ไม่ถูกต้องและการใช้งานในอนาคตจะเกิดข้อผิดพลาด) สิ่งนี้จะช่วยคุณในการค้นหาว่าเหตุใด UB จึงเกิดขึ้น และที่ใดในโค้ดของคุณจะเป็นที่ที่ดีในการค้นหา การระบุอาร์กิวเมนต์นี้หลายครั้งไม่ได้เขียนทับค่าก่อนหน้า แต่จะผนวกค่าเข้ากับรายการแทน การแสดงแท็กหลายครั้งไม่มีผล-Zmiri-track-weak-memory-loads แสดง backtrace เมื่อการจำลองหน่วยความจำที่อ่อนแอส่งคืนค่าที่ล้าสมัยจากการโหลด ซึ่งสามารถช่วยวินิจฉัยปัญหาที่หายไปภายใต้ -Zmiri-disable-weak-memory-emulation-Zmiri-tree-borrows แทนที่ Stacked Borrows ด้วยกฎ Tree Borrows Tree Borrows นั้นมีการทดลองมากกว่า Stacked Borrows ในขณะที่ Tree Borrows ยังคงฟังดูดีในแง่ของการตรวจจับการละเมิดนามแฝงทั้งหมดที่คอมไพเลอร์เวอร์ชันปัจจุบันอาจใช้ประโยชน์ มีความเป็นไปได้ว่าโมเดลนามแฝงขั้นสุดท้ายของ Rust จะเข้มงวดกว่า Tree Borrows กล่าวอีกนัยหนึ่ง หากคุณใช้ Tree Borrows แม้ว่ารหัสของคุณจะได้รับการยอมรับในวันนี้ แต่รหัสนั้นอาจถูกประกาศให้เป็น UB ในอนาคต สิ่งนี้มีโอกาสน้อยมากเมื่อใช้ Stacked Borrows-Zmiri-force-page-size= แทนที่ขนาดหน้าเริ่มต้นสำหรับสถาปัตยกรรมเป็นทวีคูณของ 1k 4 เป็นค่าเริ่มต้นสำหรับเป้าหมายส่วนใหญ่ ค่านี้ควรเป็นกำลัง 2 และไม่ใช่ศูนย์เสมอ-Zmiri-unique-is-unique ทำการตรวจสอบนามแฝงเพิ่มเติมสำหรับ core::ptr::Unique เพื่อให้แน่ใจว่าในทางทฤษฎีสามารถพิจารณาได้ว่า noalias แฟล็กนี้เป็นการทดลองและมีผลเฉพาะเมื่อใช้กับ -Zmiri-tree-borrows ธงrustc -Z ดั้งเดิมบางรายการมีความเกี่ยวข้องอย่างมากกับ Miri:
-Zmir-opt-level ควบคุมจำนวนการเพิ่มประสิทธิภาพ MIR Miri แทนที่ค่าเริ่มต้นเป็น 0 ; โปรดทราบว่าการใช้ระดับที่สูงกว่าอาจทำให้ Miri พลาดจุดบกพร่องในโปรแกรมของคุณได้ เนื่องจากข้อบกพร่องเหล่านั้นได้รับการปรับให้เหมาะสมแล้ว-Zalways-encode-mir ทำให้ MIR ดัมพ์ของสนิมแม้สำหรับฟังก์ชัน monomorphic ที่สมบูรณ์ นี่เป็นสิ่งจำเป็นเพื่อให้ Miri สามารถเรียกใช้ฟังก์ชันดังกล่าวได้ ดังนั้น Miri จึงตั้งค่าสถานะนี้ตามค่าเริ่มต้น-Zmir-emit-retag ควบคุมว่าจะปล่อยคำสั่ง Retag หรือไม่ Miri เปิดใช้งานสิ่งนี้ตามค่าเริ่มต้น เนื่องจากจำเป็นสำหรับ Stacked Borrows และ Tree Borrowsนอกจากนี้ Miri ยังจดจำตัวแปรสภาพแวดล้อมบางอย่าง:
MIRIFLAGS กำหนดธงพิเศษที่จะส่งผ่านไปยัง MiriMIRI_LIB_SRC กำหนดไดเร็กทอรีที่ Miri คาดหวังแหล่งที่มาของไลบรารีมาตรฐานที่จะสร้างและใช้สำหรับการตีความ ไดเร็กทอรีนี้ต้องชี้ไปที่ไดเร็กทอรีย่อย library ของการชำระเงินที่เก็บ rust-lang/rustMIRI_SYSROOT ระบุ sysroot ที่จะใช้ เมื่อใช้ cargo miri test / cargo miri run สิ่งนี้จะข้ามการตั้งค่าอัตโนมัติ - ตั้งค่านี้เฉพาะเมื่อคุณไม่ต้องการใช้ sysroot ที่สร้างขึ้นโดยอัตโนมัติ เมื่อเรียกใช้ cargo miri setup สิ่งนี้จะระบุตำแหน่งที่ sysroot จะถูกวางไว้MIRI_NO_STD ทำให้แน่ใจว่า sysroot ของเป้าหมายถูกสร้างขึ้นโดยไม่มี libstd ซึ่งช่วยให้สามารถทดสอบและรันโปรแกรม no_std ได้ โดยปกติไม่ควรใช้ สิ่งนี้ Miri มีฮิวริสติกในการตรวจจับเป้าหมายที่ไม่มาตรฐานตามชื่อเป้าหมาย การตั้งค่านี้บนเป้าหมายที่รองรับ libstd อาจทำให้เกิดผลลัพธ์ที่สับสนได้ extern ของ Miri Miri มีฟังก์ชัน extern บางอย่างที่โปรแกรมสามารถนำเข้าเพื่อเข้าถึงฟังก์ชันเฉพาะของ Miri มีการประกาศใน /tests/utils/miri_extern.rs
ไบนารีที่ไม่ได้ใช้ไลบรารีมาตรฐานจะต้องประกาศฟังก์ชันเช่นนี้เพื่อให้ Miri รู้ว่าควรจะเริ่มดำเนินการที่ไหน:
# [ cfg ( miri ) ]
# [ no_mangle ]
fn miri_start ( argc : isize , argv : * const * const u8 ) -> isize {
// Call the actual start function that your project implements, based on your target's conventions.
} หากคุณต้องการมีส่วนร่วมกับ Miri เยี่ยมมาก! โปรดดูคู่มือการมีส่วนร่วมของเรา
หากต้องการความช่วยเหลือในการใช้งาน Miri คุณสามารถเปิดปัญหาได้ที่นี่บน GitHub หรือใช้สตรีม Miri บน Rust Zulip
โครงการนี้เริ่มต้นโดยเป็นส่วนหนึ่งของหลักสูตรการวิจัยระดับปริญญาตรีในปี 2558 โดย @solson ที่มหาวิทยาลัยซัสแคตเชวัน มีสไลด์และรายงานจากโครงการนั้น ในปี 2559 @oli-obk เข้าร่วมเพื่อเตรียม Miri เพื่อใช้เป็นผู้ประเมิน const ในคอมไพเลอร์ Rust ในที่สุด (โดยทั่วไปสำหรับ const และเนื้อหา static ) แทนที่ผู้ประเมินเก่าที่ทำงานโดยตรงกับ AST ในปี 2560 @RalfJung ฝึกงานกับ Mozilla และเริ่มพัฒนา Miri ไปสู่เครื่องมือสำหรับการตรวจจับพฤติกรรมที่ไม่ได้กำหนด และใช้ Miri เป็นวิธีในการสำรวจผลที่ตามมาจากคำจำกัดความที่เป็นไปได้ต่าง ๆ สำหรับพฤติกรรมที่ไม่ได้กำหนดใน Rust การย้ายเอ็นจิ้น Miri ของ @ oli-obk ไปยังคอมไพเลอร์ในที่สุดก็เสร็จสิ้นในต้นปี 2561 ในขณะเดียวกันในปีต่อมา @RalfJung ได้ฝึกงานครั้งที่สองพัฒนา Miri เพิ่มเติมด้วยการสนับสนุนสำหรับการตรวจสอบค่าคงที่ประเภทพื้นฐานและตรวจสอบว่ามีการใช้การอ้างอิงตาม ตามข้อจำกัดนามแฝง
Miri พบจุดบกพร่องจำนวนหนึ่งแล้วในไลบรารีมาตรฐานของ Rust และที่อื่นๆ ซึ่งบางส่วนเรารวบรวมไว้ที่นี่ หาก Miri ช่วยคุณค้นหาจุดบกพร่อง UB เล็กๆ น้อยๆ ในโค้ดของคุณ เรายินดีเป็นอย่างยิ่งที่ PR เพิ่มมันลงในรายการ!
พบข้อบกพร่องที่แน่นอน:
Debug for vec_deque::Iter เข้าถึงหน่วยความจำที่ไม่ได้เตรียมใช้งานVec::into_iter ทำการอ่าน ZST ที่ไม่ได้จัดแนวFrom<&[T]> for Rc การสร้างการอ้างอิงที่จัดชิดไม่เพียงพอBTreeMap สร้างการอ้างอิงที่ใช้ร่วมกันซึ่งชี้ไปที่การจัดสรรน้อยเกินไปVec::append เพื่อสร้างการอ้างอิงแบบห้อยstr เปลี่ยนการอ้างอิงที่ใช้ร่วมกันให้เป็นการอ้างอิงที่ไม่แน่นอนrand ทำการอ่านที่ไม่สอดคล้องกันposix_memalign ด้วยวิธีที่ไม่ถูกต้องgetrandom เรียก getrandom syscall ในลักษณะที่ไม่ถูกต้องVec และ BTreeMap หน่วยความจำรั่วภายใต้เงื่อนไขบางประการ (ตื่นตระหนก)beefEbrCell ใช้หน่วยความจำที่ไม่ได้เตรียมใช้งานไม่ถูกต้องservo_arc สร้างการอ้างอิงที่ใช้ร่วมกันแบบห้อยต่องแต่งencoding_rs ทำการคำนวณตัวชี้นอกขอบเขตVec::from_raw_parts ไม่ถูกต้องAtomicPtr และ Box::from_raw_inThinVeccrossbeam-epoch เรียก assume_init บน MaybeUninit ที่เตรียมใช้งานบางส่วนinteger-encoding เพื่อยกเลิกการอ้างอิงตัวชี้ที่ไม่ตรงแนวrkyv กำลังสร้าง Box<[u8]> จากการจัดสรรแบบโอเวอร์ไลน์arc-swapthread::scoperegex จัดการบัฟเฟอร์ Vec ที่ไม่ได้จัดแนวอย่างไม่ถูกต้องcompare_exchange_weak ใน once_cell ไม่ถูกต้องvec::IntoIterIterator::collect แบบแทนที่portable-atomic-utilstd::mpsc (รหัสต้นฉบับในรูปแบบ crossbeam)การละเมิด Stacked Borrows พบว่าน่าจะเป็นข้อบกพร่อง (แต่ปัจจุบัน Stacked Borrows เป็นเพียงการทดลอง):
VecDeque::drain สร้างการอ้างอิงที่ไม่แน่นอนที่ทับซ้อนกันBTreeMap ต่างๆBTreeMap สร้างการอ้างอิงที่ไม่แน่นอนซึ่งทับซ้อนกับการอ้างอิงที่ใช้ร่วมกันBTreeMap::iter_mut สร้างการอ้างอิงที่ไม่แน่นอนที่ทับซ้อนกันBTreeMap โดยใช้พอยน์เตอร์ดิบนอกพื้นที่หน่วยความจำที่ถูกต้องLinkedList สร้างการอ้างอิงที่ไม่แน่นอนที่ทับซ้อนกันVec::push ทำให้การอ้างอิงที่มีอยู่เป็นโมฆะลงในเวกเตอร์align_to_mut ละเมิดเอกลักษณ์ของการอ้างอิงที่ไม่แน่นอนsized-chunks ที่สร้างการอ้างอิงที่ไม่แน่นอนนามแฝงString::push_str ทำให้การอ้างอิงที่มีอยู่ในสตริงใช้ไม่ได้ryu ใช้พอยน์เตอร์ดิบนอกพื้นที่หน่วยความจำที่ถูกต้องEnv โดยใช้ตัวชี้ดิบนอกพื้นที่หน่วยความจำที่ถูกต้องVecDeque::iter_mut สร้างการอ้างอิงที่ไม่แน่นอนที่ทับซ้อนกัน<[T]>::copy_within ใช้เงินกู้หลังจากทำให้เป็นโมฆะ ได้รับอนุญาตภายใต้ข้อใดข้อหนึ่ง
ตามตัวเลือกของคุณ
เว้นแต่คุณจะระบุไว้เป็นอย่างอื่นอย่างชัดเจน ผลงานใดๆ ที่ส่งโดยเจตนาเพื่อรวมไว้ในผลงานของคุณจะได้รับอนุญาตแบบคู่ตามข้างต้น โดยไม่มีข้อกำหนดหรือเงื่อนไขเพิ่มเติม
