1

2 つの質問があります。

まず、インライン アセンブリを使用して C プログラムを作成した場合、VST で C プログラム全体を検証できますか? それとも、検証できるのは純粋な C プログラムだけですか?

次に、 http ://vst.cs.princeton.edu/ に記載されているように、最新の VST と Compcert をUbuntu 12.04 にインストールしようとしましたが、ある時点で、.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 のインストールを試みることができる新しいシステムが他にもありますが (必要な場合)、既に 2 回試しました。

前もって感謝します。

4

3 に答える 3

0

最初: インライン アセンブリ。インライン アセンブリの推奨される方法は、CompCert の「インライン化可能な外部関数呼び出し」としてモデル化することです。次に、関数の検証可能な C 関数仕様を指定します。CompCert は、実際の関数呼び出しではなく、インライン アセンブリを生成します。これは高度な手法です。最初から使用することはお勧めしません。

2 番目: ビルド エラー。vst.cs.princeton.edu Web サイトの VST 1.5 でしたか? それは「内部 compcert」(cd compcert; ./make) でしたか、それとも「外部 compcert」でしたか? 外部の場合、正しいバージョンの CompCert (2.1) を使用していますか?

第三に、「Coqはまだ知らない」について。Coq の経験がなければ、Verifiable C を使用するのは難しいでしょう。Coq を学ぶには、 Pierce らのSoftware Foundationsをお勧めします。

于 2015-01-12T20:01:37.163 に答える
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 に答える
0

あなたのコメント (VST 1.4 だったということ) に基づいて、Coq の互換性のない (新しすぎる) バージョンを使用している可能性があります。次の 2 つの理由から、VST 1.5 を試すことをお勧めします。

  1. VST 1.5 は、最近のバージョンの Coq と互換性があります (ちなみに、CompCert 2.4 とも互換性があります)。

  2. VST 1.5 の新機能である Makefile は、使用している Coq のバージョンを明示的にチェックし、互換性のないバージョンがある場合は明確なエラー メッセージを表示します。

したがって、これで問題が解決するという保証はありませんが、良いスタートになるかもしれません。

于 2015-01-15T17:51:50.070 に答える