Stefan Bygde：「抽象解釈とエレメントのカウントに基づく
静的WCET(*)解析（STATIC WCET ANALYSIS BASEDON ABSTRACT INTERPRETATION AND COUNTINGOF ELEMENTS )」の概要(*) WCET：Worst-Case Execution Time
（最悪実行時間）

２０１６年４月
作成：舟越 和己1

原論文と本資料の目次の対応
原文の目次

本資料の目次１．序論
２．背景と関係する研究
３．フレームワーク
３．１ プログラムのシンタックス
３．２ プログラムのセマンティクス
３．３ トレースセマンティクス
３．４ コレクティングセマンティクス
３．５ 制御変数
３．６ 不動点理論
３．７ 抽象解釈
３．８ 静的解析の抽象解釈
３．９ 抽象ドメイン
３．１０ フレームワークの概要
４．ループ限界の発見
５．合同ドメイン
６．パラメトリックWCET解析
７．最小伝播アルゴリズム

１．要旨から
２．WCET解析とは？
３．プログラムのシンタックスとセマンティクス
４．プログラムのWCETの計算概要
５．制御変数とプログラムスライシング
６．静的解析の抽象解釈
７．ループ限界の発見
７．１ ループ限界解析とは？
７．２ ループ不変変数
７．３ 限定されたwidening
７．４ ループ限界解析の抽象解釈
７．５ 抽象環境でのエレメントのカウント
７．６ 合同抽象ドメイン
７．７ 合同抽象ドメインによる抽象解釈
７．８ 抽象ドメインの直積
７．９ 区間と合同ドメインの直積による抽象解釈
７．１０ 直積ドメインでのエレメントのカウント
2

1. 要旨から・リアルタイムシステムでは、システムの全てのタスク
がデッドラインを保証することが重要です。
・全てのタスクがデッドラインを保つことを確実にするためには、これらのタスクの最悪実行時間（Worst-Case
Execution Time：WCET）を知る必要があります。
・これはタスクの実行時間を測定することにより行うことができますが、これは手間がかかり、しかも一般的には安全ではありません（すなわち、最悪のケースが見つからないかもしれません）。
・タスクは全ての可能な入力の組合せや構成で測定されないので、最長の測定時間が実際に本当の最悪ケースに対応することを保証する方法はありません。
3

２．WCET解析とは？

4

2.1 最悪実行時間(WCET)解析とは？(1)・WCET解析は大まかに静的WCET解析と動的WCET解析という２つの手法に分けることができます。
・動的WCET解析は対象のプロセッサ（又はシミュレータ）で実行プログラムの端から端までの測定を実行することにより行われます。
・これは十分なカバレージを保証するために非常に広範な測定、あるいはプログラムに最悪のパスを実行させようとする試みを要求しますが、これらは非常に困難です。
・動的解析は一般に、最悪ケースが実際に見つかることを保証することはできません。従って、それはWCETの過小評価になるでしょう。
52.1 最悪実行時間(WCET)解析とは？(2)・もう一つのアプローチは、プログラムコードとその可能な入力データ及びハードウェアのモデルを静的に解析する
ことによりプログラムのWCETの安全な上界を計算する
静的WCET解析です。
・静的WCET解析は安全な上界（すなわち、少なくとも真のWCETよりは大きい）を与えるために不確実なケースに対し悲観的な仮定を行う必要があります。

→この論文では、静的WCET解析について議論します。

6

2.1 最悪実行時間(WCET)解析とは？(3)・図１．１は、測定された実行時間、解析された実行時間、
そして実際のWCETの間の関係を図示しています。
・図はまた、最良実行時間を意味するBCET(Best-Case
Execution Time)との関係も示しています。実行時間の上界(upper timing bound)と下界(lower timing bound)は各々WCETとBCETの安全な見積もりです。

図１．１ 実行時間と解析結果の関係
7

2.2 静的WCET解析の構成と概要(1)
WCET解析は３つの独立なフェーズに分割できます；・１つのフェーズはソフトウェアを解析（フロー解析）・もう一つのフェーズはハードウェア
を解析（下位レベル解析）
・最後のフェーズはWCETの見積りを計算するためにそれらの解析結果を結合します（計算）。
図２．１は解析フェーズがどのように関係しているかを示しています。
図２．１ 解析フェーズ間の関係
8

2.2 静的WCET解析の構成と概要(2)■フロー解析の概要
フロー解析、または上位レベル解析はプログラムのソース又はオブジェクトコードを解析します。このプロセスのゴールはプログラムフロー上で制約を見つけ、プログラムの様々なパーツの実行カウントの限界を見つけることです。
フロー解析の中の重要な機能には、①ループ限界解析(Loop Bound Analysis)②実行不可能なパスの検知(Infeasible Path Detection)があります。

9

2.2 静的WCET解析の構成と概要(3)①ループ限界解析(Loop Bound Analysis)
プログラムは多くの実行時間をループで費やすので、
ループの繰り返しに対する上界を見つけることが重要。
ここで紹介される解析手法は、論文[ESG+07](*)でアウトラインを示された手法で、抽象解釈、スライシング、
不変解析技術を使用してループの可能な意味論的状態をカウントすることに基づいています。
(*) Andreas Ermedahl, Christer Sandberg, Jan Gustafsson, Stefan Bygde,
and Bjorn Lisper. Loop bound analysis based on a combination of program
slicing, abstract interpretation, and invariant analysis. In Christine Rochange,
editor, Proc. 7th International Workshop on Worst-Case Execution Time Analysis(WCET’2007), Pisa, Italy, July 2007.

10

2.2 静的WCET解析の構成と概要(4)②実行不可能なパスの検知(Infeasible Path Detection)
フロー解析の目的は、正確なWCET限界を与えることができるように出来るだけ多くの正確なフローを求めることです。従って、意味制約によれば起こり得ないパスを見つけることはWCET解析の悲観論を減少させるために有効です。簡単な例として下記のコードを考えます；
このコードは文1と文2を両方共に実行することはあり
ません。

11

2.2 静的WCET解析の構成と概要(5)■下位レベル解析の概要
・下位レベル解析はハードウェア・プラットフォームの数学的モデル(パイプライン、キャッシュ、分岐予測など)を解析します。モデルは出来るだけ詳細であるべきです
が、それは控え目にしなければなりません。
・例えば、キャッシュのヒットは静的に決定することが不可能なので、キャッシュ・ヒットよりもキャッシュ・ミスを仮定するなど。
・下位レベル解析の目的はプログラムの原子的部分に対して最悪の実行時間を導くことです。プログラムの原子的部分は、プログラムの命令、プログラムの基本ブロックなどです。
12

2.2 静的WCET解析の構成と概要(6)■計算の概要・フロー解析からフローの事実が導かれ、低レベル解析
により原子最悪実行時間が計算されたとき、それらの結果はWCETの具体的な限界を得るために計算フェーズ
で結合することができます。
・計算フェーズでは、下記の解析手法が使われます；◆暗黙のパス列挙手法(IPET：Implicit Path Enumeration
Technique)：現実のサイズのプログラムのパスの数は非常に大きくなるので、最悪ケースのパスを見つけることは困難です。
その代り、IPETの概念はフローの制約と原子コストを整数線形計画(ILP：Integer Linear Programming)問題として定式化することです。これはフロー解析から得られた制約に関しコスト関数を最大化することにより行われます。
13

３．プログラムのシンタックスとセマンティクス14

3.1 プログラムのシンタックス(1)定義１．プログラムP= <VP , QP , νP > は、フローチャートで表されるソフトウェアとします。
・集合VP は図３．１のようなフローチャートのノード(node)の集合。
・集合QP ⊆VP×VP はフローチャートの弧(arc)の集合で、これはプログラムポイントとも言われます。
・集合νP はプログラムの変数の集合を表します。

図３．１ フローチャートのノード

153.1 プログラムのシンタックス(2)全てのプログラムは単一の入口と出口を持つと仮定します。
例として、プログラム
L= <VL , QL , νL > = < VL , {q0 , q1 , q2 , q3 , q4 , q5 }, { i, n } >は図３．２に描かれています。

図３．２ サンプルプログラムL
16

3.2 プログラムの入力パラメータ
定義２．プログラムは入力パラメータの集合InPを持つと仮定します。
ここでInPはプログラムPのフローに影響を与える値の集合です。
解析するプログラムのタイプに依存して、入力パラメータは異なるものを意味します。
・解析される対象が関数ならば、入力パラメータは関数の引数の値に対応します。
・プログラムのコンポーネントの場合、コンポーネントの入力ポートのデータに対応します。
・プログラムのループの場合、入力パラメータは与えられたループの限界に対応します、等。
例として、図３．２のプログラムを考えます。ここで、nの初期値はプログラムLの入力パラメータです。従って、InP = { n0 }です。
17

3.3 プログラムの環境と状態(1)■プログラムのセマンティクスは、プログラムの実行時の状態を記述します。そのために、プログラムの「環境(environment)」と「状態(state)」を定義します。
定義３．（ここでは変数は全て整数値で考えているので）プログラムPの環境とは、プログラムの変数の集合νP から整数の集合Zへの関数
σP : νP → Zです。言い換えると、環境は全ての変数に対して整数を割当てること（代入）です。プログラムPの全ての環境の集合はΣP で表されます。
定義４．プログラムPの状態s=< q, σ> ∈ QP ×ΣP は、環境に関係したプログラムポイントです。状態の集合QP ×ΣP はSP で表されます。
18

