星にゃーんのブログ

ほとんど無害。

星にゃーん2019

日記

今年の星にゃーんまとめです。だいたいベッドの上でゴロゴロしていました。 これを書くために今年の星にゃーんのツイートを全部読みました。

1月

仮面ライダー平成ジェネレーションズFOREVERを観る。 「仮面ライダーはフィクションの存在だった」から始まる平成ライダー讃歌。マジで良かった。終始アタルに感情移入して観ていたのでエンドロールで最高になってしまった。みんなも観て。夏映画のOver Quartzerも良かったよ。

HUGっと!プリキュア最終回。 めちゃくちゃ良かった。これはみんなも観たので知っていますね。ラストシーンで描かれる未来がクライアス社のある未来よりも過去なのがいいよね。

2月

大学生活を謳歌する。旅行ってのは学会とかそういうのに行かせてもらったやつです。ありがとうございます。

膝枕に関する重要な発見をする。

3月

PPLに参加しました。これは会場のホテルで売っていたモナドです。

コウメイとマウンティングを取り合う。

サークルの飲み会でクズっぽい発言をする。

ちなみにオワってます。

4月

ちょっと元気になったのでC言語でスタックマシンのVMっぽいものを実装したりした。 本当はこれを拡張してmalgo(https://github.com/takoeight0821/malgo)のバックエンドを置き換えるつもりだったけど、メリットが少ないのと必要な実装の量を考えて断念した。 似たようなアイディアで12月にmalgoをアップデートします。

仮面ライダー平成ジェネレーションズFOREVERの公開からしばらく経ったので感想をツイートする。

母にTwitterアカウントがバレる。

5月

百合デーモンコア、はじめました。

Cコンパイラを作り始める。8月のセキュキャンでセルフホストを達成します。

これはマジでそうなんですよね。

6月

バックトゥーザフューチャー真実に気づく。一番好きな映画です。

グランドジオウの変身音が好きって話を一生している。

セキュキャンに通った。

このぐらいはコンパイルできるようになる。

Amazon Prime Videoが父の日に仮面ライダーアマゾンズを観よう！とか言ってたのでツッコむ

『君待秋ラは透きとおる』を読んだ。すごい良かった。

Cコンパイラ開発でこういうバグを踏みまくる。

『お嬢さん「現実逃避、しませんか？」』を思い出す。

グッド・オーメンズを観る。すごい良かった。

7月

Cコンパイラ開発しんどいポイント。

バイト。バイト探さないと。

これ何が元ネタですか？

たまにパンツの替えが切れるようになる。買って解決した。

『アステリズムに花束を』を読む。死。

SSっぽい文章を書く。もっと色々書きたいんですがなかなか書けない。

8月

仮面ライダージオウ Over Quartzerを観た。平成ジェネレーションズFOREVERは「仮面ライダーを愛してくれたあなたへ」だったけど、Over Quartzerは「これでも食らえ！ライダーキック！！じゃあ令和になってもよろしくな！」だった。どんなミラクルも起き放題　ユニバース・フェスティバル

fusetter.com

こういうバグり方をするんですよ。

セキュキャンに行った。

ハッピーシュガーライフ全巻を一時間で読破して人生をクリアする。

仮面ライダージオウが終わったので平成が終わった。

9月

大学のサークルでOSC広島2019にブース出展した。

スクールガールストライカーズをクリアする。エピソードⅠの真エンドを観るにはガチャから出るレアなコスチュームをこの5人の分すべて引く必要があり…つまりコンプガチャみたいなもんです。

10月

2019年10月11日の夜をポケ書で明かす。

『使い魔はスマートフォン』のことを思い出す。

ちょっとバズる。

11月

GraalVMで遊んだ。思ったより楽しかったのでmalgoの開発を再開した。やっぱり言語処理系書いてるときが一番楽しいね。

ポケットモンスターシールドをやった。

12月

こんなブログを書いた。GHCのRebindableSyntaxで悪さをして遊ぶ話です。

映画フラグタイムを観た。めちゃくちゃ良かった。

最悪

『なめらかな世界と、その敵』を読んだ。めちゃくちゃ良かった。

『ゼロ年代の臨界点』を読んだ。めちゃくちゃ良かった。

最高のクリスマスイブ

malgoに多相関数を実装した。

今年も色々ありました。来年も色々あるといいな。

RebindableSyntaxとGHC.Genericsを使って'genericなif'を作る

Haskell

CoqのGallinaでは2つのコンストラクタC1, C2のある型Tの式vについて、

if v then t1 else t2

が

match v with
| C1 ... => t1
| C2 ... => t2
end

にdesugarされる。

なんだかよくわからないけどかっこいい！！！Haskellでもこれやりたい！！！ やりました。

RebindableSyntaxとGHC.Generics

RebindableSyntaxを有効化すると、 リテラルやif式、do式などのセマンティクスを独自に定義することができる。 例えば、if e1 then e2 else e3はifThenElse e1 e2 e3に変換される。ifThenElseを定義すれば、if式の動作を自分の好きなように書き換えられる！

GHC.Genericsを使うと、データ型について総称的なプログラミングが行える。 詳細は 9.1. Language options — Glasgow Haskell Compiler 8.8.1 User's Guide を読むと良い。 日本語訳は http://www.kotha.net/ghcguide_ja/7.6.2/generic-programming.html 。

GIf型クラス

というわけでGHC.Genericsを用いて総称的な'if'を実装していく。 以下に出てくるコード例では、次のGHC拡張が有効化されていると仮定する: FlexibleContexts, PolyKinds, RebindableSyntax, TypeOperators, UndecidableInstances

最初に、型の総称表現がif式の第一項になれることを表すGIf型クラスと、if式の実装であるifThenElse関数を宣言する。

class GIf f where
  gIfThenElse :: f p -> b -> b -> b

ifThenElse :: (GIf (Rep a), Generic a) => a -> b -> b -> b
ifThenElse c = gIfThenElse (from c)

和型を表す(:+:)についてGIfのインスタンスを宣言する。 例えばdata Bool = False | Trueと宣言されているとき、|の左側にあるFalseがL1、右側にあるTrueがR1にあたる。

instance GIf (a :+: b) where
  gIfThenElse (L1 _) _ x = x
  gIfThenElse (R1 _) x _ = x

K1とM1についてもGIfのインスタンスを宣言する。 K1は中身をifThenElseに適用する。M1は中身をgIfThenElseに適用する。 このことはそれぞれの型から自明に分かる。

instance (GIf (Rep c), Generic c) => GIf (K1 i c) where
  gIfThenElse (K1 x) = ifThenElse x

instance GIf f => GIf (M1 i t f) where
  gIfThenElse (M1 x) = gIfThenElse x

これで総称的な'if'が手に入った。さっそくghciで試してみよう。

ghci> :set -XRebindableSyntax
ghci> if True then 1 else 2
1
ghci> if Nothing then 1 else 2
2
ghci> if Right 'a' then 1 else 2
1

やったーーー！！！ 一つしかコンストラクタのない型ではコンパイルエラーになってほしい。確かめてみよう。

ghci> if () then 1 else 2

<interactive>:5:1: error:
    • Could not deduce (GIf U1) arising from an if expression
      from the context: Num b
        bound by the inferred type of it :: Num b => b
        at <interactive>:5:1-19
    • In the expression: if () then 1 else 2
      In an equation for ‘it’: it = if () then 1 else 2

良さそう。 3つ以上コンストラクタがある型でもコンパイルエラーになってほしい。確かめてみよう。

ghci> :t EQ
EQ :: Ordering
ghci> if EQ then 1 else 2
1

うーん…… 原因を解明しよう。Rep Orderingは以下のような型になる。

type instance Rep Ordering
  = D1
      ('MetaData "Ordering" "GHC.Types" "ghc-prim" 'False)
      (C1 ('MetaCons "LT" 'PrefixI 'False) U1
       :+: (C1 ('MetaCons "EQ" 'PrefixI 'False) U1
            :+: C1 ('MetaCons "GT" 'PrefixI 'False) U1))

M1で付加されたメタ情報を取り除くと、U1 :+: (U1 :+: U1)になる。 つまり、3つ以上のコンストラクタを持つ型は「型と和型の和型」のような入れ子構造になっている。 3つ以上のコンストラクタを持つ型を弾くには、入れ子になった(:+:)を弾く必要がある。

NotSum型クラス

入れ子になった(:+:)を弾くために、まずは型の総称表現がa :+: bでないことを表す型クラスNotSumを次のように定義する。

class NotSum (f :: k -> Type)

instance NotSum V1
instance NotSum U1
instance NotSum (a :*: b)
instance NotSum (K1 i c)
instance NotSum f => NotSum (M1 i t f)

(:+:)を除く、型の総称表現に用いられる型すべてをNotSumのインスタンスにした。 続いて、GIf (a :+: b)に型制約NotSum bを追加する。

instance NotSum b => GIf (a :+: b) where
  gIfThenElse (L1 _) _ x = x
  gIfThenElse (R1 _) x _ = x

これでうまく動くようになったはずだ。ghciで確認してみよう。

ghci> if EQ then 1 else 2

<interactive>:2:1: error:
    • Could not deduce (NotSum
                          (C1 ('MetaCons "EQ" 'PrefixI 'False) U1
                           :+: C1 ('MetaCons "GT" 'PrefixI 'False) U1))
        arising from an if expression
      from the context: Num b
        bound by the inferred type of it :: Num b => b
        at <interactive>:2:1-19
    • In the expression: if EQ then 1 else 2
      In an equation for ‘it’: it = if EQ then 1 else 2
ghci> if True then 1 else 2
1
ghci> if Nothing then 1 else 2
2
ghci> if Right 'a' then 1 else 2
1

うれしーーーー！！！！

完成したコード

gist.github.com

セキュリティ・キャンプ全国大会2019でCコンパイラ書きました

日記 コンパイラ C

はじめに

2019年8月13日から5日間開催されたセキュリティ・キャンプ全国大会2019のCコンパイラ自作ゼミに参加しました。 この記事は、応募から修了までのレポートです。 ほとんど下書き状態ですが、ここから文章が改善される気がしないのでこのまま公開します。

セキュキャンでの進捗

3ヶ月ぐらいゴリゴリコードを書いて、セルフホストCコンパイラを実装した。switch-case文や#ifdef、可変長引数とかも実装している。 リポジトリは↓

github.com

これまでの星にゃーん

一昨年は言語自作ゼミ、去年はCコンパイラゼミに応募するも通らなかった。3度目の応募で合格。参加者の中では応募回数トップタイらしい。

今年の経緯

しばらく前から精神がオワってしまいひきこもり生活を送っている。ひきこもりながらもGHCのコードリーディングや自作コンパイラ開発をやっていたがスランプに陥る。 リハビリのために何かをやろうと考え、周りを見渡すと全人類Cコンパイラ書いとる。あ、書けるんだ、と思ったので書き始めた。 低レイヤを知りたい人のためのCコンパイラ作成入門やhttps://github.com/rui314/9ccを読んで勘が掴めたので手を動かすことに。

hikaliumさんに1分でリツイートされ後がなくなる星にゃーん.jpg

うかつな発言によりCコンパイラセルフホストRTAが始まってしまった。それっぽいものは簡単に書け、1週間でif文とかが動いた。3日でセルフホストはさすがに無理。再走者求む。

せっかくなので今年もCコンパイラ自作ゼミに応募してみることにした。体力面の不安が大きかったが、どうせ家に居ても死んでるので変わらないと判断。 通った。びっくり。通ったので元気が出た。単純ですね。

事前学習ではCコンパイラを書いた。週1でruiさんとhikaliumさんとのオンラインミーティングが設定された。参考になる資料や歴史の話が盛りだくさんで面白い話を毎回できた。コーディング自体はそんなに詰まることなくスムーズに進んだ。『低レベルプログラミング』と『BINARY HACKS』の知識がかなり役立った。コンパイラの開発自体はやったことがあるのも功を奏した。それでもバグりまくって常にウンウン唸ってましたが…

実装の話

3日でセルフホストと言ったので出来るだけ早くセルフホストしたい。しかし24時間ぶっ続けで書き続ける元気はないので、出来るだけ実装をサボることにした。よくあるコードを正しく解釈できればよいとして、コーナーケースへの対応は必要ない限り行わなかった。unsignedな値すらサポートしていない。意外とunsignedとsignedの区別を付けるのが面倒。

コード量が大きくなることは目に見えていたので、あえてあまり抽象化せず愚直に書くことにした。Cで短く簡潔なコードを書くのは不可能ではないが難しい。 愚直に書くといっても冗長に書くことは避けた。何事もバランスが大事。それなりに綺麗なコードが書けたんじゃないかと思う。

スタックのアライメントがバグりにバグりまくった。バグを直したと思っても数日後にまたバグが見つかる、みたいなのを繰り返した。アラインするコードがバグってるのでxmmレジスタが絡むとセグフォするが、浮動小数点数はコンパイラではほとんど使わないのでなかなかバグが発覚しない。根本の原因は剰余演算を算数レベルで勘違いしていたことだった。わり算むずかしすぎる。 スタックのサイズをコード生成時にグローバル変数で管理するようにしていたがこれもバグの温床だったので、最終的に実行時にrspを-16でandしてアラインすることで解決した。

トークンに位置情報を持たせてエラー出力をいい感じにした。該当コードはこのあたり。 エラー出力は下記のような見た目になる。モダンっぽい雰囲気がする良いエラー出力。

$ ./hoc examples/parse_error.c
error at (1, 11)

int main( {
          ^

) expected

これはruiさんに教えてもらった中でも特に印象的なコード。しかしincludeを実装したあたりでエラー出力がセグフォするように。単一ファイルしか扱わないからとファイル自体の情報をトークンに入れておらず、includeしたファイルでソースコード文字列を指すグローバルなポインタが書き換わってるのが原因だった。 #includeを使うとprint_lineが正しく動作しなくなるバグを修正 · takoeight0821/hoc_nyan@c1390ae · GitHub

バグ、特にセグフォ周りのバグはセグフォとは関係ない（スタックトレース上に現れない）コードが直接の原因であることが多かった。GDBで落ちてる箇所の検討をつけた後、関連するコードでprintfデバッグをしまくった。watchpointとかをうまく使えばもっと楽になると思う。 GDBはgdb-pedaが役立った。Day2に他の人が使ってるのを見て存在を思い出しインストールした。自作コンパイラのバグはスタックの異常として現れることが多かったので、スタックを自動でダンプしてくれるのが便利。もっとはやく存在を思い出したかった…

アセンブリにコメントで情報（コード生成時のノードとか）を埋め込んでおくとエスパーの助けになる。stderrへのデバッグ出力がコメントになるようにしておいて、stdoutにアセンブリを吐いて合わせて眺めると埋め込むより楽そう。早い段階で .loc を出力しておくようにするのも良いかもしれない。

セルフホストを達成した時のコミットは for(;;) への対応（ 継続条件が空のforが実行されないことがあるバグを修正 · takoeight0821/hoc_nyan@83f1db0 · GitHub）。 条件が空の時に不正な値を読んでた。

GASのintel syntaxだと、 lt や and のような名前をラベル名に使えないらしい。 invalid use of operatror lt のようなエラーメッセージが出る。 とりあえずソースコード内の lt や and とかを別の名前にリネームして問題を回避した。時間ができたらこのあたりを再度調べてまとめておきたい。

異常系テストは大事だと再認識した。「このファイルはパースに失敗する」みたいなのがちゃんと失敗することを確かめておくと、いろんなバグを早期発見できる。上に書いた #include のバグもパースエラー出力のテストで発覚した。

まとめ

同じような興味と高いスキルを持つ人たちに囲まれて、一つのタスクにひたすら取り組み続ける機会は学生のうちはなかなか得難い。 なかなかタフな5日間だったが、気分はかなり爽快で良いリフレッシュになったと感じている。 実装力に自信がついたし、普段の日常会話で相当なストレスを溜めていることを自覚することもできた。 人生が変わったとまでは言えないが、間違いなく良い影響を受けたと思う。

セキュキャン期間中は6時起床24時就寝、3食毎日食べる規則正しい生活を送っていた。 しかし家に帰った翌日は16時まで寝ていた。無事生活習慣が元に戻りました。この話はこれでオワリです。

夏

小説

暑さがまだ残る夏の夜、あなたは重い鞄を引きずりながら家に向かって歩いていた。 「今日は散々な一日だった」とあなたは思う。 明日が終われば夏休みだ。それだけが救いだとあなたは感じた。

連日の猛暑でただでさえ不快だというのに、クラスメイトの悪ふざけに巻き込まれて教師にこっぴどく叱られた。 あなたはただ近くにいただけだったが、夏バテした教師にはそれを見抜くだけの判断力が残っていなかった。 あなたにも教師の体調を察する余裕がなく、なぜ自分が叱られたのか分からなかった。

数学の小テストがさっぱり解けなかったのはきっと夏のせいだとあなたは思った。 窓の外でやかましく鳴くセミが気になり、あなたは問題に集中できなかった。 そもそも明後日から夏休みなのに小テストをするのが間違っている。 あなたは心のなかでそう愚痴った。

放課後、あなたはいつもどおり部活動に向かった。 クーラーの効いた図書室には誰も居ない。 他の部員はまっすぐ帰ったのだろう、とあなたは考える。 数分後、後輩が一人やってきた。 あなた達は短く他愛もない世間話を交わす。

あなたは日が暮れて涼しくなるのを待った。 静かな時が流れた。 あなたにとってその時間は今日一日で唯一有意義なひとときだった。

帰路の半分に達したころ、後ろから花火の音がした。 あなたは振り返ったが、花火は山に隠れて見えない。 あなたはここ数年打ち上げ花火を見ていないことに気づく。 数歩歩いて、部活にほとんど誰も来なかった理由も思い当たった。 夏祭りにしては少し早いな、とあなたは呟いた。

暑さがまだ残る夏の夜、あなたは重い鞄を引きずりながら家に向かって歩いていた。 「今日は悪くない一日だ」とあなたは思う。 明後日からが夏休みだ。それだけがあなたにとって救いだった。

夢

エッセイ

いつのまにか二十歳になっていた。 日曜の朝に起きるのは難しくなったが、代わりにテレビの録画は簡単になった。 昼過ぎに目を覚まし、アイスコーヒーを飲みながら予約録画した仮面ライダーを観る。 画面の向こうで戦ってるのは10年前の劇場版限定ライダーだ。ヒーローのくせに勇気が無くて、変身するたびにパンツを見て勇気を振り絞る変わった仮面ライダー。 その映画をちゃんと観たことはない。あらすじはネットで調べて、Amazonプライムビデオで飛ばし飛ばしに眺めた。

ずっと仮面ライダーを観続けてきた。でも、一つのシリーズを全話通して観たことは一度もない。 毎年いくらか見逃す。家のテレビに録画機能が付いてもそれは変わらなかった。 毎週観るほどの熱意はなく、習慣づくこともない。 だけど途切れ途切れに観続けた。各話のあらすじは公式サイトに書いてあるから、話に追いつけなくなることはない。

驚くべきことに、仮面ライダージオウは毎週欠かさず観ている。平成仮面ライダー最終作と銘打たれたジオウには、歴代の平成仮面ライダーが毎回出てくる。 タイムマシンに乗って歴史を変えるジオウを観ながら、記憶の中をタイムトラベルしている。 親戚の子どもと鎧武の話で盛り上がった大晦日。2回も観に行ったディケイドの冬映画。 ラウズカードをすべて揃えたクリスマス。初めて変身ベルトを腰に巻いた日。

初めて観た仮面ライダーはファイズだった。灰色の怪人は死から蘇った人間で、仲間を増やすために人間を殺す。 ファイズに変身する乾巧に憧れた。ぶっきらぼうなひねくれ者だけど、誰かのために身を投げ出せる勇気を持った青年だった。 乾巧には夢が無かった。彼は誰かの夢を守るために死と戦った。最後に彼は自分の夢を見つける。 僕もいつか夢を見つけるんだろうか。そう思いながら観ていた。

ジオウに変身する常磐ソウゴには王様になるという夢があるらしい。彼は夢を叶えるだろう。それだけの意志と力を感じる。 乾巧も最終回で自分の夢を語った。「世界中の洗濯物が真っ白になるみたいにみんなが幸せになりますように」 そう言って暖かな昼下がりの土手で眠りにつく。それがただの昼寝なのか、二度目の死なのかは分からない。 少なくとも、その夢はいつか叶うと思う。

いつのまにか二十歳になった人生に嫌気がさして、元気をすっかり無くしてしまった。 本当に嫌になったわけじゃない。ただ少し疲れたから、横になって昼寝したいだけだ。 結局、夢はまだ見つかっていない。夢を守る勇気も出そうにない。

仮面ライダーにはなれなかった。もしも本物の変身ベルトを手にしたら、たぶん悪の怪人になってしまうだろう。 幸いこの世界に変身ベルトはない。仮面ライダーにも怪人にもなれないなら、夢も勇気もなくったって人を殺すことはないだろう。

時々、勇気を振り絞る夢を見る。いつかそれを正夢にするのが夢なのかもしれない。 それが叶う日まで、仮面ライダーを観続ける。途切れ途切れに。たぶん。

Homebrewで他のformulaから依存されていないformulaを列挙する

覚え書き 技術メモ

brew listでインストール済みのすべてのformulaを列挙する。 xargs -P ...でそれぞれのformulaについて、そのformulaに依存しているインストール済みのformulaの数を数える。 grep " 0"で依存されていないformulaのみを取得する。

$ brew list | xargs -P 10 -IPACKAGE sh -c "brew uses --installed PACKAGE | wc -l | xargs echo PACKAGE" | grep " 0"

参考リンク:

Coq 8.7.1でSoftware Foundationsを読もうとしてハマったメモ

技術メモ 覚え書き

Software FoundationsのProgramming Language FoundationsのEquiv.vをProof Generalで読み込んだら以下のようなエラーが出た。

Error:
The file /Users/yuya/dev/src/local/softwarefoundations/plf/Maps.vo contains library
Top.Maps and not library Maps

以下のような内容の_CoqProjectというファイルを作成すると上手く読み込めた。

-R "." Top

Coqの物理パスと論理パスの扱いに絡む問題っぽい。