John Regehrブログの2つの投稿の翻訳に注目してください。 私はそれらを1つの出版物にまとめることを決めました。第一に、彼らは小さなボリュームを持っているからです。
最初の投稿へのリンク
2番目の投稿へのリンク
パート1.未定義の動作！=安全でないプログラミング
CおよびC ++の未定義の動作（UB）は、特にコードが信頼できないデータで機能する場合、開発者にとって危険です。 ほとんどのAOT最適化コンパイラの中間表現（IR）に未定義の動作が存在することはあまり知られていません。 たとえば、LLVM IRには、Cの爆発的なUBに加えて、 undefおよび「poisoned」の値があります 。人々が心配するようになると、典型的な反応は次のとおりです。 LLVM IRはCと同じくらい悪い！」この記事では、これがなぜそんなに間違っているのかを説明します。
未定義の動作は、設計上の決定の結果です。システムの特定のレベルでのソフトウェアエラーの体系的な検出の拒否です。 このようなエラーがないことを保証する責任は、より高いレベルの抽象化にあります。 たとえば、安全な言語をマシンコードにコンパイルできることは明らかですが、マシンコードの安全性がすべての妥協しない高レベルの保証を言語の実装に課していることも明らかです。 SwiftとRustはLLVM IRでコンパイルされています。 それらのセキュリティ保証のいくつかは、生成されたコードの動的チェックによって実行され、他はタイプチェックによって行われ、LLVM IRレベルでは表されません。 つまり、LLVMレベルのUBは検出されず、SwiftとRustの安全なサブセットからのコードの問題です。 開発環境のいずれかのツールがUBがないことを確信している場合、Cでも安全に使用できます。 L4.verifiedプロジェクトはまさにそれを行います。
未定義の動作の本質は、エラーチェック操作と安全でない操作の間の接続を回避することです。 安全でない操作とは無関係のチェックは、オプティマイザーによって削除されるか、オプションとしてループから除外されます。 残りの安全でない操作は、適切に設計されたIRを使用して、最小限またはオーバーヘッドなしでプロセッサ操作にマッピングできます。 たとえば、次のSwiftコードを考えます。
func add(a : Int, b : Int)->Int { return (a & 0xffff) + (b & 0xffff); }
Swift実装は全体がオーバーフローしたときに例外をキャッチする必要があるという事実にもかかわらず、コンパイラはオーバーフローが不可能であると判断し、そのようなLLVM IRを生成します。
define i64 @add(i64 %a, i64 %b) { %0 = and i64 %a, 65535 %1 = and i64 %b, 65535 %2 = add nuw nsw i64 %0, %1 ret i64 %2 }
オーバーフローチェック付きの加算演算がチェックなしの加算演算に置き換えられただけでなく、加算命令に属性nswおよびnuwのマークが付けられました。つまり、符号付きおよび符号なしの両方のオーバーフローが定義されていません。 これらの属性自体には利点はありませんが、関数がインラインの場合、追加の最適化を引き起こす可能性があります。 SwiftテストスイートをLLVMでコンパイルすると、8つの加算命令のうち1つだけが、整数オーバーフローが未定義であることを示す属性を持ちます。
この特定の例では、最適化パスが追加がオーバーフローを引き起こさないという事実を検出する可能性があるため、nsw属性とnuw属性は冗長です。 ただし、一般的な場合、これらの属性および類似の属性には実際の価値があり、既知の内容を再発見するための高価な静的分析を回避します。 また、いくつかの事実は、後でコンパイル手順で情報が失われるため、発見されない場合があります。
一般に、未定義の動作はプログラマーに見える抽象化であり、攻撃的で危険な妥協案を提示します。パフォーマンスとコンパイラーの単純さを引き換えにプログラムの正確さを犠牲にします。 一方、マシンコードやコンパイラの中間表現など、システムの下位レベルのUBは、プログラマがシステムを認識する方法に影響を与えない内部設計決定です。 このタイプのUBでは、効率的なプログラム実行を実現するために、対応する安全でない操作からセキュリティチェックを削除できるという事実を受け入れる必要があります。
パート2.表現力豊かなプログラミング言語には、常に未定義の動作がありますか？
ハッカーニュースで、誰かが私の以前の投稿に次のようにコメントしました 。
ゲーデルの不完全性定理であるEMNIPは、どの言語にも少なくともいくつかの不明確な動作があることを意味します。
不完全性と不溶性はかなり複雑なものであることを念頭に置いて、この声明を見てみましょう。 何年も前、私は喜んでゲーデルの定理を読みました：「 不完全さは虐待につながる 」（間違いなくそれを読み直す必要があります）。
まず、UBのないプログラミング言語があります。たとえば、UB上のプログラムが「7」を出力するような言語です。 UBが何を意味するにせよ（まだ正式な定義を与えていない）、常に「7」を出力する言語にはそれがないことは明らかです。
IEEE形式の実数で基本関数を計算する式の言語など、UBを持たない便利な言語もあります。 これらの言語はチューリング完全ではないため、簡単に説明できます。すべての計算が完了し、特定の結果が得られることを確認する必要があります。
しかし、実際には、HNのコメンテーターはライスの定理を念頭に置いていました。「チューリングマシンによって認識される言語の重要な特性は決定不能です。」したがって、f（）が任意の計算である場合、プログラムが未定義の動作：
main() { f(); return 1 / 0; // UB! }
しかし、これはナンセンスです。 ライスの定理は、重要な特性にのみ適用されます。 この制限を回避するには、UBの不在が些細な特性となる言語を定義する必要があります。 これは、プログラムの各操作がすべての機能を実行するという事実によって実現されます。これは、あらゆる条件下で定義されます。 したがって、この言語のプログラムは、特定の状態で終了するか、まったく完了しない可能性があります。 実際のプログラミング言語については、通常、極端な完全な仕様は通常作成されません。これは、特に組み込みアセンブラーを含むシステムの他のレベルとの相互作用に対して言語が開かれている場合、作業が必要になるためです しかし、この問題は純粋に実用的であり、理論的には問題は存在しません。 （チューリング完全な）玩具言語または実際の言語のサブセットについて、UBなしで仕様を記述することはそれほど難しくありません。
ここで、HNの元のコメントに戻ります。これは、停止の問題ではなく、不完全性の定理に関するものです。 何を言おうかわからないし、ゲーデルの定理がプログラミング言語の不定の振る舞いにどのように関係しているかわからない。