(57)【要約】所与のプログラム内のすべての変数がプログラム内の所与の変数ｘ、ｙ、…に適用される所与の非循環数学関数ｆ（ｘ，ｙ，…）と等しいかどうかを最適化コンパイラによって判定する方法。１実施形態で、この方法は、関数ｆ（ｘ，ｙ，…）の値の諸ビットを入力ｘ、ｙ、…の諸ビットのブール関数として表すことと、すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値をｘ、ｙ、…の諸ビットのブール関数Ｖ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、すべてのステートメントｓについて、ステートメントがその下で実行される条件を入力ｘ、ｙ、…の諸ビットのブール関数Ｃ（ｓ）（ｘ，ｙ，…）として表すこととを含む。最後に、所与の変数ｖおよびプログラム・ステートメントｓについて、次のブール式Ｃ（ｓ）（ｘ，ｙ，…）Ｐ⇒Ｖ（ｓ，ｖ）（ｘ，ｙ…）＝ｆ（ｘ，ｙ，…）が成り立つかどうかの判定を、ブール充足可能性オラクルを使用して行う。第２の実施形態では、方法は、ｆ（ｘ，ｙ，…）の値を、対応する述部Ｐｊ（ｘ，ｙ，…）を有する複数の関数ｆｊ（ｘ，ｙ，…）として表すことと、すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、すべてのステートメントｓについて、ステートメントがその下で実行される条件を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｃｊ（ｓ）（ｘ，ｙ，…）として表すこととを含む。最後に、判定は、所与の変数ｖおよびプログラム・ステートメントｓについて、述部Ｐｊ（ｘ，ｙ，…）および条件Ｃｊ（ｓ）（ｘ，ｙ，…）が真である時に、必ず、Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）＝ｆｊ（ｘ，ｙ，…）であるかどうかの判定である。【特許請求の範囲】
【請求項１】
所与のプログラム内のすべての変数が前記プログラム内の所与の変数ｘ、ｙ、…に適用される所与の数学関数ｆ（ｘ，ｙ，…）と等しいかどうかを最適化コンパイラによって判定する方法であって、
関数ｆ（ｘ，ｙ，…）の値の諸ビットを入力ｘ、ｙ、…の諸ビットのブール関数として表すことと、
すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値をｘ、ｙ、…の前記諸ビットのブール関数Ｖ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、
すべてのステートメントｓについて、前記ステートメントがその下で実行される条件を前記入力ｘ、ｙ、…の前記諸ビットのブール関数Ｃ（ｓ）（ｘ，ｙ，…）として表すことと、
所与の変数ｖおよびプログラム・ステートメントｓについて、次のブール式Ｃ（ｓ）（ｘ，ｙ，…）⇒Ｖ（ｓ，ｖ）（ｘ，ｙ…）＝ｆ（ｘ，ｙ，…）が成り立つかどうかを、ブール充足可能性オラクルを使用して判定することと
を含む方法。
【請求項２】
前記数学関数ｆ（ｘ，ｙ，…）が、ハードウェアで計算可能である、請求項１に記載の方法。
【請求項３】
前記関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、ｆ（ｘ，ｙ，…）について使用可能なハードウェア命令によって計算されるようにするために、前記プログラムが変換される、請求項２に記載の方法。
【請求項４】
前記ハードウェア命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加することと、
各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することと
を含む、請求項３に記載の方法。
【請求項５】
前記プログラム変換の後に未使用のソフトウェア命令が、デッドコード除去によって除去される、請求項４に記載の方法。
【請求項６】
前記関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、使用可能な関数ｆ（ｘ，ｙ，…）によって、
命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加することと、
各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することと
によって計算されるようにするために、前記プログラムが変換される、請求項１に記載の方法。
【請求項７】
前記プログラム変換の後に未使用の命令が、デッドコード除去によって除去される、請求項６に記載の方法。
【請求項８】
所与のプログラム内のすべての変数が前記プログラム内の所与の変数ｘ、ｙ、…に適用される所与の数学関数ｆ（ｘ，ｙ，…）と等しいかどうかを最適化コンパイラによって判定する方法であって、
ｆ（ｘ，ｙ，…）の値を、対応する述部Ｐｊ（ｘ，ｙ，…）を有する複数の関数ｆｊ（ｘ，ｙ，…）として表すことと、
すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、
すべてのステートメントｓについて、前記ステートメントがその下で実行される条件を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｃｊ（ｓ）（ｘ，ｙ，…）として表すことと、
所与の変数ｖおよびプログラム・ステートメントｓについて、前記述部Ｐｊ（ｘ，ｙ，…）および前記条件Ｃｊ（ｓ）（ｘ，ｙ，…）が真である時に、必ず、Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）＝ｆｊ（ｘ，ｙ，…）であるかどうかを判定することと
を含む方法。
【請求項９】
前記数学関数ｆ（ｘ，ｙ，…）が、ハードウェアで計算可能である、請求項８に記載の方法。
【請求項１０】
前記関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、ｆ（ｘ，ｙ，…）について使用可能なハードウェア命令によって計算されるようにするために、前記プログラムが変換される、請求項９に記載の方法。
【請求項１１】
前記ハードウェア命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加することと、
各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することと
を含む、請求項１０に記載の方法。
【請求項１２】
前記プログラム変換の後に未使用のソフトウェア命令が、デッドコード除去によって除去される、請求項１０に記載の方法。
【請求項１３】
前記関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、使用可能な関数ｆ（ｘ，ｙ，…）によって、
命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加することと、
各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することと
によって計算されるようにするために、前記プログラムが変換される、請求項１に記載の方法。
【請求項１４】
前記プログラム変換の後に未使用の命令が、デッドコード除去によって除去される、請求項１３に記載の方法。
【請求項１５】
前記述部Ｐｊ（ｘ，ｙ，…）または前記関数ｆｊ（ｘ，ｙ，…）に応じて、前記コンパイラが、条件Ｃｊ（ｓ）（ｘ，ｙ，…）が成り立つかどうかとＰｊ（ｘ，ｙ，…）が成り立つ時に必ずＶｊ（ｓ，ｖ）（ｘ，ｙ，…）＝ｆｊ（ｘ，ｙ，…）であるかどうかとを判定するために前記プログラムの値の近似を使用する、請求項８に記載の方法。
【請求項１６】
前記近似が、定数伝搬、グローバル値番号付け、変数全体もしくは変数のビット範囲のいずれかに適用される範囲伝搬のうちの１つまたは複数の組合せである、請求項１５に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本願は、２００２年１１月１２日に出願した米国仮出願第６０／４２５，２５１号の利益を主張するものであり、この米国仮出願第６０／４２５，２５１号は、２００３年３月７日に出願した米国仮出願第１０／３８２，５７８号の一部継続出願であり、本願は、２００４年８月１２日に出願した米国仮出願第６０／６００，９９９号の利益を主張するものであり、これらの特許出願のすべてが、参照によって本明細書に組み込まれている。
【０００２】
本開示は、プログラム内の命令ｓのパターン認識を対象とし、具体的には、最適化コンパイラによる非循環パターンの認識を対象とする。
【背景技術】
【０００３】
本明細書で行われ、文末にリストされた参照は、本開示を理解し、実施するために、必要に応じて補明細書に組み込まれる。
【０００４】
固定小数点飽和演算は、メディア処理アプリケーションおよびディジタル信号処理アプリケーションで幅広く使用されている。Ｂビット２の補数演算ＯＰを与えられれば、その飽和相対物は、オーバーフローを検出し、結果を、表現可能な数の範囲の限度までにセットする。
ＭａｘＢ      ＯＰ（ｘ，ｙ）がオーバーフローする場合
ＯＰｓａｔ（ｘ，ｙ）＝ＭｉｎＢ    ＯＰ（ｘ，ｙ）がアンダーフローする場合  （１）
ＯＰ（ｘ，ｙ）  それ以外の場合
【０００５】
たとえば、ＧＳＭ標準規格の音声コーデックは、飽和算術演算に関して表される（非特許文献１および２）。ＴＩ社のＣ６ｘ、Ｉｎｔｅｌ社のＩＡ−３２およびＡＲＭなどの複数の現代のプロセッサ・アーキテクチャは、飽和演算命令を実施する。
【０００６】
ＡＮＳＩ  Ｃなどの標準プログラミング言語は、飽和演算の演算子を提供しない。通常、アプリケーション開発者は、基本的な２の補数算術に関してこれらの動作を実施する関数またはマクロのライブラリを含める。所与のアーキテクチャで高性能を得るために、これらのライブラリは、アセンブリでまたはベンダ固有ライブラリもしくはベンダ固有言語拡張を使用してのいずれかでコーディングされなければならない。これは、明らかに、ソフトウェアの開発および保守を複雑にする。さまざまな言語拡張および標準規格が提案されてきた（非特許文献３）。その将来は、確立されたベンダが通常は進んで標準化しないので、不明瞭である。したがって、プログラマは、ポータビリティと効率の間のトレードオフを強いられる。
【０００７】
このトレードオフを解決する形は、コンパイラが、飽和演算を実施するコード・フラグメントを自動的に認識し、これらのコードを適当な機械命令に変換することである。この解決策が有効であるためには、認識アルゴリズムが、堅牢であり、異なるコーディング・スタイルにまたがって働かなければならない。これは、抽象構文木に対する単純なパターン・マッチングから開始することができる。
【特許文献１】米国仮出願第６０／４２５，２５１号
【特許文献２】米国仮出願第１０／３８２，５７８号
【特許文献３】米国仮出願第６０／６００，９９９号
【非特許文献１】E. T. S, Institute, Digital cellular telecommunications system, ANSI-C code for the GSM Enhanced Full Rate (EFR) speech codec, (GSM 46.053), ftp://ftp.3gpp.org/specs/archive
【非特許文献２】E. T. S, Institute, Digital cellular telecommunications system, ANSI-C code for the GSM  Adaptive Multiple Rate (AMR) speech codec, (GSM 26.073), ftp://ftp.3gp.org/specs/archive
【非特許文献３】DSP-C Proposed Standard, www.dsp-c.org
【非特許文献４】J. Lind-Nielsen, BuDDy - A Binary Decision Diagram Package, http://www.itu.dk/research/buddy
【非特許文献５】P. Cuosot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of program by construction or approximation of fix points,” in POPL 1979
【非特許文献６】P. Cuosot and R. Cousot, “Systematic design of program transformation frameworks by abstract interpretation,” in Proceedings of the 29th annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, ACM Press, 2002, pp. 178-190
【非特許文献７】P. Cuosot and R. Cousot, “Automatic synthesis of optimal invariant assertions: Mathematical foundations,” in Proceedings of the 1977 symposium on Artificial intelligence and programming languages, 1977, pp. 1-12
【非特許文献８】M. N. Wegman and F. K. Zadeck, “Constant propagation with conditional branches,” TOPLAS, vol. 13, no. 2, pp. 181-210, 1991
【非特許文献９】K. Pingali, M. Beck, R. Johnson, M. Moudgill, and P. Stodghill, “Dependence flow graphs: an algebratic approach to program dependencies,” in Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.  ACM Press, 1991, pp. 67-78
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかし、そのような手法の限界は、飽和加算のさまざまな実装を考慮する時に明白になる。例が、米国仮出願第１０／３８２，５７８号に示されている。２つの飽和加算命令の両方が、式１の定義と同等であることを証明するためには、さまざまなビット操作および論理演算のシーケンスの結果の間の同等性を証明する必要がある。アドホックな手法の代わりに、形式的な代数の基礎を有する方法が必要である。
【０００９】
米国仮出願第１０／３８２，５７８号には、具体的に飽和加算および飽和減算を認識する方法が記載されている。本開示は、この以前の特許出願の原理が、すべての非循環演算に適用可能であり、包括項で表現できることを認識したものである。
【課題を解決するための手段】
【００１０】
本開示の方法は、所与のプログラム内のすべての変数がプログラム内の所与の変数ｘ、ｙ、…に適用される所与の非循環数学関数ｆ（ｘ，ｙ，…）と等しいかどうかを最適化コンパイラによって判定する。１実施形態で、この方法は、関数ｆ（ｘ，ｙ，…）の値の諸ビットを入力ｘ、ｙ、…の諸ビットのブール関数として表すことと、すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値をｘ、ｙ、…の諸ビットのブール関数Ｖ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、すべてのステートメントｓについて、ステートメントがその下で実行される条件を入力ｘ、ｙ、…の諸ビットのブール関数Ｃ（ｓ）（ｘ，ｙ，…）として表すこととを含む。最後に、所与の変数ｖおよびプログラム・ステートメントｓについて、次のブール式Ｃ（ｓ）（ｘ，ｙ，…）⇒Ｖ（ｓ，ｖ）（ｘ，ｙ…）＝ｆ（ｘ，ｙ，…）が成り立つかどうかの判定を、ブール充足可能性オラクル（ｏｒａｃｌｅ）を使用して行う。
【００１１】
第２の実施形態では、方法は、ｆ（ｘ，ｙ，…）の値を、対応する述部Ｐｊ（ｘ，ｙ，…）を有する複数の関数ｆｊ（ｘ，ｙ，…）として表すことと、すべての変数ｖおよびプログラム・ステートメントｓについて、ｓが実行される時にｖによってとられる値を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）として表すことと、すべてのステートメントｓについて、ステートメントがその下で実行される条件を、述部Ｐｊ（ｘ，ｙ，…）ごとに１つの複数の関数Ｃｊ（ｓ）（ｘ，ｙ，…）として表すこととを含む。最後に、判定は、所与の変数ｖおよびプログラム・ステートメントｓについて、述部Ｐｊ（ｘ，ｙ，…）および条件Ｃｊ（ｓ）（ｘ，ｙ，…）が真である時に、必ず、Ｖｊ（ｓ，ｖ）（ｘ，ｙ，…）＝ｆｊ（ｘ，ｙ，…）であるかどうかの判定である。
【００１２】
どちらの実施形態でも、関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、使用可能な関数ｆ（ｘ，ｙ，…）によって、命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加することと、各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することとによって計算されるようにするために、プログラムを変換することができる。プログラム変換の後に未使用の命令は、デッドコード除去によって除去される。数学関数ｆ（ｘ，ｙ，…）が、ハードウェアで計算可能である場合には、関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、ｆ（ｘ，ｙ，…）について使用可能なハードウェア命令によって計算されるようにするために、プログラムを変換することができる。
【００１３】
本発明の上記および他の態様は、添付図面と共に検討される時に、次の本発明の詳細な説明から明白になる。
【発明を実施するための最良の形態】
【００１４】
飽和算術演算の自動認識に関する技法の組を説明する。ほとんどの場合に、認識問題は、単にブール回路等価（Ｂｏｏｌｅａｎ  ｃｉｒｃｕｉｔ  ｅｑｕｉｖａｌｅｎｃｅ）の１つである。回路等価を解く費用を仮定して、抽象解釈に基づく実用的近似の組も説明する。
【００１５】
実験から、本技法が、信頼できる形で飽和演算を認識すると同時に、小さいコンパイル時オーバーヘッドを有することが示される。本方法は、飽和演算に限定されるのではなく、キャリーを伴う加算および算術シフトなど、他のイディオムの認識にも直接に適用可能である。
【００１６】
飽和演算は、非循環プログラム・フラグメントによって定義することができる。したがって、その結果および中間値を、ビット単位で、入力に関するブール式として記述することができる。この観察は、次の解決策を暗示する。
・非循環候補コード・フラグメントを与えられて、その変数の値を記述するブール式を抽出する。
・ブール式等価オラクル（ｏｒａｃｌｅ）を使用して、式のいずれかがテンプレートと一致するかどうかをテストする。
【００１７】
この方法の実際性をテストするために、オラクルとして２進決定図パッケージＢｕＤＤｙ（非特許文献４）を使用する飽和加算の認識アルゴリズムを実施した。このアルゴリズムは、候補の２の補数加算演算ｚ＝ｘ＋ｙを選び、演算に依存するプログラム内のどの値がその飽和値を担持するかを発見することを試みる。プログラムの制御フロー図の端（エッジ、ｅｄｇｅ）ごとに、このアルゴリズムは、（可能な時に必ず）そのエッジが実行される条件を計算する。その条件を、ｘ、ｙのビットに対するブール関数として表す。変数ごとに、このアルゴリズムは、すべてのエッジでの値をｘ、ｙのビットに対するブール関数として計算する。
【００１８】
ＢＤＤに基づくこのアルゴリズムの概要は、次の通りである。
ＥｘａｃｔＭａｔｃｈ（Ｇ：プログラムＣＦＧ，ＯＰ：一致させる演算）  ｛  ｒｅｐｅａｔ  ｛
−候補値ｘおよびｙを選ぶ
見つからない場合は、終了する
−Ｆが、ＯＰ（ｘ，ｙ）のビットのブール式であるものとする
−すべてのエッジｅおよび変数ｖについて
−エッジ候補Ｃ（ｅ）を計算する
−変数値Ｖ（ｅ，ｖ）を計算する
−∀ｘ，ｙ：  Ｃ（ｅ）（ｘ，ｙ）⇒（Ｆ（ｘ，ｙ）＝Ｖ（ｅ，ｖ）（ｘ，ｙ））
になるプログラムエッジｅおよび変数ｖを識別する（ブール式はＢＤＤを介してテストされる）｝｝
【００１９】
すべての候補加算演算ＯＰ（ｘ，ｙ）について、このアルゴリズムは、飽和値のブール式Ｆ（ｘ，ｙ）を形成する。このアルゴリズムは、その下でエッジｅが実行される条件Ｃ（ｅ）と、候補演算への入力に関する変数の値Ｖ（ｅ，ｖ）も表す。次に、このアルゴリズムは、実行される時に飽和値を担持するプログラム位置（エッジ）および変数を検索する。エッジ条件および変数値の計算は、標準抽象解釈問題（ｓｔａｎｄａｒｄ  ａｂｓｔｒａｃｔ  ｉｎｔｅｒｐｒｅｔａｔｉｏｎ  ｐｒｏｂｌｅｍ）（非特許文献５、６、および７）と呼ぶことができる。この場合の抽象解釈の領域は、候補入力に対するすべてのブール関数の集合である。実施形態１のこの方法を、図１に示す。
【００２０】
この第１の実施形態を使用して飽和加算を検出する時間は、長く、たとえば、ある加算が飽和加算であることを証明することを試みることが、１試行あたり１０ミリ秒を必要とした。加算の大多数をフィルタ・アウトするヒューリスティックを追加した後であっても、ＢＤＤの使用は、コンパイル時間に数十秒を追加する可能性がある。この方法を使用して飽和乗算を認識する試みを行ったが、最初の乗算についてＢＤＤを形成している間にメモリ不足になった。ハードウェアおよび／またはブール式等価もしくは充足可能性オラクルの改善があれば、この第１実施形態を、たとえば飽和乗算に使用することができる。
【００２１】
現在のハードウェアおよびブール・ソルバを使用することの難しさに対して、飽和算術演算を見つける高速近似アルゴリズムが、第２実施形態として開発された。プログラム変数の値を記述するブール式の近似を構成する。構成によって、この近似は、サイズの上限を与えられ、等価についてすばやくテストすることができる。
【００２２】
所与の飽和演算（たとえば、加算）を、複数のイディオム（たとえば、全範囲、部分範囲）を使用して実施することができ、各イディオムを、複数の形で実施することができる。各イディオムを、ステートメントおよび変数の単純なプロパティに関して記述することができる。これによって、一般的なブール充足可能性を解かずにプログラム・フラグメントの等価を提供することができる。
【００２３】
イディオム認識の問題は、次のように定義することができる。
・２の補数の演算を計算するステートメント、ｚ＝ｘ  ＯＰ  ｙを与えられる
・入力ｘ、ｙおよび結果ｚに関する飽和値の定義を与えられる。この定義は、次の述部付きの形でなければならない。
【数１】
2008510230.tif 000002
・目標は、ＯＰｓａｔ（ｘ，ｙ，ｚ）と等しいプログラム内の値を識別することである。たとえば、全範囲加算イディオムを、次式として定義することができる。
【数２】
2008510230.tif 000003
【００２４】
下に示すＧＳＭ  ＥＦＲコーデックのＬ＿ａｄｄ関数では、行１４のｒｅｔｕｒｎステートメントでのＬ＿ｖａｒ＿ｏｕｔｖａｒｉａｂｌｅの値が、この定義に一致する。これを自動的に証明できる場合には、戻り値を、飽和加算命令（ターゲット・アーキテクチャで使用可能な場合に）を使用して計算することができる。
１：  Ｗｏｒｄ３２  Ｌ＿ａｄｄ（
２：    Ｗｏｒｄ３２  Ｌ＿ｖａｒ１，  Ｗｏｒｄ３２  Ｌ＿ｖａｒ２
３：  ）｛
４：    Ｗｏｒｄ３２  Ｌ＿ｖａｒ＿ｏｕｔ；
５：    Ｌ＿ｖａｒ＿ｏｕｔ  ＝  Ｌ＿ｖａｒ１  ＋  Ｌ＿ｖａｒ２；
６：    ｉｆ  （（（Ｌ＿ｖａｒ１  ＾  Ｌ＿ｖａｒ２）  ＆  ＭＩＮ＿３２）＝＝０）
７：    ｛
８：      ｉｆ  （（Ｌ＿ｖａｒ＿ｏｕｔ  ＾  Ｌ＿ｖａｒ１）  ＆  ＭＩＮ＿３２）
９：      ｛
１０：        Ｌ＿ｖａｒ＿ｏｕｔ  ＝
１１：        （Ｌ＿ｖａｒ１  ＜  ０）  ？  ＭＩＮ＿３２  ：  ＭＡＸ＿３２；
１２：      ｝
１３：    ｝
１４：    ｒｅｔｕｒｎ  ＮＡＴＩＶＥ＿ＡＤＤＳＡＴ（Ｌ＿ｖａｒ１，Ｌ＿ｖａｒ２）；
１５：  ｝
次に、デッドコード除去が、次の最適コードを作るはずである。
１：  Ｗｏｒｄ３２  Ｌ＿ａｄｄ（
２：    Ｗｏｒｄ３２  Ｌ＿ｖａｒ１，  Ｗｏｒｄ３２  Ｌ＿ｖａｒ２
３：    ）｛
４：    ｒｅｔｕｒｎ  ＮＡＴＩＶＥ＿ＡＤＤＳＡＴ（Ｌ＿ｖａｒ１，  Ｌ＿ｖａｒ２）；
５：  ｝
【００２５】
当初に、入力プログラムは、ステートメントの制御フロー・グラフＧ＝（Ｎ，Ｅ）として表される３アドレス形式に下げられた。ノードには、一意の開始ノード、一意の終了ノード、ｘ：＝ＯＰ（ｙ，ｚ）の形の割当てステートメント、ＩＦ  （ｘ≠０）の形のスイッチ、および明示的制御フロー・マージが含まれる。
【００２６】
使用可能なスカラ型が３２ビットｉｎｔおよび１６ビットｓｈｏｒｔだけである場合に、８ビットのｓｉｇｎｅｄおよびｕｎｓｉｇｎｅｄのピクセル演算など、他のビット幅の演算への派生物を簡単に生成することができる。
【００２７】
プログラム位置と変数ｘおよびｙとを与えられ、作業は、プログラムのすべての実行で所与の関数ｆ（ｘ，ｙ）の値を担持する変数ｖを識別することである。形式的には、下記を与えられる。
・候補プログラムエッジｅ０および候補変数ｘ、ｙ。
・ヒューリスティック・ウィットネス（ｈｅｕｒｉｓｔｉｃ  ｗｉｔｎｅｓｓ）ｚ。ウィットネスは、述部を単純化するのを助ける。飽和演算の場合に、ウィットネスは、通常、非飽和演算の結果である。
・含意の離接によって表されたパターン関数ｆ（ｘ，ｙ，ｚ）
【数３】
2008510230.tif 000004
【００２８】
目標は、ｅが実行される時のｖの値がｆ（ｘ０，ｙ０，ｚ０）であるエッジｅおよび変数ｖを識別することであり、ここで、ｘ０、ｙ０、およびｚ０は、候補エッジｅ０の最も最近の実行時の候補変数の値である。
【００２９】
この実施形態では、所与の候補エッジおよび候補変数について、式２の条件ごとに抽象解釈を１回実行する。抽象解釈の各連続するインスタンス中に、述部Ｐｊが成り立つという仮定の下で、変数値Ｖ（ｅ，ａ）およびエッジ条件またはアサーションＡ（ｅ）の近似を計算する。
【００３０】
エッジアサーション（ｅｄｇｅ  ａｓｓｅｒｔｉｏｎ）Ａ（ｅ）は、そのプログラムエッジが実行される場合に成り立つ条件である。エッジアサーションＡ（ｅ）は、候補ｘ、ｙおよびウィットネスｚの関数として計算される。変数値Ｖ（ｅ，ｖ）は、エッジｅが実行される時のｖの値に関する知識を表す。Ｖ（ｅ，ｖ）も、ｘ、ｙ、およびｚの関数である。
【００３１】
プログラムは、候補エッジｅ０で、ｘ、ｙ、およびｚの値を一次変数ｘ０、ｙ０、およびｚ０に保存するように変更される。次に、すべてのエッジｅで、アサーションａｓｓｅｒｔ（Ａ（ｅ）（ｘ０，ｙ０，ｚ０））が満足され、すべての変数ｖについて、アサーションａｓｓｅｒｔ（ｖ＝＝Ｖ（ｅ，ｖ）（ｘ０，ｙ０，ｚ０））が満足される。
【００３２】
上の定義を与えられれば、変数ａは、次式が成り立つ場合に、パターン関数ｆ（ｘ，ｙ，ｚ）の値を担持する。
∀ｊ：∀ｘ，ｙ，ｚ：（Ａ（ｅ）（ｘ，ｙ，ｚ）∧Ｐｊ（ｘ，ｙ，ｚ））⇒（Ｖ（ｅ，ａ）（ｘ，ｙ，ｚ）＝ｆｊ（ｘ，ｙ，ｚ））    （３）
【００３３】
言い換えると、式２の条件Ｐｊごとに、（ａ）エッジｅが実行されない、または（ｂ）そのエッジが実行され、変数ａが適当な場合ｆｊと等しいのいずれかがテストされる。この第２実施形態を、図２に示す。
【００３４】
このアサーションおよび値を近似するために、条件または述部を近似するものと値を近似するものという２つの格子を使用する。Φは、述部の格子を表し、Λは、値の格子を表す。これらの格子は、次の要件を満足しなければならない。
・ΦとΛの両方が、一番上と一番下の要素を含まなければならない。この両方が、ミート演算子（ｍｅｅｔ  ｏｐｅｒａｔｏｒ）および比較演算子を定義しなければならない。比較演算子は、明確に形成された格子に必要である。ミート演算子は、プログラム・マージ点で使用される。
・Φは、合接、離接、および否定を定義しなければならない。Φは、真値と偽値の両方を含まなければならない。Φは、合接、離散、真、および偽に関する通常の代数規則があてはまらなければならないという点で健全でなければならない。
・中間プログラム言語でのすべての算術演算ＯＰについて、格子Λは、解釈ＯＰ：Λ×Λ→Λを定義しなければならない（すべての演算が２進であると仮定する）。
値をめいめいの述部にリンクする２つの関数
・ＭａｙＮｏｎＺｅｒｏ：Λ→Φ関数は、値がおそらくは非ゼロであり得るかどうかをテストする。
・ＭａｙＺｅｒｏ：Λ→Φ関数は、値がおそらくはゼロであり得るかどうかをテストする。
【００３５】
ＭａｙＮｏｎＺｅｒｏ関数およびＭａｙＺｅｒｏ関数が、矛盾した結果を作る必要はない。時々、ある値を、同時におそらくはゼロであり、おそらくは非ゼロであるものとして近似する必要がある場合がある。
【００３６】
これらの定義を与えられて、候補エッジｅ０、候補変数ｘ、ｙ、およびウィットネスｚに関するエッジアサーションＡ（ｅ）および変数値Ｖ（ｅ，ａ）に関するプログラムの抽象解釈が、定義される。諸式を、図３に示す。これは、式のかなり標準的な組である。マージ・ステートメントの式は、Ｗｅｇｍａｎ−Ｚａｄｅｃｋ型の片側条件付き伝搬（Ｗｅｇｍａｎ−Ｚａｄｅｃｋ  ｓｔｙｌｅ  ｏｎｅ−ｓｉｄｅ  ｃｏｎｄｉｔｉｏｎａｌ  ｐｒｏｐａｇａｔｉｏｎ）（非特許文献８および９）を可能にする。
【００３７】
全体的なアルゴリズムは、次のように要約される。
ＡｐｐｒｏｘＭａｔｃｈ（Ｇ：プログラムＣＦＧ，ＯＰ：一致させる演算）  ￥｛
ｒｅｐｅａｔ  ￥｛
−候補値ｘ、ｙおよびウィットネスｚをヒューリスティックに選ぶ
見つからない場合には、終了する
−Ｆｏｒ  ｅａｃｈ  含意Ｐｊ（ｘ，ｙ，ｚ）⇒ｆｊ（ｘ，ｙ，ｚ）（パターン関数内の）  ｛
−Ｐｊが真であると仮定する
−抽象解釈を使用してエッジアサーションＡ（ｅ）および変数値Ｖ（ｅ，ｖ）を計算する
−∀ｘ，ｙ，ｚ：（Ａ（ｅ）（ｘ，ｙ，ｚ）∧Ｐｊ（ｘ，ｙ，ｚ））⇒（Ｖ（ｅ，ａ）（ｘ，ｙ，ｚ）＝ｆｊ（ｘ，ｙ，ｚ））
を満足するエッジｅおよび変数ｖを識別する
￥｝￥｝￥｝
【００３８】
本方法が乗算、全範囲加算、および部分範囲加算にどのように適用されるかの例を続ける。本技法を飽和減算の認識に拡張することは、単純である。示されるさらなる例には、キャリーを伴う加算および算術シフトの認識が含まれる。本方法は、クリッピングなどの演算にも適用可能である。
【００３９】
Ａ．全範囲飽和加算
全範囲飽和加算に一致するために、非飽和加算演算ｚ＝ｘ＋ｙから始める。入力変数ｘおよびｙは、候補変数である。出力変数ｚは、ウィットネスである。パターン関数は、
【数４】
2008510230.tif 000005
である。オーバーフロー述部およびアンダーフロー述部は、符号テストを介して定義することができる。
【数５】
2008510230.tif 000006
この定義の比較演算子は、３２ビットの２の補数演算を使用する。
【００４０】
全範囲飽和加算のさまざまな実装は、ｘ、ｙ、およびｚの符号ビットに関する述部に基づいて分岐する、かつ／または符号ビットのビット操作を実行するのいずれかである。したがって、エッジアサーションは、符号ビットの述部（および他のもの）として表される。さらに、任意の変数ｖのビットの区間［ｐ，ｐ＋ｎ］がｘ、ｙ、およびｚのビットの区間［ｑ，ｑ＋ｎ］と等しいかどうかを記憶する。
格子Φは、次の６つの入力変数に関するすべての述部の集合である。
σｘ≡（ｘ＜０）、ｘの符号ビット
σｙ≡（ｙ＜０）、ｙの符号ビット
σｚ≡（ｚ＜０）、ｚの符号ビット
ζｘ≡（ｘ＝０）                    （６）
ζｙ≡（ｙ＝０）
ζｚ≡（ｚ＝０）
値格子Λ＝Φ３２ｘΓは、２つの格子の積として作られる。
・Φ３２は、Φ内の述部の長さ３２のすべてのベクトルの格子である。Φ３２は、ｘ、ｙ、およびｚの符号ビットに関して変数のビットを近似するのに使用される。
・Γ＝｛Ｔ  ｘｐ，ｑ，ｎ，  ｙｐ，ｑ，ｎ，  ｚｐ，ｑ，ｎ，  ⊥｝は、ｘ、ｙ、およびｚのビットの部分範囲として変数を近似するのに使用される。ｘｐ，ｑ，ｎとしての変数ｖの近似は、ｖのビットｖ［ｐ，ｐ：ｎ］がｘのビットｘ［ｑ，ｑ＋ｎ］と同一であることを意味する。
【００４１】
Λの各要素は、対＜ν，ρ＞であり、ここで、＜ν，ρ＞、ここで、ν∈Φ３２であり、ρ∈Γである。νは、ベクトル成分であり、ρは、ビット範囲成分である。
【００４２】
ベクトル成分に関する算術演算子の解釈ＯＰは、どちらかといえば単純である、すなわち、すべての算術演算について、述部を、結果のビットごとに導出することができる。ヒューリスティックには、シフトまたはビット単位演算に変換できるものを除いて、乗算演算、除算演算、および剰余演算を解釈してはならない。これらの演算の結果は、（保存的に）⊥のベクトルにセットされる。
【００４３】
ビット範囲成分に関する解釈も、どちらかといえば単純である。定数シフト演算および定数とのビット単位演算は、⊥でない出力を作る。他のすべての演算は、解釈されない。
解釈の例として、等価比較：ｃ：＝（ａ＝０）を検討されたい。ａのビット範囲成分が、ν０，０，３１  ｆｏｒ  ν∈ｘ，ｙ，ｚの形である場合に、ｃのベクトル成分に＜０  …  ０  ζν：＞をセットしなければならない。
【００４４】
ＭａｙＮｏｎＺｅｒｏ演算子およびＭａｙＺｅｒｏ演算子は、入力値の表現を、それぞれ非ゼロまたはゼロとすることができるかどうかをテストする。ＭａｙＮｏｎＺｅｒｏは、Φ３２成分のすべてのビットの離接を形成する。この離接が自明に偽ではない場合に、ＭａｙＮｏｎＺｅｒｏは、１を返す。同様に、この離接が自明に真ではない場合に、ＭａｙＺｅｒｏは、１を返す。
パターン関数の条件Ｐｊは、次のように自明にエンコードされる。
Ｏｖｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡¬σｘ∧¬σｙ∧¬σｚ
Ｕｎｄｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡σｘ∧σｙ∧σｚ      （７）
ＮｏＯｖｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡¬Ｏｖｅｒｆｌｏｗ∧¬Ｕｎｄｅｒｆｌｏｗ
候補エッジｅ０の初期値は、次の通りである。
Ｖ（ｅ０，ｘ）＝＜＜σｘ⊥…⊥＞ｘ０，０，３１＞
Ｖ（ｅ０，ｙ）＝＜＜σｙ⊥…⊥＞ｙ０，０，３１＞    （８）
Ｖ（ｅ０，ｚ）＝＜＜σｚ⊥…⊥＞ｚ０，０，３１＞
抽象解釈がこの場合にどのように働くかを示すために、次の例を検討されたい。
１：  ｉｎｔ  ａｄｄｓａｔ＿３２ｂｉｔ  （ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
２：  ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
３：  ｉｎｔ  ｔ１  ＝（〜（ｘ  ＾  ｙ）  ＆  （ｘ  ＾  ｚ））；
４：  ｉｎｔ  ｔ２  ＝  ＭＩＮ３２  ＆  ｔ１；
５：  ｉｆ  （ｔ２）  ｛
６：    ｉｎｔ  ｔ３  ＝  （ｘ  ＞＞  ３１）  ＆  １；
７：    ｚ  ＝  ＭＡＸ３２  ＋  ｔ３；
８：  ｝
９：  ｒｅｔｕｒｎ  ｚ；
１０：  ｝
ｔ１（行３）の最上位ビットだけを表すことができる。
【数６】
2008510230.tif 000007
【００４５】
ＭＩＮ３２（すなわち、０ｘ８０００００００）との合接は、ｔ１の最上位ビットを分離する。したがって、行４でのｔ２の値の表現は、
【数７】
2008510230.tif 000008
である。
【００４６】
行６および７のステートメントが実行される条件は、暗黙のテストがｔ２≠０なので、ｔ２のビットの離接によって与えられる。
【数８】
2008510230.tif 000009
【００４７】
したがって、行６および７のアサーションは、
【数９】
2008510230.tif 000010
である。ここで、Ｐは、式７によって与えられる現在の仮定（オーバーフロー、アンダーフロー、どちらもない）である。「どちらもない」を仮定する場合に、Ａ１＝０であり、それ以外の場合に非ゼロであることは、簡単にわかる。したがって、「どちらもない」仮定の下では、候補エッジでのｚへの割当てだけが、ｒｅｔｕｒｎステートメント（行９）に達する。
【００４８】
行６でのｔ３に関する計算された近似は、
Ｖ３＝＜＜０，０…０，σｘ＞，ｘ０，３１，０＞
である。すなわち、ｔ３は、ｘの符号（第３１）ビットを担持する。オーバーフローの仮定の下では、σｘ＝０である。したがって、ｚには、定数ＭＡＸ３２が割り当てられる。アンダーフローが仮定される時には、σｘ＝１であり、ｚにはＭＡＸ３２＋１＝＝ＭＩＮ３２が割り当てられる。
【００４９】
上のすべてが、オーバーフローが発生する時には値ＭＡＸ３２によって、アンダーフローが発生する時には値ＭＩＮ３２によって、それ以外の場合にはｚの最初の値によって、ｒｅｔｕｒｎステートメントに達することを証明する。これは、飽和値によってｒｅｔｕｒｎステートメントに達することを証明する。
【００５０】
Ｂ．部分範囲加算
部分範囲加算のパターン関数は、
【数１０】
2008510230.tif 000011
である。この定義での比較は、３２ビット２の補数算術を使用する。
【００５１】
部分範囲加算は、より単純である。候補加算はｚ＝ｘ＋ｙであり、ここで、ｘおよびｙは、１６ビット「ｓｈｏｒｔ」として宣言される。オーバーフロー条件、アンダーフロー条件、および非オーバーフロー条件は、ｚに対する範囲テストに関して次のように表される。
Ｏｖｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡（ｚ∈］Ｍａｘ１６，＋∞［）
Ｕｎｄｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡（ｚ∈］−∞，Ｍｉｎ１６［）
ＮｏＯｖｅｒｆｌｏｗ（ｘ，ｙ，ｚ）≡（ｚ∈［Ｍｉｎ１６，Ｍａｘ１６］）
したがって、範囲伝搬は、オーバーフロー仮定およびアンダーフロー仮定について実行され、非オーバーフロー仮定についてプロパティ「この変数はｚと等しい」を伝搬する。
【００５２】
Ｃ．乗算
固定小数点飽和乗算（１６ビットから３２ビットへ）の実装を検討されたい。
１：  ＃ｄｅｆｉｎｅ  ＭＡＸ３２  （０ｘ８０００００００）
２：  ｉｎｔ  ｍｕｌｔ＿ｓａｔ  （ｓｈｏｒｔ  ｘ，  ｓｈｏｒｔ  ｙ）  ｛
３：    ｉｎｔ  ｚ  ＝  ｘ  ＊  ｙ；
４：    ｉｆ  （ｚ  ＝  ０ｘ４０００００００）  ｛
５：      ｚ  ＝  ＭＡＸ３２；
６：    ｝
７：    ｅｌｓｅ  ｛
８：      ｚ  ＝  ２  ＊  ｚ；
９：    ｝
１０：    ｒｅｔｕｒｎ  ｚ；
１１：  ｝
【００５３】
実際には、より一般的なイディオムは、「ｋによってシフトされる乗算」のイディオムである。
１：  ＃ｄｅｆｉｎｅ  ＭＡＸ３２  （０ｘ８０００００００）
３：  ＃ｄｅｆｉｎｅ  ｋ  （……）
２：  ｉｎｔ  ｍｕｌｔ＿ｓａｔ＿ｋ  （ｓｈｏｒｔ  ｘ，  ｓｈｏｒｔ  ｙ）  ｛
３：    ｉｎｔ  ｚ  ＝  ｘ  ＊  ｙ；
４：    ｉｆ  （ｚ  ＝＝  ０ｘ４０００００００）  ｛
５：      ｚ  ＝  ＭＡＸ３２；
６：    ｝
１０：    ｒｅｔｕｒｎ  （ｚ  ＞＞  （ｋ−１））；
１１：  ｝
これによって、３２−ｋビットの固定小数点数として表される、ｘおよびｙの積が計算される。通常、ｋ＝１６である。
【００５４】
オーバーフローが発生する時にどの値が割り当てられるかを判定するために、単純に、
Ｖ（ｅ０，ｘ）＝０ｘ８０００
Ｖ（ｅ０，ｙ）＝０ｘ８０００
Ｖ（ｅ０，ｚ）＝０ｘ４０００００００
で定義される追加マッピングを伴う定数伝搬を実行する。
【００５５】
オーバーフローが発生しない時にどの値が割り当てられるかを判定するために、ある変数がどの定数（存在する場合に）と等しいか、その変数がどの定数と等しくないことがわかっているか、およびある変数にｘ、ｙ、およびｚからのビットの範囲が含まれるかどうかを記憶する。この場合の値格子は、積
Λ＝Ｃ×Ｃ×Γ
であり、ここで、格子Γは、例Ａと同一の意味を有する。格子Γは、ビット範囲を記憶するのに使用される。Ｃは、定数伝搬に一般に使用される格子である。Ｃ格子は、Ｃと同一の要素を含むが、反転された意味を有し、変数ａは、ｃｏｎｓｔ∈Ｃと絶対に等しくないことが既知の場合に、その定数を割り当てられる。
【００５６】
この算術演算の解釈は、単純である。特殊な事例を考慮して、比較の解釈のルールを定義しなければならない。等価ｃｍｐｅｑテストは、次のルールを介して解釈される。
【数１１】
2008510230.tif 000012
類似するルールが、他の比較について定義される。乗算に関する特殊なルールは、
ｍｕｌ（＜０ｘ８０００，＿，＿＞，＜＿，０ｘ８０００，＿＞）＝＜＿，０ｘ４０００００００，＿＞
である。すなわち、０ｘ８０００に０ｘ８０００以外の何かをかける場合には、絶対に０ｘ４０００００００を得ることができない。
【００５７】
＜０，０，＿＞などの矛盾した表現を作成しないようにするために、特殊な事例をも考慮しなければならず、Ｃの要素とＣの要素の両方に定数がセットされたタプルは絶対に作成してはならない。後者に定数がセットされる場合には、前者に⊥をセットする。
【００５８】
分析を単純にするために、シフトされた飽和乗算の定義を３つの場合に分割するが、そのうちの２つは、非オーバーフロー条件を扱い、次のパターン関数を与える。
【数１２】
2008510230.tif 000013
【００５９】
第１の場合では、抽象解釈は、候補エッジでのｘの初期値を＜⊥，０ｘ８０００，ｘ０，０，１５＞として実行される。第２の場合では、類似する格子値が、ｙに与えられる。両方の場合で、ウィットネスｚには、＜⊥，０ｘ４０００００００，ｚ０，０，３１＞が割り当てられる。第３のオーバーフローの場合では、割当
Ｖ（ｅ０，ｘ）＝＜０ｘ８０００，⊥，ｘ０，０，１５＞
Ｖ（ｅ０，ｙ）＝＜０ｘ８０００，⊥，ｘ０，０，１５＞
Ｖ（ｅ０，ｚ）＝＜０ｘ４０００００００，⊥，ｚ０，０，３１＞
から開始する。
【００６０】
Ｄ．キャリーを伴う加算
加算演算ｚ＝ｘ＋ｙおよびキャリーイン変数ｃｉｎを与えられて、キャリーアウト・ビットを保持する変数を識別する。加算の結果を識別することは、非常に単純であり、グローバル値番号付けを使用して、ｚ＋ｃｉｎを保持する変数を識別する。以前のプログラム分析（範囲伝搬など）に基づき重要な仮定は、ｃｉｎ∈｛０，１｝であることである。例は、次の通りである。
１：  ｉｎｔ  ａｄｄｃ（ｉｎｔ  ｘ，  ｉｎｔ  ｙ，
２：                    ｉｎｔ  ｃ＿ｉｎ，  ｉｎｔ  ＊ｐ＿ｃ＿ｏｕｔ）  ｛
３：    ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
４：    ｉｎｔ  ｃ＿ｉｎｔｅｒｎａｌ；
５：    ｉｎｔ  ｃ＿ｏｕｔ；
６：    ａｓｓｅｒｔ（ｃ  ＝＝  ０  ｜｜  ｃ  ＝＝  １）；
７：    ｉｆ  （（ｘ  ＜  ０）  ＆＆  （ｙ  ＜  ０））  ｛
８：      ｃ＿ｉｎｔｅｒｎａｌ  ＝  １；
９：    ｝
１０：    ｅｌｓｅ  ｉｆ  （ＭＩＮ３２  ＆  （（ｘ  ＾  ｙ）  ＆  〜ｚ））  ｛
１１：      ｃ＿ｉｎｔｅｒｎａｌ  ＝  １；
１２：    ｝
１３：    ｅｌｓｅ  ｛
１４：      ｃ＿ｉｎｔｅｒｎａｌ  ＝  ０；
１５：    ｝
１６：    ｉｆ  （ｚ  ＝＝  ０ｘＦＦＦＦＦＦＦＦ）  ｛  ｃ＿ｏｕｔ  ＝  ｃ＿ｉｎ；  ｝
１７：    ｅｌｓｅ  ｛  ｃ＿ｏｕｔ  ＝  ｃ＿ｉｎｔｅｒｎａｌ；｝
１８：    ＊ｐ＿ｃ＿ｏｕｔ  ＝  ｃ＿ｏｕｔ；
１９：    ｒｅｔｕｒｎ  （ｚ  ＋  ｃ＿ｉｎ）；
２０：  ｝
【００６１】
キャリーアウト・ビットのパターン関数を定義するために、まず、
【数１３】
2008510230.tif 000014
として「キャリー・インターナル」ビットを定義する。これは、余分のキャリーイン・ビットなしの、加算＄ｚ＝ｘ＋ｙ＄のキャリーアウト・ビットである。キャリーイン・ビットが存在する場合には、キャリーアウト関数は、
【数１４】
2008510230.tif 000015
として定義される。
【００６２】
これは、パターン関数である。キャリーアウト計算を検出するために、前のセクションのプロセスの一部を再利用する。抽象解釈は、仮定
ｚ＝０ｘＦＦＦＦＦＦＦＦ
ｚ≠０ｘＦＦＦＦＦＦＦＦ
の下で実行される。「定数と等しい」および「定数と等しくない」情報を伝搬する必要がある。ここでは、飽和乗算の検出のために導入したＣ格子およびＣ格子を利用する。ＣａｒｒｙＩｎｔｅｒｎａｌの計算を検出するが、このＣａｒｒｙＩｎｔｅｒｎａｌは、符号ビットσｘ、σｙ、およびσｚとキャリーイン・ビットｃｉｎとのブール述部である。これに関して、Φ３２を利用する。全体的に、値格子は、∧＝Ｃ×Ｃ×Φ３２である。
【００６３】
条件ｚ＝０ｘＦＦＦＦＦＦＦＦが、ｘおよびｙが異なる符号を有しなければならないことをも暗示することを観察されたい。したがって、第１の場合の抽象解釈は、仮定
【数１５】
2008510230.tif 000016
の下で実行される。候補エッジでは、変数ｚが、格子値
Ｖ（ｅ０，ｚ）＝＜０ｘＦＦＦＦＦＦＦＦ，，⊥，＜１，１，…，１＞＞
を割り当てられる。ｚ≠０ｘＦＦＦＦＦＦＦＦ仮定を実施するためには、ｚに初期格子値
Ｖ（ｅ０，ｚ）＝＜⊥０ｘＦＦＦＦＦＦＦＦ，＜σｚ，⊥，…，⊥＞＞
を割り当てる。
【００６４】
Ｅ．算術シフト計算。
ＡＮＳＩ  Ｃ標準規格は、第１オペランドが符号付き型である時に、右シフト演算子「ｘ＞＞ｙ」が左からどのビットを持ち込むかを定義していない。問題は、この演算子がｘの符号ビットまたはゼロのどちらを持ち込むかである。第１の場合に、これを「算術シフト」と呼び、第２の場合に「論理シフト」と呼ぶ。
【００６５】
次が、算術シフトの２つのポータブル実装である。
ｉｎｔ  ａｒｉｔｈ＿ｓｈｉｆｔ＿１  （ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｆ  （ｙ  ＜  ０）  ｛
ｒｅｔｕｒｎ  ｘ  ＜＜  （−ｙ）；
｝
ｅｌｓｅ  ｉｆ  （ｙ  ＞＝  ３１）  ｛
ｒｅｔｕｒｎ  （ｘ  ＜  ０）  ？  −１  ：  ０；
｝
ｅｌｓｅ  ｛
ｉｎｔ  ｚ  ＝  （ｘ  ＞＞  ｙ）；
ｉｎｔ  ｔ  ＝  （１  ＜＜  （３１  −  ｙ））；
ｉｆ  （ｚ  ＆  ｔ）  ｛
ｚ  ＝  ｚ  ｜  （０ｘＦＦＦＦＦＦＦＦ  ＜＜  （３２  −  ｙ））；
｝
ｒｅｔｕｒｎ  ｚ；
｝
｝
ｉｎｔ  ａｒｉｔｈ＿ｓｈｉｆｔ＿２  （ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｆ  （ｙ  ＜  ０）  ｛
ｒｅｔｕｒｎ  ｘ  ＜＜  （−ｙ）；
｝
ｅｌｓｅ  ｉｆ  （ｙ  ＞＝  ３１）  ｛
ｒｅｔｕｒｎ  （ｘ  ＜  ０）  ？  −１  ：  ０；
｝
ｅｌｓｅ  ｛
ｉｆ  （ｘ  ＜  ０）  ｛
ｒｅｔｕｒｎ  〜（〜ｘ  ＞＞  ｙ）；
｝
ｅｌｓｅ  ｛
ｒｅｔｕｒｎ  ｘ  ＞＞  ｙ；
｝
｝
｝
（ａ）変数が、ｙにおいて線形の量だけシフトされることと、（ｂ）ｐ（ｙ）がｙの線形関数である場合に、ほとんどの値が、２つのビット範囲［０：ｐ（ｙ）］および［ｐ（ｙ）＋１，３１］に分割されることとを観察されたい。２つのビット範囲の値は、定数またはおそらくは反転されたｘの部分範囲のいずれかである。
算術シフトの定義を５つの場合に分割する。
（ｘ＜＜（−ｙ））  ｙ＜０の場合
−１                ｙ≧３１∧ｘ＜０の場合
Ｓｈｒａ（ｘ，ｙ）＝０                  ｙ≧３１∧ｘ≠０の場合￥
（ｘ＞＞ｙ）        ０≦ｙ≦３０かつｘ≧０の場合
¬（¬ｘ＞＞ｙ）    ０≦ｙ≦３０かつｘ＜０の場合
（上の式の「ネイティブ」右シフト演算子の符号拡張挙動は、無関係である）。
【００６６】
上の５つの場合のそれぞれについてどのステートメントが実行されるかを判定するために、範囲と「定数と等しい」プロパティおよび「定数と等しくない」プロパティとを伝搬する。どの変数がｘ＜＜（−ｙ）、−１、０、ｘ＞＞ｙ、または¬（¬ｘ＞＞ｙ）と等しいかを判定するために、グローバル値番号付けを実行する。前に導入した値格子または成熟したコンパイラで実装されると期待される値格子のいずれかを再利用していることを観察されたい。
【００６７】
本方法は、アイデンティティが認識された時に演算子のソフトウェア実装について使用可能な場合に、コンパイラがハードウェア実装を置換することを可能にする。関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、使用可能な関数ｆ（ｘ，ｙ，…）によって、命令の呼出しｔ＝ｆ（ｘ，ｙ，…）を追加し、各ステートメントｓでの変数ｖへの各参照を、ｓでのｖの値がｆ（ｘ，ｙ，…）と等しくなるように、ｔへの参照に置換することとによって計算されるようにするために、プログラムを変換することができる。プログラム変換の後に未使用の命令は、デッドコード除去によって除去される。数学関数ｆ（ｘ，ｙ，…）が、ハードウェアで計算可能である場合には、関数ｆ（ｘ，ｙ，…）の値をとる各変数ｖの値が、ｆ（ｘ，ｙ，…）に使用可能なハードウェア命令によって計算されるようにするために、プログラムを変換することができる。
【００６８】
飽和算術演算の自動認識のための上の技法は、かなり少ないコンパイル時オーバーヘッドを有する。さらに、これらの技法は、かなり異なるイディオムを使用して表された時であっても、基礎になる飽和算術演算を認識するという点で、かなり一般的である。この手法の一般性は、構文的パターン一致を行うのではなく、基礎になる意味論的概念が系統的な形で活用されるという事実から生じる。さらに、抽象解釈は、アドホックな形ではなく、系統的な形でのこの推論の適用を可能にする。適当な意味論的要素が判定され、格子が構成されたならば、各演算の解釈を系統的に判定することができる。
【００６９】
本発明を詳細に説明し、図示したが、これが、例示および例のみとして行われ、限定として解釈されてはならないことを明瞭に理解されたい。本発明の範囲は、添付の特許請求の範囲の言葉によってのみ限定される。
【図面の簡単な説明】
【００７０】
【図１】本開示の原理を組み込んだ方法の第１の実施形態を示す流れ図である。
【図２】本開示の原理を組み込んだ方法の第１の実施形態を示す流れ図である。
【図３】図およびデータ・フローのグループを示す図である。
【図１】
2008510230.tif 000017
【図２】
2008510230.tif 000018
【図３】
2008510230.tif 000019