問題タブ [verifiable-c]

検証済みソフトウェア ツールチェーン (VST) を使用して学習しています。単純な「if-then-else」ブロックの証明に行き詰まります。

.c ファイルは次のとおりです。

次のように仕様を書きiftest()ます。

証明の手順は次のとおりです。

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec.Proof. start_function. name a _a. name r _r. forward. (*r=0*) simplify_typed_comparison. forward. (*if(E)*). go_lower. subst. normalize.

それは仮説を生成します:Post := EX x : ?214, ?215 x : environ -> mpredそして、「then」節は「go_lower」と「normalize」によって続けることはできません。

VST でプログラムを検証しようとしています。奇妙なエラー メッセージが表示されます。

私にとっては、関数シグネチャのように思えます。使用するのforward_callは、まさにここで必要なものです ( share * Z * Z * val * val)

しかし、VST は文句を言います。どこを見ればいいですか？ここで何が違うのですか？

ところで、それが役立つ場合、私の中間証明状態: 1 フォーカスされたサブゴール (フォーカスされていない: 1-0-0) 、サブゴール 1 (ID 4026)

自明な配列アクセス関数 (ファイル arr.c) を証明するのに問題があります。

clightgen arr.cこれは(ファイル arr.v)によって翻訳されます:

これがプルーフ スタート (verif_arr.v) です。

forward(verif_arr.v の最後の行) を実行した後、次の目標を達成しました。

これは を意味するFalseので、証明することはできません。ただし、c 実装は自明であり、証明は始まったばかりです。

今質問に：

仕様の何が問題なのか、なぜ証明できない目標に到達したのか?

VST バージョン:

CompCert バージョン: 2.4

コックのバージョン:

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 を実行すると、上記と同様の問題が発生しました。以下は、出力として得たものです。

以下は、失敗した補題の data_at_lemmas.v からの抜粋です (429 行目にマークを付けました)。

余談ですが、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 回試しました。

前もって感謝します。

今、簡単な配列アクセス手順 (ファイル arr.c) を証明しようとしています:

ファイルarr.cは次のように変換されarr.vます:

これが私の証明の始まりです (ファイル verif_arr.v):

戦術の後entailer!.、私は持っています：

今質問：

• 仕様set_specには前提条件があり'(array_at tint sh arr 0 100) (eval_id _arr)ます (ここで'は、フォーマットを壊すバッククォートにする必要はありません)。このステートメントが仮説リストにないのはなぜですか?

• 最初のサブゴールは、配列の 0 セル (arr + 0) を逆参照しようとしているように思えます。これは、キー番目のセル (arr + key) と等しくなければなりません。それはコードや事後条件とは何の関係もなく、確かに証明できません。ここで何がうまくいかなかったのですか？

私が使う：

VST バージョン:

CompCert バージョン: 2.4

コックのバージョン:

編集：

投稿条件の最後のlocal ...部分は冗長であることが判明しました。

2 つの関数の証明をプログラム全体の証明にまとめようとしています。

戦術を適用する前にsemax_func_cons、次の目標があります。

f_getしたがって、証明された lemma で消去するのが妥当と思われbody_getます。なぜ作戦は失敗するのか?

メッセージは役に立ちません：

今回は他を呼び出す関数を証明しています。vars.c:

私の証明開始 - verif_vars.v:

目標を誘導するもの：

関数呼び出しは内容を変更しないと述べていると思いますがarr、これは私にとっては明らかです。

この目標に対して何ができるでしょうか？ここで適用される戦術はどれですか?また、このステートメントは正確には何を意味していますか? 仕様を充実させpure0て、何も変更しないことを何らかの形で指摘する必要がありますか?

私の簡単なプログラムはvars.c次のとおりです。

証明を開始しました (ファイルverif_vars.c):

最終的に 2 つのサブゴールができました。

• 最初のものはpure0_spec事後条件から直接続きます。しかし、どうすればそれをCoqに伝えることができますか?
• admit. entailer.2 番目の目標は ( によって) に簡略化できますTT |-- emp。これも些細なことのように思えますが、それでもどうやってそれを証明できますか (SearchAbout derivesそしてSearchAbout emp一般的な補題を示していません)?

私が使用するもの: VST 1.5 (2014-10-02 で 6834P)、CompCert 2.4、Coq 8.4pl3(Jan'14) with OCaml 4.01.0。

WITH構成は、最大 8 つの変数に対してのみ定義されます。どうすれば 8 個以上を使用できますか? 例：

=>

私が使用するもの: VST 1.5 (2014-10-02 で 6834P)、CompCert 2.4、Coq 8.4pl3(Jan'14) with OCaml 4.01.0。