Спецификация ACSL функции, которая добавляет строку в динамический массив символов

Question

Я работаю над написанием спецификации ACSL для функции, которая добавляет данную строку в конец динамического массива символов.

Вот что у меня так далеко:

#include <stddef.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

#ifndef SIZE_MAX
#define SIZE_MAX ((size_t)-1)
#endif

#undef MAX
#define MAX(a, b) ((a) > (b) ? (a) : (b))

struct st_char_vector {
  char *buf;
  size_t capacity;
  size_t length;
};

/*@ predicate valid_char_vector(struct st_char_vector *vec) =
  @   \valid_read(vec) &&
  @   vec->capacity > 0 &&
  @   \valid(vec->buf + (0..vec->capacity - 1)) &&
  @   vec->length <= vec->capacity;
  @*/


/*@ requires valid_char_vector(vec);
  @ requires new_capacity >= vec->capacity;
  @ ensures valid_char_vector(vec);
  @ ensures \old(vec->length) == vec->length;
  @ ensures memcmp{Pre,Post}(vec->buf, vec->buf, vec->length) == 0;
  @ behavior err:
  @   ensures !\result;
  @   ensures \old(vec->buf) == vec->buf;
  @   ensures \old(vec->capacity) == vec->capacity;
  @ behavior ok:
  @   ensures \result;
  @   ensures vec->capacity >= new_capacity;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
static int char_vector_reallocate(struct st_char_vector *vec, size_t new_capacity);

/*@ requires valid_char_vector(vec);
  @ requires \valid_read(str + (0..str_length - 1));
  @ requires string_separated_from_extra_capacity:
  @   \separated(str + (0..str_length - 1), vec->buf + (vec->length..vec->capacity - 1));
  @ ensures valid_char_vector(vec);
  @ ensures old_content_unchanged: memcmp{Pre,Post}(vec->buf, vec->buf, \old(vec->length)) == 0;
  @ ensures \forall integer i; 0 <= i && i < \old(vec->length) ==> \old(vec->buf[i]) == vec->buf[i];
  @ behavior err:
  @   ensures !\result;
  @   ensures buf_unchanged: \old(vec->buf) == vec->buf;
  @   ensures capacity_unchanged: \old(vec->capacity) == vec->capacity;
  @   ensures length_unchanged: \old(vec->length) == vec->length;
  @ behavior ok:
  @   ensures \result;
  @   ensures str_length_added_to_length: vec->length == \old(vec->length) + str_length;
  @   ensures string_appended: memcmp{Post,Post}(vec->buf + \at(vec->length, Pre), str, str_length) == 0;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int char_vector_append(struct st_char_vector *vec, const char *str, size_t str_length) {
  if (SIZE_MAX - str_length < vec->capacity) {
    return 0;
  }

  if (vec->capacity < (vec->length + str_length)) {
    if (!char_vector_reallocate(vec, vec->capacity + str_length)) {
      //@ assert \at(vec->length, Pre) == \at(vec->length, Here);
      return 0;
    }
  }

  memcpy(vec->buf + vec->length, str, str_length);
  vec->length += str_length;

  return 1;
}

Поскольку проверка динамического выделения памяти еще не поддерживается, я добавил функцию-заполнитель char_vector_reallocate() и спецификация ACSL без показа реализации.

Используя Frama-C Sodium-20150201 и плагин WP, я не смог проверить 6 свойств:

• typed_char_vector_append_disjoint_ok_err
• typed_char_vector_append_err_post
• typed_char_vector_append_err_post_length_unchanged
• typed_char_vector_append_ok_post
• typed_char_vector_append_ok_post_str_length_added_to_length
• typed_char_vector_append_ok_post_string_appended

Я не ожидал испытать какие-либо трудности с проверкой первых 5 свойств.

Как я могу исправить ACSL так, чтобы char_vector_append() можно проверить?

(Как примечание, есть ли пример спецификации ACSL для динамического массива, который я мог бы назвать руководством?)

Answer 1

Вам не хватает assumes пункты, которые позволят WP различать ваши ok а также err случаев. Хорошим свидетельством этого является тот факт, что вы не можете доказать disjoint пункт договора. В основном, функция потерпит неудачу, если

• сумма размеров буфера и строки слишком велика, или
• буфер слишком мал, чтобы содержать строку, и
• недостаточно памяти

Чтобы смоделировать третью точку, я бы предложил использовать переменную-призрак, указывающую, достаточно ли свободной памяти для расширения вектора. В вашем случае, поскольку существует только одно распределение, простой булев флаг помешает, например: //@ ghost int mem_full,

Конечно, вам нужно адаптировать спецификации char_vector_reallocate соответственно: должно assigns mem_full И его behaviorс должен иметь assumes пункты на основе начального значения mem_full,

Наконец, есть проблема с вашим первым аргументом memcmp в ensures пункт о char_vector_reallocate И в old_content_unchanged: сам аргумент должен быть оценен в Pre-государство. В противном случае вы говорите, что все, на что указывал vec->buf (в Postсостояние) в Pre-состояния сравниваются равные были указаны vec->buf (снова в Postсостояние) в Post-государство. А именно, оценка аргументов memcmp происходит в текущем состоянии, независимо от меток, указанных в параметре.

Ниже приведена версия, для которой все доказано Alt-Ergo

#include "stdlib.h"
#include "string.h"

#ifndef SIZE_MAX
#define SIZE_MAX ((size_t)-1)
#endif

#undef MAX
#define MAX(a, b) ((a) > (b) ? (a) : (b))

struct st_char_vector {
  char *buf;
  size_t capacity;
  size_t length;
};

/*@ predicate valid_char_vector(struct st_char_vector *vec) =
  @   \valid_read(vec) &&
  @   vec->capacity > 0 &&
  @   \valid(vec->buf + (0..vec->capacity - 1)) &&
  @   vec->length <= vec->capacity;
  @*/

