2

假设有两个外部函数 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);
}
4

1 回答 1

3

确实不可能将此属性表示为单个 ACSL 谓词。实际上，这取决于程序的整个执行过程。Aorai插件允许以自动机的形式表达允许的函数调用序列，但恐怕它不能完全捕捉到你想要的。更准确地说，它无法表达令牌的生命周期重叠的场景（但足以证明您的示例的主要功能是正确的）。

也就是说，通过一些工具，应该可以提出一个通用规范。第一个技巧是声明一个 (ghost) 数组，如果相应的索引是有效标记，则其单元格不为零。

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 和 revoke 修改的状态，如下所示：

 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。

于 2012-08-29T16:07:14.927 回答