如何在VST中处理含别名参数的函数并选择对应规范？

待验证的C代码 #

void incr(int *a, int *b) {
    (*a)++;
    (*b)++;
}

void f(int *a, int *b) {
  incr(a, b);
  incr(a, a);
}

incr函数的两种规范 #

• {a ↦ n * b ↦ m} incr(a, b) {a ↦ n + 1 * b ↦ m + 1}
• {a ↦ n} incr(a, a) {a ↦ n + 2}

问题 #

在使用VST证明函数f的正确性时，应如何指定使用incr的对应规范？

相关Coq代码片段 #

From VST.floyd Require Import proofauto library.
Require Import incr.

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Definition incr_spec :=
  DECLARE _incr
  WITH a : val, n : Z, b : val, m : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n < Int.max_signed;
          Int.min_signed <= m < Int.max_signed)
    PARAMS (a; b)
    SEP (data_at Ews tint (Vint (Int.repr n)) a;
         data_at Ews tint (Vint (Int.repr m)) b)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 1))) a;
         data_at Ews tint (Vint (Int.repr (m + 1))) b).

Definition incr_spec2 :=
  DECLARE _incr
  WITH a : val, n : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n <= Int.max_signed - 2)
    PARAMS (a; a)
    SEP (data_at Ews tint (Vint (Int.repr n)) a)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 2))) a).

Definition f_spec :=
  DECLARE _f
  WITH a : val, n : Z, b : val, m : Z
  PRE [tptr tint, tptr tint]
    PROP (Int.min_signed <= n <= Int.max_signed - 3;
          Int.min_signed <= m < Int.max_signed)
    PARAMS (a; b)
    SEP (data_at Ews tint (Vint (Int.repr n)) a;
         data_at Ews tint (Vint (Int.repr m)) b)
  POST [tvoid]
    PROP ()
    RETURN ()
    SEP (data_at Ews tint (Vint (Int.repr (n + 3))) a;
         data_at Ews tint (Vint (Int.repr (m + 1))) b).

Definition Gprog := [ incr_spec; incr_spec2 ].

(* Lemma body_f : *)
(*   semax_body Vprog Gprog f_f f_spec. *)
(* Proof. *)
(*   start_function. *)
(*   forward_call. *)

具体操作方法 #

1. 为incr的两种场景定义对应规范：

   • incr_spec对应参数为两个不同指针的场景，前置条件描述了两个独立内存位置的初始值，后置条件对应各自加1的结果。
   • incr_spec2对应两个参数为同一指针的场景，前置条件限制初始值足够大（确保加2不溢出），后置条件描述该内存位置值加2的结果。

2. 将规范加入全局规范环境：
   把两个规范放入Gprog列表中，让VST在证明过程中可以从这个环境里查找匹配的函数规范。

3. 在证明流程中调用对应规范：

   • 第一次调用incr(a, b)时，直接用forward_call策略，VST会自动匹配incr_spec——当前分离逻辑上下文满足incr_spec的前置条件（两个独立的data_at断言）。
   • 第二次调用incr(a, a)时，需要用forward_call_with_spec incr_spec2策略明确指定使用该规范。此时验证前置条件：f的前置条件中n <= Int.max_signed -3，经过第一次调用后a的值变为n+1，满足n+1 <= Int.max_signed -2，符合incr_spec2的要求。

内容的提问来源于stack exchange，提问作者tymmym