C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第4回 : 符号付き整数型のチェックと動機の動機)

はじめに

この連載では、C++ の整数型の奇妙な特性、そしてその中で整数オーバーフローを引き起こさないためのオーバーフローチェッカーをどう書くか、について主に解説します。

第4回では、ようやく符号付き整数型のチェック方法に入っていきます。

連載インデックス

• 第1回 : 整数型の怪と対策の不足
• 第2回 : 符号無し整数型のチェック
• 第3回 : C言語の整数の性質を知る
• 第4回 : 符号付き整数型のチェックと動機の動機
• 第5回 : 続・符号付き整数型のチェック

動機の動機

技術的な話ではないのでこの章は読み飛ばしても構いません。

さて、第1回では何故私がオーバーフローチェッカーを書くようになったか、その動機を話しましたが、そもそもこれは根本的な動機ではありませんでした。私の当初の動機は、C++ において整数型の定義が曖昧であるため、厳密に仕様書だけ見れば整数を安全に扱うことができないことを証明し、それをもって C99 の整数の定義のようなある程度厳しい制約を次の C++ 規格 (C++17) に加えさせることでした。

私がこのために行った最初の仕事は、C++ の仕様だけを厳密に解釈したときに整数オーバーフローチェッカーを 書けない ことを証明しようとすることでした。そのためには実際にオーバーフローチェックを書ける演算を取り除いて、残った演算を厳密に評価し直すことが必要でした。最初の証明試行で、次の演算に対して整数オーバーフローチェックを書けることを証明しました。

• a + b
• a - b
• a * b
  • a >= 0 && b >= 0
  • a >= 0 && b <= 0
  • a <= 0 && b >= 0
  • a <= 0 && b <= 0
• a / b
  • a >= 0 && b > 0
  • a <= 0 && b > 0
  • a >= 0 && b < 0
  • a <= 0 && b < 0
• a % b (a / b のオーバーフローチェックが正常に実施できることが前提)

このままだと非常にマズいです。a - b や -a が軒並み安全ではないのですから。

ただ、私は減算の整数オーバーフローチェッカーが、実際には書けることを見逃していました。減算が安全にできることを証明できれば論理的には……と式を幾つかノートに書いてみると、ある気づきがありました。……あれ、これ、全部の四則演算について安全な整数オーバーフローチェッカー、書けるんじゃね¹?

ここから既存の整数オーバーフローチェッカー実装がどうなっているのかを調べてみると……ここからは第1回の通りです。上の気づきの数日後には全てのパターンについて (オーバーフローチェッカー内で用いられる式自体が整数オーバーフローを引き起こさないことを含めて) 証明してしまうこととなり、急いで "安全な整数型" のフレームワーク²を書くことになりました。

では、私はそれで C++ 規格修正を断念したのか? ……まさか。定義が曖昧な部分は整数の表現可能な範囲だけに留まらないです (第3回 でも指摘したように整数型定義の上で障害になる問題は他にもあります) し、四則演算の安全性を確認するのに自明でない式を複数使いかつそれらについて 2000 行を超える Coq 証明を書かなければならないなんて、イカれてます。それに、ただの引き算がオーバーフローチェックを挟んだり整数型の中で使用する値域を制限したりすることなく (単純な正整数の同士の引き算ですら) 便利に使えないというのは、(2 の補数にかかわるひとつの例外を除いて) プログラミングスタイルを制約してしまう悪しき習慣だと考えます (実装者が気をつければ良い、というのは、規格の側で何も対処しなくても良いという言い訳にはならないと考えます; 特に整数演算は頻繁に用いられるだけに、いちいちチェックするコストが非常に高いので……)。

というわけで、……C++17 での修正のため、協力してくれる人ないしアドバイスしてくれる人はいつでも募集しています (Twitter の @a4lg 宛にリプか何か送って頂ければ)……。

略記法

なお、ここに示す式を略記無しの C++ で書くと少々わかりづらい部分があるので、次の略記を導入します。

• nmax
  演算に使用する共通の型 (第3回 にて解説) の最大値
  つまり std::numeric_limits<T>::max()
• nmin
  演算に使用する共通の型 (第3回 にて解説) の最小値
  つまり std::numeric_limits<T>::min()

また、オーバーフローチェッカーの式といった場合、指定された演算について 整数オーバーフローなどが発生しない (安全なときに) true を、発生するときに false を返す bool 型の式 とします。

加算 (a + b)

