1

我有两个问题：

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

其次，我尝试在 Ubuntu 12.04 上安装最新的 VST 和 Compcert，如http://vst.cs.princeton.edu/上所述，但在某些时候，在将 .v 文件转换为 .vo 文件时出现错误，并显示消息为形式：'不可能将“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 片段（我已标记第 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（如果有必要的话），即使我已经尝试了两次。

提前致谢。

4

3 回答 3

0

First: inline assembly. The recommended way to do inline assembly is to model it as a CompCert "inlineable external function call"; then you give a Verifiable C function specification for the function. CompCert will generate inline assembly, not a real function call. This is an advanced technique, I wouldn't suggest starting with it.

Second: build error. Was it VST 1.5 from the vst.cs.princeton.edu website? Was it an "internal compcert" (cd compcert; ./make), or an "external compcert"? If external, do you have the right version of CompCert (2.1)?

Third, regarding "I don't know Coq yet." Verifiable C will be hard to use if you have no Coq experience. I recommend Pierce et al's Software Foundations to learn Coq.

于 2015-01-12T20:01:37.163 回答
0

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

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

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

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

于 2015-01-15T17:51:50.070 回答
0

我在使用 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.
于 2015-01-13T13:11:12.623 回答