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いますが、2 番目の例では (メモリ フィールドのサイズを考慮して) 範囲を手動で指定する必要があります。

例による 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)は、 type のオブジェクトのポインター演算を使用して理解する必要があり、実際には、バイトが有効な領域を指すようにstruct someStruct要求しています。p16 * 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))必要がありますが、それは型が 、およびであるためだけです。pstrlen(p)+1pchar*sizeof(char)=1

于 2013-03-29T20:29:22.447 に答える