まずは、加算 (a + b) について証明してみましょう。まずは、a の符号だけが分かっている場合について示します。

a が 0 以上の場合

• b <= nmax - a

これは簡単です。

1. a + b <= nmax
2. b <= nmax - a (a を移項)

b が負だったとしても、a + b (の数学的な結果) はせいぜい nmin であるため、nmin <= a + b について考える必要は (この場合) ありません。また変数の限界を考えると nmax - a も負の数になることがありません。この考え方は、後に示す 無条件に安全な 演算を列挙する際に役立ちます。

a が 0 以下の場合

• nmin - a <= b

これも簡単。

1. nmin <= a + b
2. nmin - a <= b (a を移項)

a はゼロまたは負であるため、nmin - a は nmin もしくはそれに正の数を足したものになります。

a と b の符号が異なる場合

これは a >= 0 && b <= 0 もしくは a <= 0 && b >= 0 のように、a と b が 0 を中心とした数直線の反対側に位置しているか、もしくは少なくとも片方が 0 の場合を示します。この場合ですが……。

• true

そう、オーバーフローチェックを行う必要はありません。a と b を nmin <= a && a <= nmax、nmin <= b && b <= nmax の条件を満たす限りどのように変えてみても、符号さえ異なるならば a + b は nmin と nmax の間に収まります。

このような式は、オーバーフローチェックの式の中で使う場合にはそれ自体のオーバーフローを気にしなくても良いわけです。つまり、この式は他のオーバーフローチェックにおける有用なビルディングブロック (積み木) となります。

減算 (a - b)

次は、減算 (a - b) について見てみましょう。早速、先ほど見た 無条件に安全な 演算が使用されます。

b が 0 以上の場合

• nmin + b <= a

導出過程は以下の通り。

1. nmin <= a - b
2. nmin + b <= a (b を移項)

b は 0 以上、nmin は 0 未満の数値であるため、nmin + b はまさに上記の符号が異なる加算となります。

b が 0 以下の場合

• a <= nmax + b

1. a - b <= nmax
2. a <= nmax + b (b を移項)

正の数による除算 (a / b; 0 < b)

除算に関しては、除数 (割る方の数) が正であるときと負であるときで証明の難易度が段違いであり、かつこちらに関しては他の証明におけるビルディングブロックとなるため、先に証明しておきます。……といっても、結論はシンプル。

• true

正の除算であれば a / b と a の符号は同じで、絶対値は a のそれ以下になる、というのが短くした証明アウトライン。乗除が絡むと Coq の自動証明はあまりよくはたらかないため、手動証明 (auto with zarith タクティックに頼らない証明) の割合は増えます……が、その程度です。

乗算 (a * b)

ここではまとめて示しましょう。

• a >= 0 && b >= 0 なら、a == 0 || b <= nmax / a
• a >= 0 && b <= 0 なら、a == 0 || nmin / a <= b
• a <= 0 && b >= 0 なら、b == 0 || nmin / b <= a

両方とも非負の場合 (最初のケース) について詳しく見てみましょう。

1. a * b <= nmax
2. a * b / a <= nmax / a (両辺を a で割る)
3. b <= nmax / a (a * b / a [の数学的な結果] は b に等しい)
4. a == 0 || b <= nmax / a (ゼロ除算を避ける式を追加)

ステップ 2 で、両辺を割っていることに注意してください。というのも、整数を扱う際に除算は切り捨てを伴うため、その結果について非常に厳密に考えなければならないからです。とはいえ、次のような定理は無条件で成立します。

• a <= b かつ c > 0 なら、a / c <= b / c
• a <= b かつ c < 0 なら、b / c <= a / c

また、nmax / a は前章で解説した正整数による除算であり、それ自身がオーバーフローやゼロ除算を発生させることがありません (a == 0 || を先につけているため、a が 0 である場合には nmax / a 自体評価されない)。

さて、これで順方向については証明できましたが、オーバーフローチェッカーの式が返す結果が実際の整数オーバーフローと 1対1 対応していることを示すには、逆方向についてもちゃんと証明しないとなりません。つまり、a、b とも非負である場合、次のような定理の証明も必要です。

• nmin < 0
• 0 < nmax
• 0 <= a かつ a <= nmax
• 0 <= b かつ b <= nmax

以上の前提を満たし、かつ a == 0 || b <= nmax / a を満たすならば、
nmin <= a * b かつ a * b <= nmax を満たす。

