記錄合法值

Question

假設兩個外部函數init（）和revoke（）。 Init（）返回「有效」值，revoke（）使其無效。我喜歡驗證use（）只使用初始化但未被撤銷的值。我不知道如何將此屬性描述爲謂詞（想想隨機會話ID）或其他。

#include <lib.h> 

// "ensures valid_val(\result)" 
extern int init(); 
extern revoke(int); 

/* 
@ assigns \nothing; 
@ require valid_val(val); 
*/ 
void use(int val) { 
    ... 
} 

int main() { 
    int v = init(); 
    use(v); 
    revoke(v); 
} 

Answer 1

確實無法將此屬性表示爲單個ACSL謂詞。實際上，這取決於整個程序的執行。 Aorai插件允許以自動機的形式表達允許的函數調用序列，但恐怕它不能完全捕獲你想要的內容。更確切地說，它不能表示場景中令牌的壽命重疊的場景（但它足以證明你的例子的主要功能是正確的）。

這就是說，用一點儀器，應該有可能提出一個通用規範。如果相應的索引是有效的標記，則第一個技巧是聲明單元格非零的（虛影）數組。

typedef int token; 

/*@ ghost extern int valid_token[]; */ 

/*@ predicate is_valid(token t) = valid_token[t] != 0; */ 

/*@ 
    assigns valid_token[\at(\result,Post)]; 
    ensures is_valid(\result); 
*/ 
extern token init(); 

/*@ 
    requires is_valid(t); 
    assigns valid_token[t]; 
    ensures !is_valid(t); 
*/ 
extern revoke(token t); 

/*@ 
@ requires is_valid(val); 
@ assigns \nothing; 
*/ 
void use(token val) { 

} 

/*@ requires \forall token t; !is_valid(t); */ 
int main() { 
    token v = init(); 
    use(v); 
    revoke(v); 
} 

如果我們使用數組沒有定義大小的事實似乎有點腥，幾乎是純粹的ACSL的解決辦法是使用一個未定義的謂詞，其真值取決於由init和撤銷修改的狀態，如在：

typedef int token; 

/*@ ghost int glob_state; */ 

/*@ axiomatic validity { 
    predicate valid_token{L}(token t) reads glob_state; 
} 
*/ 

/*@ predicate unchanged_token{L1,L2}(token t) = 
    \forall token t1; t!=t1 ==> 
    valid_token{L1}(t1) <==> valid_token{L2}(t1); 
*/ 

/*@ 
    assigns glob_state; 
    ensures valid_token(\result); 
    ensures unchanged_token{Pre,Here}(\result); 
*/ 
extern token init(); 

/*@ 
    requires valid_token(t); 
    assigns glob_state; 
    ensures !valid_token(t); 
    ensures unchanged_token{Pre,Here}(t); 
*/ 
extern revoke(token t); 

/*@ 
@ requires valid_token(val); 
@ assigns \nothing; 
*/ 
void use(token val) { 

} 

/*@ requires \forall token t; !valid_token(t); */ 
int main() { 
    token v = init(); 
    use(v); 
    revoke(v); 
} 

功能，分配glob_state可能會修改謂詞。實際上，它只改變參數的一個值，因此輔助謂詞表示所有令牌的有效性，但在L1和L2之間保持不變。