3.3 プログラムの環境と状態(2)■環境と状態の例
InP = { i=i0, n=2 } ：初期パラメータ
右のサンプルプログラムLには２つの変数 i, nがあります(n=2固定）。
従って、プログラムLの変数の集合νL = { i, n }となり、
環境σL : νL → Z はプログラムの進行によりその値が変化します。
これはプログラムの状態< q, σL>として具体的に示すことができます。
<q0 , [i→i0][n→2] >, <q1 , [i→0][n→2] >, ・・・
環境σL

19

3.4 プログラムのセマンティクス関数
定義５．プログラムPのセマンティック関数τPとは、状態から状態への写像です。
■セマンティック関数はプログラムの意味を定義します。すなわち、フローチャートの各ノードが現在の状態に何を行うかをフォーマルに定義します。
■セマンティック関数によりプログラムの実行時の状態の変化を表す方法に「トレースセマンティクス」と「コレクティングセマンティクス」
があります。
（WCETとして重要なのはコレクティングセマンティクスです）

20

3.5 トレースセマンティクス(1)■トレースセマンティクス
・プログラムのトレースT(s)とは、状態sが遷移する列です。状態sがs0→s1→s2→・・・と遷移するとき、これをT(s) = s0 s1 s2 ・・・ （T(s) = s0 , s1 , s2 ,・・の様に”,”を付けても良い）というシーケンスで表記します。
τを１つの状態から他の状態への写像とし、s0 s1・・・がトレースのとき、そのエレメントsj は
sj = τ( sj-1 )(j≧1)
として定義されます。
（例） ３．３(2)の例では、
s0=<q0 , [i→i0][n→2] > s1=<q1 , [i→0][n→2] >・・・

・トレースセマンティクスは（初期の状態から出発する）プログラムの全ての可能なトレースの集合として定義されます。
21

3.5 トレースセマンティクス(2)■トレースセマンティクスの例（P. Cousot : 「抽象解釈の非公式な概要」より）
下の図は、プログラムの状態の遷移をトレースとして時間的に表現したもの。トレースが色分けされているのは、初期条件により可能なトレースが複数存在するため。

22

3.5 トレースセマンティクス(3)■トレースセマンティクスの説明（P. Cousot : 「形式手法に基づく抽象解釈と将来への挑戦」より）
プログラムの可能な計算は、プログラムの実行が進展するとき
マシンの状態の進化を表すトレースによりモデル化される。
・有限のトレースによりモデル化される有限の実行は、長さ|σ|=nの状態の有限のシーケンスσ=σ0・・・σn-1である。
・終了しない実行は、(長さ|σ|=∞の)状態の無限のシーケンス
σ=σ0σ1・・・である無限のトレースによりモデル化される。
→これを図示すると、下のように表現される；

23

3.5 トレースセマンティクス(4)■トレースセマンティクスの例（サンプルプログラムL）
初期パラメータとしてi=i0, n=2の場合を考えます；
InP = { i=i0, n=2 } ：初期パラメータ
このときのトレースは次のように
なります；

24

3.5 トレースセマンティクス(5)■サンプルプログラムLでnの値を変えると別のトレースになります。
例えば、初期パラメータとしてi=i0, n=1の場合、
InP = { i=i0, n=1 } ：初期パラメータ
このときのトレースは次のように
なります；
Trace
<q0 , [i→i0][n→1] ><q1 , [i→0][n→1] ><q2 , [i→0][n→1] ><q4 , [i→0][n→1] ><q5 , [i→1][n→1] ><q2 , [i→1][n→1] ><q4 , [i→1][n→1] ><q5 , [i→2][n→1] ><q2 , [i→2][n→1] ><q3 , [i→2][n→1] >25

3.6 コレクティングセマンティクス(1)-1 Rev.
■コレクティングセマンティクスの定義
コレクティングセマンティクスとは、プログラムの任意の実行により生じる「状態の集合」です。(The set of states which may occur during
any execution of a program is known as the collecting semantics)●：状態(status)

Collecting semantics■プログラムPの状態の集合Sの関数CSP
CSP(S)=S∪{τP(s) | s ∈S}∪IP ・・・(1)
ここで、IPはプログラムPの初期状態の集合→ CSPは、状態の集合Sを(IPを含む)次の状態の集合に移す関数
τPはプログラムのある時点の状態を次の時点の状態に移す関数であり、これを「セマンティック関数(semantic function)」と言います。
26

3.6 コレクティングセマンティクス(1)-2 Rev.
■関数CSPの性質
SがプログラムPを実行したときに生じる全ての状態に一致（すなわち、Sがコレクティングセマンティクスである）
ことと、
S=CSP(S)が成立すること（即ち、CSPの不動点）とは同じです。
従って、プログラムPのコレクティングセマンティクスは
関数CSPの不動点(fix point)として特徴付けることができます。
すなわち、CSPの不動点をfixCSPとすると、コレクティングセマンティクス=fixCSP

27

3.6 コレクティングセマンティクス(2) Rev.
■コレクティングセマンティクス構成の例（P. Cousot : 「抽象解釈の
非公式な概要」より）→図のように、状態を纏めて遷移させている。

IP
式(1)でS=IPとすると、CSP(CSP(IP)）
CSP(IP)=IP∪{τP(s) | s∈IP}∪IP =CSP(IP)∪{τP(s)|s∈CSP(IP)}∪IP= IP∪{τP(s) | s∈IP}
関数CSPにより初期状態の集合IPから出発して状態の集合の遷移の単調増大列
IP⊆CSP(IP)⊆CSP2(IP)⊆CSP3(IP)⊆・・・が出来ます。この列の上限をSとすると、Sに関数CSPを作用させても不変です。
すなわち、S=CSP(S)
このSがプログラムPの全ての状態集合、すなわちコレクティングセマンティクスです。

28

3.6 コレクティングセマンティクス(3) Rev.
■コレクティングセマンティクスの作り方の例
サンプルプログラムLでn=1, 2としたとき２つの遷移ができます
が、コレクティングセマンティクスはこれらの状態の集合です。
InP = { i=i0, n=1, n=2 } ：初期パラメータ
コレクティングセマンティクス{ <q0 , [i→i0][n→1]>, <q0 , [i→i0][n→2]> ,<q1 , [i→0][n→1]>, <q1 , [i→0][n→2]> ,<q2 , [i→0][n→1]>, <q2 , [i→0][n→2]> ,<q4 , [i→0][n→1]>, <q4 , [i→0][n→2]> ,<q5 , [i→1][n→1]>, <q5 , [i→1][n→2]> ,<q2 , [i→1][n→1]>, <q2 , [i→1][n→2]> ,<q4 , [i→1][n→1]>, <q4 , [i→1][n→2]> ,<q5 , [i→2][n→1]>, <q5 , [i→2][n→2]> ,<q2 , [i→2][n→1]>, <q2 , [i→2][n→2]> ,<q3 , [i→2][n→1]>, <q4 , [i→2][n→2]> ,<q5 , [i→3][n→2]>,<q2 , [i→3][n→2]>,<q3 , [i→3][n→2]> }29

４．プログラムのWCETの計算概要30

4.1 プログラムの原子WCET(1)・ここでは主にフロー解析に焦点を当てますが、現実的な時間を見積もるためのWCET解析のためには、低レベルの解析が必要です。しかし、低レベルの解析は決して自明ではありません。
・そこで、ここでは低レベルの解析が存在し、それがプログラムの各原子部分（ノード）に対して最悪実行時間を提供すると仮定します。 これを原子WCETと言います。
・具体的には、低レベル解析の結果は各プログラムポイントに対して原子WCETを関係させる関数となります；

この関数ｌ(エル）の値はミリセカンドやクロックサイクルなどです。

31

4.1 プログラムの原子WCET(2)■原子WCETの例（サンプルプログラムL）
右のフローで、各プログラムポイントと対応する原子部分とその原子WCETを
q0⇔初期値設定=1q1⇔i:=0（代入処理）=3
q2⇔結合ノード（結合処理）=1
q4 , q3⇔i<=n（分岐処理）=2
q5⇔i:=i+1（代入処理）=8とすると、関数ｌ(エル）は下記と
なります。

32

4.2 トレースセマンティクスによるWCET計算■前頁で与えられた原子WCETの値をコストとしてトレースの各通過点に与えると、トレース実行によるWCETは通過点に与えられたコストの累積値として求まります(n=2とした場合）。

33

4.3 トレースセマンティクスによるWCET計算の問題点■前頁のように、トレースセマンティクスによるWCET計算は、データの入力値により発生するトレースを全て調べて、その中で最悪の実行時間を求めることになるので現実的ではありません（起こり得るすべてのトレースに対して計算することになる）。
また、トレース自身も有限であるとは限りません。
■一方、コレクティングセマンティクスは起こり得るすべての状態を含んでいるので、これに対するWCET計算を次頁以降で考えます。

34

4.4 コレクティングセマンティクスによるWCET計算(1)Rev.
■プログラムPのコレクティングセマンティクスfixCSp（という状態の集合）をプログラムポイントqにより分割した集合、すなわち、CSqp = プログラムポイントがq となるfixCSpの要素の集合を考えます。
このとき、CSqpの要素の数を |CSqp| とすると、|CSqp| = プログラムPの任意のトレースでプログラムポイントがqとなる状態の数の上限値となります。
→次頁の例で説明（厳密な証明は省略）。
35

4.4 コレクティングセマンティクスによるWCET計算(3) Rev.
■３．６(5)の例では、CSqLは次のようになります；
fixCSL={ <q0 , [i→i0][n→1]>, <q0 , [i→i0][n→2]> ,<q1 , [i→0][n→1]>, <q1 , [i→0][n→2]> ,<q2 , [i→0][n→1]>, <q2 , [i→0][n→2]> ,<q4 , [i→0][n→1]>, <q4 , [i→0][n→2]> ,<q5 , [i→1][n→1]>, <q5 , [i→1][n→2]> ,<q2 , [i→1][n→1]>, <q2 , [i→1][n→2]> ,<q4 , [i→1][n→1]>, <q4 , [i→1][n→2]> ,<q5 , [i→2][n→1]>, <q5 , [i→2][n→2]> ,<q2 , [i→2][n→1]>, <q2 , [i→2][n→2]> ,<q3 , [i→2][n→1]>, <q4 , [i→2][n→2]> ,<q5 , [i→3][n→2]>,<q2 , [i→3][n→2]>,<q3 , [i→3][n→2]> }CSq0L={<q0 , [i→i0][n→1]>, <q0 , [i→i0][n→2]> }CSq1L= {<q1 , [i→0][n→1]>, <q1 , [i→0][n→2]> }CSq2L= {<q2 , [i→0][n→1]>, <q2 , [i→0][n→2]> } ,{<q2 , [i→1][n→1]>, <q2 , [i→1][n→2]> } ,{<q2 , [i→2][n→1]>, <q2 , [i→2][n→2]> } ,{<q2 , [i→3][n→2]> } ,CSq4L= {<q4 , [i→0][n→1]>, <q4 , [i→0][n→2]> } ,{<q4 , [i→1][n→1]>, <q4 , [i→1][n→2]> } ,{<q4 , [i→2][n→2]> }CSq5L={<q5 , [i→1][n→1]>, <q5 , [i→1][n→2]> } ,{<q5 , [i→2][n→1]>, <q5 , [i→2][n→2]> } ,{<q5 , [i→3][n→2]> } ,CSq3L= {<q3 , [i→2][n→1]> } ,{<q3 , [i→3][n→2]> }各要素の数は、|CSq0L|=1, |CSq1L|=1, |CSq2L|=4, |CSq4L|=3, |CSq5L|=3, |CSq3L|=2となります。

36

4.4 コレクティングセマンティクスによるWCET計算(4) Rev.
一方、プログラムL任意のトレースは青、赤の２ラインなので、
Trace<q0 , [i→i0][n→1] ><q1 , [i→0][n→1] ><q2 , [i→0][n→1] ><q4 , [i→0][n→1] ><q5 , [i→1][n→1] ><q2 , [i→1][n→1] ><q4 , [i→1][n→1] ><q5 , [i→2][n→1] ><q2 , [i→2][n→1] ><q3 , [i→2][n→1] >青のトレースでプログラム
ポイントが・q0となる状態の数=1・q1となる状態の数=1・q2となる状態の数=4・q4となる状態の数=2・q5となる状態の数=3・q3となる状態の数=2
赤のトレースでは・q0となる状態の数=1・q1となる状態の数=1・q2となる状態の数=4・q4となる状態の数=3・q5となる状態の数=3・q3となる状態の数=1

両方の結果の大きい方の値を取ると、・q0となる状態の数=1 ・q1となる状態の数=1 ・q2となる状態の数=4 ・q4となる状態の数=3・q5となる状態の数=3 ・q3となる状態の数=1となり、「 |CSqL|=プログラムLの任意のトレースでプログラムポイントがqとなる状態の数の上限値」が成立します。
37

4.4 コレクティングセマンティクスによるWCET計算(5) Rev.
■全てのトレースは有限トレースであるという制限内でコレクティングセマンティクスを考えたとき、|CSqP|が原子WCETの繰り返し回数なので、プログラムPのWCETPの上限は各プログラムポイントqに対応する原子WCET=を使用してと表すことができます。
→次頁にトレースが２個（状態の集合が２個以内の要素）の場合の例を示します。

38

4.4 コレクティングセマンティクスによるWCET計算(6) Rev.
■コレクティングセマンティクスのCSqの例（サンプルプログラムL）
サンプルプログラムLでn=1, 2としたとき
CSqは次のようになります；
InP = { i=i0, n=1, n=2 } ：初期パラメータ|CSq0L|=|CSq1L|=1, |CSq3L|=1, |CSq2L|=4,|CSq4L|=|CSq5L|=3なので、= l(q0)*1+l(q1)*1+l(q2)*4+l(q4)*3+l(q5)*3+l(q3)*1=1*1+3*1+1*4+2*3+8*3+2*1=1+3+4+6+24+2=40

39

4.4 コレクティングセマンティクスによるWCET計算(7) Rev.
■４．４(3)より、プログラムPのWCETPの上限はと表すことができます。
しかし、この上限の式には下記の問題があります；(i) |CSqP|を効率的にかつ具体的に求める手法が示されていない。
(ii)無限ループのように無限のトレースを持つプログラムに対してもWCETを求めることができるようにしなければならない。
(iii)上限の式は、全てのプログラムポイントに対してΣを求めているが、プログラムの開始から終了までの可能なパスの中で最大のものを求めるようにしなければならない。

40

4.4 コレクティングセマンティクスによるWCET計算(8) Rev.
・(i), (ii)に対する対応策は、ループ繰り返し回数の上限値の近似を求めること(loop bound analysis)。
→抽象解釈によるその求め方の概要は、①プログラムの変数の抽象化世界でコレクティングセマンティクス
S=CS(S)の近似S〜を(widening/narrowingにより）求めます。この結果、S〜から各プログラムポイントqでの各変数の存在範囲の近似が求まります。
②ここで特にループ繰り返し変数に着目するとその上限値の近似（すなわち、ループ処理の繰り返し回数の近似）が得られます。
→WCET計算で必要な「抽象解釈の結果の情報」はループ処理の繰り返し回数の近似値で、これに特化した解析として
ループ限界解析(Loop bound analysis)があります。
→これの詳細は次回の予定。
41

4.4 コレクティングセマンティクスによるWCET計算(9)・(iii)に対する対応策は、整数線形計画(ILP：Integer Linear
Programming)です。
→下図でノードの横の値はノードの実行時間。ILPはstart(a)からend(f)までのパスで(Σ実行時間)をMaxにする問題。

AbsIntより
42

５．制御変数とプログラムスライシング

43

５．１ 制御変数(1)■WCETの近似式の過大近似を減少させる最初のステップは、|CSqP|の計算に全ての変数を使用する必要がないことを示すことです。
■プログラムの変数は次の２種類に分けることができます；①制御変数・・・プログラムの制御フローに影響を与える変数②非制御変数・・・制御変数でない変数（例）右のフローで、・変数I はその値により制御フローの流れを変えるので、制御変数。
・変数J, K は非制御変数。

44

５．１ 制御変数(2)■制御変数と非制御変数の性質①１つのトレース内で同じプログラムポイントを持つ異なる状態は、制御変数の値を変えることにより実現される。
②同じプログラムポイントを持ち、非制御変数のみが異なる状態は、異なるトレースに属さなければならない。
pt=0（例）右のプログラムでK=1, 2を入力すると、
下記の２つのトレースになります；
pt=1①の例：青、②の例：赤 の部分
pt=2<pt=1, [K→1]><pt=1, [K→2]>→<pt=2, [K→1][I→2]>
pt=3→<pt=2, [K→2][I→2]>→<pt=3, [K→1][I→2][J→6]> →<pt=3, [K→2][I→2][J→7]>
pt=4→<pt=4, [K→1][I→2][J→6]> →<pt=4, [K→2][I→2][J→7]>→<pt=5, [K→1][I→3][J→6]> →<pt=5, [K→2][I→3][J→7]> pt=5→<pt=6, [K→1][I→3][J→9]> →<pt=6, [K→2][I→3][J→10]> pt=6→<pt=7, [K→1][I→3][J→9]> →<pt=7, [K→2][I→3][J→10]>→<pt=4, [K→1][I→3][J→9]> →<pt=4, [K→2][I→3][J→10]> pt=7→<pt=5, [K→1][I→4][J→9]> →<pt=5, [K→2][I→4][J→10]> pt=8→<pt=6, [K→1][I→4][J→12]> →<pt=6, [K→2][I→4][J→13]>→<pt=7, [K→1][I→4][J→12]> →<pt=7, [K→2][I→4][J→13]> pt=9
・・・
・・・

45

５．１ 制御変数(3)・非制御変数の性質「同じプログラムポイントqを持ち、非制御変数のみが異なる状態は、異なるトレースに属さなければならない。」
から、CSqPの要素が「非制御変数のみが異なる状態」の集合
ならば、|CSqP|=1となります。
（例）前頁の例では、
CSq3P={<pt=3, [K→1][I→2][J→6]>, <pt=3, [K→2][I→2][J→7]>}
・また、制御変数の性質「１つのトレース内で同じプログラムポイントを持つ異なる状態は、
制御変数の値を変えることにより実現される。」
から、ループ処理の|CSqP|を求める計算では制御変数のみに着目すればよいので、非制御変数は完全に無視できます。
→このことは、WCETの計算では対象のプログラムから計算に必要な部分を切り出すことが可能であることを示唆しています（これをProgram slicingと言います）。
46

５．２ プログラムスライシング(1)・プログラムスライシングは、ループの限界を見つけるために
ループの繰り返し回数と関係のない文や変数をプログラムから取り除くプロセスです。
・プログラムスライスは、（スライシング基準により）与えられた変数の集合に直接、又は間接に影響する文が取り除かれたプログラムです。
■WCET解析においては、非制御変数を取り除くためにプログラム
スライシングが使用されます。
→次頁に例

47

５．２ プログラムスライシング(2)・右のプログラムには２つのループがあります；
L1 = {q2 , q3 , q4 , q5 , q6 , q7 , q8 , q9 }L2 = {q5 , q6 , q7 }L1

ループL1では、iがループ制御変数、jが非制御変数なのでループカウントに関係する部分だけ取り出したもの
がL1のスライシングです。これはL1から{q4 , q5 , q6 , q7 , q8 }を除いたものです。すなわち、
L1のスライス={q2 , q3 , q9 }一方、ループL2では取り除くものはありません。

L248

６．静的解析の抽象解釈

49

６．１ フローチャートの弧のタイプ■右図のように、プログラムは・単一の入力ノード（開始ノード）：∇・代入ノード：・テストノード（条件付きノード）：・接合ノード→ループ接合( )と単純接合(○)
・出口ノード：∇から構成されています。これに対応して下記 q9の（ノードとノードを結ぶ）弧が定義され、各弧にはプログラムポイントqが対応します；
・開始弧(Start arc)・・・右図では、q0・代入弧(Assignment arc)・・・q1, q5, q7, q9・接合弧(Merge arc)・・・q2, q8
・条件付き弧(Conditional arc)・・・q3, q4, q6, q10

q0
q1
q2

q3

q10

q4

q6

q5

q7
q8

：プログラムポイント50

６．２ プログラムの変数の値の集合■プログラムの取り得る状態s=<q, σ>の集合をSとします。
qはプログラムポイント、σは「環境（変数の値）」なので、状態の集合Sに対してそのプログラムポイントがqとなるような「環境（変数∇の値）」の集合をS(q)で表します。
q0

例えば、右のプログラムでは、
S(q1)=(x, {0}) ・・・・ (x, {0})の意味は、x=0のこと
S(q2)は、ループ回数と共に値が増えて行きます；
q4
ループ1回目：S(q2)=(x, {0})ループ2回目：S(q2)=(x, {0, 1}) ・・・意味は、x=0, 1のこと
ループ3回目：S(q2)=(x, {0, 1, 2})
・・・

x:=0
q1

q2
X < 100
true

q3

false
q5

x:=x+151

６．３ 抽象化写像(1)■抽象解釈では、状態の環境（変数の値）部分S(q)を、抽象化写像αにより、それを含む単純な領域S^(q)に移すことを考えます（逆の写像γも定義されます）。
S(q), S^(q)が存在する領域を各々、具体ドメイン、抽象ドメインと
言います。
S(q)

α

S^(q)

＜抽象化写像の例1＞
Cを整数全体の部分集合とするとき、抽象化写像αをα( C )=[min( C ), max( C )]により定義すると、前頁の例で、「ループ3回目：S(q2)=(x, {0, 1, 2})」はS^(q2)=α((x, {0, 1, 2}))=(x, [0, 2])となります。
即ち、このαは変数xの値の集合を区間に抽象化している。
52

６．３ 抽象化写像(2)＜抽象化写像の例2＞
例１は変数がxのみの場合でしたが、変数がx, yの２次元になった場合を考えます。例えば、プログラムポイントqでS(q)が下の左図のような点に分布したとします。このとき、最も単純な抽象化は「区間の直積」です。
より正確な抽象化の例には「凸多面体（注）」による近似があります。
（注）凸多面体の定義は次頁参照。
3232S^(q)={(x, [3, 27]),(y, [4, 32])}

α
4

S(q)=

4

3

3

27

27

32

S^(q)=x, yの一次不等式群

α’
4
3

27
53

６．３ 抽象化写像(3)（注）凸多面体(convex polyhedron)とは、有限個の閉半空間の共通部分となる集合です。
ここで、閉半空間とは、「n次元実ベクトルa=(a1,・・・, an)と実数a0により定まる1次不等式 (線形不等式)
a1x1+・・・+ anxn≦a0を満たす点x=(x1,・・・, xn)全体からなる集合」のことです。

（例）２次元の凸多面体（凸多角形）-x1 + x2 ≦ 1-x2 ≦ -1
-x1 – x2 ≦ -5

多面体が凸であるとは、多面体の内部の任意の２点を結ぶ
Lineがその多面体の内部に含まれること

x2

x1

54

６．４ フローチャート上の抽象解釈■フローチャート上の抽象解釈は、フローチャートの各プログラム
ポイントに対してS^(q)を求めます。これは弧のタイプ別に求めます。
すなわち、
q0・開始弧に対してS^(q)を求める。
q1
・開始弧以外は直前のS^(q)に対してプログラムの処理
q2を実行したときのS^(q’)を求めます。
（例）代入処理の場合、入力のS^(qpre)が与えられたときの出力のS^(q)を求めます。
qpre ・・・ S^(q )
pre

q3
q9

x=e
q

・・・

S^(q)

次頁以降に、弧のタイプ別の求め方を示します。

q10

q4

q6

q5

q7
q8

：プログラムポイント55

６．５ フローチャート上の抽象解釈：開始弧■開始弧は開始ノードから出る弧です。
抽象解釈では起こり得る全ての値を想定して問題を解くので、開始弧では、変数の値は入力値の全ての可能な値を考えます。
したがって、qが開始弧ならばS^(q)=α(各変数の任意の値)となります。
（例１）プログラムの変数がxのみならば、抽象化を区間とした場合
α(xの任意の値)=(x, [-∞, +∞])
（例２）プログラムの変数がx, yならば、抽象化を区間の直積とした場合
α(x, yの任意の値)={(x, [-∞, +∞]), (y, [-∞, +∞])}

56

６．６ フローチャート上の抽象解釈：代入弧 (1)■代入ノードの式をx=e（eは算術式（注））とし、この代入弧のプロ
グラムポイントをqとします。また、プログラムポイントqに対してその前のプログラムポイントをqpreとし、プログラムポイントがqpreとなる抽象環境の集合をS^(qpre)とします。
（注）例えばeが一次式ならば、e=a1x1+a2x2+・・・+amxm

このとき、プログラムポイントqでの抽象環境の集合S^(q)は、次のようになります；
qpre ・・・ S^(q )pre・S^(qpre)の変数≠x では、
S^(q)=S^(qpre)
x=e・S^(qpre)の変数=x では、
q・・・ S^(q)S^(q)=α(e)ここで、α(e)の計算はeの計算の抽象バージョンが要求されます。
→次頁の例を参照。
57

６．６ フローチャート上の抽象解釈：代入弧 (2)（例１）抽象ドメインが区間の例。このときS^(q)は？
qpre ・・・ S^(qpre)={(x, [0, 3]), (y, [1, 2])}x=x+y+1q

代入ノード
・・・ S^(q)=?

（解）S^(q)の変数yではS^(qpre)のyの値がそのまま入るのでS^(q)= (y, [1, 2]) ・・・①
S^(q)の変数xでは、α(x+y+1)を計算します。
抽象ドメインの区間の足し算+を[a, b]+[c, d]=[a+c, b+d]で定義すると、S^(q)=α(x+y+1)=(x, [0, 3]+[1, 2]+[1, 1] )=(x, [2, 6])・・・②①、②より、S^(q)={(x, [2, 6]), (y, [1, 2]) }58

６．６ フローチャート上の抽象解釈：代入弧 (3)（例２）抽象ドメインが凸多面体の例。このときS^(q)は？
→凸多角形は連立一次不等式で表現され、「凸多面体の線形写像による像はまた凸多面体になる」という多面体幾何の定理からS^(q)も凸多面体になります。
代入ノード（注）x2:=x1+x2/2+1

S^(qpre)上記の線形変換により
x1→x1’, x2→x2’と変換されたとすると、x1’=x1, x2’:=x1+x2/2+1となります。従って、変換前の座標は変換後の座標により表現されます；x2=2x2’-2x1’-2
この式をx2≧1に代入すると
2x2’-2x1’-2≧1から
2x2’-2x1’≧3 が求まります。

S^(q)（注）上記の議論は代入ノードの式が線形の場合。非線形の場合は別の方法が必要。

59

６．７ フローチャート上の抽象解釈：単純接合弧(1)■ループでない単純接合ならば、接合前の値の集合の和なので下記が成立します；
S^(q)=S^(qpre)∪S^(qpre’)

qpre

qpre’
q

（例１）抽象ドメインが区間の例。このときS^(q)は？
S^(qpre)={ (x, [1, 1] ) }, S^(qpre’)={ (x, [2, 2]) }とするとき、S^(q)={ (x, [1, 1]∪[2, 2] ) }={ (x, [1, 2] ) }となります。

60

６．７ フローチャート上の抽象解釈：単純接合弧(2)（例２）抽象ドメインが凸多面体の例。このときS^(q)は？
入力がP1, P2（凸多面体）のとき、その和P1∪P2は凸多面体になるとは限りません。
従って、単純接合ノードの出力としては「P1∪P2を含む最小の凸多面体、
すなわちP1∪P2の凸包(convex-hull(P1∪P2))」を採用します。
（注）凸包とは？
部分集合Sに対し、Sを含む最小の凸集合を凸包と言い、convex-hull(S)で表します。convex-hull(S)はSの要素の凸結合全体からなる集合です。即ち、convex-hull(S)={a1x1+・・・+akxk | a1+・・・+ak=1, ai≧0 , xi∈S (i=1,・・・, k), k∈N }●Sが凸集合である。⇔ convex-hull(S)=Sが成立します。
次頁に凸多面体の単純接合の具体例を示します。
61

６．７ フローチャート上の抽象解釈：単純接合弧(3)単純接合ノードへの２つの入力を、S^(qpre)={ x1≧0, x2≧0, x1+x2≦1 }、 , S^(qpre’)={ x1≧1, x2=2 }とすると、
出力S^(q)はS^(q)=convex-hull(S^(qpre), S^(qpre’))={ 0≦x2≦2, x1≧0, x2-x1≦1 }となります（下の図参照）。
x2

S^(qpre’)

2

1

x2
qpre

qpre’

S^(qpre)

1

q
1

2

S^(q)

x1
1

x1

62

６．８ フローチャート上の抽象解釈：ループ接合弧(1)■ループ接合弧の場合、widening、narrowingによりループを解消します。
iteration 1

qpre

iteration 2

qpre
qpre’

この方向の入力なし

q

プログラムポイントqでの変数の値の集合は、S^(q)=S^(qpre)

qプログラムポイントqでの変数の値の集合はS^(qpre)∪S^(qpre’)以上から、プログラムポイントqにおいてΦ⊆S^(q)=S^(qpre)⊆S^(qpre)∪S^(qpre’)という単調増加列ができます。この列に対してwideningの列を作ると、
y0=Φ, y1=y0∇S^(qpre)=Φ∇S^(qpre)=S^(qpre),y2=y1∇(S^(qpre)∪S^(qpre’))=S^(q)∇(S^(qpre)∪S^(qpre’))となり、Φ⊆S^（q）⊆S^(q)∇(S^(qpre)∪S^(qpre’))という列ができます。wideningの性質からS^(q)∇(S^(qpre)∪S^(qpre’))はプログラムポイントqでの変数の値を全て含む集合となります。これをS^(q)の近似値とし、S^(q)∇=S^(q)∇(S^(qpre)∪S^(qpre’))と置ます。
63

６．８ フローチャート上の抽象解釈：ループ接合弧(2)iteration 3では、wideningの結果のS^(q)∇に対してS^(q)∇⊇(S^(qpre)∪S^(qpre’))という単調減少列ができ、S^(q)∇Δ(S^(qpre)∪S^(qpre’))というnarrowingが作れます。
これが、ループ接合弧のS^(q)の抽象解釈による近似値となります。

iteration 2

qpre

iteration 3

qpre

qpre’

qpre’

q
wideningの結果からS^(q)∇=S^(q)∇(S^(qpre)∪S^(qpre’))qプログラムポイントqでの変数の値の集合はnarrowingを求める；
S^(q)Δ=S^(q)∇Δ(S^(qpre)∪S^(qpre’))→これにより、ループに依存しない変数の値の近似値が求まります。
64

６．９ フローチャート上の抽象解釈：条件付き弧(1)■条件付きノードからは２つの弧が出ています。
Q(v1,・・・,vm)は変数v1,・・・,vmに関する条件式。

S^(qpre)Q(v1,・・・,vm)

このとき、qを条件付きノードから出るTrueの弧のプログラムポイントとすると、

True

S^(q)

False

S^(q)

S^(q)={条件式Q(v1,・・・,vm)が真となるような S^(qpre)の変数の値の集合（区間）}同様に、qを条件付きノードから出るFalseの弧のプログラム
ポイントとすると、
S^(q)={条件式Q(v1,・・・,vm)が偽となるような S^(qpre)の変数の値の集合(区間)}65

６．９ フローチャート上の抽象解釈：条件付き弧(2)（例１）抽象ドメインが区間の例。このときS^(q)は？
（解）条件式x≧yが真となる領域は図の黄色の領域です。

S^(qpre)={ (x, [-∞, +∞] ), (y, [1, 10]) }

y

y=x

10

x≧y
True

1

1

10

x

S^(q)=?

False
S^(q)=?

従って、qがtrueパスの場合は、区間の直積で考えるとS^(q)={条件式x≧yが真となるような S^(qpre)の変数xの区間=[1, +∞],
変数yの区間=[1, 10]}={(x, [1, +∞]), (y, [1, 10])}qがfalseパスの場合は、区間の直積で考えるとS^(q)={条件式x≧yが偽となるような S^(qpre)の変数xの区間=[−∞, 9],
変数yの区間=[1, 10]}={(x, [−∞, 9]), (y, [1, 10])}66

６．９ フローチャート上の抽象解釈：条件付き弧(3)（例２）抽象ドメインが凸多面体の例。このときS^(q)は？
テストノードの条件式が線形ならば、条件式は超平面Hとなるので、テストノードの出力は、入力の凸多面体S^(qpre)と、Hの共通部分S^(qpre)∩Hとなります。
（例）代入式がx1+6≧2x2、入力の多面体が左端の場合、Trueパスの出力は下記；
テストノードH: x1+6≧2x2
S^(qpre)Hの境界
S^(q)=S^(qpre)∩H67

６．１０ フローチャート上の抽象解釈：まとめプログラムの弧のタイプ別の抽象解釈をまとめると次のようになります；●qが開始弧ならば、S^(q)=α(各変数の任意の値)●qが代入弧ならば、・S^(qpre)の変数≠x では、S^(q)=S^(qpre)
・S^(qpre)の変数=x では、S^(q)=α(e)●qが単純接合弧ならば、S^(q)=S^(qpre)∪S^(qpre’)●qがループ接合弧ならば、・最初の２回のループはwidening：S^(q)∇=S^(q)∇(S^(qpre)∪S^(qpre’))・３回目のループはnarrowing：S^(q)Δ=S^(q)∇Δ(S^(qpre)∪S^(qpre’))によりループ処理から抜け出す。
●qが条件付きノードから出るTrueの弧ならば、S^(q)={条件式Q(v1,・・・,vm)が真となるような S^(qpre)の変数の値の集合（区間）}●qが条件付きノードから出るFalseの弧ならば、S^(q)={条件式Q(v1,・・・,vm)が偽となるような S^(qpre)の変数の値の集合（区間）}
これを簡単なプログラムに適用した例を次頁以降に示します。

68６．１１ プログラム例１（抽象ドメイン=区間で考える場合）■右のプログラムの変数xの最終の値を抽象解釈で求めます。

∇

x:=0
q1

一変数なので抽象ドメインは区間とします。
S^(q0)=α(xの任意の値)=(x, [-∞, +∞])
S^(q1)=(x,α(0))=(x, [0, 0])
S^(q2)∇=S^(q1)∇(S^(q1)∪S^(q4))=(x, [0, 0])∇([0, 0]∪[1, 1])=(x, [0, 0])∇[0, 1]=(x, [0, ∞]) q4
S^(q3)={条件式x<100が真となるようなS^(q2)=(x, [0, ∞])の変数の区間}=(x, [0, 99])
S^(q4)=(x,α(x+1))=(x, [0, 99]+[1, 1])=(x, [1, 100])

q0

q2
X < 100
true

q3

false
q5

x:=x+1

S^(q2)Δ=S^(q2)∇Δ(S^(q1)∪S^(q4))=(x,[0, ∞])Δ([0, 0]∪[1, 100])=(x, [0, ∞])Δ[0, 100])=(x, [0, 100])
S^(q5)={条件式x<100が偽となるようなS^(q2)Δ=(x, [0, 100])の変数の区間}=(x, [100, 100]) 従って、x=100が求める解。
69

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (1)∇■右のプログラムでzero divideが発生しないかを抽象解釈で考えます。
S^(q0)=α(I, J, Kの任意の値)={(I, J, K) | -∞≦I, J, K≦+∞}S^(q1)={(I, J, K) | -∞≦I, J≦+∞, -231≦K≦231-1}
S^(q2)={(I, J, K) | I=2, -∞≦J≦+∞, -231≦K≦231-1}
S^(q3)={(I, J, K) | I=2, J=K+5, -231≦K≦231-1}

次に、S^(q4)∇=S^(q3)∇(S^(q3)∪S^(q7))を求めるために(S^(q3)∪S^(q7))を求めます。
(S^(q3)∪S^(q7))={(I, J, K) | I=2, J=K+5, -231≦K≦231-1}∪{(I, J, K) | I=3, J=K+5+3, -231≦K≦231-1}={(I, J, K) | I=2, J=K+5, -231≦K≦231-1}∪{(I, J, K) | I=3, J=K+8, -231≦K≦231-1}
次頁にこれの幾何学的意味を調べます。

q0

K=ioread_i32( )

q1
I=2
q2
J=K+5
q3
q4
q7

I < 10true q5

false

q8

I=I+1
q6

…/(I-J)

J=J+3

△

q9
70

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (2)■S^(q3)∪S^(q7)={(I, J, K) | I=2, J=K+5, -231≦K≦231-1}∪{(I, J, K) | I=3, J=K+8, -231≦K≦231-1}
下の左図のようにS^(q3)∪S^(q7)は３次元空間の２つの平行な直線の和なので凸多面体にはなりません。そこで、これを凸多面体で近似するために２つの直線の凸包cnvex-hull(S^(q3), S^(q7))を考えます。これは２つの直線{I=2, J=K+5},{I=3, J=K+8} (Kは任意）を通る平面3I-J+K-1=0（次頁）上にあり、２つの直線の間Kの領域です。
K

S^(q3)
S^(q7)
8
J

5
−5

2 3

I

cnvex-hull(S^(q3), S^(q7))

−8

−5
8
J

・(3, 0, −8)I

5S^(q3)とS^(q7)の凸包・(3, 8, 0)

2 3

・(3, 8, 0)−8・(3, 0, −8)
平面
3I-J+K-1=071

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (3)■２つの直線{I=2, J=K+5}, {I=3, J=K+8} (Kは任意）を通る平面を求めること。
（説明）３次元(I, J, K)空間での平面の式は
a*I+b*J+c*K+d=0 ・・・①と表されます。
①が直線{I=2, J=K+5} (Kは任意）上にあるとすると、
2a+b(K+5)+c*K+d=0 ・・・②
同様に①が, 直線{I=3, J=K+8} (Kは任意）上にあるとすると、
3a+b(K+8)+c*k+d=0 ・・・③が成立します。
②から③を引くと、a=-3b ・・・④
また、②はKの任意の値に対して成立するのでK=0でも成立。
従って、2a+5b+d=0④より a=-3bなので、d=bが求まります。
また、②でK=1と置くと、2a+6b+c+d=0
従って、c=-d以上から、a=-3b, d=b, c=-d=-b→①は-3b*I+b*J-b*K+b=0 すなわち、-3I+J-K+1=0が求める平面の式。
72

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (4)■以上の議論からS^(q4)∇=S^(q3)∇(S^(q3)∪S^(q7))の(S^(q3)∪S^(q7))の部分はcnvex-hull(S^(q3), S^(q7))に置換えます。すなわち、
S^(q4)∇=S^(q3)∇cnvex-hull(S^(q3), S^(q7))
多面体のwideningからこれは、下図のようにS^(q3)からcnvex-hull(S^(q3), S^(q7))
へ変るときに移動する（安定しない）辺（ の辺）を取り除いたもの（赤の→方向に半平面として無限に広がる）になります。 即ち、平面3I-J+K-1=0で2≦I≦+∞,-231≦K≦231-1の部分。従って、
S^(q4)∇={(I, J, K)| 2≦I≦+∞, 3I-J+K-1=0, -231≦K≦231-1}
K

cnvex-hull(S^(q3), S^(q7))

2 3

IS^(q3)={(I, J, K) | I=2, J=K+5,-231≦K≦231-1}

I

−5

−5
J

2

5

5
8

K

・(3, 8, 0)−8・(3, 0, −8)

J 4)∇
S^(q
=S^(q3)∇cnvex-hull(S^(q3), S^(q7))
73

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (5)■前頁の結果からS^(q4)∇={(I, J, K)| 2≦I≦+∞, 3I-J+K-1=0, -231≦K≦231-1}
したがって、S^(q5)={条件式I<10が真となるようなS^(q4)∇={(I, J, K)| 2≦I≦+∞, 3I-J+K-1=0,-231≦K≦231-1}の変数の区間}={(I, J, K)| 2≦I≦9, 3I-J+K-1=0, -231≦K≦231-1}
I=I+1なのでS^(q6)={(I, J, K)| 3≦I≦10, 3(I+1)-J+K-1=0, -231≦K≦231-1}={(I, J, K)| 3≦I≦10, 3I-J+K+2=0, -231≦K≦231-1}
J=J+3なのでS^(q7)={(I, J, K)| 3≦I≦10, 3I-(J+3)+K+2=0, -231≦K≦231-1}={(I, J, K)| 3≦I≦10, 3I-J+K-1=0, -231≦K≦231-1}

74

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (6)■Iteration 3 ではnarrowingを考えるので、S^(q4)Δ=S^(q4)∇Δcnvex-hull(S^(q3), S^(q7))を求めます。そのためにまず■cnvex-hull(S^(q3), S^(q7))を求めます。
cnvex-hull(S^(q3), S^(q7))= cnvex-hull({(I, J, K) | I=2, J=K+5, -231≦K≦231-1},{(I, J, K)| 3≦I≦10, 3I-J+K-1=0, -231≦K≦231-1}={(I, J, K)| 2≦I≦10, 3I-J+K-1=0, -231≦K≦231-1}
K

K

2 3

S^(q3)

10

cnvex-hull(S^(q3), S^(q7))

2

10

S^(q7)
8

5
−5
−8

29

J

S^(q3)とS^(q7)
の凸包

5
−5

29
−29

J

−29

75

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (7)
従って、S^(q4)Δ={(I, J, K)| 2≦I≦10, 3I-J+K-1=0, -231≦K≦231-1}となります。

S^(q4)Δ=S^(q4)∇Δcnvex-hull(S^(q3), S^(q7))

76

６．１１ プログラム例２（抽象ドメイン=多面体で考える場合） (8)これでループ処理からは抜けるのでS^(q5)={条件式I<10が偽となるようなS^(q4)Δ={(I, J, K)| 2≦I≦10, 3I-J+K-1=0,-231≦K≦231-1}の変数の区間}={(I, J, K)| I=10, 3I-J+K-1=0, -231≦K≦231-1}
従って、S^(q8)={(I, J, K) | I=10, 3I-J+K-1=0, -231≦K≦231-1}
Xerror={(I, J, K) | (I, J, K)∈S^(q8) , I=J }={(I, J, K) | I=J=10, K=-19}
すなわち、I=10, J=10, K=-19のときZero divideとなることが分かります。

77

７．ループ限界の発見
７．１ ループ限界解析とは？
７．２ ループ不変変数
７．３ 限定されたwidening
７．４ ループ限界解析の抽象解釈
７．５ 抽象環境でのエレメントのカウント
７．６ 合同抽象ドメイン
７．７ 合同抽象ドメインによる抽象解釈
７．８ 抽象ドメインの直積
７．９ 区間と合同抽象ドメインの直積による抽象解釈
７．１０ 直積ドメインでのエレメントのカウント

78７．１ ループ限界解析とは？
■プログラムは多くの実行時間をループで費やすので、 ループの繰り返しに対する上界を見つけることが重要。
ループ限界解析(Loop Bound Analysis)は、論文[ESG+07](*)でアウトラインを示された手法で、抽象解釈、スライシング、不変解析技術を使用してループの可能な意味論的状態をカウントすることに基づいています。
→スライシングは、５．２のプログラムスライシングを参照。
不変解析については
次頁参照。

79

７．２ ループ不変変数■「ループ不変変数」とは、ループ本体で値が変化しない変数です。
不変解析(invariant analysis)はこれを見つける技術です。
→ここでは、ループ不変変数の説明だけをします。
■ループの名称を L とし、プログラムの変数の集合をVP、ループ不変変数の集合を IL ととすると、
IL = VP - （ループLで値が更新される変数）（例）右のプログラムには２つのループがあります；
L1 = {q2 , q3 , q4 , q5 , q8 , q9 }L2 = {q5 , q6 , q7 }このとき、 VP ={ i, j }なので
IL1={ i, j } – { i }={ j }IL2={ i, j } – { j }={ i }80

７．３ 限定されたwidening■CをプログラムPの変数の集合VPの部分集合とするとき、限定されたwidening∇Cを次のように定義します；
・変数v∈Cならば
X∇CY=Y(v)・変数v∉Cならば、
X∇CY=X∇Y(v)→これは、ループ不変変数をwideningの計算でスルーさせるために使用します。
ループLのループ不変変数の集合を IL とするときS(q)∇=S(q)∇IL(S(qpre)∪S(qpre’))
この意味は、wideningが「ループLで変化の可能性のある変数」に対してのみ実行されることです。

81７．４ ループ限界解析の抽象解釈(1)■右のプログラムの抽象解釈を求めます。
Cを整数全体の部分集合とするとき、抽象化写像をα( C )=[min( C ), max( C )] とします（区間への抽象）。
①大きなループ(iに関するループ)のiteration=1の場合
S^1(q0)=α(i, jの任意の値)={(i, [-∞, +∞]), (j, [-∞, +∞])}
S^1(q1)={(i,α(1)), (j, [-∞, +∞])}={(i, [1, 1]), (j, [-∞, +∞])}
S^1(q2)∇=S^1(q2)∇{j}(S^1(q1)∪S^0(q9))=S^1(q1)∇{j}(S^1(q1)∪Φ)=S^1(q1)∇{j}S^1(q1)=S^1(q1)={(i, [1, 1]), (j, [-∞, +∞])}
S^1(q3)=S^1(q2)∇∩(i, [-∞, 100])={(i, [1, 1]), (j, [-∞, +∞])}
S^1(q4)=S^1(q3)∩(j, [1, 1])={(i, [1, 1]), (j, [1, 1])}S^1(q5)∇=S^1(q5)∇{i}(S^1(q4)∪S^1(q7))=S^1(q4)∇{i}(S^1(q4)∪Φ)=S^1(q4)∇{i}S^1(q4)=S^1(q4)={(i, [1, 1]), (j, [1, 1])}→i=j=[1, 1]なので条件式i≦jは常に成立し、q6へのパスに行きます（q8のパスへは行かない）；S^1(q6)={条件式j≦iが真となるようなS^1(q5)∇={(i, [1, 1]), (j, [1, 1])}の変数の区間の最大値}={(i, [1, 1]), (j, [1, 1])}S^1(q7)={(i, [1, 1]), (j, α(j+1))}={(i, [1, 1]), (j, [2, 2])}
次に、jに関するループの限定されたwideningを考えます。

82

７．４ ループ限界解析の抽象解釈(2)S^1-1(q5)∇=S^(q5)∇{i}(S^(q4)∪S^(q7))={(i, [1, 1]), (j, [1, 1])}∇{i}({(i, [1, 1]), (j, [1, 1])}∪{(i, [1, 1]), (j, [2, 2])})={(i, [1, 1]), (j, [1, 1])}∇{i}({(i, [1, 1]), (j, [1, 2])})={(i, [1, 1]), (j, [1, 1])∇(j, [1, 2])}={(i, [1, 1]), (j, [1, +∞])}
S^1-1(q6)={条件式j≦iが真となるようなS^1(q5)∇={(i, [1, 1]), (j, [1, +∞])}の変数の区間の最大値}={(i, [1, 1]), (j, [1, 1])}S^1-1(q7)={(i, [1, 1]), (j, α(j+1))}={(i, [1, 1]), (j, [2, 2])}
一方、今度はq8のパスへ進む値が生じます；
S^1(q8)={条件式j≦iが偽となるようなS^1-1(q5)∇={(i, [1, 1]), (j, [1, +∞])}の変数の区間の最大値}={(i, [1, 1]), (j, [2, +∞])}
S^1(q9)={(i, α(i+2)), (j, [2, +∞])}={(i, [3, 3]), (j, [2, +∞])}

83

７．４ ループ限界解析の抽象解釈(3)②大きなループ(iに関するループ)のiteration=2の場合
S^2(q2)∇=S^1(q2)∇∇{j}(S^1(q1)∪S^1(q9))={(i, [1, 1]), (j, [-∞, +∞])}∇{j}({(i, [1, 1]), (j, [-∞, +∞])}∪{(i, [3, 3]), (j, [2, +∞])})={(i, [1, 1])∇(i, [1, 3]), (j, [-∞, +∞])∪(j, [2, +∞]))}={(i, [1, +∞]), (j, [-∞, +∞])}
S^2(q3)=S^2(q2)∇∩(i, [-∞, 100])={(i, [1, +∞], (j, [-∞, +∞])} ∩(i, [-∞, 100])={(i, [1, 100], (j, [-∞, +∞])}
S^2(q4)=S^2(q3)∩(j, [1, 1])={(i, [1, 100], (j, [1, 1])}S^2(q5)∇=S^1-1(q5)∇∇{i}(S^2(q4)∪S^1-1(q7))={(i, [1, 1]), (j, [1, +∞])}∇{i}({(i, [1, 100], (j, [1, 1])}∪{(i, [1, 1]), (j, [2, 2])})={(i, [1, 100]), (j, [1, +∞])∇(j, [1, 2])}={(i, [1, 100]), (j, [1, +∞])}
S^2(q6)={条件式j≦iが真となるようなS^2(q5)∇={(i, [1, 100]), (j, [1, +∞])}の変数の区間の最大値}={(i, [1, 100]), (j, [1, 100])}
S^2(q7)={(i, [1, 1]), (j, α(j+1))}={(i, [1, 100]), (j, [2, 101])}S^2(q8)={条件式j≦iが偽となるようなS^2(q5)∇={(i, [1, 100]), (j, [1, +∞])}の変数の区間の最大値}={(i, [1, 100]), (j, [2, +∞])}
S^2(q9)={(i, α(i+2)), (j, [2, +∞])}={(i, [3, 102]), (j, [2, +∞])}
S^2(q10)={条件式 i≦100が偽となるようなS^2(q2)∇={(i, [1, +∞], (j, [-∞, +∞])}の変数の区間の最大値}={(i, [101, +∞]), (j, [-∞, +∞])}
84

７．４ ループ限界解析の抽象解釈(4)③大きなループ(iに関するループ)のiteration=3の場合、今度はnarrowingを考えます；
S^3(q2)Δ=S^2(q2)∇Δ{j}(S^1(q1)∪S^2(q9))={(i, [1, +∞]), (j, [-∞, +∞])}Δ{j}({(i, [1, 1]), (j, [-∞, +∞])}∪{(i, [3, 102]), (j, [2, +∞])})={(i, [1, +∞])Δ(i; [1, 102]), (j, [-∞, +∞])∪(j, [2, +∞]))={(i; [1, 102]), (j, [-∞, +∞])}(i,[1, 1])∪(I, [3, 102])=(I, [1, 102])S^3(q3)=S^3(q2)Δ∩(i, [-∞, 100])={(i; [1, 102]), (j, [-∞, +∞])}∩(i, [-∞, 100])区間の包含、和、積は下記で定義。
={(i, [1, 100], (j, [-∞, +∞])}[a, b]⊆[a’, b’] ⇔ a ≥ a’ ∧ b ≤ b’S^3(q4)=S^3(q3)∩(j, [1, 1])={(i, [1, 100], (j, [1, 1])}[a, b]∪[a’, b’] = [min(a, a’), max(b, b’)]3
2
3
2
[a, b]∩[a’, b’] = [max(a, a’), min(b, b’)]S^ (q5)Δ=S^ (q5)∇Δ{i}(S^ (q4)∪S^ (q7))={(i, [1, 100]), (j, [1, +∞])} Δ{i}({(i, [1, 100], (j, [1, 1])}∪{(i, [1, 100]), (j, [2, 101])})={(i, [1, 100]), (j, [1, +∞])Δ(j, [1, 101])}={(i, [1, 100]), (j, [1, 101])}S^3(q6)={条件式j≦iが真となるようなS^3(q5)Δ={(i, [1, 100]), (j, [1, 101])}の変数の区間の最大値}={(i, [1, 100]), (j, [1, 100])}
S^3(q7)={(i, [1, 1]), (j, α(j+1))}={(i, [1, 100]), (j, [2, 101])}
また、S^3(q8)={条件式j≦iが偽となるようなS^3(q5)Δ={(i, [1, 100]), (j, [1, 101])}の変数の区間の最大値}={(i, [1, 100]), (j, [2, 101])}S^3(q9)={(i, α(i+2)), (j, [2, 101])}={(i, [3, 102]), (j, [2, 101])}S^3(q10)={条件式 i≦100が偽となるようなS^3(q2)Δ={(i; [1, 102]), (j, [-∞, +∞])}の変数の区間の最大値}={(i, [101, 102]), (j, [-∞, +∞])}
85

７．４ ループ限界解析の抽象解釈(5)
従って、抽象解釈はiteration=3の結果として下記になり、各プログラムポイントでの変数i, jの値の範囲（の近似値）が求まります；
S^1(q0)={(i, [-∞, +∞]), (j, [-∞, +∞])}
S^1(q1)={(i, [1, 1]), (j, [-∞, +∞])}
S^3(q2)Δ={(i; [1, 102]), (j, [-∞, +∞])}
S^3(q3)={(i, [1, 100]), (j, [-∞, +∞])}
S^3(q4)={(i, [1, 100]), (j, [1, 1])}S^3(q5)Δ={(i, [1, 100]), (j, [1, 101])}S^3(q6)={(i, [1, 100]), (j, [1, 100])}
S^3(q7)={(i, [1, 100]), (j, [2, 101])}S^3(q8)={(i, [1, 100]), (j, [2, 101])}S^3(q9)={(i, [3, 102]), (j, [2, 101])}S^3(q10)={(i, [101, 102]), (j, [-∞, +∞])}
86

７．５ 抽象環境でのエレメントのカウント(1)
前頁の結果から右のプログラムの各プログラムポイントqの通過回数|q|を求めます；
ループ処理以外では、|q0|=|q1|=|q10|=1

ループ処理では、ループL1とL2のスライシングを使用します； 5.2(2)より
L1のスライス={q2 , q3 , q9 }L2 のスライス= {q5 , q6 , q7 }L1

L2

ループL1のスライスでq3の通過回数|q3|はループL1の繰り返し回数となる
ので、これを前頁の結果S^3(q3)={(i, [1, 100]), (j, [-∞, +∞])}から求めます。この式において、jはループL1のループ不変変数なのでL1のループ繰り返しとは無関係。従って、|q3|=|(i, [1, 100])|=10087

７．５ 抽象環境でのエレメントのカウント(2)ループL2のスライスでq6の通過回数|q6|はループL2の繰り返し回数となる
ので、これを前頁の結果
S^3(q6)={(i, [1, 100]), (j, [1, 100])}
から求めます。この式において、iはループL2のループ不変変数なので、|q6|=|(j, [1, 100])|=100が求まります。

L1

L2

88

７．５ 抽象環境でのエレメントのカウント(3)■右のフローで、各プログラムポイントと対応する原子部分とその原子WCETを
q0⇔初期値設定=1, q1⇔i:=1（代入）=3
q2 ,q5⇔結合ノード（結合）=1
q3 , q6, q8, q10⇔i<=n（分岐）=2
q4⇔j:=1（代入）=3
q7⇔j:=j+1（代入）=8, q9⇔i:=i+1（代入）=8とすると、各プログラムポイントに対して原子WCETを関係させる関数ｌ(エル）は下記；
l(q0)=1, l(q1)=l(q4)=3, l(q2)=l(q5)=1,
l(q3)=l(q6)=l(q8)=l(q10)=2, l(q7)=l(q9)=8
従って、WCETの近似値=l(q0)*|q0|+l(q1)*|q1|+l(q10)*|q10|+{l(q2)+l(q3)+l(q4)+(l(q5)+l(q6)+l(q7))*|q6|+l(q8)+l(q9)}*|q3|=1*1+3*1+2*1+{1+2+3+(1+2+8)*100+2+8}*100
ループL2=6+{16+11*100}*100=111606

ループL1

89

７．５ 抽象環境でのエレメントのカウント(4)■WCET近似値の評価
正確なループ回数は次のように求まります；
i=1→j=1→j=i=1→j=j+1=1+1=2→j=2>i=1→i=i+2=1+2=3
i=3→j=1→j=1<i=3→j=j+1=1+1=2
L2のループ回数=3→j=2<i=3→j=j+1=2+1=3→j=i=3→j=j+1=4→j=4>i=3→i=i+2=3+2=5
i=5→j=1→j=1<i=5→j=j+1=1+1=2→j=2<i=5→j=j+1=2+1=3 L2のループ回数=5→j=3<i=5→j=j+1=3+1=4→j=4<i=5→j=j+1=4+1=5→j=i=5→j=j+1=5+1=6 →j=6>i=5→i=i+2=5+2=7

ループL1の1周目
ループL1の2周目
ループL1の3周目

・・・・・・

ループL1
i=99→j=1→j=1<i=5→j=j+1=1+1=2の50周目→j=2<i=5→j=j+1=2+1=3
L2のループ回数=99
・・・→j=i=99→j=j+1=99+1=100→j=100>i=99→i=i+2=99+2=10190

７．５ 抽象環境でのエレメントのカウント(5)従って、ループの処理時間は次のようになります；
i=1のとき、l(q2)+l(q3)+l(q4)+1*{l(q5)+l(q6)+l(q7)}+l(q8)+l(q9)i=3のとき、l(q2)+l(q3)+l(q4)+3*{l(q5)+l(q6)+l(q7)}+l(q8)+l(q9)i=5のとき、l(q2)+l(q3)+l(q4)+5*{l(q5)+l(q6)+l(q7)}+l(q8)+l(q9)・・・
i=99のとき、l(q2)+l(q3)+l(q4)+99*{l(q5)+l(q6)+l(q7)}+l(q8)+l(q9)i=101のとき、l(q2)+l(q10)以上の合計を求めると、
50*{l(q2)+l(q3)+l(q4)+l(q8)+l(q9)}+2451*{l(q5)+l(q6)+l(q7)}+l(q2)+l(q10)ここで、1+3+5+・・・+99=Σ2(k-1)+1=2Σk -99=51*50-99=2451 (k=1,2,・・・,50)

従って、正確な処理時間はl(q0)+l(q1)+50*{l(q2)+l(q3)+l(q4)+l(q8)+l(q9)}+2451*{l(q5)+l(q6)+l(q7)}+l(q2)+l(q10)=1+3+50*(1+2+3+2+8)+2451*(1+2+8)+1+2=4+50*16+2451*11+3=4+800+26961+3=27768
91

７．５ 抽象環境でのエレメントのカウント(6)７．５（３）のWCET近似値=111606は、実際のWCET=27768の約4倍(111606/27768)となります。
以上から変数i, jの値の範囲を区間により抽象化した方法による
WCETは実際のWCETに較べて相当な幅があり、改善の余地があります。
→これについては、「区間の抽象化」に加えて「合同式による抽象化(Congruence Abstraction)」を適用することにより対応
します（次頁以降参照）。

92

７．６ 合同抽象ドメイン(1)■定義(k を法とする合同)
k を与えられた一つの自然数とします。
a; b を二つの整数とするとき，もしa−b が k で割り切れるならば，
a とb はk を法として合同であるといい，a ≡ b mod kと表します。
→これは、「整数a, bは割る数をmとした場合、余りが等しい」ことを意味します。（例）10≡4 mod 3, 100≡1 mod 3 等。
■今度は 1 mod 2 という式を考えてみます。
この意味は「2で割ると余りが1の整数」です。このような整数の集合は、{・・・, -7, -5, -3, -1, 1, 3, 5, 7, ・・・} です。
これは、1+2Zと同じです（Z={・・・, -3, -2, -1, 0, 1, 2, 3, ・・・})。
一般に、
m mod k を満たす整数の集合= m + kZとなります。
93

７．６ 合同抽象ドメイン(2)■合同式による抽象化（例1）A={-1, 1, 3}とすると、Aの要素は「2で割ると余りが1」の数です。
一方、「2で割ると余りが1」の数の全体は、1 mod 2 = 1 + 2Z で表されます。このとき、抽象化写像αはAに1 + 2Zを対応させます；
α(A) = 1 + 2Z
-1

1
A

3

α

・・・ -5-3-1

1
3
1 + 2Z5

7 ・・・（例２）A={2, 5, 11}とすると、Aの要素は「3で割ると余りが2」の数です。
この3という数字は、Aの要素の差（5-2=3, 11-2=9, 11-5=6）の最大
公約数=3として求まります。従って、α(A) = 2 + gcl(3, 9, 6)Z = 2 + 3Z
（注）gcl：greatest common divisor
94

７．６ 合同抽象ドメイン(3)■合同式による抽象化は一般に下記で表されます。
α(A) = a0 + (Aの全ての要素の差の最大公約数）Z
ここで、a0 = Aの負でない最小の数
但し、Aの要素が１個（A={a0})の場合は、それ自身に等しい；
α(A)=a0 + 0Z
（例1）A={-1, 1, 3}とすると、a0=1,
Aの全ての要素の差の最大公約数=gcl(|3-(-1)|, |3-1|, |1-(-1)|)=gcl(4, 2, 2)=2 従って、α(A)=1+2Z（例２）A={ 1 }とすると、
α(A)=1+0Z

95

７．６ 合同抽象ドメイン(4)■合同抽象ドメインの演算（例1：積）(1+2Z)∩^(2+3Z)を考えます。
・・・ -5・・・ -41 + 2Z-3-1-1・・・ -1

1

3

2

5

5

5

7

9

8

11 13 ・・・

11 ・・・

11 ・・・

2 + 3Z

5 + 6Z

一般に、(m+kZ)∩^(m’+k’Z) = m’’+ lcm(k, k’)Z （注）lcm：least common multipleとなります。ここで、m’’は(m+kZ)∩(m’+k’Z)の要素。
→上の例では、5∈(1+2Z)∩(2+3Z), 2と3の最小公倍数=6なので、(1+2Z)∩^(2+3Z)=5+6Z
96

７．６ 合同抽象ドメイン(5)（例2：和）(1+2Z)∪^(3+4Z)を考えます。

・・・ -5

1 + 2Z-3・・・ -5・・・ -5

-1

1

-1

3

5

7

9

11 ・・・

7

3

11 13 ・・・
3 + 4Z

1 + 2Z
-3

-1

1

3

5

7

9

11 13 ・・・

一般に、
(m+kZ)∪^(m’+k’Z) = m+ gcd{ |m-m’|, k, k’}Zとなります。ここで、gcdは最大公約数。
→上の例では、m=1, gcd{ |1-3|, 2, 4}=2なので、(1+2Z)∪^(3+4Z)=1+2Z
97

７．７ 合同抽象ドメインによる抽象解釈(1)■合同抽象ドメインにより右のプログラムの抽象解釈を求めます。
①大きなループ(iに関するループ)のiteration=1の場合
任意の整数の集合は、「1で割ると余りが0」の整数の集合なので、0+1Z で表されます。
従って、
S^1(q0)=α(i, jの任意の値)={(i, 0+1Z), (j, 0+1Z)}α({1})=1+0Zなので、
S^1(q1)={(i,α(1)), (j, 0+1Z)}={(i, 1+0Z), (j, 0+1Z)}S^1(q2)∇=S^1(q2)∇{j}(S^1(q1)∪S^0(q9))=S^1(q1)∇{j}(S^1(q1)∪Φ)=S^1(q1)∇{j}S^1(q1)=S^1(q1)={(i, 1+0Z), (j, 0+1Z)}S^1(q3)={(i, 1+0Z), (j, 0+1Z)}S^1(q4)=S^1(q3)∩(j, α({1}))=S^1(q3)∩(j, 1+0Z)={(i, 1+0Z), (j, 0+1Z)∩(j, 1+0Z)}={(i, 1+0Z), (j, 1+0Z)}
S^1(q5)∇=S^1(q5)∇{i}(S^1(q4)∪S^1(q7))=S^1(q4)∇{i}(S^1(q4)∪Φ)=S^1(q4)∇{i}S^1(q4)=S^1(q4)={(i, 1+0Z), (j, 1+0Z)}→i=j=1+0Zなので条件式i≦jは常に成立し、q6へのパスに行きます（q8のパスへは行かない）；
98７．７ 合同抽象ドメインによる抽象解釈(2)S^1(q6)={条件式j≦iが真となるようなS^1(q5)∇={(i, 1+0Z), (j, 1+0Z)}の変数の値の集合}={(i, 1+0Z), (j, 1+0Z)}
S^1(q7)={(i, 1+0Z), (j, α(j+1))}={(i, 1+0Z), (j, 2+0Z)}
次に、jに関するループの限定されたwideningを考えます。
S^1-1(q5)∇=S^(q5)∇{i}(S^(q4)∪S^(q7))={(i, 1+0Z), (j, 1+0Z)}∇{i}({(i, 1+0Z), (j, 1+0Z)}∪{(i, 1+0Z), (j, 2+0Z)})={(i, 1+0Z), (j, 1+0Z)}∇{i}({(i, 1+0Z), (j, 1+0Z)})={(i, 1+0Z), (j, 1+0Z)∇(j, 1+0Z) }={(i, 1+0Z), (j, 1+0Z)}
S^1-1(q6)={条件式j≦iが真となるようなS^1(q5)∇={(i, 1+0Z), (j, 1+0Z)}の変数の値の集合}={(i, 1+0Z), (j, 1+0Z)}
S^1-1(q7)={(i, 1+0Z), (j, α(j+1))}={(i, 1+0Z), (j, 2+0Z)}
一方、今度はq8のパスへ進む値が生じます；
S^1(q8)={条件式j≦iが偽となるようなS^1-1(q5)∇={(i, 1+0Z), (j, 1+0Z)}の変数の値の集合}={(i, 1+0Z), (j, 2+Z)}S^1(q9)={(i, α(i+2)), (j, 1+1Z)}={(i, 3+0Z), (j, 2+0Z)}99

７．７ 合同抽象ドメインによる抽象解釈(3)③大きなループ(iに関するループ)のiteration=2の場合
S^2(q2)∇=S^1(q2)∇∇{j}(S^1(q1)∪S^1(q9))={(i, 1+0Z), (j, 0+1Z)}∇{j}({(i, 1+0Z), (j, 0+1Z)}∪{(i, 3+0Z), (j, 1+0Z)})={(i, 1+0Z), (j, 0+1Z)}∇{j}{(i, 1+2Z), (j, 0+1Z)}={(i, 1+0Z)∇(i, 0+2Z), (j, 0+1Z)∪(j, 0+1Z)}={(i, 1+2Z), (j, 0+1Z)}S^2(q3)={(i, 1+2Z), (j, 0+1Z)}S^2(q4)=S^2(q3)∩(j, α({1})={(i, 1+2Z), (j, 0+1Z)}∩(j, 1+0Z)}={(i, 1+2Z), (j, 1+0Z)}
S^2(q5)∇=S^1-1(q5)∇∇{i}(S^2(q4)∪S^1-1(q7))={(i, 1+0Z), (j, 1+0Z)}∇{i}({(i, 1+2Z), (j, 1+0Z)}∪{(i, 1+0Z), (j, 2+0Z)})={(i, 1+0Z), (j, 1+0Z)}∇{i}({(i, 1+2Z), (j, 0+1Z)})={(i, 1+2Z), (j, 1+0Z)∇(j, 0+1Z)}={(i, 1+2Z), (j, 0+1Z)}S^2(q6)={条件式j≦iが真となるようなS^2(q5)∇={(i, 1+2Z), (j, 0+1Z)}の変数の値の集合}={(i, 1+2Z), (j, 0+1Z)}S^2(q7)={(i, 1+2Z), (j, α(j+1))}={(i, 1+2Z), (0+1Z)}S^2(q8)={条件式j≦iが偽となるようなS^2(q5)∇={(i, 1+2Z), (j, 0+1Z)}の変数の値の集合}={(i, 1+2Z), (j, 0+1Z)}S^2(q9)={(i, α(i+2)), (j, 0+1Z)}={(i, 1+2Z), (j, 0+1Z)}S^2(q10)={条件式 i≦100が偽となるようなS^2(q2)∇={(i, 1+2Z), (j, 0+1Z)}の変数の値の集合}={(i, 1+2Z), (j, 0+1Z)}100

７．７ 合同抽象ドメインによる抽象解釈(4)②大きなループ(iに関するループ)のiteration=3の場合、今度はnarrowingを考えます；
S^3(q2)Δ=S^2(q2)∇Δ{j}(S^1(q1)∪S^2(q9))={(i, 1+2Z), (j, 0+1Z)}Δ{j}({(i, 1+0Z), (j, 0+1Z)∪{(i, 1+2Z), (j, 0+1Z)})={(i, 1+2Z), (j, 0+1Z)}Δ{j}({(i, 1+2Z), (j, 0+1Z)})={(i, 1+2Z)Δ((i, 1+2Z)), (j, 0+1Z))={(i, 1+2Z), (j, 0+1Z)}→S^3(q2)Δ= S^2(q2)∇なので、iteration=3はiteration=2と同じ結果になります。

101

７．７ 合同抽象ドメインによる抽象解釈(5)■以上のまとめ①大きなループ(iに関するループ)のiteration=1の場合
S^1(q0)={(i, 0+1Z), (j, 0+1Z)}S^1(q1)= {(i, 1+0Z), (j, 0+1Z)}S^1(q2)∇= {(i, 1+0Z), (j, 0+1Z)}S^1(q3)={(i, 1+0Z), (j, 0+1Z)}S^1(q4)= {(i, 1+0Z), (j, 1+0Z)}
S^1(q5)∇= {(i, 1+0Z), (j, 1+0Z)}
S^1(q6)= {(i, 1+0Z), (j, 1+0Z)}
S^1(q7)= {(i, 1+0Z), (j, 2+0Z)}
次に、jに関するループの限定されたwideningを考えます。
S^1-1(q5)∇= {(i, 1+0Z), (j, 1+0Z)}
S^1-1(q6)= {(i, 1+0Z), (j, 1+0Z)}
S^1-1(q7)= {(i, 1+0Z), (j, 2+0Z)}
一方、今度はq8のパスへ進む値が生じます；
S^1(q8)= {(i, 1+0Z), (j, 2+Z)}S^1(q9)= {(i, 3+0Z), (j, 2+0Z)}102

７．７ 合同抽象ドメインによる抽象解釈(6)②大きなループ(iに関するループ)のiteration=2の場合
S^2(q2)∇={(i, 1+2Z), (j, 0+1Z)}S^2(q3)={(i, 1+2Z), (j, 0+1Z)}S^2(q4)={(i, 1+2Z), (j, 1+0Z)}
S^2(q5)∇= {(i, 1+2Z), (j, 0+1Z)}S^2(q6)= {(i, 1+2Z), (j, 0+1Z)}S^2(q7)= {(i, 1+2Z), (0+1Z)}S^2(q8)= {(i, 1+2Z), (j, 0+1Z)}S^2(q9)={(i, 1+2Z), (j, 0+1Z)}S^2(q10)= {(i, 1+2Z), (j, 0+1Z)}③大きなループ(iに関するループ)のiteration=3の場合
S^3(q2)∇={(i, 1+2Z), (j, 0+1Z)}
S^3(q3)={(i, 1+2Z), (j, 0+1Z)}
S^3(q4)={(i, 1+2Z), (j, 1+0Z)}
S^3(q5)∇= {(i, 1+2Z), (j, 0+1Z)}
S^3(q6)= {(i, 1+2Z), (j, 0+1Z)}
S^3(q7)= {(i, 1+2Z), (0+1Z)}
S^3(q8)= {(i, 1+2Z), (j, 0+1Z)}
S^3(q9)={(i, 1+2Z), (j, 0+1Z)}
S^3(q10)= {(i, 1+2Z), (j, 0+1Z)}103

７．８ 抽象ドメインの直積■２つの抽象化写像αA, αBの組により抽象化ドメインの直積を考えることが
できます。
S(q)

<αA, αB><S^A(q), S^B(q)>（例）区間と合同ドメインの直積
Cを整数全体の集合の部分集合とするとき、αA( C )=[min( C ), max( C )]αB( C ) = a0 + (Cの全ての要素の差の最大公約数）Z
ここで、a0 = Cの負でない最小の数
このとき、区間と合同ドメインの直積は<αA(C), αB(C)>104７．９ 区間と合同抽象ドメインの直積による抽象解釈
区間と合同抽象ドメインの抽象解釈の各々のIteration=3の結果より
それらの直積は下記のようになります。
<S^A1(q0), S^B1(q0)> = < {(i, [-∞, +∞]), (j, [-∞, +∞])} , {(i, 0+1Z), (j, 0+1Z)} ><S^A1(q1), S^B1(q1)> = < {(i, [1, 1]), (j, [-∞, +∞])} , {(i, 1+0Z), (j, 0+1Z)} ><S^A1(q2)Δ, S^B1(q2)Δ> = < {(i; [1, 102]), (j, [-∞, +∞])} , {(i, 1+2Z), (j, 0+1Z)} ><S^A1(q3), S^B1(q3)> = < {(i, [1, 100]), (j, [-∞, +∞])} , {(i, 1+2Z), (j, 0+1Z)} ><S^A1(q4), S^B1(q4)> = < {(i, [1, 100]), (j, [1, 1])} , {(i, 1+2Z), (j, 1+0Z)} ><S^A1(q5)Δ, S^B1(q5)Δ> = < {(i, [1, 100]), (j, [1, 101])} , {(i, 1+2Z), (j, 0+1Z)} ><S^A1(q7), S^B1(q7)> = < {(i, [1, 100]), (j, [2, 101])} , {(i, 1+2Z), (0+1Z)} ><S^A1(q8), S^B1(q8)> = < {(i, [1, 100]), (j, [2, 101])} , {(i, 1+2Z), (j, 0+1Z)} ><S^A1(q9), S^B1(q9)> = < {(i, [3, 102]), (j, [2, 101])} , {(i, 1+2Z), (j, 0+1Z)} ><S^A1(q10), S^B1(q10)> = < {(i, [101, 102]), (j, [-∞, +∞])} , {(i, 1+2Z), (j, 0+1Z)} >

105

７．１０

直積ドメインでのエレメントのカウント(1)

前頁の結果から右のプログラムの各プログラムポイントqの通過回数|q|を求めます；
ループ処理以外では、|q0|=|q1|=|q10|=1
ループ処理では、ループL1とL2のスライシングを使用します； 5.2(2)より
L1のスライス={q2 , q3 , q9 }L2 のスライス= {q5 , q6 , q7 }ループL1のスライスでq3の通過回数|q3|はループL1の繰り返し回数となる
ので、これを前頁の結果

L1

L2<S^A1(q3), S^B1(q3)> = < {(i, [1, 100]), (j, [-∞, +∞])} , {(i, 1+2Z), (j, 0+1Z)} >から求めます。この式において、jはループL1のループ不変変数なのでL1のループ繰り返しとは無関係。
従って、|q3|=|(i, [1, 100])かつ(i, 1+2Z)|=50
106

７．１０

直積ドメインでのエレメントのカウント(2)ループL2のスライスでq6の通過回数|q6|はループL2の繰り返し回数となるので、これを前頁の結果<S^A1(q6), S^B1(q6)> = < {(i, [1, 100]), (j, [1, 100])} , {(i, 1+2Z), (j, 0+1Z)} >から求めます。この式において、iはループL2のループ不変変数なので、|q6|=|(j, [1, 100])かつ(j, 0+1Z)|=100が求まります。

L1

L2

107

７．１０

直積ドメインでのエレメントのカウント(3)■右のフローで、各プログラムポイントと対応する原子部分とその原子WCETを
q0⇔初期値設定=1, q1⇔i:=1（代入）=3
q2 ,q5⇔結合ノード（結合）=1
q3 , q6, q8, q10⇔i<=n（分岐）=2
q4⇔j:=1（代入）=3
q7⇔j:=j+1（代入）=8, q9⇔i:=i+1（代入）=8とすると、各プログラムポイントに対して原子WCETを関係させる関数ｌ(エル）は下記；
l(q0)=1, l(q1)=l(q4)=3, l(q2)=l(q5)=1,
l(q3)=l(q6)=l(q8)=l(q10)=2, l(q7)=l(q9)=8
従って、WCETの近似値=l(q0)*|q0|+l(q1)*|q1|+l(q10)*|q10|+{l(q2)+l(q3)+l(q4)+(l(q5)+l(q6)+l(q7))*|q6|+l(q8)+l(q9)}*|q3|=1*1+3*1+2*1+{1+2+3+(1+2+8)*100+2+8}*100
ループL2=6+{16+11*100}*50=55806

ループL1

108

７．１０

直積ドメインでのエレメントのカウント(4)７．１０（３）のWCET近似値=55806は、実際のWCET=27768の約2倍(55806/27768)となります。これは区間ドメインのみによるWCETを改善しています。

109

END

110