Удовлетворяет ли Доказательство обязательств по memcpy?[Frama-С]

Question

Мы использовали Frama-C для «экспериментального» статического анализа в коммерческом проекте (интегрирован в наш CI, с несколькими выборочными проверками блокировки в небольшом разделе всей кодовой базы).

Одна из возникающих проблем связана с выполнением обязательств по проверке, которые плагин wp генерирует каждый раз, когда сталкивается с вызовом memcpy.В частности, три обязательства ниже:

Из примечаний 'цели' похоже, что Frama-C пытается доказать, что память назначения и источника действительны,

Я пытался добавить requires \valid() предварительные условия, но это, похоже, не помогает.В этих случаях вызов memcpy в тестируемой функции копирует данные из входного параметра в функцию и помещает эти данные в локальную переменную (в пределах области действия функции).

Чтобы еще больше усложнить ситуациюлокальная переменная, в которую копируются данные, является атрибутом в упакованной структуре.

Конкретно, я надеюсь, что кто-то сможет поделиться некоторыми реальными примерами использования memcpy, когда цели, введенные wp, могут быть выполнены (например, какие предварительные условия я должен добавить, чтобы сделать его доказуемым)?)

Если это имеет значение, я использую Frama-C Magnesium-20151002 (в соответствии с apt-get для Ubuntu 16, это «актуально») и вызывает следующие параметры:

frama-c -wp -wp-split -wp-dynamic -lib-entry -wp-proof alt-ergo -wp-report

Также связано, но отсутствует четкий рабочий пример: Frama-c: Проблемы с пониманием моделей памяти WP

Answer 1

Как вы упомянули в своем комментарии, правильное решение состоит в том, чтобы использовать -wp-model "Typed+Cast", чтобы позволить WP принимать преобразования в / из void* (точнее, он будет считать, что p и (void*)p одинаковывещь для любого указателя, которого будет достаточно для доказательства requires из memcpy).Теперь, как упоминалось в ответе на вопрос, с которым вы связаны, главная проблема этой модели памяти (и причина, по которой она не используется по умолчанию) заключается в том, что она по своей сути небезопасна : он опирается на гипотезы, которые по определению не могут быть оценены самой WP.Вот небольшой пример, который выдвигает на первый план эту проблему:

int x;
char* c;

/*@ assigns c;
    ensures c == ((char *)&x);
*/
void g(void) {
  c = &x;
}

/*@ assigns \nothing;
    ensures \separated(&x,c);
*/
void f() {
}

void main () {
g();
f();
//@ assert \false;
}

В основном, модель памяти по умолчанию Typed обеспечивает разделение между местоположением, на которое указывают c и x (то есть постусловиеf), потому что int и char различны, и вы не можете ни доказать постусловие g, ни использовать его в качестве гипотезы для получения \false в main, потому что равенство можетне будет выражено в модели вообще.

Теперь, если вы используете Typed+Cast, постусловие g теперь правильно понято, и доказать это совершенно тривиально.WP не позволит вам доказать в то же время, что &x и c разделены, потому что они вместе участвуют в задании.Однако в f такого назначения не существует, и постусловие также легко доказывается, что приводит к доказательству \false в main, поскольку у нас есть два противоречивых утверждения о &x и c.В более общем смысле, WP использует локальный анализ псевдонимов для отслеживания потенциальных псевдонимов между указателями разных типов (глобальный анализ не позволит использовать модульный анализатор).Таким образом, передача опции -wp-model +Cast может рассматриваться как способ сказать WP: «Поверьте мне, программа не будет создавать псевдонимы с ошибками».Однако можно передавать информацию о псевдониме вручную (или с помощью, например, еще не написанного плагина глобального обнаружения псевдонимов).Например, с опцией -wp-alias-vars x,c постусловие f становится Unknown (то есть разделение между &x и c больше не является предположением, даже для f).