Drop Checkerの規則をちゃんと理解する

概要: Drop CheckerはRustのボローチェッカに付属する追加の検査器で、コンパイラが自動で挿入するdrop処理の安全性を保証するためのものである。これの詳細な規則とその正当性を理解したかったので自分なりに整理した。

dropckの概要についてはRustonomiconの説明とか以前の記事とかを参照。

注意: 本記事の内容はコンパイラの実装との対応をとっていないので実際の実装とは異なる可能性がある。

規格

用語

  • Drop::drop(): ユーザー定義のデストラクタ自体
  • mem::drop_in_place(): 値をデストラクトするために Drop::drop()再帰的に呼び出す一連の手続き

mem::drop_in_place() の実装は型ごとにコンパイラが生成するが、大雑把に言うと以下のようになる:

struct Foo {
    bar: Bar,
    baz: Baz,
}

fn drop_in_place<T>(foo: &mut T) where T == Foo {
    // Drop::drop() を呼ぶ (存在すれば)
    <Foo as Drop>::drop(foo);
    // 各メンバについて再帰的に呼ぶ
    drop_in_place(&mut foo.bar);
    drop_in_place(&mut foo.baz);
}

問題

mem::drop_in_place() の呼び出しを挿入するとライフタイム条件が壊れる

    {
+------ let x = ..;
| +---- :
| | 'in :
| +---- :
| 'out  << mem::drop_in_place(&mut x); >> // コンパイラが挿入するdrop
+------
    }

このとき、

  • xの型自体に 'in が全く使えないのは困る。これは相互参照するデータを作るために必要。
  • しかし、 drop_in_placeの途中で 'in は使えなくなるから、 drop_in_place'in に関してフルアクセスできる保証はない

解決方法

mem::drop_in_place の中では、 x に関係するライフタイム全てが有効であるとは限らないことにする。例えば、 x: Foo<'a> を使う関数は、通常 'a がまだ有効であることを仮定してよいが、 mem::drop_in_place に関してはこれを仮定できない場合がある。そのかわり、以下のルールに従って、一部のライフタイムに関してだけは、その有効性を仮定してよい。

コンパイラは、それらのライフタイムが上記の 'out まで生存すること (つまり 'in よりも真に長く生存すること) をチェックする。

drop_lifetimes 収集の流れ

mem::drop_in_place<T> で有効性を仮定してよいライフタイムの一覧を drop_lifetimes(T) と呼ぶことにする。 mem::drop_in_place<T> は以下の手順で定義される。

  1. Drop::drop() が触れうるライフタイムを列挙する。
  2. mem::drop_in_place() がどのように再帰的に呼ばれうるかを調べる。
  3. 1の情報を2の構造に沿って再帰的に収集する。

Drop::drop() が触れうるライフタイムの列挙

例として、 Foo<'a, 'b, T, U> という型を考える。この Drop::drop() が触れうるライフタイムの一覧を、以下のように保守的に列挙する。

FooDrop を実装していない場合

Drop で何もしないことがはっきりわかるので、どのライフタイムも必要ではない。

user_drop_lifetimes(Foo<'a, 'b, T, U>) = {}

FooDrop を実装している場合

保守的に、全てのパラメーターのライフタイムを仮定する。

user_drop_lifetimes(Foo<'a, 'b, T, U>) = {'a, 'b} ∪ {Tの全てのライフタイム} ∪ {Uの全てのライフタイム}

FooDrop 実装が #[may_dangle] を持っている場合

unsafe#[may_dangle] を組み合わせることで、ユーザーの責任で「このライフタイムしか使わない」と宣言することができる。例えば、

unsafe impl<'a, #[may_dangle] 'b, T, #[may_dangle] U> Drop for Foo<'a, 'b, T, U> { .. }

の場合、

user_drop_lifetimes(Foo<'a, 'b, T, U>) = {'a} ∪ {Tの全てのライフタイム}

となる。

mem::drop_in_place()再帰的呼び出し構造

この再帰呼び出し構造のことを、単に「型Tが型Uを所有する」ともいう。これは、「mem::drop_in_place<T>() の中で mem::drop_in_place<U>() が呼び出されうる」という関係を近似したものである。例えば、 structenumdrop_in_place 内では、全てのメンバの drop_in_place が呼び出されうる。

実際にコンパイラで検査をするさいは、循環的な所有関係があることに注意する必要がある。

この規則はほぼ上の説明通りだが、以下の2点に注意が必要である。

  • PhantomData<T>T を所有する。
  • [T; 0]T を所有する。

user_drop_lifetimes再帰的に収集する

結局、 drop_lifetimes は以下のように定義される。

drop_lifetimes(T) = { 'a | T は U を所有し、 'a ∈ user_drop_lifetimes(U) である }

最終的な規約

  • <T as Drop>::drop() 内では、 drop_lifetimes(T) (user_drop_lifetimes(T) ではないことに注意) の有効性のみを仮定できる。
    • #[may_dangle] を使わない限りは、自動的に保証される。
  • 上記の規約により、 mem::drop_in_place<T>() も、 drop_lifetimes(T) の有効性のみを仮定すれば安全であることが保証される。
  • 逆に、利用する側では、以下の条件がチェックされる: 型 T の値がdropされるとき、 drop_lifetimes(T) のライフタイムはその値よりも真に長く生存する必要がある。

最後に Rc で復習

Rc は以下のように定義されている。

struct Rc<T: ?Sized> {
    ポインタ,
    _marker: PhantomData<T>,
}

unsafe impl<#[may_dangle] T: ?Sized> Drop for Rc<T> {
    fn drop(&mut self) {
        ...
        mem::drop_in_place::<T>(ポインタ);
        ...
    }
}

