具有可寻址局部变量的规范

Question

我想了解 VST 如何处理（可寻址的）局部变量，所以我写了这个函数：

int main() {
    int x = 5, y = 7;
    int *a = &x;
    int *b = &y;

    *a = 8;
    *b = 9;

    return x;
}

然后我尝试用下面的规范来验证它：

Definition main_spec :=
 DECLARE _main
  WITH p : int (* still toying with things, couldn't figure out how to drop this *)
  PRE [ ]
   PROP ()
   LOCAL ()
   SEP ()
  POST [ tint ]
   EX i : Z,
   PROP ( i = 8 )
   LOCAL (temp ret_temp  (Vint (Int.repr i)))
   SEP ().

一切顺利，只需使用 (forward) 直到 return 语句我剩下来证明以下内容

data_at Tsh tint (vint 9) v_y * data_at Tsh tint (vint 8) v_x |-- FF

这似乎应该是无法证明的（请注意，到目前为止我刚刚应用了 forward）。我期待一些说明在局部变量被取消分配后堆是空的，即emp |-- emp。

有什么地方可以让我了解更多相关信息吗？

谢谢！

附加信息：我深入研究了 FF post 条件的来源，它来自 typecheck_expr，特别是, Evar 的情况:

  | Evar id ty =>
      match access_mode ty with
      | By_reference =>
          match get_var_type Delta id with
          | Some ty' =>
              tc_bool (eqb_type ty ty')
                (mismatch_context_type ty ty')
          | None =>
              tc_FF
                (var_not_in_tycontext Delta id)
          end
      | _ => tc_FF (deref_byvalue ty) (* ?? *)
      end

除非我读错了，否则这似乎表明您不能按值访问局部变量。这只是一个疏忽吗？还是语义中有什么东西阻止了这种情况？

Answer 1

您使用的是哪个版本的 VST？在最近的主分支版本（提交 506f8e7）中，以下简单的证明工作得很好。

Lemma body_main: semax_body Vprog Gprog f_main 
main_spec.
Proof.
start_function.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
forward.
Exists 8.
entailer!.
Qed.

Answer 2

失败的原因是您忘记了 clightgen 的 -normalize 标志。如果您使用 clightgen -normalize 而不是 clightgen 翻译 .c 文件，它应该可以正常工作。

具有可寻址局部变量的规范

Specifications with Addressable Local Variables

verifiable-c