将字符串附加到动态字符数组的函数的 ACSL 规范
ACSL specification of a function that appends a string to a dynamic character array
我正在为将给定字符串附加到动态字符数组末尾的函数编写 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 规范示例,我可以将其作为指南参考?)
您缺少允许 WP 区分您的 ok
和 err
案例的 assumes
条款。一个很好的证据就是你无法证明合同的 disjoint
条款。基本上,如果
函数将失败
- 缓冲区和字符串的总和太大,或
- 缓冲区太小,无法容纳字符串,和
- 剩余内存不足
为了对第三点进行建模,我建议使用一个幽灵变量来指示是否有足够的空闲内存来扩展向量。在你的情况下,因为只有一个分配,一个简单的布尔标志就可以了,例如//@ ghost int mem_full
.
当然,您需要相应地调整 char_vector_reallocate
的规范:它应该 assigns mem_full
并且它的 behavior
应该有 assumes
基于初始值的子句mem_full
.
最后,char_vector_reallocate
的 ensures
子句和 old_content_unchanged
中 memcmp
的第一个参数存在问题:参数本身应在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;
}
我正在为将给定字符串附加到动态字符数组末尾的函数编写 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 规范示例,我可以将其作为指南参考?)
您缺少允许 WP 区分您的 ok
和 err
案例的 assumes
条款。一个很好的证据就是你无法证明合同的 disjoint
条款。基本上,如果
- 缓冲区和字符串的总和太大,或
- 缓冲区太小,无法容纳字符串,和
- 剩余内存不足
为了对第三点进行建模,我建议使用一个幽灵变量来指示是否有足够的空闲内存来扩展向量。在你的情况下,因为只有一个分配,一个简单的布尔标志就可以了,例如//@ ghost int mem_full
.
当然,您需要相应地调整 char_vector_reallocate
的规范:它应该 assigns mem_full
并且它的 behavior
应该有 assumes
基于初始值的子句mem_full
.
最后,char_vector_reallocate
的 ensures
子句和 old_content_unchanged
中 memcmp
的第一个参数存在问题:参数本身应在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;
}