I am working on writing an ACSL specification for a function that appends a given string to the end of a dynamic character array.
Here is what I have so far:
#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;
}
Because verification of dynamic memory allocation is not yet supported, I have added a placeholder function char_vector_reallocate() and ACSL specification without showing the implementation.
Using Frama-C Sodium-20150201 and the WP plugin, I have been unable to verify 6 properties:
I was not expecting to experience any difficulty with verifying the first 5 properties.
How can I fix the ACSL so that char_vector_append() can be verified?
(As a sidenote, is there an example ACSL specification for a dynamic array that I could refer to as a guide?)
You're lacking assumes clauses that will allow WP to discriminate between your ok and err cases. A good witness of that is the fact that you cannot prove the disjoint clause of the contract. Basically, the function will fail if
In order to model the third point, I'd suggest to use a ghost variable indicating whether there is enough free memory to extend the vector. In your case, as there is only one allocation, a simple boolean flag will do the trick, e.g. //@ ghost int mem_full.
Of course, you need to adapt the spec of char_vector_reallocate accordingly: it should assigns mem_full and its behaviors should have assumes clauses based on the initial value of mem_full.
Finally, there is an issue with your first argument of memcmp in the ensures clause of char_vector_reallocate and in old_content_unchanged: the argument itself should be evaluated in the Pre-state. Otherwise, you're saying that whatever was pointed at by vec->buf (in the Post-state) in the Pre-state compares equal to was is pointed at by vec->buf (again in the Post-state) in the Post-state. Namely, the evaluation of the arguments to memcmp occurs in the current state, regardless of the labels given in parameter.
Below is a version for which everything is proved by 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;
}