画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較

マシンビジョンの検査プログラムでは、3×3 のフィルターが画像の端で外側の画素を読んだり、幅と高さを取り違えて別の行に書き込んだりする誤りがよく起きます。テストに使った画像の大きさでは表に出ず、別のカメラにつないだときに初めて落ちることもあります。この記事では Ada のサブセットである SPARK で画像処理を書き、こうした画像の外へのアクセスが起きないことを GNATprove で証明します。

答えの要点は次のとおりです。2値化と 3×3 の平滑化は画像の型と事前条件を決めれば、実行時エラーが起きないことを証明できます。ラベルの対応表の添字を型で制限すれば、連結成分のラベリングでも同じ証明が通ります。ただし、ラベル付けの結果が正しいことや、仮ラベルの数が上限を超えないことまでは証明していません。証明できたユニットだけ実行時の検査を外すと、-O2 では C で書いた同じ処理とほぼ同じ速さになりました。

コードは2026年11月10日に確かめました。ビルドとテストは Ubuntu 24.04 の GNAT 13.3.0 で行い、GitHub Actions の Ubuntu 24.04 のランナーでも Alire 2.1.1 で入れた GNAT 16.1.0 で行いました。テストの10件はどちらの環境でも、検査を外したビルドを含めてすべて通りました。証明は同じランナーで GNATprove 16.1.0 を使って行いました。速度は GNAT 13.3.0 で測りました。SPARK と GNATprove の基本は「SPARKによる形式検証入門」で、契約の読み方は「AIが書いたコードをSPARKで証明する」で説明しています。

画像の外を読み書きする誤りが起きる場所

画像の外へアクセスする誤りは、だいたい決まった場所で起きます。1つ目は近傍を読む処理の端です。3×3 のフィルターを画像全体に掛けると、先頭の行では上の行を、最後の列では右の列を読もうとします。2つ目は行と列の取り違えです。幅と高さが同じテスト画像では誤りが表に出ず、横長のカメラ画像で初めて範囲を外れます。3つ目はラベリングのように、画素から求めた値を別の表の添字に使う処理です。値が想定の範囲を外れると、表の外を読み書きします。

C ではどれもエラーにならず、ほかのメモリを読み書きします。Ada では添字の検査が実行時に働いて Constraint_Error になりますが、検査装置の稼働中に例外が出れば、処理はそこで止まります。SPARK なら、こうした検査が事前条件を満たすどの入力でも失敗しないことを、実行する前に証明できます。SPARK のユーザーガイドは、実行時エラーがないことを証明する段階を Silver と呼んでいます。その効果として、バッファオーバーフローや整数のオーバーフローで制御の流れを乗っ取られないことと、検査を外してコンパイルしても誤動作しないことを挙げています¹。

flowchart TB
        accTitle: 画像の外へアクセスする誤りが起きる場所
        accDescr: 近傍を読む処理の端、行と列の取り違え、画素から求めた値を表の添字に使う処理の3か所で画像の外へのアクセスが起き、Cではエラーにならずにほかのメモリを読み書きし、Adaでは実行時の検査で例外になり、SPARKでは実行前に証明で見つけることを示す。
        A["近傍を読む処理の端"] --> D["画像の外へのアクセス"]
        B["行と列の取り違え"] --> D
        C["画素から求めた値を添字に使う"] --> D
        D --> E["C（ほかのメモリを読み書き）"]
        D --> F["Ada（実行時の検査で例外）"]
        D --> G["SPARK（実行前に証明で見つける）"]

図1: 画像の外へのアクセスは3か所で起きやすく、言語によって表れ方が違う。

図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全11件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle

画像を Ada の型で表す

まず画像の型を決めます。行と列の添字にそれぞれ範囲を持たせた部分型を作り、画素は 0 から 255 までのモジュラー型にします。画像は行と列の範囲をオブジェクトごとに決める2次元の配列です。

package Images with SPARK_Mode is

   Max_Width  : constant := 4096;
   Max_Height : constant := 4096;

   subtype Row    is Natural range 0 .. Max_Height - 1;
   subtype Column is Natural range 0 .. Max_Width - 1;

   type Pixel is mod 2 ** 8;

   type Image is array (Row range <>, Column range <>) of Pixel;

   function Same_Shape (A, B : Image) return Boolean is
     (A'First (1) = B'First (1) and then A'Last (1) = B'Last (1)
      and then A'First (2) = B'First (2) and then A'Last (2) = B'Last (2));

end Images;

Image は配列の範囲を決めない型なので、640×480 の画像も 1920×1200 の画像も同じ型で扱えます。各画像の範囲は Img'Range (1)（行）と Img'Range (2)（列）で取り出せます。Same_Shape は2つの画像の行と列の範囲が等しいことを表す関数で、あとで事前条件に使います。式関数として仕様に書いたので、GNATprove はほかのユニットの証明でもこの比較の中身を使えます²。幅と高さの上限は 4096 にしました。添字を 0 から始めたのは、C やカメラの SDK の添字と合わせるためです。

flowchart TB
        accTitle: 画像の型の組み立て
        accDescr: 画像の型Imageは、行の部分型Rowと列の部分型Columnを添字に、画素の型Pixelを要素に持つ2次元配列で、Same_Shapeが2つの画像の行と列の範囲が等しいかを表すことを示す。
        R["Row（0〜4095）"] --> I["Image（2次元配列）"]
        C["Column（0〜4095）"] --> I
        P["Pixel（0〜255）"] --> I
        I --> S["Same_Shape（範囲が等しいか）"]

図2: 画像の型は行と列の範囲と画素の型から組み立てる。

2値化は型と事前条件だけで証明できる