加減算であった場合は順方向が証明できれば似たようなアプローチで逆方向も簡単に証明できましたが、乗除においてはそこまで単純な話ではありません。次のように、かなり証明は長くなります。

1. a == 0 の場合、a * b は 0 であり、0 <= nmax を満たすことから成立。
2. a != 0 の場合、前提 0 <= a より 0 < a が成立。
3. 次の補題を証明 (Coq においては標準ライブラリ内):
   すべての p、q (0 <= p、0 < q) について、q * (p / q) <= p
4. nmin <= a * b であることを、次のように分割して証明:
   • nmin <= 0
   • 0 <= a * b (どちらも簡単)
5. a * b <= nmax であることを、次のように分割して証明:
   • a * b <= a * (nmax / a) (事前条件の右側、両辺に左から a を掛けることで与式が成立)
   • a * (nmax / a) <= nmax (補題より成立)

さて、ここで証明しなかったケースに、a および b が負である、というものがあります。このケースにおいては、正整数による除算を使えるような明らかなとっかかりが存在しないのです。そのため、最初私はこれについては証明できないものと考えていました (後になって証明できることが分かるのですが、少なくとも次回に解説する場合分けが必要になります)。

負の数同士の除算 (a / b; a <= 0 && b < 0)

(注: 第2回 で出題した練習問題の答えが書かれています)

除数が正である場合には a / b の符号が a と同じであることを利用して絶対値に関する直感をオーバーフローを引き起こさないことを証明するために転用することができましたが、除数が負である場合、a / b の符号が a と逆になることがネックになります。2 の補数表現を用いた 8-bit 整数においても -128 を -1 で割ったときその型の範囲内に入らないことがあるように、整数型の正負の表現範囲について何ら仮定を置けない場合には絶対値に関して何か証明したとしてもそこから有用な結果を導くことが非常に困難になるのです。

とはいえ、負の数同士の除算なら、さらなる場合分けを導入することなく証明できます。

• a <= 0 かつ b < 0 なら、b < a || b < nmin / nmax || nmax * b < a - b

練習問題で見せた誤ったオーバーフローチェッカーの式は、細かい所を省けば nmax * b <= a でしたが、正しいものでは nmax * b < a - b となっています。どうしてこのようになったのか、まずは私が最初に陥った誤った証明過程を見てみましょう。

1. a / b <= nmax
2. 両辺に負の数 b を掛け、nmax * b <= b * (a / b)
3. b * (a / b) を変形し、a にする
4. 結果として、nmax * b <= a が証明できるはずなのだが、試行錯誤しても証明できない……!?

この中で誤っているのは? ……上までの章を十分理解しながら読んだ人なら分かるように、ステップ 3 です。実数や有理数のドメインでは b * (a / b) と等価である式 (b * a) / b なら a に変形しても良かったでしょうが、整数ドメインにおいては先に切り捨ての入る除算が入ってしまっているため、b * (a / b) は一般に a ではないのです。

この誤りをやらかしてからは次の過ちを避けるため、コンピュータによる総当たり検証を併用するようになりました。総当たり検証は漏れがないことを証明できませんが、反例が出てこないことは証明を完遂する上では良い兆候です (Coq をはじめとした多くの証明支援処理系では、矛盾があってもそれを証明完了のギリギリ前まで辻褄合わせしてしまうことができるので、証明途中では明確な矛盾が見えづらいことがあるのです)。

正しい証明は、この問題を避けるためにはるかに複雑になります。なお、b < a および b < nmin / nmax については補助的な式である (とはいえ、証明自体はかなりの量となる) ため、ここでは nmax * b < a - b という重要な部分についてのみ証明を見てみましょう。

証明 (順方向):

• nmin < 0
• 0 < nmax
• nmin <= a かつ a <= 0
• nmin <= b かつ b <= 0
• b != 0

以上の前提を満たし、かつ

nmin <= a / b かつ a / b <= nmax

を満たすならば、値域制限のない整数ドメインでは

nmax * b < a - b

を満たす。

1. a / b <= nmax (条件の右側だけ取り出す)
2. nmax * b <= b * (a / b) (負整数 b を両辺に掛ける)
3. b * (a / b) < a - b を次のように証明:
   1. b * (a / b) < a - b
   2. a - (a % b) < a - b (C++ 仕様における (a/b)*b + a%b == a という関係式より)
   3. b < a % b (a からの減算を消去)
   4. 1. を直接証明 (a、a % b はいずれも 0 以下、かつ a % b は絶対値で b のそれを下回る)
