2

自明な配列アクセス関数 (ファイル 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

コックのバージョン:

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

1 に答える 1

2

「標準」の Verifiable-C では、ロード ステートメント内のトップ レベルを除き、式でメモリ参照を行うことはできません。

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

ここで、e はメモリにアクセスしない任意の式です。

または、store ステートメント、a[e1] = e2; または e1->field = e2; ここで、e1 と e2 はメモリにアクセスしません。

return ステートメント内でメモリ参照を行うことはできません。次のようにプログラムを因数分解する必要があります。

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

そして証明を進めます。

私たちは拡張機能、つまり「非標準」の Verifiable C を検討しています。この拡張機能では、メモリ参照を他のコンテキストの式内にネストすることができます。しかし、これがプログラムについて推論する良い方法であるかどうかはまったく明らかではありません。実験する価値があります。

前提条件で「False」を取得している理由は、メモリ参照が含まれているため、式 arr[key] が有効な式として型チェックされないためです。このような状況では、より良いエラー メッセージ フィードバックに取り組む必要があります。

于 2015-01-12T13:59:03.340 に答える