Test suite Anda lolos. Pemeriksa tipe Anda hijau. Anda rilis. Dua jam kemudian, produksi melemparkan IndexError pada kasus tepi yang tidak terpikirkan untuk diuji.

Pengujian menemukan bug. Tipe mencegah sebagian. Keduanya tidak membuktikan program Anda bebas dari kesalahan runtime. Untuk itu, Anda membutuhkan sesuatu yang lebih kuat: cara untuk bernalar tentang setiap eksekusi yang mungkin, sekaligus, tanpa menjalankan kode.

Interpretasi abstrak adalah teknik yang memungkinkan hal ini. Ia menyuplai analisis statis di dalam Astrée, Infer milik Facebook, dan jaminan kebenaran dalam pemeriksa pinjaman Rust. Ia juga menjelaskan mengapa sebagian besar pemasaran “positif palsu nol” untuk analisis statis adalah kebohongan.

Kesalahan runtime adalah masalah ketercapaian

Kesalahan runtime hanyalah operasi yang mencapai keadaan buruk. Pembagian dengan nol, dereferensi null, luapan penyangga, indeks di luar batas. Masing-masing terjadi karena eksekusi mencapai titik program di mana operasi tersebut tidak aman.

Untuk membuktikan tidak ada kesalahan runtime yang ada, Anda perlu membuktikan setiap operasi tidak aman tidak dapat dicapai dalam setiap eksekusi yang mungkin. Setiap masukan. Setiap cabang. Setiap iterasi perulangan.

Pengujian menyeluruh mustahil untuk apa pun kecuali program mainan. Eksekusi simbolik tidak mudah diskalakan karena ledakan jalur menghancurkan Anda. Interpretasi abstrak mengambil jalur berbeda: ia menyerah mengetahui nilai eksak, dan sebagai gantinya melacak properti perkiraan yang dijamin mencakup setiap eksekusi nyata.

Apa yang sebenarnya dilakukan interpretasi abstrak

Interpretasi abstrak diperkenalkan oleh Patrick dan Radhia Cousot pada tahun 1976. Ide intinya indah dalam kesederhanaannya: jalankan program Anda, tetapi alih-alih menghitung dengan angka nyata, string, dan pointer, Anda menghitung dengan representasi abstrak yang melebih-aproksimasi nilai-nilai nyata.

Pikirkan ini sebagai penggantian eksekusi konkret Anda dengan eksekusi “bayangan” yang melacak properti yang Anda pedulikan. Alih-alih mengetahui x = 42, Anda mungkin mengetahui x > 0. Alih-alih mengetahui arr memiliki panjang 10, Anda mungkin mengetahui arr tidak kosong.

Kendala kuncinya adalah kebenaran. Setiap keadaan konkret harus direpresentasikan oleh beberapa keadaan abstrak. Jika eksekusi abstrak mengatakan suatu operasi aman, maka setiap eksekusi konkret yang direpresentasikannya aman. Harganya adalah presisi: jika keadaan abstrak terlalu samar, Anda mendapat positif palsu (peringatan semu tentang operasi aman).

Contoh konkret: analisis interval

Berikut adalah interpreter abstrak minimal yang membuktikan pembagian dengan nol mustahil. Ia melacak rentang yang mungkin dari setiap variabel menggunakan interval.

# A tiny abstract interpreter for interval analysis
from dataclasses import dataclass
from typing import Dict

@dataclass(frozen=True)
class Interval:
    lo: float
    hi: float

    def __contains__(self, val: float) -> bool:
        return self.lo <= val <= self.hi

TOP = Interval(float("-inf"), float("inf"))

def eval_expr(env: Dict[str, Interval], expr) -> Interval:
    if isinstance(expr, int):
        return Interval(float(expr), float(expr))
    if isinstance(expr, str):
        return env.get(expr, TOP)
    if expr[0] == "+":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo + r.lo, l.hi + r.hi)
    if expr[0] == "-":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo - r.hi, l.hi - r.lo)
    if expr[0] == "*":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        products = [l.lo * r.lo, l.lo * r.hi, l.hi * r.lo, l.hi * r.hi]
        return Interval(min(products), max(products))
    if expr[0] == "/":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        if r.lo <= 0 <= r.hi:
            raise ValueError("Possible division by zero")
        return TOP
    raise ValueError(f"Unknown expr: {expr}")

def merge_envs(env1: Dict[str, Interval], env2: Dict[str, Interval]) -> Dict[str, Interval]:
    keys = set(env1) | set(env2)
    result = {}
    for k in keys:
        a = env1.get(k, TOP)
        b = env2.get(k, TOP)
        result[k] = Interval(min(a.lo, b.lo), max(a.hi, b.hi))
    return result

def analyze(program, env: Dict[str, Interval]) -> Dict[str, Interval]:
    env = dict(env)
    for stmt in program:
        if stmt[0] == "assign":
            _, var, expr = stmt
            env[var] = eval_expr(env, expr)
        elif stmt[0] == "if":
            _, cond, true_branch, false_branch = stmt
            t_env = analyze(true_branch, dict(env))
            f_env = analyze(false_branch, dict(env))
            env = merge_envs(t_env, f_env)
        elif stmt[0] == "while":
            _, cond, body = stmt
            old = dict(env)
            for _ in range(10):
                new = analyze(body, dict(old))
                changed = False
                for k in set(old) | set(new):
                    prev = old.get(k, TOP)
                    curr = new.get(k, TOP)
                    widened = Interval(min(prev.lo, curr.lo), max(prev.hi, curr.hi))
                    if widened.lo != prev.lo or widened.hi != prev.hi:
                        changed = True
                    old[k] = widened
                if not changed:
                    break
            env = old
    return env

