c - Frama-C/WP/ACSL 在结构上正确使用\valid

Question

我对如何在结构上正确使用\valid 注释有一些疑问。

struct someStruct{
    int size1;
    int size2;
    char *str1;
    char *str2;
}

验证结构内存安全的正确谓词是:

/*@
    predicate validStruct(struct someStruct *p) =
       \valid(p) && 
       \valid(p->str1+(0..((p->size1)-1))) && 
       \valid(p->str2+(0..((p->size2)-1)));
@*/

或

/*@
    predicate validStruct(struct someStruct *p) =
       // 16 bytes: 2 int * 4 bytes + 2 pointers* 4 bytes.
       // Although may depend on implementation and system arch
       \valid(p+(0..15) &&   
       \valid(p->str1+(0..((p->size1)-1))) && 
       \valid(p->str2+(0..((p->size2)-1)));
@*/

第一个示例假设 \valid(p) (其中 p 是指向结构的指针)确保它指向的结构的内存安全，而第二个我必须手动指定范围(考虑到内存字段的大小)

查看 ACSL by Example 中的 Stack 示例(第 125 页)。他们采用第一个例子。但是在很多地方 \valid(some_string+(0..strlen(some_string)))用于确保这些特定内存位置的内存安全。

编辑:

回应给出的答案。一个正确的内存安全谓词(取自 stdio.h)

struct _IO_file {
    int _IO_fileno;     /* Underlying file descriptor */
    _Bool _IO_eof;      /* End of file flag */
    _Bool _IO_error;    /* Error flag */
};
typedef struct _IO_file FILE;


struct _IO_file_pvt {
    struct _IO_file pub;    /* Data exported to inlines */
    struct _IO_file_pvt *prev, *next;
    char *buf;      /* Buffer */
    char *data;     /* Location of input data in buffer */
    unsigned int ibytes;    /* Input data bytes in buffer */
    unsigned int obytes;    /* Output data bytes in buffer */
    unsigned int bufsiz;    /* Total size of buffer */
    enum _IO_bufmode bufmode; /* Type of buffering */
};

将是，例如:

/*@

predicate valid_FILE(FILE *f) = 
    \valid(f) && f->_IO_fileno >= 0;

predicate valid_IO_file_pvt(struct _IO_file_pvt *f) = 
    \valid(f)
    // buffer offset
    && f->buf == (char *)f + ((sizeof(*f) + 4*sizeof(void *) - 1)
                                        & ~(4*sizeof(void *) - 1))
    // 16K
    && f->bufsiz == 16384
    && 0 <= f->ibytes <= f->bufsiz
    && 0 <= f->obytes <= f->bufsiz
    && valid_FILE(&(f->pub))
    && (f->next != \null ==> \valid(f->next))
    && (f->prev != \null ==> \valid(f->prev))
    // 16384 + 32 (ungetc_slop)
    && \valid(f->buf+(0..(f->bufsiz+32-1)))
    // data points to address in valid buffer region
    && f->buf <= f->data < (f->buf + f->bufsiz + 32)
;
@*/

Answer 1

解决方案 1 显然是好的，因为它抽象了编译器和 Frama-C 中的 Cil 选择的内存布局。

解决方案 2 实际上是不正确的。您的范围 p+(0..15)必须在 struct someStruct 类型的对象上使用指针算术来理解，而您实际上是在请求 p指向一个区域，其中 16 * sizeof(struct someStruct)字节有效。

对于标准内存布局，解决方案 2 的正确重构应该是

\valid(((char*)p)+(0..15))

事实上，ACSL 引用手册明确提到了以下等价的第 56 页。(为了清楚起见，我已经删除了标签。)

\valid(p) <==> \valid(((char*)p)+(0..sizeof(*p))

对于弦乐，类型转换 (char*)p变得多余，因为字符串已经是指向 char 的指针。因此，写作 valid(p+(0..strlen(p))要求 p指向内存的地方 strlen(p)+1字节是有效的——但只是因为 p有类型 char* , 和 sizeof(char)=1 .