ポイントとして、 RcDrop 実装は T#[may_dangle] がついている。これは mem::drop_in_place::<T> を呼んでいるから、一見おかしいように見える。しかし実は問題ない。確かに、 #[may_dangle] の効果により

user_drop_lifetimes(Rc<T>) = {}

となるが、 PhantomData<T> があるので

drop_lifetimes(Rc<T>) = drop_lifetimes(T)

となる。

上の規約で

  • <T as Drop>::drop() 内では、 drop_lifetimes(T) の有効性のみを仮定できる。

  • <T as Drop>::drop() 内では、 user_drop_lifetimes(T) の有効性のみを仮定できる。

と書かなかったのはそのためである。

なお、 RcPhantomData<T>#[may_dangle] をやめて

struct Rc<T: ?Sized> {
    ポインタ,
}

impl<T: ?Sized> Drop for Rc<T> {
    fn drop(&mut self) {
        ...
        mem::drop_in_place::<T>(ポインタ);
        ...
    }
}

としても安全だと思われる。しかし、この場合は

drop_lifetimes(Rc<T>) = drop_lifetimes(T)

ではなく

drop_lifetimes(Rc<T>) = lifetimes(T) (T の全てのライフタイム)

となってしまう。つまり、この状態だとdropckはより厳しい挙動をしてしまう。つまり、この2つの違いは、

  • Tdrop_in_place を呼ぶだけなら、 PhantomData<T> を使って #[may_dangle] T とすることで、 drop_lifetimes(T) の保証のみを得ることができる。
  • T に対してより一般的な処理をするなら、何もしないことで lifetimes(T) の保証を得ることができる。 (そのぶんdropckが厳しくなる)

といえる。

RFC1238時代はどう違ったか

RFC1238とRFC1327の違いは、単に #[may_dangle] の粒度の違いだけである。

例えば、RFC1238では

impl<'a, 'b, T, U> Drop for Foo<'a, 'b, T, U> {
    #[unsafe_destructor_blind_to_params]
    fn drop(&mut self) { .. }
}

と書くと、今でいう

unsafe impl<#[may_dangle] 'a, #[may_dangle] 'b, #[may_dangle] T, #[may_dangle] U> Drop for Foo<'a, 'b, T, U> { .. }

と同じ意味になる。このように #[may_dangle] を一括で適用するしかないので、

unsafe impl<'a, #[may_dangle] 'b, T, #[may_dangle] U> Drop for Foo<'a, 'b, T, U> { .. }

と同等の記述はできない。

RFC0769時代はどう違ったか

RFC0769の時点ではパラメトリシティを用いて、より積極的に安全性を推論していた。パラメトリシティとは、例えば

fn foo<T: Sync>(x: T) { .. }

のような関数があったときに、 foox に対してできることは限られている (具体的には drop するか forget するくらいしかない) という仮定である。

この仮定が成立する理由は、 foox に関して、 Sized + Sync であるという限定的な情報しか持っていないからである。 x: T: Sync だとわかっても、 Sync は何もメソッドを持たないので、特にできることがないということになる。

しかし、現在はこのパラメトリシティという仮定は崩れている。特殊化を用いると、

fn foo<T: Sync>(x: T) {
    // 何もしない
}
fn foo<T: Sync + Foo>(x: T) {
    // TがFooを実装していたときは、何かをする
    x.foo();
}

のように、 T があるトレイトを実装しているときだけ実装を切り替えるということができる。(実際にはトレイト実装か固有実装を経由しないと特殊化できないので、もう少しコードを書く必要がある)

RFC0769時点では、このパラメトリシティを用いて「マーカートレイトのみを持つ型パラメーター」には自動的に #[may_dangle] が仮定される仕様だった。

RFC0769より前はどうだったか

RFC0769より前は、drop checkerはなかった。つまり現在でいうところの user_drop_lifetimes(T) = {} が仮定されていた。

これを保証するため、ジェネリクスパラメーターを持つ Drop は全てunsafeで、 #[unsafe_destructor] が必要だった。これがRFC0769の "Sound Generic Drop" という名称の由来である。

まとめ

Drop Checkerの規則について、 #[may_dangle] の意味を含めてまとめてみた。Drop で変な処理をするunsafeなコードを書くときはこの点を理解しておくとunsoundnessを踏み抜きにくくなると思われる。

SSHのホスト鍵設定

ホスト鍵とは