2値化はしきい値以上の画素を 255 に、それ未満の画素を 0 にする処理です。入力と出力の範囲が同じであることを事前条件に書き、すべての画素がしきい値との比較の結果になることを事後条件に書きます。

   procedure Binarize
     (Source    : Image;
      Threshold : Pixel;
      Target    : in out Image)
   with
     Pre  => Same_Shape (Source, Target),
     Post =>
       (for all Y in Source'Range (1) =>
          (for all X in Source'Range (2) =>
             Target (Y, X) =
               (if Source (Y, X) >= Threshold then 255 else 0)));

出力の Target は in out にしました。呼び出し側が確保した配列の範囲は out の引数でも使えるので、out にできないわけではありません。out にすると、要素を1つずつ書く入れ子のループで配列全体が初期化されたことを GNATprove に示す必要があり、そのための指定（Relaxed_Initialization など）が要ると考えられます。この記事では out の形は試していません。in out にしたので、SPARK で書いた呼び出し側は、呼ぶ前に Target を初期化しておく必要があります。ラベリングの Labels と Parent も同じです。本体は入力の範囲でループを回して出力に書き込みます。

   procedure Binarize
     (Source    : Image;
      Threshold : Pixel;
      Target    : in out Image)
   is
   begin
      for Y in Source'Range (1) loop
         for X in Source'Range (2) loop
            Target (Y, X) := (if Source (Y, X) >= Threshold then 255 else 0);

            pragma Loop_Invariant
              (for all C in Source'First (2) .. X =>
                 Target (Y, C) =
                   (if Source (Y, C) >= Threshold then 255 else 0));
            pragma Loop_Invariant
              (for all R in Source'First (1) .. Y - 1 =>
                 (for all C in Source'Range (2) =>
                    Target (R, C) =
                      (if Source (R, C) >= Threshold then 255 else 0)));
         end loop;

         pragma Loop_Invariant
           (for all R in Source'First (1) .. Y =>
              (for all C in Source'Range (2) =>
                 Target (R, C) =
                   (if Source (R, C) >= Threshold then 255 else 0)));
      end loop;
   end Binarize;

Source (Y, X) の添字はループの範囲そのものなので、検査が失敗しないことは明らかです。Target (Y, X) の添字は、事前条件の Same_Shape から入力と同じ範囲にあることが分かります。画像の外にアクセスしないことを示すだけなら、ループ不変条件は要りません。

ループ不変条件は事後条件のために書きました。内側のループでは、いまの行の X 列目までと、それより上の行がすべて正しいことを書き、外側のループでは、Y 行目までのすべての行が正しいことを書いています。SPARK のユーザーガイドによれば、ループが配列を書き換えるときは、書き換えていない部分が変わらないことも不変条件に書く必要がある場合があります。これを frame condition と呼びます³。上の行が正しいまま残ることを書いた2つ目の不変条件は、すでに書いた範囲が崩れないことを示す点で、これと同じ役割をします。

flowchart TB
        accTitle: 2値化のループ不変条件が表す範囲
        accDescr: 内側のループの不変条件が、Y行目より上のすべての行と、Y行目のX列目までが正しく書けていることを表し、外側のループの不変条件がY行目までのすべての行を表し、ループを抜けると事後条件のすべての画素に広がることを示す。
        A["Y 行目より上の行（すべて正しい）"] --> C["内側のループの不変条件"]
        B["Y 行目の X 列目まで（正しい）"] --> C
        C --> D["外側のループの不変条件（Y 行目まで）"]
        D --> E["事後条件（すべての画素）"]

図3: 不変条件が保証する範囲はループが進むにつれて広がり、最後に事後条件になる。

3×3 の平滑化で縁を読みに行く誤り

平滑化は各画素を周りの 3×3 の画素の平均で置き換える処理です。最初に、範囲を考えずに画像全体でループを回すコードを書いてみます。

      for Y in Source'Range (1) loop
         for X in Source'Range (2) loop
            Sum := Natural (Source (Y - 1, X - 1))
                 + Natural (Source (Y - 1, X))
                 + Natural (Source (Y - 1, X + 1))
                 + Natural (Source (Y, X - 1))
                 + Natural (Source (Y, X))
                 + Natural (Source (Y, X + 1))
                 + Natural (Source (Y + 1, X - 1))
                 + Natural (Source (Y + 1, X))
                 + Natural (Source (Y + 1, X + 1));
            Target (Y, X) := Pixel (Sum / 9);
         end loop;
      end loop;

C で同じように書いても、コンパイルは通ります。GNATprove にかけると、近傍の添字の検査を証明できないと4か所で報告されました。報告は添字のずらし方（Y - 1、X - 1、Y + 1、X + 1）ごとに1か所ずつでしたが、範囲の外になりうる添字は12か所あります。報告の数が危ない添字の数を表すわけではありません。そのうちの1つが次の出力です。

 medium: array index check might fail
--> smooth_bug.adb:13:39
   13 |                     + Natural (Source (Y - 1, X + 1))
      |                                        ~~^~~
      + reason for check: result of subtraction must be a valid index into the array
      + provers reached time limit before completing the proof

Y が先頭の行のとき、Y - 1 は画像の範囲の外です。GNATprove は証明できなかった検査について、場所と、検査が求める条件（ここでは引き算の結果が配列の正しい添字であること）を示します。--level を指定すると失敗する値の例（反例）も生成されることがありますが⁴、この実行では反例は表示されず、証明器が時間の上限に達したと表示されました。行と列を取り違えて Source (X, Y) と書いたコードでも、Source (X, Y) の2つの添字の検査を証明できないと報告されました。

