2

我对如何在结构上正确使用 \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中的堆栈示例（第 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)
;
@*/
4

1 回答 1

3

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

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

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

\有效(((char*)p)+(0..15))

事实上，ACSL 参考手册明确提到了以下等效第 56 页。（为了清楚起见，我删除了标签。）

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

For strings, the cast (char*)p becomes superfluous, as strings are already pointers to char. Thus, writing valid(p+(0..strlen(p)) requires that p points to a memory are where strlen(p)+1 bytes are valid -- but only because p has type char*, and sizeof(char)=1.

于 2013-03-29T20:29:22.447 回答