Спецификация 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 Натрий-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 s должны иметь assumes положения на основе первоначальной стоимости mem_full.

Наконец, есть проблема с первым аргументом memcmp в предложении о char_vector_reallocateensures и в old_content_unchanged: сам аргумент должен быть оценен в Pre -состоянии.В противном случае вы говорите, что все, на что указывал vec->buf (в Post -state) в Pre -стате, сравнивается с равным нулю, указывается vec->buf (опять же в Post -state) в Post -state. А именно, оценка аргументов 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; 
}