直したコードは縁の1画素を除いた内側だけでループを回し、縁には入力をそのまま写します。

   procedure Smooth_3x3
     (Source : Image;
      Target : in out Image)
   with
     Pre => Source'Length (1) > 0
              and then Source'Length (2) > 0
              and then Same_Shape (Source, Target);

   procedure Smooth_3x3
     (Source : Image;
      Target : in out Image)
   is
      Sum : Natural;
   begin
      Target := Source;

      for Y in Source'First (1) + 1 .. Source'Last (1) - 1 loop
         for X in Source'First (2) + 1 .. Source'Last (2) - 1 loop
            Sum := Natural (Source (Y - 1, X - 1))
                 + Natural (Source (Y - 1, X))
                 + Natural (Source (Y - 1, X + 1))
                 + Natural (Source (Y, X - 1))
                 + Natural (Source (Y, X))
                 + Natural (Source (Y, X + 1))
                 + Natural (Source (Y + 1, X - 1))
                 + Natural (Source (Y + 1, X))
                 + Natural (Source (Y + 1, X + 1));
            Target (Y, X) := Pixel (Sum / 9);
         end loop;
      end loop;
   end Smooth_3x3;

ループの範囲を内側に絞ったので、Y - 1 から Y + 1 までと X - 1 から X + 1 までは、どれも画像の中に収まります。画像が縦横どちらかで3画素に満たない場合は、内側の範囲が空になり、出力は入力の写しになります。Target := Source の配列の長さの検査は、事前条件の Same_Shape から証明されます。9つの画素の合計は 255 の9倍の 2295 を超えないので、Natural であふれないことと、9で割った結果が Pixel の範囲に収まることも証明されます。

flowchart TB
        accTitle: 平滑化のループの範囲
        accDescr: 画像全体でループを回すコードは先頭の行でY-1が範囲の外になってGNATproveが添字の検査を証明できず、縁を除いた内側でループを回して縁には入力を写すコードはすべての検査を証明できることを示す。
        A["3×3 の平滑化"] --> B["画像全体でループ"]
        A --> C["縁を除いた内側でループ"]
        B --> D["先頭の行で Y - 1 が範囲の外"]
        D --> E["添字の検査を証明できない"]
        C --> F["縁には入力をそのまま写す"]
        F --> G["すべての検査を証明"]

図4: ループの範囲を内側に絞ると、近傍の添字がすべて画像の中に収まる。

空の画像で範囲の計算があふれる

事前条件の「画像が空でない」という2行は、最初は書いていませんでした。Same_Shape だけの事前条件で GNATprove にかけると、内側の範囲を計算する Source'First (1) + 1 と Source'Last (1) - 1、列の同じ2つの計算の4か所で、あふれの検査を証明できないと報告されました。

 medium: overflow check might fail, cannot prove upper bound for Source'First (1) + 1
--> image_ops.adb:40:33
   40 |          for Y in Source'First (1) + 1 .. Source'Last (1) - 1 loop
      |                   ~~~~~~~~~~~~~~~~~^~~
      + reason for check: result of addition must fit in a 32-bits machine integer
      + provers reached time limit before completing the proof

原因は空の画像です。Ada では、空の範囲の境界は部分型の範囲に収まっていなくてよく、配列の添字が取る範囲もこの規則で確かめられます⁵⁶。そのため、行の範囲が Integer'Last .. Integer'Last - 1 という空の画像も Image 型として作れます。このとき Source'First (1) + 1 は Integer の範囲を超えます。実際に GNAT 13.3.0 でこの画像を渡すと、image_ops.adb の40行目で Constraint_Error（overflow check failed）が発生しました。

そこで、画像が縦横とも空でないことを事前条件に足しました。空でない画像なら範囲の境界は Row と Column に収まるので、+ 1 と - 1 はあふれません。テストでは同じ空の画像を渡すと、事前条件の検査で Assertion_Error になることを確かめています。

flowchart TB
        accTitle: 空の画像で範囲の計算があふれる理由
        accDescr: 空の範囲の境界は部分型の外にあってよいので、範囲がInteger'Lastから始まる空の画像を作れ、そのFirst足す1がIntegerの範囲を超えるため、画像が空でないことを事前条件に足すと境界がRowとColumnに収まってあふれなくなることを示す。
        A["空の範囲の境界は部分型の外でもよい"] --> B["Integer'Last から始まる空の画像"]
        B --> C["First（1）+ 1 があふれる"]
        C --> D["事前条件に空でないことを足す"]
        D --> E["境界は Row と Column に収まる"]

図5: 空の画像では範囲の境界が添字の型の外にありうるので、事前条件で空の画像を除く。

事前条件を守る責任は呼び出し側にある

GNATprove は本体を証明するときに、事前条件が成り立つと仮定します。その代わり、SPARK で書いた呼び出し側では、呼ぶたびに事前条件が成り立つことを証明する必要があります²。入力と出力に同じ画像を渡すような、引数どうしの重なりも、SPARK の呼び出し側では GNATprove が調べます⁷。

問題は SPARK ではないコードから呼ぶ場合です。カメラの SDK から画像を受け取る部分や、C# のアプリから呼ばれる部分は、SPARK の外に置くことが多く、そこでは事前条件が守られている保証がありません。証明していないコードから証明したサブプログラムを呼ぶ場合について、SPARK のユーザーガイドは pragma Assertion_Policy で事前条件を実行時に検査するよう勧めています⁸。そこで、証明した image_ops.ads と labeling.ads の先頭に、事前条件の検査だけを有効にする指定を書きました。

pragma Assertion_Policy (Pre => Check);
with Images; use Images;

package Image_Ops with SPARK_Mode is

