0

现在我试图证明一个简单的数组访问过程（文件 arr.c）：

void set(int* arr, int key, int val)
{
    arr[key] = val;
}

该文件arr.c被翻译为arr.v：

...
Definition f_set := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_arr, (tptr tint)) :: (_key, tint) :: (_val, tint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body :=
(Sassign
  (Ederef
    (Ebinop Oadd (Etempvar _arr (tptr tint)) (Etempvar _key tint)
      (tptr tint)) tint) (Etempvar _val tint))
|}.
...

这是我证明的开头（文件verif_arr.v）：

Require Import floyd.proofauto.
Require Import arr.

Local Open Scope logic.
Local Open Scope Z.

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

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

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  entailer!.

战术之后entailer!.，我得到了：

3 subgoals, subgoal 1 (ID 1261)

  Espec : OracleKind
  sh : share
  k : Z
  arr : Z -> val
  H : 0 <= k < 100
  H0 : forall i : Z, 0 <= i < 100 -> is_int (arr i)
  H1 : writable_share sh
  Delta := abbreviate : tycontext
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  karg : name _key
  arrarg : name _arr
  valarg : name _val
  rho : environ
  H2 : repr k (eval_id _key rho)
  POSTCONDITION := abbreviate : ret_assert
  H3 : isptr (eval_id _arr rho)
  ============================
   offset_val (Int.repr (sizeof tint * 0)) (eval_id _arr rho) =
   force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))

subgoal 2 (ID 1266) is:
 ?890 = force_val (sem_cast_neutral (eval_id _val rho))
subgoal 3 (ID 1235) is:
 semax Delta
   (PROP  ()
    LOCAL  (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr);
    `(eq v) (eval_id _val); `isptr (eval_id _arr))
    SEP  (`(array_at tint sh (upd arr 0 ?890) 0 100) (eval_id _arr)))
   (Sreturn None) POSTCONDITION

现在的问题：

  • 在规范set_spec中有一个前提条件'(array_at tint sh arr 0 100) (eval_id _arr)（这里'应该是反引号，这会破坏格式）。为什么这个陈述没有出现在假设列表中？

  • 第一个子目标在我看来就像它试图取消引用数组的 0 单元格 (arr + 0)，它应该等于第一个关键单元格 (arr + key)。这与代码或后置条件无关，当然无法证明。这里出了什么问题？

我用：

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

编辑：

后置条件的最后local ...一部分被证明是多余的。

4

1 回答 1

0

  • 首先，前提条件'(array_at tint sh arr 0 100) (eval_id _arr)实际上存在abbreviate于 Delta 假设中。

  • 其次，事实证明，这种entailer!.策略并不安全，并且可以从符合条件的目标中产生无法证明的目标。在这种情况下，

    • 首先，我需要提供额外的条件is_int v才能将其分配给“所有整数”数组的单元格。似乎 VST 无法从 CompCert 注释中推断出类型。
    • 然后entailer!.我不需要先分别证明右侧的所有命题，然后我可以申请entailer组合假设。

以下是正确的规格和证明：

Inductive repr : Z -> val -> Prop :=
| mk_repr : forall z, z >= 0 -> z < Int.modulus -> repr z (Vint (Int.repr z)).

Function aPut (arr:Z -> val) (k:Z) (v:val) : Z -> val :=
  fun (kk:Z) => if (Z.eq_dec k kk) then v else arr kk.

Definition set_spec :=
  DECLARE _set
    WITH sh : share, k : Z, arr : Z->val, vk : val, v : val, varr : val
    PRE [_key OF tint, _val OF tint, _arr OF (tptr tint)]
        PROP (0 <= k < 100; forall i, 0 <= i < 100 -> is_int (arr i);
              writable_share sh; repr k vk; is_int v)
        LOCAL (`(eq vk) (eval_id _key);
               `(eq varr) (eval_id _arr);
               `(eq v) (eval_id _val);
               `isptr (eval_id _arr))
        SEP (`(array_at tint sh arr
                        0 100) (eval_id _arr))
    POST [tvoid] `(array_at tint sh (aPut arr k v)
                            0 100 varr).

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

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
  start_function.
  name karg _key.
  name arrarg _arr.
  name valarg _val.
  forward.
  instantiate (1:=v).
  instantiate (2:=k).
  assert (offset_val (Int.repr (sizeof tint * k)) (eval_id _arr rho) =
          force_val (sem_add_pi tint (eval_id _arr rho) (eval_id _key rho))).
  inversion H2.
  rewrite sem_add_pi_ptr.
  unfold force_val.
  apply f_equal2.
  rewrite mul_repr.
  auto.
  auto.
  assumption.

  assert (eval_id _val rho = force_val (sem_cast_neutral (eval_id _val rho))).
  apply is_int_e in H3.
  destruct H3 as [n VtoN].
  rewrite VtoN.
  auto.
  entailer.
  forward.
Qed.
于 2015-01-14T21:23:01.970 回答