如何推理 VST 中的数组访问？

Question

我无法证明一个简单的数组访问函数（文件 arr.c）：

int get(int* arr, int key)
{
    return arr[key];
}

由 clightgen arr.c 翻译成（文件 arr.v）：

...
Definition f_get := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := ((_arr, (tptr tint)) :: (_key, tint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body :=
(Sreturn (Some (Ederef
                 (Ebinop Oadd (Etempvar _arr (tptr tint))
                   (Etempvar _key tint) (tptr tint)) tint)))
|}.
...

证明开始(verif_arr.v):

Require Import floyd.proofauto.
Require Import arr.

Local Open Scope logic.
Local Open Scope Z.

Definition get_spec :=
  DECLARE _get
    WITH sh : share, k : Z, arr : Z->val, vk : val, varr : val
    PRE [_key OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i))
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tint] `(array_at tint sh arr
                           0 100 varr) &&
                 local(`(eq (arr k)) retval).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get_spec :: nil.

Lemma body_get: semax_body Vprog Gprog f_get get_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  forward.

执行 forward（verif_arr.v 的最后一行）后，我实现了以下目标：

 array_at tint sh arr 0 100 arrarg
 |-- !!(False /\ False /\ arr k = Vundef) &&
     array_at tint sh arr 0 100 arrarg

这意味着False，所以我无法证明。但是，c 实现很简单，证明才刚刚开始。

现在回答问题：

规范有什么问题，为什么它达到了无法证明的目标？

VST版本:

Definition svn_rev := "6834P".
Definition release := "1.5".
Definition date := "2014-10-02".

CompCert 版本：2.4

Coq 版本:

The Coq Proof Assistant, version 8.4pl3 (January 2014)
compiled on Jan 19 2014 23:14:16 with OCaml 4.01.0

Answer 1

在 "standard" Verifiable-C 中，内存引用不能出现在表达式中，除非在加载语句的顶层：

x = a[e];    or     x = *(e.field);  (same as    x = e->field;)

其中 e 是任何不访问内存的表达式。

或者，商店声明， a[e1] = e2;或者 e1->field = e2；其中 e1 和 e2 不访问内存。

内存引用不得出现在 return 语句中。您必须按如下方式分解您的程序：

int x;
x = arr[key];
return x;

然后继续证明。

我们正在考虑扩展，即 "nonstandard" 可验证 C，其中内存引用可以嵌套在其他上下文中的表达式中；但完全不清楚这是对程序进行推理的好方法。这将是值得的实验。

你在前提条件中获得 "False" 的原因是表达式 arr[key] 没有作为有效表达式进行类型检查，因为它包含内存引用。在这种情况下，我们需要努力改进错误消息反馈。

如何推理 VST 中的数组访问？

How to reason about array access in VST?

verification

coq

verifiable-c