Странная цель VST при проверке хранилища массивов

Сейчас я пытаюсь доказать тривиальную процедуру доступа к массиву (файл 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))
|}.
...

Вот начало моего доказательства (файл verify_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) (здесь вместо ' должен быть backtick, который нарушает форматирование). Почему этого утверждения нет в списке гипотез?

  • Мне кажется, что первая подцель пытается разыменовать ячейку 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 ... часть в постовом состоянии оказалась избыточной.

Источник

1 ответ

Решение

  • Во-первых, предварительное условие '(array_at tint sh arr 0 100) (eval_id _arr) на самом деле присутствует позади abbreviate в гипотезе дельты.

  • Во-вторых, оказалось, что 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.
Источник
Другие вопросы по тегам