SSHの鍵はデジタル署名用の秘密鍵であり、本人確認に使われる。いわゆるid_rsaは、ユーザー側の本人確認のために使われる。

一方、SSHサーバー側も専用の秘密鍵を所有している。これは /etc/ssh/ssh_host_{dsa,ecdsa,ed25519,rsa}_key のような場所に保管されている。SSH接続の際には、これを使った公開鍵認証も行われる。クライアント側の .ssh/known_hosts と照らし合わせてチェックする。

ホスト鍵がないと何が問題か

もし悪意ある第三者が通信を盗聴・改竄できる場合、偽のサーバーと通信させることができてしまう。すると、適切な暗号を用いて全くの別人と会話しているという本末転倒な状態になる。偽のサーバー上と気付かずにsudoパスワードを入れたら困ったことになるかもしれない。

HashKnownHostsをオフにする

筆者は、ホスト鍵を安全に運用するために、HashKnownHostsオフにするべきだと考えている。

そもそも HashKnownHosts とは、 .ssh/known_hosts においてホスト名をハッシュ化して保存するオプションである。ハッシュ化をしない場合、 known_hosts の各行は以下のようになっている。

example.com ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHayNTYAAAAIbmlzdHAyNTYAAABBBAHOh5LY0tU5hZGZn4iFvUQ9EJSGW7n9KbTXj5WK5AEIQNB5ShhNPwJcXqtc5hxwEmBX2VSdjUFkIT6U2Otur7w=

HashKnownHosts を使うと、「ホスト名またはIPアドレス」「署名方式」「公開鍵」のうち、「ホスト名またはIPアドレス」の部分がハッシュ化され、

|1|tbdGjw+HE9Clw2hC7ezBLOMGFGI=|xOtpgqDyfDlT/PB7cYm442R1+zY= ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHayNTYAAAAIbmlzdHAyNTYAAABBBAHOh5LY0tU5hZGZn4iFvUQ9EJSGW7n9KbTXj5WK5AEIQNB5ShhNPwJcXqtc5hxwEmBX2VSdjUFkIT6U2Otur7w=

のようになる(|1|ソルト|ハッシュ|)。ハッシュ化することで、

  • 特定のホスト名が、この行に該当するかどうかは判定できる。
  • しかし、この行だけ見て、ホスト名を復元することは困難である。

となる。つまり、

  • HashKnownHostsメリット: known_hosts が漏洩しても、接続先ホストの情報が復元できない。
  • HashKnownHostsデメリット: known_hosts の管理が困難になる。どのホストを信任しているかわからないため、偽のホストを信頼してしまう危険性が増える。

と考えられる。接続先ホストの情報は仮に漏れても大きな影響はなさそうだし、むしろ known_hosts が漏洩するような状況では秘密鍵など他の重要な情報も漏れている状況だから、メリットがデメリットに釣り合わないと思う。

known_hosts を管理する

ここでは、ホスト名のハッシュ化を止めた上で、 known_hosts をきちんと管理することを考えたい。前述のとおり、 known_hosts の基本フォーマットは

ホスト名またはIPアドレス 署名方式 公開鍵 (コメント)

である。また、 # で始まる行もコメントである。

「ホスト名またはIPアドレス」の部分の詳細なフォーマットは以下の通り。

  • 基本的には、 gitlab.com とか 52.167.219.168 のようにホスト名またはIPアドレスがそのまま使える。
  • 22番以外のポートのときは、 [example.com]:60022 とか [192.0.2.23]:60022 のように[]づけで表記する。
  • , で複数のホスト名またはIPアドレスを並べることができる。ホスト名とIPアドレスを並べてもよい。 (ハッシュ化していないときのみ)
  • * は0文字以上のワイルドカードとして使える。 (ハッシュ化していないときのみ)
  • ? は1文字のワイルドカードとして使える。 (ハッシュ化していないときのみ)

例えば、GitHubとGitLabのための known_hosts は以下のように書ける。

# GitHub -- marked CheckHostIP no
github.com ssh-rsa AAAAB3NzaC1yc2EAAAABIwAAAQEAq2A7hRGmdnm9tUDbO9IDSwBK6TbQa+PXYPCPy6rbTrTtw7PHkccKrpp0yVhp5HdEIcKr6pLlVDBfOLX9QUsyCOV0wzfjIJNlGEYsdlLJizHhbn2mUjvSAHQqZETYP81eFzLQNnPHt4EVVUh7VfDESU84KezmD5QlWpXLmvU31/yMf+Se8xhHTvKSCZIFImWwoG6mbUoWf9nzpIoaSjB+weqqUUmpaaasXVal72J+UX2B+2RPW3RcT0eOzQgqlJL3RKrTJvdsjE3JEAvGq3lGHSZXy28G3skua2SmVi/w4yCE6gbODqnTWlg7+wC604ydGXA8VJiS5ap43JXiUFFAaQ==