GNAT は -gnata を付けたときに、事前条件や事後条件、ループ不変条件をまとめて実行時に検査します⁹。-gnata ではなくこの指定にしたのは、事前条件だけを残すためです。2値化のループ不変条件まで検査すると、画素ごとに、それまでに書いた範囲全体を確かめる式を評価することになります。

この指定は呼ばれる側のユニットに書く必要があります。-gnatG でコンパイラーが展開したコードを見ると、事前条件の検査は呼ばれる側の Binarize や Smooth_3x3 の先頭に組み込まれていました。GNAT 13.3.0 で試すと、指定を書かずに image_ops.adb を -gnatp でコンパイルした場合、呼ぶ側を -gnata でコンパイルしても、空の画像を渡した平滑化は例外を出さずに戻りました。これは検査を外した状態での誤った実行で、規格は結果を定めていません¹⁰。指定を書いたあとは、-gnatp でコンパイルしても事前条件の検査で Assertion_Error になりました。

flowchart TB
        accTitle: 事前条件を確かめる場所
        accDescr: SPARKの呼び出し側ではGNATproveが呼び出しのたびに事前条件を証明し、SPARKではない呼び出し側からの呼び出しでは呼ばれる側に組み込んだ実行時の検査で事前条件を確かめ、本体はどちらの場合も事前条件が成り立つと仮定して証明されることを示す。
        A["SPARK の呼び出し側"] -->|"GNATprove が証明"| C["事前条件"]
        B["SPARK ではない呼び出し側"] -->|"呼ばれる側で実行時に検査"| C
        C --> D["本体の証明の前提"]

図6: 事前条件は、呼び出し側が SPARK かどうかで確かめ方が変わる。

flowchart TB
        accTitle: 検査を外したビルドで事前条件を残す方法
        accDescr: 証明していない呼び出し側から呼ぶとき、事前条件の検査は呼ばれる側のユニットに組み込まれるので、呼ばれる側の仕様にAssertion_Policyの指定があれば-gnatpでコンパイルしても事前条件が検査され、指定がなければ呼ぶ側に-gnataを付けても検査されず、空の画像で例外を出さずに戻ったことを示す。
        A["証明していない呼び出し側"] --> B["Smooth_3x3 の呼び出し"]
        B --> C{"呼ばれる側に指定があるか"}
        C -->|"ある"| D["-gnatp でも事前条件を検査"]
        C -->|"ない"| E["呼ぶ側の -gnata は効かない"]
        E --> F["空の画像で例外を出さずに戻った"]

図7: 事前条件の検査は呼ばれる側に組み込まれるので、指定も呼ばれる側の仕様に書く。

ラベリングでは対応表の添字を型で制限する

連結成分のラベリングは、2値画像のつながった画素の塊ごとに番号を付ける処理です。ここでは、Rosenfeld と Pfaltz が示した、2回の走査でラベルを付ける方法を使います¹¹。4近傍（上下左右）でつながった画素を同じ塊とします。

1回目の走査では画素ごとに上と左の画素のラベルを見ます。どちらにもラベルがなければ新しいラベルを付け、片方だけにあればそのラベルを写し、両方にあれば2つのラベルが同じ塊に属することを対応表に記録します。2回目の走査では各画素のラベルをその塊の代表のラベルに置き換えます。最後に、代表のラベルの数を数えると、塊の数になります。

flowchart TB
        accTitle: 2回の走査によるラベリング
        accDescr: 1回目の走査で上と左の画素のラベルを見て、新しいラベルを付けるか、ラベルを写すか、2つのラベルを対応表で同じ塊にまとめ、2回目の走査で各画素のラベルを代表のラベルに置き換え、最後に代表の数を数えることを示す。
        A["1回目の走査"] --> B{"上と左のラベル"}
        B -->|"どちらもない"| C["新しいラベルを付ける"]
        B -->|"片方だけある"| D["そのラベルを写す"]
        B -->|"両方ある"| E["対応表で同じ塊にまとめる"]
        C --> F["2回目の走査で代表のラベルにそろえる"]
        D --> F
        E --> F
        F --> G["代表のラベルの数を数える"]

図8: 1回目の走査で仮のラベルと対応を記録し、2回目で代表のラベルにそろえる。

型は次のように決めました。

with Images; use Images;

package Labeling with SPARK_Mode is

   Max_Labels : constant := 2 ** 22;

   subtype Label    is Natural range 0 .. Max_Labels;  --  0 は背景
   subtype Label_Id is Label range 1 .. Max_Labels;

   type Label_Image  is array (Row range <>, Column range <>) of Label;
   type Parent_Table is array (Label_Id) of Label_Id;

   procedure Label_Components
     (Source  : Image;
      Labels  : in out Label_Image;
      Parent  : in out Parent_Table;
      Count   : out Natural;
      Success : out Boolean)
   with
     Pre => Labels'First (1) = Source'First (1)
              and then Labels'Last (1) = Source'Last (1)
              and then Labels'First (2) = Source'First (2)
              and then Labels'Last (2) = Source'Last (2);

end Labeling;

Parent_Table は添字の型も要素の型も Label_Id なので、表から取り出した値はどれも表の正しい添字になります。代表を探す Find は Parent (Root) をたどり続けるだけです。Root の型も Label_Id なので、この添字には証明すべき検査が生じず、GNATprove の出力でも Find の検査は0件でした。ループ不変条件も要りません。

   procedure Find
     (Parent : Parent_Table;
      L      : Label_Id;
      Root   : out Label_Id)
   is
   begin
      Root := L;
      while Parent (Root) /= Root loop
         Root := Parent (Root);
      end loop;
   end Find;