# Example program: y = 10 / (x + 1) where x >= 0
program = [
    ("assign", "t", ("+", "x", 1)),
    ("assign", "y", ("/", 10, "t")),
]

# This should pass: x >= 0 means t >= 1, so no division by zero
safe_env = analyze(program, {"x": Interval(0, 100)})
print("Safe env:", safe_env)

# This should fail: x could be -1
try:
    bad_env = analyze(program, {"x": Interval(-5, 5)})
except ValueError as e:
    print("Caught:", e)

Jalankan. Kasus pertama membuktikan keamanan karena interval untuk t adalah [1.0, 101.0], yang mengecualikan nol. Kasus kedua dengan benar menandai risiko karena t bisa bernilai nol ketika x adalah -1.

Penangan if menggabungkan kedua cabang dengan mengambil gabungan interval. Penangan while mengulang hingga interval berhenti tumbuh (titik tetap). Ini adalah inti dari interpretasi abstrak: Anda menukar nilai eksak dengan aproksimasi berlebih yang dijamin, dan Anda membuktikan keamanan dengan menunjukkan keadaan buruk berada di luar aproksimasi.

Di mana ini gagal: dinding presisi

Contoh di atas berukuran mainan. Program nyata memiliki aliasing, rekursi, alokasi heap, dan perulangan dengan batas bergantung data. Masing-masing menghancurkan presisi dengan cara yang dapat diprediksi.

Pertimbangkan sebuah perulangan yang menaikkan i dari 0 hingga 100. Analisis interval yang naif mungkin melebarkan i menjadi [0, +inf) dan tidak pernah memulihkan batas atas. Anda membutuhkan domain relasional (seperti polihedra atau oktagon) untuk melacak bahwa i <= 100. Domain-domain tersebut bersifat kubik atau eksponensial dalam jumlah variabel. Untuk program dengan 1.000 variabel, Anda tidak menjalankan analisis polihedra.

Inilah mengapa alat komersial membuat pilihan berbeda. Astrée menggunakan kisi domain abstrak yang dipilih dengan cermat, disetel tangan untuk C tertanam. Infer menggunakan logika pemisahan dan bi-abduksi untuk diskalakan hingga jutaan baris kode seluler, tetapi ia menyerah pada kebenaran untuk beberapa fitur bahasa. Pemeriksa pinjaman Rust pada dasarnya adalah interpreter abstrak dengan satu domain yang sangat presisi: kepemilikan.

Pertukaran yang tidak dapat Anda hindari

Kebenaran, presisi, dan skalabilitas. Pilih dua.

Sebuah analisis yang benar dengan presisi tinggi tidak akan diskalakan melewati small modules. Sebuah analisis yang dapat diskalakan dan benar akan menenggelamkan Anda dalam positif palsu. Sebuah analisis yang dapat diskalakan dan presisi akan melewatkan bug nyata.

Pilihan domain abstrak Anda adalah kenop penyetelan. Interval cepat dan tidak presisi. Polihedra presisi dan lambat. Abstraksi predikat berada di tengah dan menyuplai sebagian besar pemeriksa model perangkat lunak.

Cara menggunakannya secara nyata

Anda mungkin tidak akan menulis interpreter abstrak Anda sendiri. Anda akan menggunakan yang sudah ada.

Untuk C dan sistem tertanam, Astrée dan Frama-C adalah pilihan yang matang. Plugin EVA Frama-C melakukan analisis interval dan memori pada kode C dunia nyata.

Untuk Rust, sistem tipe sudah mengkodekan domain abstrak kepemilikan. Miri adalah interpreter, bukan interpreter abstrak, tetapi ia menangkap perilaku tak terdefinisi yang dilewatkan oleh sistem tipe.

Untuk kode tujuan umum, Infer dari Meta adalah yang paling mendekati interpreter abstrak yang dapat diskalakan untuk Java, C++, dan Objective-C. Ia menemukan bug dereferensi null dan kebocoran memori nyata dalam production codebases.

Jika Anda ingin bereksperimen, mulailah dengan analisis tanda atau analisis interval sederhana pada bahasa yang Anda parsing sendiri. Dragon Book mencakup analisis aliran data. Principles of Program Analysis karya Nielson dan Nielson adalah referensi standar untuk interpretasi abstrak secara khusus.

Membuktikan yang negatif

Interpretasi abstrak tidak akan membuat kode Anda bebas bug. Apa yang ia berikan adalah kerangka kerja matematis untuk membuktikan kelas-kelas kesalahan runtime tertentu mustahil terjadi. Bukti itu hanya sebaik domain abstrak Anda, strategi melebarkan Anda, dan kesediaan Anda untuk mentolerir positif palsu.

Sebagian besar tim mendapat nilai lebih dari pengujian yang baik dan sistem tipe yang benar. Tetapi ketika Anda menulis kode di mana kesalahan runtime berarti satelit jatuh dari langit, interpretasi abstrak adalah cara Anda tidur nyenyak di malam hari.