# GitLab
gitlab.com,52.167.219.168 ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHAyNTYAAAAIbmlzdHAyNTYAAABBBFSMqzJeV9rUzU4kWitGjeR4PWSa29SPqJ1fVkhtj3Hw9xjLVXVYrU9QlYWrOLXBpQ6KWjbjTDTdDkoohFzgbEY=
gitlab.com,52.167.219.168 ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQCsj2bNKTBSpIYDEGk9KxsGh3mySTRgMtXL583qmBpzeQ+jqCMRgBqB98u3z++J1sKlXHWfM9dyhSevkMwSbhoR8XIq/U0tCNyokEi/ueaBMCvbcTHhO7FcwzY92WK4Yt0aGROY5qX2UKSeOvuP4D6TPqKF1onrSzH9bx9XUf2lEdWT/ia1NEKjunUqu1xOB/StKDHMoX4/OKyIzuS0q/T1zOATthvasJFoPrAjkohTyaDUz2LN5JoH839hViyEG82yB+MjcFV5MU3N1l1QL3cVUCh93xSaua1N85qivl+siMkPGbO5xR/En4iEY6K2XPASUEMaieWVNTRCtJ4S8H+9
gitlab.com,52.167.219.168 ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIAfuCHKVTjquxvt6CM6tdG4SLp1Btn/nOeHHE5UOzRdf

CheckHostIP をオフにする

ホスト鍵は基本的に、接続しようとしたDNS名と照合される。しかし、 CheckHostIP が有効の場合、IPアドレスに対しても照合が行われる。

普通、DNSの対応付けが変わっていても、接続先のサーバーが想定通りのホスト鍵を返せば信頼してもよいはずなので、 CheckHostIP は予防的な意味合いが強いと思われる。特に、GitHubのようにDNSラウンドロビンを使っている場合は面倒なので、上記のワイルドカードを使うか、そもそも CheckHostIP を外してしまうのがよいと思う。 (GitHubのIPアドレス一覧)

StrictHostKeyChecking の有効化

想定していないホスト鍵が送られてきたとき、SSHは以下のように振る舞う。

  • 別のホスト鍵を既に知っている場合、問答無用で接続拒否になる。オレオレ詐欺で言うところの「母ちゃん俺だよ、携帯番号変えたからさ」というやつである。どうしても接続するならknown_hostsを手動かコマンドでいじる必要がある。
  • 未知のホストの場合
    • StrictHostKeyChecking yes の場合: 接続拒否する。
    • StrictHostKeyChecking no の場合: known_hostsに追加して続行する。
    • StrictHostKeyChecking ask の場合(デフォルト): ユーザーの答えに応じて上のどちらかの処理をする。

.ssh/config に入っているホストにしか接続しないような生活であれば、どれもそれほど変わらないと思う。筆者は StrictHostKeyChecking yes にしておき、新規ホストを追加したとき、そのホストに対して一時的に StrictHostKeyChecking ask を付与している。

EC2への対処

EC2のように、同じIPアドレスのマシンを消したりまた立ち上げたりしていると、既知のホスト鍵との衝突でどうしても接続拒否になってしまう。せっかく known_hosts をちゃんと管理しているので、テキストエディタで消してしまうとよいと思うが、ホスト鍵のチェックを強制的に省略する方法もあるにはある

UpdateHostKeys の有効化

UpdateHostKeys ask とすると、ホスト鍵が更新されたときに、新しいホスト鍵を known_hosts に追加することができる。(以前のホスト鍵で認証したあとで送られてくるので、問題はない。) サーバー側をうまく設定すれば、キーローテーションをすることもできる。

まとめと宣伝

known_hosts はちゃんと管理することもできる。ちなみに known_hostsauthorized_keys を正しくハイライトするVimプラグインを作ったのでぜひ。

WSL+Xming環境整備

WSLとXmingを組み合わせていい感じに環境整備できてきたので記録をとる。

WSLとXmingについて

  • WSLはWindows上でLinuxのプロセスを実行する機能である。互換性は完全ではないが、多くのソフトウェアが動くようになっている。ただし、そのままではGUIは動かない。
  • XmingWindows上で動作するXサーバーのうちの一つ (Cygwin/Xの派生) である。XはLinuxで使えるGUIの仕組みで、画面側がXサーバー、アプリ側がXクライアントとなってTCP経由で接続できるという特徴がある。ここではWSL側をクライアントにしてXmingに繋ぐことで、GUIを使えるようにする。

Xming最新版の取得

Xmingの最新版のビルドを入手するには£10.00程度の寄付が必要である。多くの人は2007年(!!!)のバージョンを使っている。そういうわけなので巷の評判は気にせず最新版を入手するといいと思う。 (たとえば、勝手に英語キーボード設定になる問題には今のところ遭遇していない)

同ページの寄付に関するセクションに詳しい説明がある。以下は勝手に翻訳したもの

