Как обрабатывать цели "Forall (closed_wrt_vars (eq _z')) P " в VST?

На этот раз я проверяю функцию вызова другого. vars.c:

int pure0 ()
{
    return 0;
}

int get0(int* arr)
{
    int z = pure0();
    return 0;
}

Мое доказательство начала - verif_vars.v:

Require Import floyd.proofauto.
Require Import vars.

Local Open Scope logic.
Local Open Scope Z.

Definition get0_spec :=
  DECLARE _get0
    WITH sh : share, arr : Z->val, varr : val
    PRE [_arr OF (tptr tint)]
        PROP ()
        LOCAL (`(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).

Definition pure0_spec :=
  DECLARE _pure0
    WITH sh : share
    PRE []
        PROP ()
        LOCAL ()
        SEP ()
    POST [tint] local(`(eq (Vint (Int.repr 0))) retval).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get0_spec :: pure0_spec ::nil.

Lemma body_pure0: semax_body Vprog Gprog f_pure0 pure0_spec.
Proof.
  start_function.
  forward.
Qed.


Lemma body_get0: semax_body Vprog Gprog f_get0 get0_spec.
Proof.
  start_function.
  name arrarg _arr.
  forward_call (sh).
  entailer!.

Что побуждает к цели:

2 subgoals, subgoal 1 (ID 566)

  Espec : OracleKind
  sh : share
  arr : Z -> val
  varr : val
  Delta := abbreviate : tycontext
  POSTCONDITION := abbreviate : ret_assert
  MORE_COMMANDS := abbreviate : statement
  Struct_env := abbreviate : type_id_env.type_id_env
  arrarg : name _arr
  ============================
   Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

subgoal 2 (ID 567) is:
 DO_THE_after_call_TACTIC_NOW

Я полагаю, это говорит о том, что вызов функции не меняет arr содержание, что вполне очевидно для меня.

Что я могу сделать с этой целью? Какая тактика применяется здесь, и что именно означает утверждение? Должен ли я обогатить pure0 Спец как-то указать, что это ничего не меняет?

Источник

3 ответа

Решение

ПЕРВЫЙ: при написании вопросов VST/Verifiable-C, пожалуйста, укажите, какую версию VST вы используете. Похоже, вы используете 1.4.

ВТОРОЙ: я не уверен, что это отвечает на все ваши вопросы, но,

"closed_wrt_vars SP" говорит, что поднятое утверждение P закрыто относительно всех переменных в наборе S. То есть S - это набор идентификаторов языка C, которые могут обозначать неадресуемые локальные переменные ("temps", а не "vars"). "). P является утверждением формы "environment->mpred", а "closed" означает, что если вы измените "environment", чтобы иметь разные значения для любой из переменных в наборе S, то истинность P не изменится.

"Forall" - это стандартный предикат библиотеки Coq для применения предиката к списку. Так,

 Forall (closed_wrt_vars (eq _z')) [`(array_at tint sh arr 0 100 varr)]

означает, что набор S будет единственным набором, содержащим только переменную _z'. Здесь мы утверждаем, что все предикаты в списке закрыты по отношению к S. В списке ровно один предикат, и он "тривиально поднят", то есть для любого предиката (P: mpred), поднятый предикат

`(Р)

эквивалентно (fun rho:environment => P). Итак, тривиально: `P не волнует, что вы делаете с rho, включая изменение значения _z'.

"Авто с закрытым" (или, чтобы быть уверенным, "авто 50 с закрытым") должно позаботиться об этом, и вы указываете, что оно позаботится об этом. Итак, я предполагаю, что остальная часть вашего вопроса была "что здесь происходит?", И я надеюсь, что я ответил на него.

Источник

Решение, используемое в vst/progs/verif_reverse.v:

auto with closed.

К сожалению, он отвечает только на половину вопросов.

Источник

Кстати (не имеет отношения к вашему вопросу), предварительное условие `isptr (eval_id _arr) для get0, вероятно, не требуется. Это подразумевается уже `(array_at tint sh arr 0 100) (eval_id _arr)),

Кроме того, предположим, что вы хотели `isptr (eval_id _arr) в вашем предварительном условии; Вы могли бы написать это как,

   PROP (isptr varr)
   LOCAL (`(eq varr) (eval_id _arr))
   SEP (`(array_at tint sh arr 0 100 varr))

что (в некотором смысле) проще и более "канонично".

Источник
Другие вопросы по тегам