//@ ghost extern int mem_full;

/*@ requires valid_char_vector(vec);
  @ requires new_capacity >= vec->capacity;
  @ assigns mem_full;
  @ ensures valid_char_vector(vec);
  @ ensures \old(vec->length) == vec->length;
  @ ensures valid_char_vector(vec);
  @ ensures memcmp{Pre,Post}(\at(vec->buf,Pre), vec->buf, vec->length) == 0;
  @ behavior err:
      assumes mem_full;
  @   ensures !\result;
  @   ensures \old(vec->buf) == vec->buf;
  @   ensures \old(vec->capacity) == vec->capacity;
  @ behavior ok:
      assumes !mem_full;
  @   ensures \result;
  @   ensures vec->capacity >= new_capacity;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
static int char_vector_reallocate(struct st_char_vector *vec, size_t new_capacity);

/*@ requires valid_char_vector(vec);
  @ requires \valid_read(str + (0..str_length - 1));
  @ requires string_separated_from_extra_capacity:
  @   \separated(str + (0..str_length - 1), vec->buf + (vec->length..vec->capacity - 1));
  @ ensures valid_char_vector(vec);
  @ ensures old_content_unchanged: memcmp{Pre,Post}(\at(vec->buf,Pre), vec->buf, \old(vec->length)) == 0;
  @ ensures \forall integer i; 0 <= i && i < \old(vec->length) ==> \old(vec->buf[i]) == vec->buf[i];
  @ behavior err:
      assumes vec->capacity+str_length>SIZE_MAX || 
      (vec->length+str_length>vec->capacity && mem_full);
  @   ensures !\result;
  @   ensures buf_unchanged: \old(vec->buf) == vec->buf;
  @   ensures capacity_unchanged: \old(vec->capacity) == vec->capacity;
  @   ensures length_unchanged: \old(vec->length) == vec->length;
  @ behavior ok:
      assumes vec->capacity+str_length<=SIZE_MAX && 
      (vec->length+str_length<=vec->capacity || !mem_full);
  @   ensures \result;
  @   ensures str_length_added_to_length: vec->length == \old(vec->length) + str_length;
  @   ensures string_appended: memcmp{Post,Post}(vec->buf + \at(vec->length, Pre), str, str_length) == 0;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int char_vector_append(struct st_char_vector *vec, const char *str, size_t str_length) {
  if (SIZE_MAX - str_length < vec->capacity) {
    return 0;
  }

  if (vec->capacity < (vec->length + str_length)) {
    if (!char_vector_reallocate(vec, vec->capacity + str_length)) {
      return 0;
    }
  }
   memcpy(vec->buf + vec->length, str, str_length);
  vec->length += str_length;

  return 1;
}