寄付をすると、ドナーパスワードがメールで送られます。それを使うことで、XmingのWebリリース版と開発スナップショット版を個人利用のために取得することができます。パスワードは、PayPalの支払い履歴に記載されているメールアドレスに対して送られます。そのため、支払いメールアドレスが有効なメールアドレスであることと、私のISPのメールサーバー ([WWW]zen.co.uk 、例えば smarthost01.mail.zen.net.uk) をブロックしていないことを確認しておいてください。寄付以外の方法(コードやパッチなど)で貢献をした場合や、パスワードが送られてこない場合は、私に連絡をしてください。また、PayPalを使えず、代替手段が必要な場合も、私にメール (訳注: ここにメールアドレスが書いてあります) で連絡をしてください。寄付金額として10ポンドを提案していますが、これより低い金額だと手数料の割合が高くなってしまうからです。注意: 上のボタンを経由してPayPalで支払いをする場合、PayPalのアカウントは必要ありませんが、クッキーを有効にする必要があります。

寄付はPayPal経由と書いてあるが、PayPalは日本からの寄付を許可していない(おそらく法的な理由)。その場合は上にあるように作者にメールをするとよい。以下は筆者の送ったメールの例

Subject: Want to donate from Japan

Text:

I want to donate to Xming from Japan, from which I can’t donate money via PayPal due to legal reasons. Could you offer alternatives if any?

Masaki Hara

すると代替手段を教えてもらえる。筆者は、作者からPayPalの支払いリンクを送ってもらう方法(日本から寄付はできないが、支払いはできる)を選んだ。

Subject: Re: Re: Want to donate from Japan

Text:

Thank you! Can I receive a payment link then?

しばらくするとPayPalの支払いリンクを送ってもらえるので、それに対して£10.00支払うと、パスワードが送られてくる。

Xmingのインストール

今回はWSLから呼び出す形での利用のみを想定しているのでPuTTY連携は考えない。そのため以下の2つをインストールする。

Xming-fontsはXming-x64のあとにインストールする。逆順にすると C:\Program Files (x86)\Xming にインストールしようとしてしまう。

ちなみにこのXming-fontsだが、ほぼEmacs用である。GTKやQtなどで作られているGUIアプリはクライアント側(Linux側)のフォントを参照するからである。

Xmingの起動

はじめはXming Launchなどを使って起動してみるとよいが、オプションがわかってしまったあとはショートカットを作るほうが楽だ。

"C:\Program Files\Xming\Xming.exe" :0 -clipboard -multiwindow -xkbmodel jp106 -xkblayout jp -dpi auto -wgl へのショートカットを作成した。

  • :0 は画面の番号で、これに6000を足したTCPポートで通信が行われる。
  • -clipboard によりWindows側のクリップボードと共有する。
  • -multiwindowXmingのモードの一つで、Linux側のウインドウ1個がWindows側のウインドウ1個に対応する。
  • -xkbmodel jp106 -xkblayout jp は日本語キーボード配列を指定している。
  • -dpi autoWindows側のDPIを継承する。筆者のコンピューターはNew Surface Proで、高DPI環境だが、この設定だけでかなりうまく設定される。
  • -wglOpenGLアクセラレーションを有効化する。

WSLの設定 (Ubuntuのインストール)

Bash on Ubuntu on Windowsをインストールしてみよう! - Qiita」に従ってWSLを設定した。WSLの上では他のディストリビューションも動かせるが、ここではUbuntuを仮定する。

Xfce4のインストール

bash.exeを起動して xfce4-sesson, xfce4-goodies, gnome-keyring, fonts-vlgothic, fcitx-skk をインストールした。 (ここで日本語フォントを入れておかないと、Xming-fontの有無に関係なく日本語が化けて困ることになる)

起動スクリプトの作成

以下のような内容のスクリプトを /home/qnighy/Xming.sh に置いた。

#!/bin/bash

# ホームから開始したいので
cd
# パーミッション777のファイルが量産されると困るので
umask 0022
# localhost:0.0の略で、これでXmingに繋がることになる
export DISPLAY=:0.0
# 必ずXming経由でOpenGLを使う
export LIBGL_ALWAYS_INDIRECT=1

# gnome-keyringをスタート (SSH鍵を覚えさせたいので)
eval $(gnome-keyring-daemon --start --components=pkcs11,secrets,ssh)
export GNOME_KEYRING_CONTROL SSH_AUTH_SOCK

# インプットメソッドの設定 (fcitxの場合)
IM=fcitx
export XMODIFIERS="@im=$IM"
export GTK_IM_MODULE=$IM
export QT_IM_MODULE=$IM
export NO_AT_BRIDGE=1
# 全角/半角キーが連打される例のやつを防ぐ
xset -r 49
# fcitxを起動
fcitx

# SHLVLを0に下げてからターミナルを起動
SHLVL=0 xfce4-terminal

bash.exe -l /home/qnighy/xming.sh のように実行するとターミナルが出てくる。やっほい

ショートカットの作成

bash.exeを黙らせたいので、無言で実行するためのユーティリティーを導入する。

The Run utilityからrun-x64.zipをダウンロードして、中にあるrun.exeC:\Windows\System32\にコピーする。 (Xmingの作者が作っている模様)

その後、 C:\Windows\System32\run.exe C:\Windows\System32\bash.exe -l /home/qnighy/xming.sh に対してショートカットを作成する。

アイコンをいい感じにする

Xmingの作るウインドウは、極力Linux側のアイコンを反映するが、上手くいかないことがある。特にxfce4-terminalは上手くいかなかったので、手動で設定する。

