1.10 - תקינות והתנהגות לא מוגדרת - הרצאה

הקוד עבד אתמול

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

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

הקוד הבא מדגים הנחה שהמהדר רשאי לנצל:

bool grows(int value) {
    return value + 1 > value;
}

לכל ערך שעבורו החיבור החתום מוגדר ואינו גולש, התוצאה נכונה. אם הקורא מוסר את הערך המרבי של int, החיבור יוצר signed overflow. לא מתקנים זאת על ידי ציפייה שהערך יסתובב למספר שלילי; זאת אינה ההבטחה של חיבור signed ב־C++20.

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

בדיקה לפני הפעולה

תוכנית שרוצה להגדיל מספר ולדווח על חריגה צריכה לבדוק לפני החיבור:

#include <cstdio>
#include <limits>
#include <optional>

std::optional<int> increment_checked(int value) {
    if (value == std::numeric_limits<int>::max()) {
        return std::nullopt;
    }
    return value + 1;
}

int main() {
    if (auto result = increment_checked(5)) {
        std::printf("%d\n", *result);
    }
    if (!increment_checked(std::numeric_limits<int>::max())) {
        std::puts("overflow rejected");
    }
}

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

דוגמת חקירה עם AddressSanitizer

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

#include <cstdio>

int main() {
    int* value = new int(42);
    delete value;
    std::printf("%d\n", *value);
}

שומרים את הקוד בקובץ use_after_free.cpp ובונים עם סביבת MSVC שתומכת ב־AddressSanitizer:

cl /nologo /std:c++20 /EHsc /Zi /Od /fsanitize=address use_after_free.cpp /Fe:uaf.exe
uaf.exe

הכלי מוסיף instrumentation ומידע עזר כדי לזהות סוגים מסוימים של גישות לא חוקיות. תצורת כלים נתמכת אמורה לדווח כאן על heap-use-after-free, עם מידע על גישה, הקצאה ושחרור. אם הכלי חסר או שהדוגמה אינה נבנית, בודקים את התקנתו ולא מסירים את הדגל כדי להציג הרצה רגילה כבדיקת תקינות.

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

שלוש כתובות שצריך לחבר

בחקירת use-after-free לא מספיק להסתכל בשורת הקריסה. צריך לזהות את מקום ההקצאה, את מקום השחרור ואת מקום הגישה המאוחרת. אם הם נמצאים ברכיבים שונים, מציירים מי העביר למי pointer ומה כל רכיב חשב על משך החיים.

איפוס pointer אחד אחרי delete יכול להפוך שימוש דרך אותו משתנה לקריסה מוקדמת יותר, אבל אינו מאפס aliases אחרים. גם הוספת sleep אינה תיקון: היא רק משנה את ההסתברות שהאחסון ימוחזר לפני השימוש.

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

סדר הערכה ותופעות לוואי

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

int i = 0;
// int result = i++ + i++;

ב־C++20 שתי ההגדלות בביטוי הזה אינן מקבלות את סדר ה־sequencing שנדרש כדי להפוך את השימוש לבטוח. הפתרון אינו לבחור סדר שנראה טבעי משמאל לימין, אלא לפרק את הפעולות להצהרות נפרדות ולכתוב במפורש את ההתנהגות הרצויה.

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

ערך שלא הוגדר

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

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

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

גבולות הכלים

כלי sanitizer מחפש משפחות מסוימות של כשלים בהרצות שבוצעו. הוא אינו מוכיח שכל input עתידי תקין, ואינו מבין תמיד את כל חוזי המשאבים של מערכת ההפעלה. גם static analysis עשוי להחמיץ נתיב או לדווח על מקרה שאינו אפשרי לפי invariant חיצוני.

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

תחקיר שאפשר לשחזר

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

במקרה של grows אפשר להוכיח את הכשל מכללי arithmetic, גם בלי לראות פלט מוזר. במקרה של use-after-free אפשר להוכיח את הפרת החיים ולהשתמש ב־sanitizer כדי לקשר אותה למקומות בקוד. בשני המקרים אנחנו מתקנים את הסיבה ולא רק את התוצאה שנראתה בהרצה אחת.

לקריאה נוספת ראו את דוגמאות Microsoft לאבחון גישה אחרי שחרור.