VST forward_call 非标准调用约定失败

Question

我正在使用 VST 2.5 和 Coq 8.11.0

使用非标准调用约定对函数执行 forward_call 时出错。最小代码示例：

struct t {
  int t_1;
  int t_2;
};

struct t test_aux() {
  struct t ret;
  ret.t_1 = 1;
  ret.t_2 = 2;
  return ret;
}

void test_f() {
  test_aux();
}

VST 规格：

Require Import VST.floyd.proofauto. 
Require Import example.

Definition Vprog : varspecs. mk_varspecs prog. Defined. Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Open Scope Z.

Definition aux_spec : ident * funspec :=   DECLARE _test_aux
    WITH res : val
    PRE [tptr (Tstruct _t noattr)]
      PROP ()
      PARAMS (res)
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) res)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP (data_at Tsh (Tstruct _t noattr) 
                   (Vint (Int.repr 1), Vint (Int.repr 2)) res).

Definition test_spec : ident * funspec :=   DECLARE _test_f
    WITH temp : val
    PRE []
      PROP ()
      PARAMS ()
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) temp)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP ().

Definition Gprog := ltac:(with_library prog [aux_spec; test_spec]).

Theorem test : semax_body Vprog Gprog f_test_f test_spec. Proof.   start_function.   Fail forward_call (nullval). Admitted.

错误：

Unable to unify  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid cc_default" with  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid
    {|
    cc_vararg := false;
    cc_unproto := false;
    cc_structret := true |}".

我不知道这是错误还是有意为之，所以我在这里有几个问题：

1) 这是一个错误吗？

2) 如果不是，有什么解决方法可以证明这种情况？

更新：

我们运行在使用以下解决结构复制限制的变通方法后解决了这个问题：我们在 Coq 中定义了一个 struct_normalize : statement -> statement 函数，用逐字段赋值替换结构赋值。因此，我们假设我们正在调用的函数中没有结构复制。也就是说，我们可以从上面的例子中验证test_aux。所以问题是：

forward_call 是否仅因为 test_aux AST 中的 cc_structret := true 而失败？
鉴于我们规范化函数并从函数主体中删除结构复制，相应地更改 structret 值并继续证明是否安全？

Answer 1

遗憾的是，VST 不支持结构复制、结构传递或结构返回。另见。所以不修改这个程序是无法验证的。

VST forward_call 非标准调用约定失败

VST forward_call fail on non-standard calling convention

c

coq

formal-verification

verifiable-c