Coq 编译器错误：无法将“4”与“8”统一起来。用 VST 制作

Question

我有两个问题：

首先，如果我使用内联汇编编写 C 程序，我可以在 VST 中验证整个 C 程序吗？还是只有纯C程序可以验证？

其次，我尝试在 Ubuntu 12.04 上安装最新的 VST 和 Compcert，如 http://vst.cs.princeton.edu/ 所述，但在某些时候，在将 .v 文件转换为 .vo 文件时出现错误，并显示以下形式的消息：'Impossible to将“2”与“8”统一起来。我认为这个错误是在制作compcert时发生的，但我不确定。

然后我尝试使用本指南在 Ubuntu 14.04 上安装 VST：'http://ninj4.net/2014/05/16/hello-vst-hello-verifiable-c.html'。我安装了与指南中相同版本的 Coq、OCaml 和 Menhir。后来当我在 vst 目录中运行 make 时，我遇到了与上面类似的问题。以下是我得到的输出：

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 的 sn-p（我已标记第 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 in a Hurry”，虽然使用过 HOL）。我有其他新系统，我可以尝试在其上安装 VST（如果有必要的话），即使我已经尝试了两次。

提前致谢。

Answer 1

首先：内联汇编。进行内联汇编的推荐方法是将其建模为 CompCert “可内联外部函数调用”；然后你给这个函数一个可验证的 C 函数规范。 CompCert 将生成内联汇编，而不是真正的函数调用。这是一项先进的技术，我不建议从它开始。

第二：构建错误。是来自 vst.cs.princeton.edu 网站的 VST 1.5 吗？它是“内部compcert”（cd compcert；./make）还是“外部compcert”？如果外接， 您是否拥有正确版本的 CompCert (2.1)？

第三，关于“我还不知道 Coq”。可验证的 C 将很难使用，如果你 没有 Coq 经验。我推荐 Pierce 等人的 Software Foundations 来学习 Coq。

Answer 2

我在使用 CompCert 2.4 安装 VST 1.5 时遇到了同样的问题。作为一种解决方法，我在有问题的地方放置了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.

Answer 3

根据您的评论（它是 VST 1.4），一种可能性是您的 Coq 版本不兼容（太新）。我建议您可以尝试 VST 1.5，原因有两个：

1. VST 1.5 与最新版本的 Coq 兼容 （顺便说一下，使用 CompCert 2.4）

2. VST 1.5 中的新功能，Makefile 明确检查您拥有的 Coq 版本， 如果您有不兼容的版本，则会给出明确的错误消息。

因此，不能保证这会解决问题，但它可能是一个好的开始。