3.4 - בניית הפשטה בטוחה וסקירת חובות ההוכחה - הרצאה

ממשק בטוח צריך להיות בטוח גם ללקוח יצירתי

נניח שכתבנו פונקציה בטוחה שמקבלת raw pointer ואורך ומחזירה פרוסה. בגוף הוספנו unsafe וקראנו ל־from_raw_parts. הדוגמה שלנו משתמשת במצביע תקף ועובדת, אבל לקוח אחר יכול למסור null או כתובת שכבר שוחררה. אם החתימה אינה מטילה עליו שום חובה מיוחדת, הפונקציה שלנו חשפה API שאינו sound.

המשמעות של soundness היא שכל שימוש מותר דרך הממשק הבטוח שומר על חוזי השפה. בדיקת הדוגמה שבחרנו אינה מספיקה. צריך לשאול אילו ערכים הקורא רשאי למסור, אילו סדרי פעולות הוא רשאי לבצע, והאם ניתן באמצעותם להגיע להפרת זיכרון בתוך המימוש שלנו.

טיעון על שני טווחים

נבנה גרסה לימודית בטוחה של חלוקת פרוסה בלעדית. המקור כבר מספק חיי נתון, יישור ואתחול. עלינו להוכיח שהחלוקה נשארת בטווח ושהתוצאות אינן חופפות.

fn split_checked<T>(values: &mut [T], middle: usize)
    -> Option<(&mut [T], &mut [T])>
{
    let len = values.len();
    if middle > len {
        return None;
    }
    let pointer = values.as_mut_ptr();
    // SAFETY: the original slice grants exclusive access to len elements.
    // The checked split partitions that region into disjoint ranges.
    // Both returned borrows are tied to the original borrow.
    unsafe {
        Some((
            std::slice::from_raw_parts_mut(pointer, middle),
            std::slice::from_raw_parts_mut(pointer.add(middle), len - middle),
        ))
    }
}

fn main() {
    let mut values = [1, 2, 3, 4];
    let (left, right) = split_checked(&mut values, 2).unwrap();
    left[0] = 10;
    right[0] = 30;
    assert_eq!(values, [10, 2, 30, 4]);
}

הבדיקה מתבצעת לפני חישוב ההפרש ולפני הוספת offset. שני הטווחים יחד מכסים בדיוק את המקור ואינם חופפים באיברים. חיי ההפניות המוחזרות קשורים להשאלת values, ולכן הקורא אינו יכול להשתמש במקור באופן שסותר את ההרשאה כל עוד התוצאות עוד בשימוש.

הטיעון צריך להתייחס גם לחיתוך באפס ובסוף. פרוסה ריקה עדיין דורשת מצביע מתאים לפי חוזה הבנייה, והמצביע שמגיע מפרוסה קיימת מספק את הבסיס לכך. עבור טיפוסים בגודל אפס הכתובות עשויות להיות זהות, אבל הטווחים הלוגיים עדיין מחולקים. אין לבדוק soundness רק באמצעות השוואת כתובות מספריות.

פונקציה לא בטוחה מצהירה על חובות הקורא

אם באמת צריך לקבל raw pointer חיצוני, ניתן להגדיר פונקציה unsafe ולתעד את החובות שלה. המילה unsafe אינה הודעה שהמימוש עושה משהו חשוד; היא מציינת תנאי שהמערכת הטיפוסית אינה אוכפת עבור הקורא.

דוגמת חתימה כזאת צריכה לומר שהמצביע מייצג טווח תקף, מאוחסן ומיושר, שהבייטים מאותחלים ושחיי האחסון מכסים את ההפניה המוחזרת. אם מוחזרת הפניה בלעדית, נדרשת גם בלעדיות מתאימה. זמן חיים חופשי בחתימה אינו יוצר אף אחת מן העובדות האלה.

גם בתוך unsafe fn נכתוב בלוק unsafe מפורש סביב הפעולה שדורשת אותו. כך אפשר להבחין בין חובות הקורא לבין הפעולות שבהן המימוש מסתמך עליהן. במהדורת השפה שבקורס נרצה שההבחנה תהיה גלויה גם כאשר הקומפיילר יכול להסתפק באזהרה לפי הגדרות הלינט.

מעטפת שמחזיקה את יחס ההשאלה

נבנה עטיפה למצביע שנוצר מהפניה בלעדית. הסמן שלה מבטא את ההשאלה המקורית:

use std::marker::PhantomData;
use std::ptr::NonNull;

struct Borrowed<'a, T> {
    pointer: NonNull<T>,
    lifetime: PhantomData<&'a mut T>,
}

impl<'a, T> Borrowed<'a, T> {
    fn new(value: &'a mut T) -> Self {
        Self { pointer: NonNull::from(value), lifetime: PhantomData }
    }
    fn get(&self) -> &T {
        // SAFETY: construction keeps the original exclusive borrow alive;
        // a shared borrow of the wrapper only exposes shared access.
        unsafe { self.pointer.as_ref() }
    }
    fn get_mut(&mut self) -> &mut T {
        // SAFETY: mutable access to the wrapper is exclusive and no
        // existing returned borrow can overlap this use.
        unsafe { self.pointer.as_mut() }
    }
}

fn main() {
    let mut value = 7;
    {
        let mut borrowed = Borrowed::new(&mut value);
        *borrowed.get_mut() += 1;
        assert_eq!(*borrowed.get(), 8);
    }
    assert_eq!(value, 8);
}

העטיפה אינה צריכה כאן יתרון ביצועים כדי להצדיק מוצר אמיתי; היא כלי לימוד לקשר בין מצביע גולמי, זמן חיים וממשק בטוח. לא הוספנו constructor בטוח ממספר שרירותי, ולא הוספנו מימוש ידני של Send או Sync. כל הרחבה כזאת הייתה מוסיפה חובת הוכחה חדשה.

סקירה לפי פעולות לקוח

כדי לבדוק מעטפת, נסו להשתמש בה בסדרים לא נוחים: לבקש שתי הפניות בלעדיות, להשמיד את המקור מוקדם, להעביר את העטיפה למקום אחר ולקרוא מתודה אחרי שינוי. חלק מהניסיונות צריכים להידחות בזמן קומפילציה, ואחרים צריכים להיות חוקיים ולשמור על הנתונים.

בדיקה חשובה נוספת היא פאניקה באמצע פעולה. האם כבר נכתב ערך אבל מונה הבעלות עוד לא עודכן? האם guard קיים בזמן קריאה ל־callback חיצוני? בדיקה עם קלט רגיל אינה מכסה את המעברים האלה, ולכן נפרק את הפעולה לנקודות שבהן האינווריאנט משתנה.

המבחן המרכזי אינו כמה בלוקי unsafe הצלחנו להסתיר. המבחן הוא האם הלקוחות הבטוחים מקבלים יכולות שאכן אפשר לקיים. הגדרת התקפות והבטיחות במפרט נותנת את המסגרת, והקוד שלנו צריך לספק את הטיעון המיוחד למבנה שהוא מנהל.