VCCサーベイ

vcc-survey.rd

= VCCサーベイ
[2018-04-15 15:00]

<<<VCC
<<<サーベイ

https://archive.codeplex.com/?p=vcc

論文を以下に置いた:

file:///home/kiwamu/Dropbox/doc/VCC

== 知りたいこと

=== unionの扱い

```
$ pwd
/home/kiwamu/Dropbox/doc/VCC
$ pdfgrep union *
--snip--
1-s2.0-S1571066109004150-main.pdf:For unions we have the additional complication that only one of the fields
--snip--
28ff3644-78f3-46ea-b83e-df4452086459.pdf:If a union includes a member of value type, exactly one of these
--snip--
fda99f81-18b5-45ae-8f49-5b28c747dcc3.pdf:                                                                         A C union defines a group of objects that share memory addresses.
```

=== ビットフィールドの扱い

```
$ pwd
/home/kiwamu/Dropbox/doc/VCC
$ pdfgrep bitfields *
1-s2.0-S1571066109004150-main.pdf:  This does not include bitfields, see section 6.3.
1-s2.0-S1571066109004150-main.pdf:types like unions, arrays, and bitfields are incorporated into the typed model
1-s2.0-S1571066109004150-main.pdf:to interpret several fields of integer types (particularly bitfields) as one integer
1-s2.0-S1571066109004150-main.pdf:     To discharge formulas involving bitfields, we had been using a decision
```

=== アセンブラの扱い

```
$ pwd
/home/kiwamu/Dropbox/doc/VCC
$ pdfgrep Assembly *
tphol2009.pdf:C and Assembly Code. System software requires interaction between C and
tphol2009.pdf:Assembly verification in VCC is discussed in [5].
$ pdfgrep assembly *
1-s2.0-S1571066109004150-main.pdf:the memory safety of approx 4500 lines of the x86 assembly code by translat-
fda99f81-18b5-45ae-8f49-5b28c747dcc3.pdf:issues a warning if there is more than one volatile physical memory     assembly instruction. It takes a memory location and two values.
tphol2009.pdf:assembly code. This involves subtleties such as the semantics of calls between C
tphol2009.pdf:and assembly (in each direction), and consideration of which hardware resources
tphol2009.pdf:(100KLOC of C, 5KLOC of assembly) that runs directly on x64 hardware. The
tphol2009.pdf:plemented: to generate contracts for assembly functions from their C correspon-
tphol2009.pdf:an industrial microkernel), the FLINT project [30] (verification of an assembly
```

[5]はこれらしい: https://www.microsoft.com/en-us/research/publication/vx86-x86-assembler-simulated-in-c-powered-by-automated-theorem-proving/

=== vcc-tutorial-col1w.pdf

コード例が多いので一番最初に読むと良さそう。また理論面も説明をはぶいてくれるので数学音痴にはありがたい。

* object invariantsはstruct/union両方に打ち込める
* decreases節の推論が賢いっぽい
* union_reinterpretで有効なunionを切り換える
* メモリはblobとして確保され、object化すると対応するblobが無効になる

xxx

=== 1-s2.0-S1571066109004150-main.pdf

xxx 重点的に読む

=== Vx86Amast2008.pdf

xxx 検証に関係ありそうなところを読む

=== tphol2009.pdf

xxx 上記の後でざっくり読む

=== 28ff3644-78f3-46ea-b83e-df4452086459.pdf

xxx 上記の後でざっくり読む

=== fda99f81-18b5-45ae-8f49-5b28c747dcc3.pdf

xxx 上記の後でざっくり読む

=== 10.1.1.625.6594.pdf

あんまり重要そうじゃないので、ざっくり読んで終えた。並列実行に対する検証の理論面が中心だった印象。

== VCCをWindowsで試してみる

新川のMacBook Air上のWindowsにインストールしてみる。
バイナリ配布はもう残っておらず、ソースからビルドするしかないようだ:

https://github.com/microsoft/vcc

* Visual Studio Community 2017とF#をインストール
* Vcc.slnを開いてビルド(.NET 2.0のままプロジェクトをビルドする)

が、Vcc.slnのビルドに成功しない。。。やはりVisual Studio Community 2015が必要なのか。。。

https://my.visualstudio.com/Downloads?PId=2226 からVisual Studio Community 2015がダウンロードできた。

* Visual Studio Community 2015とF#をインストール
* Vcc.slnを開いてビルド
* .NET Core SDKに誘導されるのでインストール

ビルドエラーになる。あきらめるか。。。

== VCCをオンラインで試してみる

https://rise4fun.com/Vcc

Gitからサンプルコードを選んでみると以下が見つかった:

```
$ find . -name "*.c"
./vcc/Docs/SyntaxUpdate/PageSet.c
./vcc/Docs/SyntaxUpdate/FromTutorial/done/03_lsearch.c
--snip--
./vcc/Docs/Tutorial/7.0.arraySet.c
./vcc/Docs/Tutorial/5.7.solutions.c
./vcc/Docs/Tutorial/c/03_lsearch.c
--snip--
./vcc/Plugins/Vcc2Plugins/SeparationLogicTests/testsuite/array_without_size.c
--snip--
./vcc/Demo/ssort.c
--snip--
./vcc/Tools/VccSyntaxCoverter/example.c
./vcc/Test/testsuite/vacid-0/RedBlackTrees.c
--snip--
./vcc/Test/testsuite/examples3/ByteString.c
--snip--
./vcc/Test/testsuite/old_tutorial/inc.c
--snip--
./vcc/Test/testsuite/vscomp2010/vscomp2010_p3_v2.c
```

なんとなくだけど、vcc/Docs/とvcc/Demo/を読めば良さそう。
が、Demoの下は複数ファイルにまたがっているものも多いのでオンラインで実行できないかもしれない。後回し。

=== vcc/Docs/Tutorial/以下のCファイルをオンラインで実行してみる:

xxx

=== vcc/Docs/SyntaxUpdate/以下のCファイルをオンラインで実行してみる

xxx

=== vcc/Demo/以下のCファイルを読む

xxx

== xxx 買えたら読む https://link.springer.com/chapter/10.1007/978-3-642-14295-6_42