はじめに

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

第5回では、第4回で証明できなかった一部の符号付き整数型のチェック方法から入っていきます。この回の内容は第4回と直結しているため、まずそちらを読んでから読み始めることを強く推奨します。

連載インデックス

特性による場合分け

第1回で指摘した、C++ では存在する可能性のある異常な整数型は、正の値と負の値のバランスが取れていない異常なものとなっています。

とはいえ、完全に無秩序となってしまうわけではありません。実際には、いくつかの単純なパターンに分類することが可能です。ということで、今回主要な場合分けに使う 3 つの排他的な特性を紹介しましょう。

均等
このパターンでは、負の数は正の数と同じだけ存在します。つまり、nmin = -nmax が成り立ちます。 C 言語の整数表現の中では、"1 の補数" と "符号と絶対値" が該当します。
負方向のバイアス
このパターンでは、負の数は正の数より多く存在します。つまり、nmin < -nmax が成り立ちます。 C 言語の整数表現の中では、"2 の補数" が該当しますが、それ以外のパターンも存在可能です。
正方向のバイアス
このパターンは "負方向のバイアス" とは逆に、正の数が負の数より多く存在します。つまり、-nmin < nmax です。これは C 言語 (C99 以降) には存在し得ないパターンです。

これをどうやって判別するかですが、主に 2 つの方法があります。

減算を用い、0 - nmin や 0 - nmax がオーバーフローを引き起こさない (安全) か調べる
- 両方とも安全なら "均等"
- 0 - nmax のみ安全なら "負方向のバイアス"
- 0 - nmin のみ安全なら "正方向のバイアス"
加算を用い、nmin + nmax の特性から
- 0 なら "均等"
- 負なら "負方向のバイアス"
- 正なら "正方向のバイアス"

上記 2 つの手法は、いずれもそれ自身が整数オーバーフローを引き起こすことがありません (前者は証明済みのオーバーフローチェックを使用するため、後者はチェックの必要ない符号の異なる加算を用いるため)。

そのため、安全に符号付き整数型の特性を調べることができます。

負整数同士の乗算 (`a * b`; `a <= 0 && b <= 0`)

さて、第4回で証明し損ねたこのパターンについてはどうなるでしょうか?

a == 0 || nmax / a <= b ("均等" もしくは "負方向のバイアス" の場合)
a == 0 || -b <= nmax / -a ("正方向のバイアス" の場合)

前者は、正の数を負の数で割る除算を用いています。結果は負の数になりますが、"均等" もしくは "負方向のバイアス" に該当する整数型なら、結果の負の数は必ず表現できます。そのため、場合分けをしなかった場合安全とは見なされなかった nmax / a を使うことができています。

後者では、残念ながらその手法が使えません。しかし、"正方向のバイアス" に該当する整数型なら正の数の方が表現可能な幅が広いため、負の整数 a に対する -a が必ず表現可能です (-b も同様)。そのため、正の数同士の乗算で使用していた式を変形して用いることが可能となります。

安全な除算 (`a / b`; `b != 0`)

ここでは、除数は常に非零とします。このとき、(上記の負整数同士の乗算と似た根拠により) 極めて簡単な判定で除算が安全か否かを判定できるものが複数存在します。

"均等" (無条件)
"負方向のバイアス" (b > 0 または a >= 0)
"正方向のバイアス" (b > 0 または a <= 0)

正整数 / 負整数 (`a / b`; `a >= 0 && b < 0`)

これも、第4回で証明し損ねたこのパターンです。しかし、"均等" および "負方向のバイアス" 時については上で無条件に安全だと示しているため、証明すべきパターンは "正方向のバイアス" 時のみです。

nmax / -nmin < -b || a + b < nmin * b ("正方向のバイアス" 時; a >= 0 && b < 0)

この式はやや複雑ですが、負整数同士の除算よりはまだ簡単です。

-nmin、-b は "正方向のバイアス" の性質によって安全、a + b は符号が異なるため無条件で安全 (これが簡単になっている理由)、そして nmin * b については事前に評価される nmax / -nmin < -b によってオーバーフローを引き起こすパターンを網羅しています。そのため、オーバーフローチェッカーの式自体が整数オーバーフローを引き起こすことはありません。

除算まとめ

"均等"

	`b > 0`	`b < 0`
`a >= 0`	`true`	`true`
`a <= 0`	`true`	`true`

"負方向のバイアス"

	`b > 0`	`b < 0`
