Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Может, я что-то не понимаю, но

PD>int n,m;
PD>read(m,n); // ввод откуда-то
PD>int a[m]; // выделяем память и создаем массив
PD>a[n] = 1;

PD>Как можно этот фрагмент статически проверить ? При корректных m и n все будет замечательно. При большом n мы свободно сейчас можем уехать в адреса ядра, за что и получим AV
PD>А статически — как ?

В принципе, идея простая. Можем ли мы сказать, глядя на этот код, что он 100% корректен? Нет. Мы этого не можем утверждать. И верификатор, естественно, тоже не может. Результат? Ошибка компиляции.

Как сделать, чтобы код скомпилировался? Убедить верификатор в том, что код безопасен.

int n,m;
read(m,n); // ввод откуда-то
if (stack_available(m))  // stack_available - специальная функция, известная верификатору
{
    int a[m]; // выделяем память и создаем массив

    if (is_valid_index(a, n))   // is_valid_index - специальная функция, известная верификатору
    {
        a[n] = 1;
    }
    else
    {
        // тут мы хотели обратиться по некорректному адресу, но рантайм-проверка нам не дала
        // что делать? наверное вернуть ошибку или выдать какое-то сообщение
    }
}
else
{
    // тут рантайм-проверка показала, что места на стеке нет, создать массив мы не можем
    // и что же нам делать? ну, что угодно, можно вернуть ошибку или терминировать процесс
}

Так что сама идея довольно простая. Там, где верификатор не знает, корректная операция или нет — он заставляет программиста вставить рантайм-проверку.

Конечно, эти явные проверки замусоривают код, но потенциальный выигрыш в том, что их может быть не так уж много. Это как типы данных. Если мы хотим принять в функцию int, то компилятор не даст нам туда сунуть string. Аналогичным образом мы можем потребовать предусловие наподобие "is_valid_index" и тогда внутри функции этой проверки уже не будет — она будет где-то выше по стеку вызовов.

Да, такой код писать сложнее. Но это возможно. Примерно так пишут софт для марсоходов и самолетов. Я думаю, что такой вариант возможен для самых низкоуровневых частей ОС, а что-то более высокоуровневое можно писать уже на управляемых языках, более тормозных, но и более простых.