Drop Checkerの規則をちゃんと理解する
概要: Drop CheckerはRustのボローチェッカに付属する追加の検査器で、コンパイラが自動で挿入するdrop処理の安全性を保証するためのものである。これの詳細な規則とその正当性を理解したかったので自分なりに整理した。
dropckの概要についてはRustonomiconの説明とか以前の記事とかを参照。
注意: 本記事の内容はコンパイラの実装との対応をとっていないので実際の実装とは異なる可能性がある。
規格
用語
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>
は以下の手順で定義される。
Drop::drop()
が触れうるライフタイムの列挙
例として、 Foo<'a, 'b, T, U>
という型を考える。この Drop::drop()
が触れうるライフタイムの一覧を、以下のように保守的に列挙する。
Foo
が Drop
を実装していない場合
Drop
で何もしないことがはっきりわかるので、どのライフタイムも必要ではない。
user_drop_lifetimes(Foo<'a, 'b, T, U>) = {}
Foo
が Drop
を実装している場合
保守的に、全てのパラメーターのライフタイムを仮定する。
user_drop_lifetimes(Foo<'a, 'b, T, U>) = {'a, 'b} ∪ {Tの全てのライフタイム} ∪ {Uの全てのライフタイム}
Foo
の Drop
実装が #[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>()
が呼び出されうる」という関係を近似したものである。例えば、 struct
や enum
の drop_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>(ポインタ); ... } }
ポイントとして、 Rc
の Drop
実装は 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)
の有効性のみを仮定できる。
と書かなかったのはそのためである。
なお、 Rc
で PhantomData<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つの違いは、
T
のdrop_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) { .. }
のような関数があったときに、 foo
が x
に対してできることは限られている (具体的には drop
するか forget
するくらいしかない) という仮定である。
この仮定が成立する理由は、 foo
が x
に関して、 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_hosts
と authorized_keys
を正しくハイライトするVimプラグインを作ったのでぜひ。
再帰的余代数について
最近、再帰的余代数という概念について少し勉強したので、証明をまとめてPDFにした。
動機など細かいところには触れられていないが、以下のことが証明されている。
WSL+Xming環境整備
WSLとXmingを組み合わせていい感じに環境整備できてきたので記録をとる。
WSLとXmingについて
- WSLはWindows上でLinuxのプロセスを実行する機能である。互換性は完全ではないが、多くのソフトウェアが動くようになっている。ただし、そのままではGUIは動かない。
- XmingはWindows上で動作する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側のクリップボードと共有する。-multiwindow
はXmingのモードの一つで、Linux側のウインドウ1個がWindows側のウインドウ1個に対応する。-xkbmodel jp106
-xkblayout jp
は日本語キーボード配列を指定している。-dpi auto
でWindows側のDPIを継承する。筆者のコンピューターはNew Surface Proで、高DPI環境だが、この設定だけでかなりうまく設定される。-wgl
でOpenGLのアクセラレーションを有効化する。
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.exe
をC:\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に変換できる。
作ったicoをWindows側に置く。まずショートカットが不恰好なのでショートカットのアイコンに設定する。
続いて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
とやると楽かもしれない。
困っていること
古い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_member
をrb_group_member
にリネームすることで解決できた。歴史的にはこの変更はr13240とr26682の組み合わせといえる。
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の一部、r10392、r11594をbackportして、srcdir
の解釈を正しくするよう少し改造を加えることで解決できた。
成果物
現時点での成果物をqnighy/ruby-1.9.2p0とqnighy/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
オプションがついていない。以下のようなMakefileをthys
の直下に置くとよい。(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の改造に取り組んでいるところから見るに、そのうち対応すると思われる。