frama-c - 跟踪法律值(value)

Question

假设有两个外部函数 init() 和 revoke()。 Init() 返回“有效”值，revoke() 使它们无效。我想验证 use() 只使用已初始化但未撤销的值。我不知道如何将此属性描述为谓词(想想随机 session 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 插件允许以自动机的形式表达允许的函数调用序列，但恐怕它无法完全捕获您想要的内容。更准确地说，它无法表达 token 生命周期重叠的场景(但它完全足以证明示例的主要功能是正确的)。

也就是说，通过一些工具，应该可以得出一个通用的规范。第一个技巧是声明一个(幽灵)数组，其单元格非零，当且仅当相应的索引是有效标记时。

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 之间保持不变。