Coq编译器错误:无法将"4“与"8”统一。使用VST make

Question

我有两个问题：

首先，如果我用内联汇编写一个C程序，那么我可以用VST验证整个C程序吗？还是只有纯C程序才能被验证？

其次，我尝试在Ubuntu12.04的http://vst.cs.princeton.edu/上安装最新的VST和Compcert，但是在将.v文件转换成.vo文件的过程中，出现了一个错误信息：‘不可能把"2“和”8“统一起来。我想这个错误是在compcert的制作过程中发生的，但我不确定。

然后我尝试在Ubuntu14.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片段(我已经标记了第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函数规范。

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

Answer 2

我在CompCert 2.4上安装VST1.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. VST1.5与较新版本的Coq兼容(顺便说一句，与CompCert 2.4兼容)
2. 在Vst1.5中，Makefile会显式检查您的Coq的版本，如果您有不兼容的版本，它会给出明确的错误消息。

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