4. nmax * b < a - b (2. および 3. の式を併せて)

証明 (逆方向):

• nmin < 0
• 0 < nmax
• nmin <= a かつ a <= 0
• nmin <= b かつ b <= 0
• b != 0

以上の前提を満たし、かつ値域制限のない整数ドメインで

nmax * b < a - b

を満たすならば、

nmin <= a / b かつ a / b <= nmax

を満たす。

1. nmin <= a / b が前提成立時は常に成立することを証明 (0 <= a / b より)
2. a - b <= b * (a / b) - b を次のように証明:
   1. a - b <= b * (a / b) - b
   2. a <= b * (a / b) (b による減算を除去)
   3. a <= b * (-a / -b) (除算の性質)
   4. -b * (-a / -b) <= -a (両辺に -1 を掛けて整理)
   5. 1. を、乗算の際使用した補題を用いて証明
3. nmax * b < b * (a / b) - b (条件と 2. を併せて)
4. a / b - 1 < nmax
   (両辺を負整数 b で割る [すべての項が b の倍数であるためこの変形が整数ドメインでも成立])
5. a / b <= nmax (整数ドメインにおいて不等号を整理)

前述のオーバーフローチェッカーの式には nmin / nmax、nmax * b、a - b という 3 つの式が入りますが、nmin / nmax は正整数による除算で無条件に安全、nmax * b は b < nmin / nmax を満たさないならば安全、a - b は b < a を満たさないなら余裕を持って安全³なので、最初に示したオーバーフローチェッカーの式が成り立ちます。

剰余 (a % b; b != 0)

こちらについては、第2回 と同じように、a / b がオーバーフローなどを引き起こさないなら⁴ a % b もオーバーフローを引き起こさないという一方向の定理を証明します。証明アウトラインは Coq 証明においては符号による場合分けを含むためやや複雑ですが、ここでは場合分けを省略したものを掲載します。

1. C++ (C++11 以降) における a % b の絶対値は a 以下であることを証明する。
2. C++ (C++11 以降) における a % b の符号は a と同じになることを証明する。
3. 1. および 2. より、a % b は a またはそれ以上に 0 に近いことを導く。
4. nmin <= a、a <= nmax、nmin < 0、0 < nmax という前提から、
   nmin <= a % b かつ a % b <= nmax (証明完了)

ここまでで証明したこと / 次回予告

さて、ここまでで、四則演算 (+剰余) の中で証明を完了させたのは次のケースです。

• a + b
• a - b
• a * b
  • a >= 0 && b >= 0
  • a >= 0 && b <= 0
  • a <= 0 && b >= 0
  • a <= 0 && b <= 0
• a / b
  • a >= 0 && b > 0
  • a <= 0 && b > 0
  • a >= 0 && b < 0
  • a <= 0 && b < 0
• a % b (a / b のオーバーフローチェックが正常に実施できることが前提)

乗算と除算のそれぞれ 1 ケースが残っていますが、これらは今までの証明戦略では証明できません。これを証明するには、nmin と nmax の関係について場合分けを行う必要があります。

またこの場合分けやさらなる仮定の追加を行うと、遅い演算を可能な限り避けることも可能になります。第5回ではそれらについて考えながら四則演算のオーバーフローチェッカーを完成させましょう。

さいごになりますが、ここにある証明は概要をなんとなく理解できるようにかなり簡略化 (一部については Coq 版の証明とは別物に) しています。簡略化の過程で誤りが混入していたら、申し訳ありません。ただし、結論となるオーバーフローチェッカーの式に関しては Coq を使用して厳密に証明していますので、信じてもらって良いと思います。

1. 減算を証明しただけではオーバーフローチェッカーの存在を証明できないケースに負の数同士の除算がありますが、これは同時期に減算の証明無し (つまり整数型の特性に対する特別なチェック無し) に書けることを独立して証明しました。 ↩

2. 一部 [特に型/キャストの取り扱い周り] については Boost に入れられることが検討されている Safe Numerics の設計を参考にしたつもりですが……ポリシーの違いか、結局別物になりつつあります。 ↩

3. これに関しては逆が一般には成立しません。ただオーバーフローチェッカーの証明を単純化して b < a を消去するには、片方向の証明だけで問題ないのです。 ↩

4. ただし、この仮定は本当は必要ありません。 ↩