Ошибка VST forward_call при нестандартном соглашении о вызовах - PullRequest
Новая
       72

Ошибка VST forward_call при нестандартном соглашении о вызовах

2 голосов
/ 21 апреля 2020

Я использую VST 2.5 и Coq 8.11.0

Произошла ошибка при выполнении функции forward_call с нестандартным соглашением о вызовах. Пример минимального кода: 

struct t {
  int t_1;
  int t_2;
};

struct t test_aux() {
  struct t ret;
  ret.t_1 = 1;
  ret.t_2 = 2;
  return ret;
}

void test_f() {
  test_aux();
}

Спецификации VST: 

Require Import VST.floyd.proofauto. 
Require Import example.

Definition Vprog : varspecs. mk_varspecs prog. Defined. Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Open Scope Z.

Definition aux_spec : ident * funspec :=   DECLARE _test_aux
    WITH res : val
    PRE [tptr (Tstruct _t noattr)]
      PROP ()
      PARAMS (res)
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) res)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP (data_at Tsh (Tstruct _t noattr) 
                   (Vint (Int.repr 1), Vint (Int.repr 2)) res).

Definition test_spec : ident * funspec :=   DECLARE _test_f
    WITH temp : val
    PRE []
      PROP ()
      PARAMS ()
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) temp)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP ().

Definition Gprog := ltac:(with_library prog [aux_spec; test_spec]).

Theorem test : semax_body Vprog Gprog f_test_f test_spec. Proof.   start_function.   Fail forward_call (nullval). Admitted.

Ошибка: 

Unable to unify  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid cc_default" with  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid
    {|
    cc_vararg := false;
    cc_unproto := false;
    cc_structret := true |}".

Я не знаю, является ли это ошибкой или предполагаемым поведением, поэтому у меня есть несколько вопросов здесь:

1) Это ошибка?

2) Если нет, какие обходные пути существуют, чтобы доказать такие случаи?

ОБНОВЛЕНИЕ:

Мы столкнулись с этой проблемой после использования следующего обходного пути для ограничения структурного копирования: мы определяем функцию struct_normalize : statement -> statement в Coq, которая заменяет структурные назначения полевыми назначениями. Следовательно, мы работаем в предположении, что в вызываемой функции нет структурного копирования. То есть мы можем проверить test_aux из приведенного выше примера. Итак, вопросы:

Сбой forward_call только потому, что cc_structret := true в test_aux AST?

Учитывая, что мы нормализуем функции и удаляем копирование структуры из тел функции, безопасно ли соответственно изменить значение structret и продолжить проверку?

1 Ответ

2 голосов
/ 21 апреля 2020

К сожалению, VST не поддерживает копирование структуры, передачу структуры или возвращение структуры. Смотри также этот вопрос . Поэтому вы не можете проверить эту программу, не изменив ее.

...