Ошибка компилятора Coq: невозможно объединить "4" с "8". с VST сделать

У меня есть два вопроса:

Во-первых, если я напишу программу на C со встроенной сборкой, могу ли я проверить всю программу на C в VST? Или это только программы на чистом C, которые можно проверить?

Во-вторых, я попытался установить последние версии VST и Compcert, как указано на http://vst.cs.princeton.edu/ в Ubuntu 12.04, но в какой-то момент произошла ошибка при преобразовании файлов.v в файлы.vo с сообщением форма: "Невозможно объединить"2"с"8"". Я думаю, что эта ошибка произошла во время сборки compcert, но я не уверен.

Затем я попытался установить VST на Ubuntu 14.04, используя это руководство: " http://ninj4.net/2014/05/16/hello-vst-hello-verifiable-c.html". Я установил те же версии Coq, OCaml и Menhir, что и в руководстве. Позже, когда я запустил make в каталоге vst, у меня возникла та же проблема, что и выше. Вот что я получил в качестве вывода:

Makefile:289: .depend: No such file or directory  
coqdep -slash  -I msl -as msl  -I sepcomp -as sepcomp'...  
...  
...  
'COQC floyd/forward_lemmas.v  
COQC floyd/array_lemmas.v  
COQC floyd/data_at_lemmas.v  
COQC floyd/globals_lemmas.v  
File "/home/jhagl/verifiable-c/vst/floyd/data_at_lemmas.v", line 429, characters 49-60:  
Error: Impossible to unify "4" with "8".  
make: ** * [floyd/data_at_lemmas.vo] Error 1  
make: *** Waiting for unfinished jobs....

Ниже приведен фрагмент из data_at_lemmas.v леммы, которая не работает (я отметил строку 429):

Lemma align_chunk_alignof: forall t ch, access_mode t = By_value ch -> legal_alignas_type t = true -> alignof t = Memdata.align_chunk ch.  
Proof.  
Transparent alignof.  
  intros.  
  destruct t; inversion H.  
  - unfold legal_alignas_type in H0.  
    simpl in H0.  
    destruct i, s; inversion H2; simpl;  
    destruct (attr_alignas a); try inversion H0; reflexivity.  
  - unfold legal_alignas_type in H0.  
    simpl in H0.  
    destruct s; inversion H2; simpl;  
    destruct (attr_alignas a); try inversion H0; admit. (* Tlong uncompatible problem *)  
  - unfold legal_alignas_type in H0.  
    simpl in H0.  
    destruct f; inversion H2; simpl;  
(\* Line 429 *)    destruct (attr_alignas a); try inversion H0; reflexivity.  
  - unfold legal_alignas_type in H0.  
simpl in H0.  
    inversion H2; simpl;
destruct (attr_alignas a); try inversion H0; reflexivity.  
Opaque alignof.  
Qed.

Кроме того, я попытался выполнить следующую команду в bash:./configure -toolprefix arm-none-eabi- arm-eabi -no-runtime-libи получил это сообщение об ошибке:./configure: 65: shift: can't shift that manyНо ./configure -toolprefix arm-none-eabi- arm-eabi работал. Это не было проблемой, так как я изменил Makefile.config.

Любые предложения о том, как это исправить? Я еще не знаю Coq (я только что прочитал руководство "Coq в спешке" и использовал HOL). У меня есть другие свежие системы, на которых я могу попытаться установить VST (если это необходимо), хотя я уже пробовал дважды.

Заранее спасибо.

Источник

3 ответа

Первое: встроенная сборка. Рекомендуемый способ выполнения встроенной сборки состоит в том, чтобы смоделировать его как "встроенный вызов внешней функции" CompCert; затем вы даете спецификацию функции Verifiable C для этой функции. CompCert будет генерировать встроенную сборку, а не вызов реальной функции. Это продвинутая техника, я бы не советовал начинать с нее.

Второе: ошибка сборки. Это был VST 1.5 с сайта vst.cs.princeton.edu? Был ли это "внутренний compcert" (cd compcert; ./make) или "внешний compcert"? Если внешняя, у вас есть правильная версия CompCert (2.1)?

В-третьих, в отношении "я еще не знаю Coq". Verifiable C будет трудно использовать, если у вас нет опыта Coq. Я рекомендую Основы программного обеспечения Pierce et al., Чтобы выучить Coq.

Источник

У меня была такая же проблема при установке VST 1.5 с CompCert 2.4. В качестве обходного пути я разместил admit тактика в проблемных местах. Например Ваша лемма теперь выглядит так (обратите внимание на комментарий (*!!! ... *)):

Lemma align_chunk_alignof: forall t ch, access_mode t = By_value ch -> legal_alignas_type t = true -> alignof t = Memdata.align_chunk ch.
Proof.
Transparent alignof.
  intros.
  destruct t; inversion H.
  - unfold legal_alignas_type in H0.
    simpl in H0.
    destruct i, s; inversion H2; simpl;
    destruct (attr_alignas a); try inversion H0; reflexivity.
  - unfold legal_alignas_type in H0.
    simpl in H0.
    destruct s; inversion H2; simpl;
    destruct (attr_alignas a); try inversion H0; admit. (* Tlong uncompatible problem *)
  - unfold legal_alignas_type in H0.
    simpl in H0.
    destruct f; inversion H2; simpl.
    destruct (attr_alignas a). try inversion H0; reflexivity.
    reflexivity.
    destruct (attr_alignas a).  (* try inversion H0. *)
    inversion H0.
    admit. (* !!! that didn't work out. I can't proove 4=8 *)
  - unfold legal_alignas_type in H0.
    simpl in H0.
    inversion H2; simpl;
    destruct (attr_alignas a); try inversion H0; reflexivity.
Opaque alignof.
Qed.
Источник

Исходя из вашего комментария (что это был VST 1.4), одна возможность состоит в том, что у вас есть несовместимая (слишком новая) версия Coq. Я предлагаю вам попробовать VST 1.5 по двум причинам:

  1. VST 1.5 совместим с более свежими версиями Coq (и с CompCert 2.4, кстати)

  2. Новое в VST 1.5, Makefile явно проверяет, какая у вас версия Coq, и выдает четкое сообщение об ошибке, если у вас несовместимая версия.

Таким образом, нет никакой гарантии, что это решит проблему, но это может быть хорошим началом.

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