`a >= 0`	`true`	`true`
`a <= 0`	`true`	`b < a` または `b < nmin / nmax` または `nmax * b < a - b`

"正方向のバイアス"

	`b > 0`	`b < 0`
`a >= 0`	`true`	`nmax / -nmin < -b` または `a + b < nmin * b`
`a <= 0`	`true`	`true`

除算チェックの最適化 : 2 の補数

上でまとめたように、"均等" でないパターンには複雑な式による判定が含まれます。ところがここで問題になるのは、2 の補数です。近年一般的なコンピュータ向けのアーキテクチャにおける符号付き整数表現は 2 の補数がベースとなっており、先ほどの大きな分類の中では "負方向のバイアス" に分類されます。しかし、一般的によく利用される (かつ C 言語でも "均等" ではない中で唯一許可される) パターンでここまで大きな判定をしなければならないのは時間の無駄です。"負方向のバイアス" の中でも、特に "2 の補数" だけに特化した最適化をしておくべきでしょう。

Coq での証明においては、2 の補数を一般化した条件として、nmin = -nmax - 1 を使用しました。実際には 2 の補数では現れない (-nmin が 2 の累乗にならない) パターンも含まれますが、除算チェックの最適化を行うのにはこの程度の一般化で十分です。

b != 0 && (b != -1 || a != nmin)

Coq の証明においては、"均等" な整数型に対して負の数を 1 個付け加えた形で証明しました。大雑把に言えば、次のような形です。

b が nmin (付け加えた負の数) である場合には a / b は十分小さくなる
a が nmin である場合、b が -1 でない限り a / b は十分小さくなる
いずれにも当てはまらない場合、"均等" な整数型の条件を当てはめることができ、0 でないすべての b に対して除算は安全である

他の演算について

四則演算+剰余、そして簡単であるためここでは紹介しないインクリメントとデクリメントを除く演算については、オーバーフローチェックを行う際にはやや (型の特性; 例えば 2 進表現であることを仮定、簡易チェックするなどで) 妥協を行う必要があるかもしれません。とはいえ、C++ 規格の既存の規定を利用して、多少はそれっぽくまとめることは可能です。

整数の型を厳密に評価する

ここまででは、暗黙のうちに次の条件で証明してきました。

中置演算子の左右の型は等しい
演算結果の型は与えられたオペランドの型に等しい

ここで、実際の C++ 規格を扱う上で忘れてはいけないことに整数昇格 (第3回で解説) があります。

整数昇格が行われる際には必ず元の型のすべての値が表現可能な型に変換される (nmin_promoted <= nmin、nmax <= nmax_promoted) ため、結果の型を与えられたオペランドの型に戻す際にはオーバーフローチェッカーの式は常に正しいとみなすことができます。しかし、演算結果の型を戻さない場合には、この式は正しくなくなります。

具体例を見てみましょう。

unsigned char c1 = 255;
unsigned char c2 = 1;
auto result = c1 + c2;

もし unsigned char が 8-bit 符号無し整数だった場合、255 + 1 は unsigned char の表現可能範囲は超えます。しかし整数昇格により、result は必ず (規格準拠した処理系なら) int 型の 256 になります。

これへのライブラリ的な対策は、C 言語の規格上の動作と同様、オーバーフローチェックを整数昇格後の型で行うことです。もし足し算の後 unsigned char 型の値が必要になった場合、型を変換する際にチェックすれば良いわけです。もちろん、元の型を考慮して最適化することもできるでしょう。

次回予告

次の第6回では、実用的なライブラリを構築するための (多分) 最後のピース、"比較" について評価します。比較は型のキャストに対するチェックを実施するのに必要不可欠なものです。これが特定の条件の下で安全だということを示すのには、複雑な証明こそ必要ありませんが、C/C++ に対するある程度の知識を要します。そうそう、折角なので、次回証明する主要な命題を見せておきましょう。

それぞれ符号無し整数型の変数 a、b があったとき、a < b などの比較は無条件に安全である。
それぞれ符号有り整数型の変数 a、b があったとき、a < b などの比較は無条件に安全である。
0 以上の値を持つ変数 a、b (それぞれ任意の整数型) があったとき、a < b などの比較は無条件に安全である。

ここでは、a、b の整数型は同じであっても異なっていても構わないものとします。特に 3 番目の命題は、符号無し整数型と符号有り整数型、という組み合わせでも問題ありません。

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