Find を関数ではなく手続きにしたのは、必ず終わることの証明を求められないようにするためです。GNATprove は通常の関数については必ず終わることを無条件に検証し、手続きについては Always_Terminates を付けたときだけ検証します¹²。Find が終わることは、使っているラベルがどれも自分以下の番号を指していることから言えますが、それを証明するには、対応表全体についての不変条件が要ります。この記事では、証明の対象を実行時エラーがないことに絞りました。

1回目の走査は次のとおりです。

      for Y in Source'Range (1) loop
         for X in Source'Range (2) loop
            if Source (Y, X) = 0 then
               Labels (Y, X) := 0;
            else
               Up   := (if Y > Source'First (1) then Labels (Y - 1, X) else 0);
               Left := (if X > Source'First (2) then Labels (Y, X - 1) else 0);

               if Up = 0 and then Left = 0 then
                  if Next > Max_Labels then
                     return;  --  ラベルが足りない
                  end if;
                  Parent (Next) := Next;
                  Labels (Y, X) := Next;
                  Next := Next + 1;
               elsif Left = 0 then
                  Labels (Y, X) := Up;
               elsif Up = 0 then
                  Labels (Y, X) := Left;
               else
                  Find (Parent, Up, Root_Up);
                  Find (Parent, Left, Root_Left);
                  if Root_Up < Root_Left then
                     Parent (Root_Left) := Root_Up;
                  elsif Root_Left < Root_Up then
                     Parent (Root_Up) := Root_Left;
                  end if;
                  Labels (Y, X) := Label'Min (Root_Up, Root_Left);
               end if;
            end if;
         end loop;
      end loop;

上と左の画素を読む前に、Y > Source'First (1) と X > Source'First (2) を確かめているので、先頭の行と列でも画像の外は読みません。Labels の範囲は事前条件で Source と等しいので、Labels (Y - 1, X) の添字の検査も証明されます。

新しいラベルを付ける前には、Next が Max_Labels を超えていないかを確かめ、超えていたら Success を False のまま戻ります。この確認がなければ、Next が Max_Labels + 1 になったところで Parent (Next) に書くことになり、添字の検査が失敗します。上限がかかるのは塊の数ではなく、1回目の走査で付ける仮ラベルの数です。仮ラベルはあとで同じ塊にまとめられるものも1つずつ数えます。1行の中で新しい仮ラベルが付く画素は隣り合わないので、1行では多くても幅の半分（切り上げ）、画像全体では「高さ × 幅の半分（切り上げ）」個です。これが上限の 4,194,304 以下の画像（たとえば幅 4096、高さ 2048 まで）は、どんな模様でも失敗しません。4096×4096 の市松模様は、4近傍では画素がすべて別の塊になるので、仮ラベルが 8,388,608 個要ります。テストではこの画像で Success が False になることを確かめました。塊が少なくても失敗することはあります。(X + Y) mod 3 /= 2 の画素を前景にした斜めの縞の画像は、3000×3000 では成功して塊は 2,000 個でした。4096×4096 では、計算すると塊は約 2,730 個しかありませんが、仮ラベルが足りず Success が False になりました（GNAT 13.3.0 で確かめました）。失敗したときの Labels には途中までの仮ラベルが残っているので、使わないでください。

flowchart TB
        accTitle: 対応表の添字を型で制限する
        accDescr: Parent_Tableは添字も要素もLabel_Idなので、表から取り出した値がそのまま正しい添字になってFindの添字には検査が生じず、新しいラベルを付ける前にはNextが上限以下かを確かめ、超えていたら失敗を返すことを示す。
        A["Parent_Table（添字も要素も Label_Id）"] --> B["取り出した値はそのまま正しい添字"]
        B --> C["Find の添字には検査が生じない"]
        D["新しいラベルを付ける"] --> E{"Next が上限以下か"}
        E -->|"はい"| F["Parent（Next）に書く"]
        E -->|"いいえ"| G["Success を False のまま戻る"]

図9: 型で添字を制限する部分と、実行時に上限を確かめる部分を分ける。

ラベリングについて GNATprove で証明したのは、実行時エラーがないことだけです。同じ塊の画素に同じラベルが付き、別の塊には別のラベルが付くという結果の正しさは、証明していません。結果はテストで確かめました。テストのプログラムでは U の字の形でラベルの値と塊の数を、離れた2つの塊と 4×4 の市松模様で塊の数を確かめています。C で書いた同じ処理とも結果を比べ、64×48（45個の塊）と 1920×1200（10,477個の塊）の画像でラベルの値まで一致しました。ただし C の処理は同じ手順を移したものなので、一致して分かるのは移し方が正しいことだけです。そこで別の方法とも比べました。乱数で作った 1×1 から 9×9 までの画像2万個（添字の始まりも 0 から 4 まで変えたもの）で、塗りつぶしで求めた塊の分け方とラベリングの結果を比べ、9画素を直接足して求めた平均と平滑化の結果も比べました。食い違いは0件でした。この比較はテストのプログラムとは別に GNAT 13.3.0 で動かしました。

flowchart TB
        accTitle: ラベリングで確かめたことと確かめていないこと
        accDescr: 実行時エラーがないことはGNATproveで証明し、ラベル付けの結果は小さな画像のテスト、乱数の画像での塗りつぶしとの比較、Cの実装との比較で確かめ、Findが終わることと仮ラベルの数が上限を超えないことは確かめておらず、上限を超えたら失敗を返すことを示す。
        A["ラベリング"] --> P["GNATprove で証明"]
        A --> T["テストで確認"]
        A --> U["未確認"]
        P --> B["実行時エラーがない"]
        T --> C["結果が期待どおり"]
        U --> D["Find が終わる"]
        U --> E["仮ラベルが上限を超えない"]
        E -.-> F["超えたら失敗を返す"]

図10: ラベリングでは証明、テスト、未確認の範囲を分けて扱う。

GNATprove の実行結果

証明は Alire で入れた GNATprove を次のコマンドで実行しました。

alr exec -- gnatprove -P img_proof.gpr -j0 --level=2 --report=all

--report=all を付けると、証明できた検査も一つずつ表示されます。

事前条件に「画像が空でない」を足す前の実行では、107件の検査のうち103件が証明され、残る4件は、前の節で示した平滑化で内側の範囲を求める計算でした。2値化の26件とラベリングの32件はすべて証明され、2値化の事後条件とループ不変条件も証明されました。

事前条件を足したあとは107件すべての検査が証明され、出力の最後に Success: all checks proved (107 checks). と表示されました。内訳は、証明器が証明した97件（2値化26件、平滑化39件、ラベリング32件）と、フロー解析で確かめた変数の初期化9件とサブプログラムの終了1件です。わざと誤りを入れたコードでは、前の節で示したとおり、添字の検査を証明できないと報告されます。

flowchart TB
        accTitle: GNATproveが検査を証明する流れ
        accDescr: GNATproveがSPARKのコードの添字と範囲とあふれの検査と契約を証明しようとし、証明できたものと、場所と理由を添えて報告するものに分けることを示す。
        A["SPARK のコード"] --> B["GNATprove"]
        B --> C["添字・範囲・あふれの検査と契約"]
        C --> D["証明できた"]
        C --> E["証明できない（場所と理由を示す）"]

図11: GNATprove は検査と契約を一つずつ証明し、証明できないものは場所と理由を添えて報告する。

証明できたユニットだけ実行時の検査を外す

GNAT は添字や範囲、あふれの検査を既定で有効にします。-gnatp を付けると、そのユニットは pragma Suppress (All_Checks) があるものとしてコンパイルされ、妥当性の検査も外れます¹³。Ada の規格は、検査を外した状態でその検査が失敗する状況が起きたら、実行は誤り（erroneous）になると定めています¹⁰。証明していないコードで検査を外すと、C と同じく、画像の外へのアクセスが何を引き起こすか分からなくなります。

SPARK のユーザーガイドは、プログラム全体に -gnatp を付けたり pragma Suppress を使ったりする方法には、誤りや攻撃から守られなくなるという問題があると説明しています。そのうえで、GNATprove で実行時エラーがないことを証明した部分だけ検査を外す方法を勧めています¹⁴。gprbuild ではソースファイルごとにコンパイラーのスイッチを指定できるので¹⁵、証明できた image_ops.adb と labeling.adb にだけ -gnatp を付けました。

   package Compiler is
      --  Ada と同じ GCC で C もコンパイルする（clang が選ばれないようにする）
      for Driver ("C") use "gcc";
      for Switches ("C") use (Opt, "-Wall");
      case Build is
         when "test" =>
            for Switches ("Ada") use ("-O1", "-g", "-gnata", "-gnateA", "-gnatwa");
         when "checks" =>
            for Switches ("Ada") use (Opt, "-gnatwa");
         when "nochecks" =>
            for Switches ("Ada") use (Opt, "-gnatwa");
            --  証明できた単位だけ、実行時の検査を外す
            for Switches ("image_ops.adb") use (Opt, "-gnatp");
            for Switches ("labeling.adb") use (Opt, "-gnatp");
      end case;
   end Compiler;

Opt は最適化のスイッチ（-O2 か -O3）を選ぶ変数です。テスト用のプログラムと速度を測るプログラムには、nochecks でも検査を残しています。証明したユニットの事前条件は、-gnatp を付けても前の節の pragma Assertion_Policy で検査されます。テストでも nochecks のビルドで、空の画像が事前条件の検査で止まることを確かめました。test のビルドの -gnateA は、呼び出しの実引数どうしが重なっていないかを実行時に確かめるスイッチです⁹。

検査を外す前に、SPARK のユーザーガイドが挙げる前提も確かめます⁸。証明していない呼び出し側からは、事前条件を守ってもらう必要があります。干渉しうる入力と出力を重ねて渡さないことも前提です。C# や SDK のコードから Smooth_3x3 (A, A) のように同じ画像を入力と出力に渡すと、エラーにならずに誤った結果になりえます。GNAT 13.3.0 で試すと、-gnateA を付けないビルドでは Smooth_3x3 (A, A) が例外を出さずに戻り、別々の画像に書いた場合と違う結果になりました。-gnateA を付けたテストのビルドでは、同じ呼び出しが Program_Error（aliased parameters）になりました。入力は正しい値でなければならず、たとえば Label の範囲を外れた値が入った配列を渡されることは想定していません。スタックのあふれ（Storage_Error）は GNATprove の対象外です。この記事の例では大きな画像と対応表をヒープに確保して渡し、スタックには置いていません。

flowchart TB
        accTitle: 実行時の検査を外す範囲の決め方
        accDescr: GNATproveですべての検査を証明できたユニットだけに-gnatpを付け、証明できなかったユニットは検査を残し、SPARKではない呼び出し側から呼ぶ場合は事前条件を実行時に検査することを示す。
        A{"すべての検査を証明できたか"} -->|"はい"| B["そのファイルだけ -gnatp"]
        A -->|"いいえ"| C["検査を残す"]
        B --> D{"呼び出し側は SPARK か"}
        D -->|"はい"| E["そのまま"]
        D -->|"いいえ"| F["事前条件を実行時に検査"]

図12: 検査を外すのは証明できたユニットだけにし、境界の事前条件は残す。

C で書いた同じ処理と速度を比べる

C で同じ3つの処理を書き（ラベリングも同じ順序で対応表をまとめる）、Ada の測定用のプログラムから両方を呼んで時間を比べました。毎回、Ada と C の結果が画素の値とラベルの値まで一致することを確かめています。測定の条件は次のとおりです。

• 画像は 1920×1200 で、擬似乱数で作りました。ラベリングにはその画像に平滑化を2回かけてから2値化した画像（10,477個の塊）を使いました。
• 2値化は200回、平滑化は100回、ラベリングは20回を1組として時間を測り、7組の中央値を1回あたりの時間にしました。この測定を4つのビルドで交互に7回ずつ繰り返し、表には7回の中央値と、Ada と C の比の最小から最大までを載せました。
• 「検査あり」は言語の検査（添字・範囲・あふれ）と、pragma Assertion_Policy で残した事前条件の検査です。事後条件とループ不変条件はどのビルドでも実行していません。
• 環境は Intel Xeon 2.10GHz の4コアのクラウドのコンテナ（Ubuntu 24.04、Linux 6.18）で、Ada も C も GCC 13.3.0（GNAT 13.3.0）でコンパイルしました。同じコンテナでほかの作業も動いていたので、比には2〜3割のばらつきがあります。表の値は目安として読んでください。

最初に測ったとき（事前条件の検査を残す指定を足す前のコード）は、-O2 で検査を残した Ada に比べて、C の2値化が約20倍、平滑化が約7倍速くなりました。gprbuild が C のコンパイラーとして clang（18.1.3）を選んでいて、clang の -O2 がこれらのループをベクトル化していたためです（-Rpass=loop-vectorize で確かめました）。指定を足した今のコードで、C だけを clang でコンパイルし直して3回測ると、2値化は約9〜10倍、平滑化は約6〜8倍でした。Ada と同じ GCC で比べるため、前の節の gpr ファイルで C の Driver を gcc に固定しました¹⁵。言語の速さを比べる前に、両方を同じコンパイラーと同じスイッチでコンパイルしているかを確かめる必要があります。

flowchart TB
        accTitle: 速度の比べ方
        accDescr: 測定用のAdaのプログラムが、同じGCCでコンパイルしたAdaの実装とCの実装を同じ画像で呼び、時間を測り、結果が画素の値とラベルの値まで一致することを毎回確かめることを示す。
        A["測定用のプログラム（Ada）"] --> B["Ada の実装"]
        A --> C["C の実装"]
        B --> D["同じ GCC 13.3.0 でコンパイル"]
        C --> D
        A --> E["時間を測る"]
        A --> F["結果の一致を毎回確かめる"]

図13: Ada と C の実装を同じコンパイラーでコンパイルし、同じ画像で結果と時間を比べる。

時間は Ada の1回あたりの時間です。検査ありのビルドで同時に測った C の時間（7回の中央値）は、-O2 では2値化が 1.77 ms、平滑化が 3.92 ms、ラベリングが 22.6 ms、-O3 では 0.182 ms、1.08 ms、20.5 ms でした。

-O2 では、検査を残すと平滑化は C の1.4〜2.1倍、ラベリングは約1.2倍の時間がかかり、証明したユニットの検査を外すと C とほぼ同じになりました。SPARK のユーザーガイドは、実行時の検査で実行時間が増えるのはふつう1割程度で、何度も呼ばれるコードではそれよりずっと増えることがあると書いています¹⁴。画素ごとのループはその何度も呼ばれるコードに当たります。-gnatG でフロントエンドが展開したコード（最適化の前の段階）を見ると、2値化では Source の添字の検査は消えていて、Target の行と列の添字の検査が画素ごとのループの中にありました。平滑化では、近傍の画素を読むたびに添字の検査が入っていました。

2値化だけは -O2 で検査を残しても C とほぼ同じ速さでした。これは事前条件の検査を残したためと考えられます。pragma Assertion_Policy の指定を外したコードと交互に5回ずつ測ると、検査を残した2値化は、指定がないときは C の2.02〜2.11倍、指定があるときは0.98〜1.02倍でした。入口で Same_Shape を確かめたあとは Target の範囲が Source と同じだと分かるので、GCC がループの中の Target の添字の検査を消せたのだと考えられます。次の段落のベクトル化の報告も、指定があるかどうかで変わりました。

GCC 12 からは -O2 でもベクトル化が有効ですが、コストモデルが very-cheap で、データの重なりなどを実行時に確かめる必要があるループはベクトル化しません¹⁶¹⁷。GCC 13.3.0 の -fopt-info-vec-missed で確かめると、-O2 の2値化のループは、Ada も C も「実行時に重なりを確かめる必要がある（would need a runtime alias check）」としてベクトル化されませんでした。事前条件の指定を外した Ada では、理由が「ループの中に分岐がある（control flow in loop）」になりました。平滑化のループは理由が分かれ、C と検査を外した Ada は同じく重なりの確認が理由でしたが、検査を残した Ada は「ループの中に分岐がある」が理由でした。ベクトル化を妨げていたのは、添字の検査による分岐です。

flowchart TB
        accTitle: -O2でループがベクトル化されなかった理由
        accDescr: GCC 13.3.0の-O2では、2値化のループはどのビルドでも、平滑化のループはCと検査を外したAdaで、実行時に重なりを確かめる必要があるためにベクトル化されず、検査を残したAdaの平滑化は添字の検査の分岐のためにベクトル化されず、-O3では重なりを確かめる版を作ることと分岐をループの外へ出すことでどちらもベクトル化されたことを示す。
        A["-O2 でベクトル化されない理由"] --> B["重なりの確認が要る（2値化など）"]
        A --> C["検査の分岐がある（検査ありの平滑化）"]
        B --> F["-O3：重なりを確かめる版を作る"]
        C --> G["-O3：分岐をループの外へ出す"]
        F --> H["-O3 ではベクトル化された"]
        G --> H

図14: -O2 でベクトル化を妨げた理由は、処理と検査の有無で違った。

-O3 では、2値化と平滑化で検査の有無による差がなくなりました。-O3 ではコストモデルが dynamic になり、重なりを実行時に確かめるコードを別に作ってベクトル化します。2値化は検査を残したままでもベクトル化されました。-O2 でコストモデルだけを dynamic にしても、2値化はベクトル化されました。平滑化も -O3 では検査を残したままベクトル化されましたが、-fno-unswitch-loops を付けるとベクトル化されませんでした。-O3 で有効になるループのアンスイッチング（ループの中の条件分岐をループの外へ出す最適化）が、検査の分岐を外へ出したためと考えられます¹⁷。ベクトル化されないラベリングでは、-O3 でも検査を残すと C より時間がかかりました。

flowchart TB
        accTitle: 検査を外したときの効果の違い
        accDescr: 検査を残したとき、-O2ではループがベクトル化されず平滑化とラベリングがCより遅くなり（2値化は事前条件の検査で添字の検査が消えてCと同程度）、-O3では2値化と平滑化がベクトル化されてラベリングだけがCより遅くなり、どちらの場合も証明したユニットの検査を外すとCと同程度になることを示す。
        A["検査を残したときの時間"] --> B["-O2（ベクトル化されない）"]
        A --> C["-O3（2値化と平滑化はベクトル化）"]
        B --> D["平滑化とラベリングが C より遅い"]
        C --> E["ラベリングだけ C より遅い"]
        D -.-> F["検査を外すと C と同程度"]
        E -.-> F

図15: 検査を外す効果は最適化の段階とループの形で変わる。

装置に載せる前に、実際に使うコンパイラーとスイッチで、検査ありとなしの両方を測ってから決めるのが確実です。

試した環境と確かめていないこと

この記事のコードについて、確かめた範囲をまとめます。

• 環境: ビルドとテストは Ubuntu 24.04 の GNAT 13.3.0 と、GitHub Actions の Ubuntu 24.04 のランナーの GNAT 16.1.0（Alire 2.1.1）で行いました。証明は同じランナーの GNATprove 16.1.0 で、--level=2 で行いました。速度は GNAT 13.3.0（GCC 13.3.0）で測りました。検証に使ったプロジェクト一式（gpr ファイルやテスト用のプログラム）は公開しておらず、記事のコードはその抜粋です。
• GNATprove で証明したこと: 2値化、3×3 の平滑化、ラベリングで、添字、範囲、あふれの検査が事前条件を満たすどの入力でも失敗しないこと。2値化の結果が事後条件のとおりになること。
• テストで確かめたこと: 平滑化とラベリングの結果が期待どおりであること（小さな画像の期待値、乱数で作った小さな画像2万個での別の方法との一致、C で書いた同じ処理との一致）。仮ラベルが足りなくなる画像で失敗を返すこと。空の画像が平滑化の事前条件の検査で止まること（検査を外したビルドを含む）。-gnateA を付けたビルドで、入力と出力に同じ画像を渡すと Program_Error になること。
• 確かめていないこと: Find が必ず終わること。平滑化とラベリングの結果の正しさの証明。スタックのあふれ。Windows と実際のカメラの画像での動作。

結果の正しさまで証明するには、ラベリングでは対応表全体についての不変条件を書く必要があります。画像の外へのアクセスがないことを先に証明し、結果の正しさはテストで確かめるという分け方なら、ループ不変条件をほとんど書かずに、境界外アクセスという深刻な不具合をなくせます。

関連記事

この記事はシリーズ「Ada とマシンビジョン」の1本です。シリーズのほかの記事です。

• GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー
• 取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
• Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る
• ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ

関係する既存の記事です。

• SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
• AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる
• Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで
• GigE Vision・USB3 Visionカメラの取りこぼし ── 原因の切り分けとWindows側の設定

参考リンク

関連する記事

同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。

関連トピック

このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。

このテーマがつながるサービス

この記事は次のサービスページにつながります。近い入口からご覧ください。

よくある質問

この記事のテーマについて、相談時によくある質問をまとめています。

画像処理のコードが画像の外を読み書きしないことは、SPARKで証明できますか？

できます。この記事では、2値化、3×3の平滑化、連結成分のラベリングについて、添字や範囲の検査が事前条件を満たすどの入力でも失敗しないことをGNATproveで証明しました。画像の型に行と列の範囲を持たせ、入力と出力の範囲が等しいことを事前条件に書くのが出発点です。

証明したら実行時の検査を外してよいですか？

GNATproveですべての検査を証明できたユニットだけ外すのが、SPARKのユーザーガイドの勧める方法です。証明していないコードから呼ぶ場合に備えて、証明したユニットの仕様にpragma Assertion_Policy (Pre => Check)を書き、事前条件の検査は残します。この記事の測定では、-O2で証明したユニットの検査を外すと、Cで書いた同じ処理とほぼ同じ速さになりました。

ラベリングの何を証明して、何を証明していませんか？

実行時エラーがないことは証明しました。ラベル付けの結果が正しいこと、代表のラベルを探す処理が必ず終わること、仮ラベルの数が上限を超えないことは証明していません。結果は小さな画像のテスト、乱数で作った小さな画像での別の方法との比較、Cで書いた同じ処理との比較で確かめました。仮ラベルの数が上限を超える画像では、失敗を返します。

著者プロフィール

記事の著者プロフィールページです。

小村 豪

合同会社小村ソフト 代表

Windows ソフト開発、技術相談、不具合調査を中心に、既存資産が残る案件や原因が見えにくい障害調査に強みがあります。