抽象解釈は博士学位が必要に聞こえる。もうそうではない
Inferを使ってCIパイプラインで形式的静的解析を実行する方法。動作する設定と現実的なトレードオフを紹介する。
抽象解釈は、エンジニアがタブを閉じてしまうような言葉だ。束理論を一学期学ばなければ理解できないようなものに聞こえる。ほとんどの開発者は、それが研究論文の世界のもので、プルリクエストの世界のものではないと思い込んでいる。…
static-analysis
6 posts
LLMは静的解析の警告を優先順位付けできる。ただし、なぜかは説明できない
大規模言語モデルは静的解析の偽陽性の選別に役立つが、抽象解釈のようにプログラムの意味論を理解しているわけではない。両者を組み合わせる方法を解説する。
あなたの静的解析ツールは金曜日の午後に847件の警告を出力した。統計的には、そのうち5%から15%が実際のバグだ。残りは偽陽性だ：生成コード内のデッドストア、ツールには怪しく見えるが人間には明らかなヌルチェック、関係のないハッシュ関数内の整数オーバーフロー。 手作業で仕分けするのは精神的に exhausting…
Metaはプログラムを実行しない静的解析ツールで本番コードから10万件のバグを発見した
MetaのInferは抽象解釈と双方向誘導を用いて、コードの構造を推論することでヌル参照、メモリリーク、競合状態を検出する。実行は不要だ。仕組みと自社コードベースでの活用方法を解説する。
Metaは、コードがユーザーに到達する前に静的解析ツールが捉えた10万件以上のバグ修正をリリースしてきた。そのツールはInferと呼ばれ、オープンソースであり、コードを実行しない。コードを読み込み、コードが可能な動作の数学モデルを構築し、特定の有害な事象が起こりえないことを証明する。あるいは、それが起こりうる経路を発見…
静的解析は飛行機が墜落しないことを証明できない。だが、もっと有益なことは証明できる。
抽象解釈はあらゆる可能なプログラム状態を過大近似する。抽象化の中でゼロ除算が到達不可能なら、実際のコードでも到達不可能である。以下に、その仕組みと限界を解説する。
静的解析は、飛行機が墜落しないことを証明することはできない。しかし、高度計の制御ループが決してゼロ除算を起こさないこと、配列の範囲外を決して参照しないこと、固定小数点アキュムレータが決してオーバーフローしないことは証明できる。この区別が重要なのは、一方は物理、空気力学、そして応力下のアルミニウムに関する主張であり、他方…
コードにランタイムエラーがないことを証明する方法（そして、なぜ諦めるかもしれない理由）
抽象解釈を使えば、実行前にランタイムエラーが発生しないことを証明できる。実際の仕組み、難しさ、そしてツールチェーンでの位置づけを解説する。
テストスイートは通過した。型チェッカーも緑色だ。リリースする。2時間後、本番環境で誰もテストしようとしなかったエッジケースで が発生する。…
Fuck-u-code: AIパイプラインが見落としていた Deterministic 品質ゲート
型チェック、lint、設計ルールはある。でも deterministic スタックは複雑性、重複、命名の惨状を見抜けない。$0で解決する方法を紹介する。
今のAIコードパイプラインの実態を正直に見てみよう。 Cursor や Claude Code でコードを生成する。TypeScript の strict モードが型の不一致を捕捉するから、 を実行する。ESLint…