まず imagemagick を入れて、以下のようにしてicoファイルを作成する。

convert /usr/share/icons/elementary-xfce/apps/*/xfce-terminal.png xfce-terminal.ico

同じ方法で色々なアイコンをicoに変換できる。

作ったicoWindows側に置く。まずショートカットが不恰好なのでショートカットのアイコンに設定する。

続いてXmingrcをいじる。Xmingrcのデフォルト設定は C:\Program Files\Xming\Xmingrc にあるので、これを C:\Users\qnighy\Xmingrc にコピーする。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    &Usage execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    "Host &Finder" finder
    separator
}
RootMenu apps
SilentExit
Debug "Using the default Xmingrc configuration file."

これを弄って以下のようにした。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    "&Usage" execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    separator
}
RootMenu apps
SilentExit
Icons {
    # アイコンを上書き
    xfce4-terminal C:\Users\qnighy\xfce-terminal.ico
}

こうするとウインドウクラスかウインドウ名がxfce4-terminalであるようなウインドウには、指定したアイコンを使うようになる (Xmingrcの説明も参照)

ところで、ウインドウクラスを調べるには xprop コマンドを使う。 xprop を実行したあと、調べたいウインドウをクリックすると、以下のように色々な属性が表示される。

$ xprop
_NET_WM_STATE(ATOM) = 
_NET_WM_USER_TIME(CARDINAL) = 3901640
_WINDOWSWM_NATIVE_HWND(INTEGER) = 328280, 0
WM_STATE(WM_STATE):
        window state: Normal
        icon window: 0x0
WM_HINTS(WM_HINTS):
        Client accepts input or input focus: True
        Initial state is Normal State.
        window id # of group leader: 0xe00001
XdndAware(ATOM) = BITMAP
_MOTIF_DRAG_RECEIVER_INFO(_MOTIF_DRAG_RECEIVER_INFO) = 0x6c, 0x0, 0x5, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x10, 0x0, 0x0, 0x0
WM_WINDOW_ROLE(STRING) = "xfce4-terminal-1506224785--565597661"
_NET_WM_SYNC_REQUEST_COUNTER(CARDINAL) = 14680070
_NET_WM_WINDOW_TYPE(ATOM) = _NET_WM_WINDOW_TYPE_NORMAL
_NET_WM_USER_TIME_WINDOW(WINDOW): window id # 0xe00005
WM_CLIENT_LEADER(WINDOW): window id # 0xe00001
_NET_WM_PID(CARDINAL) = 20
WM_LOCALE_NAME(STRING) = "ja_JP.UTF-8"
WM_CLIENT_MACHINE(STRING) = "qnighy-chris"
WM_NORMAL_HINTS(WM_SIZE_HINTS):
        user specified size: 362 by 0
        program specified minimum size: 93 by 116
        program specified resize increment: 19 by 38
        program specified base size: 17 by 40
        window gravity: NorthWest
WM_PROTOCOLS(ATOM): protocols  WM_DELETE_WINDOW, WM_TAKE_FOCUS, _NET_WM_PING, _NET_WM_SYNC_REQUEST
WM_CLASS(STRING) = "xfce4-terminal", "Xfce4-terminal"
WM_ICON_NAME(STRING) = "Terminal - xprop"
_NET_WM_ICON_NAME(UTF8_STRING) = "Terminal - xprop"
WM_NAME(STRING) = "Terminal - xprop"
_NET_WM_NAME(UTF8_STRING) = "Terminal - xprop"

このうち WM_CLASS と書かれているものがウインドウクラスにあたる。はじめから xprop | grep WM_CLASS とやると楽かもしれない。

困っていること

  • dbusがうまく動かない。redditとかに色々書いてあるけど手元ではまだ動いていない。
  • OpenGLで複雑なことをしようとすると厳しい。なぜかGLSLのコンパイルが通らない。
  • 他にも変なシステムコールは通らないので、そういうことをやるときは仮想マシンを立ち上げる。

古いRubyをビルドする

動機

現時点でRubyの最新版は2.4, サポートされているのは2.2までで、2.1以前はメンテナンス対象外である。そのような古いバージョンを動かすのは決してよいことではない。

しかし実のところ、現在でも多くのWindowsマシンで、Ruby1.8.1とRuby1.9.2p0が動作している。具体的には、RPGツクールXP, RPGツクールVXというソフトウェアで作られたゲームはRuby1.8.1の処理系とともに配布されており、RPGツクールVX Aceというソフトウェアで作られたゲームはRuby1.9.2p0の処理系とともに配布されている。既に多くのゲームが世に送り出されているのみならず、これらのいずれのツールも、未だにそれぞれ根強い人気があり、今でも多くの名作が作られている。「ふりーむ」というサイトで「RPGツクール XP」と検索した結果からも、その人気を伺い知ることができる。

そういった事情から筆者はRuby1.8.1とRuby1.9.2p0に強い興味があり、ビルドを試みたところ、いくつかの問題があった。

前提

とりあえず、Ubuntu 16.04 x86_64でのビルドを想定している。アーキテクチャを拡大すれば、より多くの問題が顕在化するかもしれない。

Ruby1.9.2p0の問題

Ruby1.9.2p0を現代の環境でビルドすると、以下の問題があった。

  • 継続・コルーチン処理が最適化で壊れる
  • bisonでコンパイルエラーになる

継続・コルーチン処理が最適化で壊れる

Fiberやcall/ccの処理はスタックのコピーによって実現されているが、コンパイラによってはspレジスタの最適化によりこの処理が壊れてしまい、処理系がサイレントに死ぬことがある。これはr34278をbackportすることで解決できた。

bisonでコンパイルエラーになる

pure-parser周りの仕様変更により新しめのbisonでコンパイルできない。これはr42282をbackportすることで解決できた。

Ruby1.8.1の問題

Ruby1.8.1を現代の環境でビルドすると、以下の問題があった。

  • group_memberの衝突
  • bisonとの組み合わせでGCが壊れる
  • autoconf2.6x系列でビルドできない

group_memberの衝突

file.cで定義されているgroup_memberと、Cライブラリのgroup_memberが衝突する。これはgroup_memberrb_group_memberにリネームすることで解決できた。歴史的にはこの変更はr13240r26682の組み合わせといえる。

bisonとの組み合わせでGCが壊れる

ある程度新しいbisonはLRのセマンティックバリューのスタックをヒープで管理することがあるが、この場合Ruby1.8.1だとヒープ上のセマンティックバリューのマーク漏れが発生する。ノードのnd_fileが汚染された結果、次のGCのタイミングでGCのフリーノードの直前のRVALUEの最後の1バイトが破壊され、その1バイトがノードからのポインタになっていた場合に領域外参照でサイレントに死ぬ。これはr9355, r9405, r9416, r9382, r9639をbackportすることで解決できた。

autoconf2.6x系列でビルドできない

いくつかの複合的な問題からautoconf2.6系列でビルドできない。これはr10189の一部、r10392r11594をbackportして、srcdirの解釈を正しくするよう少し改造を加えることで解決できた。

成果物

現時点での成果物をqnighy/ruby-1.9.2p0qnighy/ruby-1.8.1に置いてある。

Rust-proofを使ってみる

概要: Rust-proofはElectrolysisと同様にRustプログラムから検証条件を抽出するが、LeanではなくSMTソルバであるZ3向けの検証条件を出力する。こちらも開発が放棄されているように見えるが現在もビルド可能である。

準備

テスト用リポジトリを準備する

$ cargo new rustproof-test
$ cd rustproof-test

該当のnightlyバージョンを取得する (Electrolysisと同様、Rust-proofもコンパイラプラグインのため、特定のnightlyバージョンに強く依存している)

$ rustup override set nightly-2016-08-12

Z3をインストール

$ sudo apt install z3

使ってみる

Cargo.toml に以下の依存関係を書く

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git", rev = "654b004" }

src/lib.rs に以下のように関数を書く。これはEXAMPLESに掲載されているものとほぼ同様だが、5:i32のような型つきリテラル5i32に置き換えてある。

// feature(plugin) を有効化してrustproofをロード
#![feature(plugin)]
#![plugin(rustproof)]

// #[condition] によりコンパイル時にrustproofによるチェックが走る

#[condition(pre="(x:i32 <= i32::MAX - 5i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="(x:i32 <= i32::MAX - 4i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five_invalid(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="true", post="(x:bool==true IMPLIES return:bool==false) && (x:bool==false IMPLIES return:bool==true)")]
pub fn boolean_not(x:bool) -> bool {
    if x == true {
        false
    } else {
        true
    }
}

検証を実行するには単にコンパイラを起動すればよい。

$ cargo build
   Compiling rustproof-test v0.1.0

fn add_five(..) Verification Condition is valid.


fn boolean_not(..)  Verification Condition is valid.


fn add_five_invalid(..) Verification Condition is not valid.

(model 
  (define-fun x () (_ BitVec 32)
    #x7ffffffb)
)

    Finished debug [unoptimized + debuginfo] target(s) in 42.84 secs

まとめ

大変よい試みだが、古すぎるのが残念だと思う。rust-proofが開発された経緯は不明だが、documentsというディレクトリに不穏な資料が残されているので見てみると面白いかもしれない。

Electrolysisを使ってみた

概要: ElectrolysisはRustの検証条件をLEANに出力するプロジェクトである。これを使ってみた。

Electrolysisとは

Electrolysis (electrolysis: 電解) はSebastian Ullrich氏の修士研究で開発されたプロジェクトで、Rustプログラムの正当性や計算量に関する検証条件をLean Theorem Proverの命題として出力する機能を提供する。

なお、GitHubの様子だと、このプロジェクトは修論の日付からほぼ開発がストップしているようだ。Ullrich氏はその後、Electrolysisの成果の一部をLEANに還元するなどの活動をしているようだ。

Electrolysisの実行

以下、Ubuntu 16.04を仮定する。

ElectrolysisはRustのコンパイラプラグインとして実装されているため、Rustの特定のnightlyバージョンに強く依存している。また、libcore自体を検証ターゲットにしているため、Rustコンパイラソースコード自体も取得する必要がある。

$ git clone https://github.com/Kha/electrolysis.git
$ cd electrolysis
$ rustup override add $(cat rust-nightly-version)
$ rustup component add rust-src
$ cargo run core
$ cargo run alloc
$ cargo run collections
$ cargo run fixedbitset

petgraphに対する検証条件の出力

petgraphに対する検証条件の出力はやや面倒である。まずpetgraphを取得してビルドする。

$ git submodule update --init
$ cd thys/petgraph/src
$ cargo build
$ cd ../../..

次に thys/petgraph/config.toml を編集して、libfixedbitsetのrlibのハッシュを適切に置き換える。例えば、

rustc_args = "thys/petgraph/src/src/lib.rs --crate-name petgraph --crate-type lib -L dependency=thys/petgraph/src/target/debug/deps --extern fixedbitset=thys/petgraph/src/target/debug/deps/libfixedbitset-0ba3fe99bd419295.rlib"

targets = [
  "algo.scc",
]

とすると以下が通る。

$ cargo run petgraph

Lean2のビルド

Leanは現在、過去の証明との互換性のために残されている0.2.0系列と、最新の3.0.0系列がある。Electrolysisに適しているのは0.2.0系列なので、そちらを使う。

また、lean2のビルドスクリプトにはninjaを取得する部分があるが、ninjaの取得先が削除されてしまっているので、以下のパッチを当てる必要がある。(以下これをlinja.patchと呼ぶ)

diff --git a/bin/linja.in b/bin/linja.in
index 926f33e..10ee37d 100755
--- a/bin/linja.in
+++ b/bin/linja.in
@@ -239,7 +239,7 @@ def show_download_progress(*data):
     log_nonewline("Download: size\t= %i kb, packet: %i/%i" % (file_size, downloaded_packets, total_packets+1))
 
 def get_ninja_url():
-    prefix = "https://leanprover.github.io/bin/"
+    prefix = "https://github.com/leanprover/leanprover.github.io/raw/8fb36e926a3c4df8b84bfafedb7f39687f24b93b/bin/"
     if platform.architecture()[0] == "64bit":
         if platform.system() == "Linux":
             return prefix + "ninja-1.5.1-linux-x86_64"
$ sudo apt install python3 git libgmp-dev libmpfr-dev
$ git clone https://github.com/leanprover/lean2.git
$ cd lean2
$ patch -p1 < path/to/linja.patch
$ mkdir -p build/release
$ cd build/release
$ cmake -DCMAKE_BUILD_TYPE=Release ../../src
$ make -j4 install DESTDIR=.

上の例ではDESTDIR=.を指定することで./usr/localにインストールしているが、これを外せば/usr/localにインストールされる。

検証条件に対するLEAN2の実行

lean2にはlean3のような--makeオプションがついていない。以下のようなMakefilethysの直下に置くとよい。(LEANDIRを適切に変更する)

#!/usr/bin/make -f

LEANDIR = /somewhere/lean2/build/release/usr/local
LEAN = $(LEANDIR)/bin/lean

LEAN_SOURCES = $(shell find . -name '*.lean')
LEAN_BINARIES = $(LEAN_SOURCES:.lean=.olean)
LEAN_DEPFILES = $(LEAN_SOURCES:.lean=.d)

all:
  $(MAKE) deps
  $(MAKE) all2

deps: $(LEAN_DEPFILES)

all2: $(LEAN_BINARIES)

clean:
  $(RM) $(LEAN_DEPFILES) $(LEAN_BINARIES)

.PHONY: all deps all2 clean

%.d: %.lean
  (echo $<:; $(LEAN) --deps $<) | tr '\n' ' ' > $@

%.olean: %.lean
  $(LEAN) $< -o $@

-include $(LEAN_DEPFILES)

これを配置した上で thys 直下で make を実行すると、証明がコンパイルされる。

まとめと感想

Electrolysisの機能を一通り動かすことができた。

実は別のRustバージョンや別のLeanバージョンで動かせないか検討したがかなり困難であることがわかった。

Rustの検証プロジェクトではむしろRustBeltが有名で、メンバーから考えてもかなり期待が持てる。RustBeltとElectrolysisは以下のように異なる。

  • 検証の目的: RustBeltはunsafeな動作を含むより低レベルな操作に対し、UBを踏まないなどの証明をターゲットにしている。Electrolysisはより高級な変換で、アルゴリズムの正当性や計算量の検証を目指している。
  • ロジック: RustBeltは高階並行分離論理フレームワークIrisに立脚している。
  • 証明支援系: RustBeltはCoqで検証する。ElectrolysisはLeanで検証する。
  • 検証条件の抽出: Electrolysisは実際のRustコード(MIR)からの抽出に対応している。RustBeltは今のところMIRからの抽出には対応していない(Coq側の対応するコードは手動で書かれている)が、Ralf Jung氏が最近MIRの改造に取り組んでいるところから見るに、そのうち対応すると思われる。