GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー

GigE Vision のカメラは撮った画像を GVSP（GigE Vision Streaming Protocol）で UDP のパケットに分けて送ります¹。受信する側はパケットの先頭にあるヘッダーを読んで、どの画像の何番目のパケットかを知ってから画像を組み立てます。ヘッダーの読み方を誤ると、短いパケットや壊れたパケットが届いたときに受信バッファの外を読んでしまいます。

Ada のレコードの表現句（record representation clause）は、各フィールドをバイト列のどこに置くかを指定します²。ヘッダーの配置図をそのまま型として書けます。ただし、受け取ったバイト列にその型を重ねて読む方法には落とし穴があります。この記事では表現句で書いたヘッダーの型と、バイト列から1フィールドずつ読み出す関数を比べます。どんなパケットを受けても読み出す関数が範囲外を読まないことを、SPARK で証明します。

先に結論を書くと、ネットワークから届くバイト列は長さを確かめてから1フィールドずつ読み出すほうが安全です。表現句の型は配置を示す資料として使う用途や、長さと値を確かめた後に使う用途に向いています。

コードは2026年11月10日に、手元の Ubuntu 24.04 の GNAT 13.3.0 でビルドして動かしました。証明は GitHub Actions の Ubuntu 24.04 のランナーで、Alire で入れた GNATprove（FSF 16.1.0）を使って行いました。同じランナーで Alire の GNAT 16.1.0 を使ってビルドして動かしても、出力は手元と同じでした。実際のカメラにはつないでおらず、試したパケットは手で組み立てたバイト列です。GigE Vision の仕様書は A3（Association for Advancing Automation）が配布していますが³、この記事では参照していません。フィールドの配置は公開されている Wireshark の GVSP の解析部⁴と、オープンソースのカメラ用ライブラリ Aravis の定義⁵を突き合わせて書きました。どちらにもない項目は書いていません。

GVSP のパケットとヘッダーの並び

カメラは1枚の画像を leader、payload、trailer の3種類のパケットに分けて送ります。leader には画像の幅・高さ・画素の形式が入り、payload には画素のデータが入ります。trailer は画像の終わりを知らせます。この3種類のほかに、leader・payload・trailer を1つにまとめた形式や H.264 などの形式も、Wireshark と Aravis の両方が定義しています⁴⁵。

flowchart TB
        accTitle: 1枚の画像を運ぶ GVSP のパケットの順序
        accDescr: カメラが1枚の画像を leader、複数の payload、trailer の順に送り、受信側がブロック ID とパケット ID で画像を組み立てることを示す。
        A["カメラ"] --> B["leader（幅・高さ・画素の形式）"]
        B --> C["複数の payload（画素のデータ）"]
        C --> D["trailer（画像の終わり）"]
        D --> E["受信側が ID で組み立てる"]

図1: 1枚の画像は leader、payload、trailer の順に送られ、受信側はブロック ID とパケット ID で組み立てる。

どのパケットも先頭にヘッダーがあり、ヘッダーは2バイトの状態コードで始まります。以下ではバイトの位置をパケットの先頭を0として数えます。ヘッダーには2つの形があります。位置4のバイトの最上位ビットが拡張 ID のフラグで、0 なら標準 ID の8バイトのヘッダー、1 なら拡張 ID の20バイトのヘッダーです。どちらの形でも、位置4のバイトの残りの7ビットがパケットの形式を表し、1 が leader、2 が trailer、3 が payload です。値はすべてビッグエンディアン（上位のバイトが先）で並んでいます⁴⁵。

flowchart TB
        accTitle: 標準 ID のヘッダー（8バイト）
        accDescr: 標準 ID のヘッダーが、状態コード2バイト、ブロック ID 2バイト、拡張 ID のフラグと形式の1バイト、パケット ID 3バイトの順に並ぶことを示す。
        A["位置0〜1：状態コード"] --> B["位置2〜3：ブロック ID（16ビット）"]
        B --> C["位置4：拡張 ID のフラグ（1ビット）"]
        C --> C2["位置4：形式（7ビット）"]
        C2 --> D["位置5〜7：パケット ID（24ビット）"]

図2: 標準 ID のヘッダーは8バイトで、ブロック ID が16ビット、パケット ID が24ビット。

拡張 ID のヘッダーでは、ブロック ID が64ビット、パケット ID が32ビットに広がります。標準 ID でブロック ID が入っていた位置2〜3にはフラグが入り、Wireshark はその中に再送されたパケットであることを示すビットなどを定義しています。位置5〜7はパケット ID としては使われず、パケット ID は位置16からの4バイトに移ります⁴⁵。

flowchart TB
        accTitle: 拡張 ID のヘッダー（20バイト）
        accDescr: 拡張 ID のヘッダーが、状態コード、フラグ、拡張 ID のフラグと形式、使わない3バイト、64ビットのブロック ID、32ビットのパケット ID の順に並ぶことを示す。
        A["位置0〜1：状態コード"] --> B["位置2〜3：フラグ"]
        B --> C["位置4：拡張 ID のフラグと形式"]
        C --> D["位置5〜7：パケット ID には使わない"]
        D --> E["位置8〜15：ブロック ID（64ビット）"]
        E --> F["位置16〜19：パケット ID（32ビット）"]

図3: 拡張 ID のヘッダーは20バイトで、ブロック ID とパケット ID の位置が標準 ID と違う。

画像の leader では、ヘッダーの直後に36バイトの情報が続きます。Wireshark と Aravis の定義を突き合わせると、並びは次のとおりです。先頭の2バイトはこの記事では読みません（Wireshark は先頭の1バイトだけを Field Info として解析し、Aravis は2バイトを16ビットの flags と定義しています）。Payload Type の値 0x0001 が画像を表し、0x4000 のビットは画像の後ろに付加情報（chunk）があることを表します⁴⁵。

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

表現句でヘッダーを型として書く

標準 ID のヘッダーを表現句で Ada の型にすると次のようになります。at の後ろがレコードの先頭からのバイトの位置、range の後ろがそのバイトから数えたビットの範囲です。

with Interfaces; use Interfaces;
with System;

package Gvsp_Layout is

   type Format_Code is
     (Leader, Trailer, Payload, All_In, H264, Multi_Zone, Multi_Part, Gen_DC);
   for Format_Code use
     (Leader => 1, Trailer => 2, Payload => 3, All_In => 4,
      H264 => 5, Multi_Zone => 6, Multi_Part => 7, Gen_DC => 8);
   for Format_Code'Size use 7;

   type Packet_Id_24 is mod 2 ** 24;

   --  標準 ID のヘッダー（8 バイト）
   type Standard_Header is record
      Status      : Unsigned_16;
      Block_Id    : Unsigned_16;
      Extended_Id : Boolean;
      Format      : Format_Code;
      Packet_Id   : Packet_Id_24;
   end record
     with Bit_Order            => System.High_Order_First,
          Scalar_Storage_Order => System.High_Order_First,
          Size                 => 64;

   for Standard_Header use record
      Status      at 0 range 0 .. 15;
      Block_Id    at 2 range 0 .. 15;
      Extended_Id at 4 range 0 .. 0;
      Format      at 4 range 1 .. 7;
      Packet_Id   at 5 range 0 .. 23;
   end record;

end Gvsp_Layout;

ヘッダーの図と型の宣言が1対1で対応するので、配置を確かめるときに読みやすい書き方です。形式は列挙型にして、for Format_Code use で各値に1〜8を割り当てています。

型に付けた2つの指定は役割が違います。

• Bit_Order は Ada の標準の属性で、表現句のビット番号の数え方を決めます。High_Order_First にすると、0番が最上位のビットになります⁶。ネットワークのヘッダーの図と同じ数え方なので、拡張 ID のフラグを at 4 range 0 .. 0 と書けます。
• Scalar_Storage_Order は GNAT 独自の属性で、標準の Ada にはありません。レコードの中の整数をメモリにどのバイト順で置くかを決めます⁷。GNAT のマニュアルは、レコードに指定するときは Bit_Order と同じ値にするよう定めています。

flowchart TB
        accTitle: Bit_Order と Scalar_Storage_Order の役割
        accDescr: Bit_Order は表現句のビット番号の数え方を決め、Scalar_Storage_Order は複数バイトの整数のバイト順を決め、両方そろってビッグエンディアンのヘッダーを正しく読めることを示す。
        A["表現句のレコード型"] --> B["Bit_Order（標準の属性）"]
        A --> C["Scalar_Storage_Order（GNAT 独自）"]
        B --> D["ビット番号の数え方が変わる"]
        C --> E["整数のバイト順が変わる"]
        D --> F["両方そろうと正しく読める"]
        E --> F

図4: Bit_Order はビット番号の数え方を、Scalar_Storage_Order は整数のバイト順を決める。

Bit_Order だけでは足りないことを、同じ4バイト 00 00 00 2A を2つの型で読んで確かめました。片方は Bit_Order だけを付けた型、もう片方は Scalar_Storage_Order も付けた型で、どちらもブロック ID を位置2〜3に置いています。x86-64 で動かした結果は次のとおりです。

Scalar_Storage_Order なし: Block_Id = 10752
Scalar_Storage_Order あり: Block_Id = 42

10752 は16進数で 0x2A00 です。x86-64 はリトルエンディアンなので、Bit_Order だけの型ではメモリで先にあるバイトを下位のバイトとして読み、42 が 10752 になりました。

次に、8バイトのバイト列を Ada.Unchecked_Conversion で Standard_Header に変換して読みます。変換元の型は後で説明するパーサーと同じ Gvsp.Byte_Array の8要素の部分型です。

   subtype Header_Bytes is Byte_Array (0 .. 7);

   function To_Header is
     new Ada.Unchecked_Conversion (Header_Bytes, Standard_Header);

   procedure Show (Label : String; Packet : Byte_Array) is
   begin
      declare
         H : constant Standard_Header :=
           To_Header (Packet (Packet'First .. Packet'First + 7));
      begin
         Put (Label & ": Block_Id =" & H.Block_Id'Image
              & " Packet_Id =" & H.Packet_Id'Image);
         if H.Format'Valid then
            Put_Line (" Format = " & H.Format'Image);
         else
            Put_Line (" Format は不正な値");
         end if;
      end;
   exception
      when Constraint_Error =>
         Put_Line (Label & ": Constraint_Error");
   end Show;

形式が3（payload）の正しいヘッダー、形式のバイトが 0x09 の壊れたヘッダー、5バイトしかないパケットの3つを渡しました。

Good  : Block_Id = 42 Packet_Id = 258 Format = PAYLOAD
Broken: Block_Id = 42 Packet_Id = 258 Format は不正な値
Short : Constraint_Error

正しいヘッダーはブロック ID 42、パケット ID 258（0x000102）と読めました。残りの2つは次に説明する落とし穴に当たっています。

バイト列に型を重ねるときの落とし穴

表現句の型でヘッダーを読む方法には、4つの落とし穴があります。

flowchart TB
        accTitle: 型を重ねて読むときの落とし穴
        accDescr: 受け取ったバイト列に表現句の型を重ねて読むと、番地による重ね合わせ、短いパケット、形式の不正な値、拡張 ID による長さの違いの4つで問題が起きることを示す。
        A["受け取ったバイト列に型を重ねる"] --> B["番地で重ねる"]
        A --> C["短いパケット"]
        A --> D["形式が想定外の値"]
        A --> E["拡張 ID"]
        B --> F["格納順を変える型は GNAT が非対応"]
        C --> G["大きさが足りない"]
        D --> H["列挙型が不正な値"]
        E --> I["1つの型で表せない"]

図5: 型を重ねて読む方法は、番地、長さ、値、ヘッダーの形の4か所で問題が起きる。

番地で重ねる方法は GNAT が動作を保証しない

C の構造体のポインターのように、受信バッファの番地にレコードを置く書き方（with Address => Buffer'Address）もできます。ただし、番地を指定したオブジェクトでは、その番地が型に合っていることをプログラマーが保証する必要があります。合っていなければ実行は erroneous（言語として結果を定めない状態）になります⁸。型の Alignment に合わない番地に置いた場合も同じです。さらに GNAT のマニュアルはスカラーの格納順を変える重ね合わせには対応しないと書いており、そうした書き方には警告を出すとしています。対応しているのは Ada.Unchecked_Conversion による変換です⁷。この記事の例が変換を使っているのはそのためです。

実際に、Scalar_Storage_Order を付けた Standard_Header を Byte_Array の番地に重ねる宣言を GNAT 13.3.0 でコンパイルすると、次の警告が出ました。

overlay_warning.adb:7:59: warning: overlay changes scalar storage order [enabled by default]

短いパケットでは型の大きさに足りない

変換するには、ちょうど8バイトのバイト列が要ります。5バイトのパケットから8バイトを切り出そうとすると、Ada は配列の範囲の検査で Constraint_Error を出します。上の Short の行がその結果です。C で構造体のポインターを重ねた場合と違い、範囲外を黙って読むことはありません。

ただし、-gnatp などで検査を外したビルドでは、この検査も消えます。検査を外した状態で範囲外を読むと、実行は erroneous です⁹。また、検査が残っていても、受信のループで例外が出れば、例外を捕まえない限り受信が止まります。

形式に想定外の値が来ると列挙型が不正な値になる

形式のバイトが 0x09 のヘッダーを変換すると、Format には1〜8のどれでもない値が入ります。Ada は型のどの値も表さない表現を不正な表現（invalid representation）と呼びます。レコードのようなスカラーでない型への Unchecked_Conversion で結果が型の値を表さないとき、その効果は処理系が定め、結果は異常（abnormal）になりえます¹⁰。異常なオブジェクトを使うと実行は erroneous になります。スカラーの型への変換の結果が不正なときの扱いは、データの妥当性の規則が定めています¹¹。'Valid 属性は、変換などで作ったデータが正しい値かを確かめるためにあります¹²。上の例では、H.Format'Valid が偽になり、「不正な値」と表示しました。

それでもこの例の動作が定まっているのは、GNAT が同じ大きさの型の間の Unchecked_Conversion を、ビットをそのまま写すものと定めているためです¹³。レコードの各成分はバイト列のビットの写しで、不正な値になるのは Format の成分だけです。そのため Block_Id などを読んだうえで、'Valid で Format を確かめられます。これは処理系が定める動作で、ほかの処理系でも同じになるとは限りません。

flowchart TB
        accTitle: 変換した値を使う前に Valid で確かめる
        accDescr: Unchecked_Conversion で作ったヘッダーの形式を、使う前に Valid 属性で確かめ、偽ならパケットを捨てることを示す。
        A["Unchecked_Conversion でヘッダーを作る"] --> B{"Format'Valid は真か"}
        B -->|"真"| C["形式に応じて処理する"]
        B -->|"偽"| D["パケットを捨てる"]

図6: 変換で作った列挙型の値は使う前に Valid で確かめる。

'Valid を呼び忘れても、コンパイラーはエラーも警告も出しません。確かめるべきフィールドが増えるほど、忘れやすくなります。

拡張 ID ではヘッダーの形そのものが変わる

拡張 ID のフラグが立つと、ヘッダーは20バイトになり、ブロック ID とパケット ID の位置も変わります。どちらの型で読むかは位置4のバイトのフラグを読んでからでないと決まりません。結局、型を重ねる前にバイトを1つ読むことになります。

長さを確かめてからバイト列を読み出す

落とし穴を避けるには、パケットの長さを確かめてから、必要なバイトを1つずつ読み出して値を組み立てます。受け取ったバイトの配列と、そこから読み出す関数を次のように宣言しました。

   --  UDP のデータ部の最大長より大きい値を、添字の上限にする。
   subtype Packet_Index is Natural range 0 .. 65_535;
   type Byte_Array is array (Packet_Index range <>) of Unsigned_8;

読み出した値を入れるヘッダーの型、形式、結果、長さの定数は次のように宣言しました。ヘッダーの型には表現句を付けず、バイトの並びとは切り離しています。

   type Packet_Format is
     (Leader, Trailer, Payload, All_In, H264, Multi_Zone, Multi_Part, Gen_DC);

   type Parse_Result is (Ok, Too_Short, Unknown_Format, Not_Leader, Not_Image);

   Standard_Header_Length : constant := 8;
   Extended_Header_Length : constant := 20;
   Image_Leader_Length    : constant := 36;

   type Gvsp_Header is record
      Status_Code : Unsigned_16   := 0;
      Flags       : Unsigned_16   := 0;  --  拡張 ID のときだけ
      Extended_Id : Boolean       := False;
      Format      : Packet_Format := Leader;
      Block_Id    : Unsigned_64   := 0;
      Packet_Id   : Unsigned_32   := 0;
      Data_Offset : Natural       := 0;  --  データ部の先頭（パケットの先頭から）
   end record;

   function Read_U16 (P : Byte_Array; Offset : Natural) return Unsigned_16
   with Pre => P'Length >= 2 and then Offset <= P'Length - 2;

   function Read_U32 (P : Byte_Array; Offset : Natural) return Unsigned_32
   with Pre => P'Length >= 4 and then Offset <= P'Length - 4;

   function Read_U64 (P : Byte_Array; Offset : Natural) return Unsigned_64
   with Pre => P'Length >= 8 and then Offset <= P'Length - 8;

   procedure Parse_Header
     (Packet : Byte_Array;
      Header : out Gvsp_Header;
      Result : out Parse_Result)
   with
     Post =>
       (if Result = Ok then
          Header.Data_Offset in Standard_Header_Length | Extended_Header_Length
          and then Header.Data_Offset <= Packet'Length);

設計で決めたことは3つです。

• 添字の計算があふれないことを証明で扱いやすくするため、添字の上限を65535にしました。
• 読み出す関数はパケットの先頭からの位置（Offset）を受け取り、P'First + Offset から読みます。受信バッファから切り出した部分配列のように、先頭の添字が0でない配列にも使えます。
• Read_U16 の事前条件（Pre）は「2バイトを読める位置であること」です。呼び出す側はこの条件を満たす長さの確認を先に書く必要があります。

flowchart TB
        accTitle: Read_U16 の事前条件と配列の範囲
        accDescr: Read_U16 の事前条件 Offset が P'Length - 2 以下であれば、読む2つの添字 P'First + Offset と P'First + Offset + 1 がどちらも配列の範囲に入ることを示す。
        A["事前条件：Offset ≦ P'Length − 2"] --> B["P'First + Offset は範囲内"]
        A --> C["P'First + Offset + 1 は範囲内"]
        B --> D["2バイトを範囲外なしで読める"]
        C --> D

図7: 事前条件を満たせば、Read_U16 が読む2つの添字はどちらも配列の範囲に入る。

読み出す関数とヘッダーを読む手続きの本体は次のとおりです。手続きでは読み出す関数を呼ぶ前に必ず長さを確かめています。

   function Read_U16 (P : Byte_Array; Offset : Natural) return Unsigned_16 is
     (Shift_Left (Unsigned_16 (P (P'First + Offset)), 8)
      or Unsigned_16 (P (P'First + Offset + 1)));

   function Read_U32 (P : Byte_Array; Offset : Natural) return Unsigned_32 is
     (Shift_Left (Unsigned_32 (P (P'First + Offset)), 24)
      or Shift_Left (Unsigned_32 (P (P'First + Offset + 1)), 16)
      or Shift_Left (Unsigned_32 (P (P'First + Offset + 2)), 8)
      or Unsigned_32 (P (P'First + Offset + 3)));

   function Read_U64 (P : Byte_Array; Offset : Natural) return Unsigned_64 is
     (Shift_Left (Unsigned_64 (Read_U32 (P, Offset)), 32)
      or Unsigned_64 (Read_U32 (P, Offset + 4)));

   procedure Parse_Header
     (Packet : Byte_Array;
      Header : out Gvsp_Header;
      Result : out Parse_Result)
   is
      Format_Byte : Unsigned_8;
      Format_Code : Unsigned_8;
   begin
      Header := (others => <>);

      if Packet'Length < Standard_Header_Length then
         Result := Too_Short;
         return;
      end if;

      Header.Status_Code := Read_U16 (Packet, 0);
      Format_Byte        := Packet (Packet'First + 4);
      Header.Extended_Id := (Format_Byte and 16#80#) /= 0;
      Format_Code        := Format_Byte and 16#7F#;

      if Format_Code not in 1 .. 8 then
         Result := Unknown_Format;
         return;
      end if;
      Header.Format := Packet_Format'Val (Format_Code - 1);

      if Header.Extended_Id then
         if Packet'Length < Extended_Header_Length then
            Result := Too_Short;
            return;
         end if;
         Header.Flags       := Read_U16 (Packet, 2);
         Header.Block_Id    := Read_U64 (Packet, 8);
         Header.Packet_Id   := Read_U32 (Packet, 16);
         Header.Data_Offset := Extended_Header_Length;
      else
         Header.Block_Id    := Unsigned_64 (Read_U16 (Packet, 2));
         Header.Packet_Id   := Read_U32 (Packet, 4) and 16#00FF_FFFF#;
         Header.Data_Offset := Standard_Header_Length;
      end if;

      Result := Ok;
   end Parse_Header;

形式の値は1〜8に入ることを確かめてから列挙型に変えます。そのため、不正な値の列挙型は作られません。バイト順はシフトで組み立てるので、Scalar_Storage_Order にも CPU のエンディアンにも左右されません。

flowchart TB
        accTitle: Parse_Header の判断の順序
        accDescr: Parse_Header が、8バイト以上か、形式が1から8か、拡張 ID なら20バイト以上かを順に確かめ、条件を満たさなければ Too_Short か Unknown_Format を返し、満たせばヘッダーを読んで Ok を返すことを示す。
        A["パケットを受け取る"] --> B{"8バイト以上か"}
        B -->|"いいえ"| X["Too_Short"]
        B -->|"はい"| C{"形式は1〜8か"}
        C -->|"いいえ"| Y["Unknown_Format"]
        C -->|"はい"| D{"拡張 ID か"}
        D -->|"はい"| E{"20バイト以上か"}
        E -->|"いいえ"| X
        E -->|"はい"| F["64ビットの ID を読んで Ok"]
        D -->|"いいえ"| G["16ビットと24ビットの ID を読んで Ok"]

図8: Parse_Header は長さと形式を確かめてから ID を読む。

画像の leader を読む Parse_Image_Leader も同じ形で、データ部が36バイトあることを確かめてから各フィールドを読みます。Payload Type は Wireshark と Aravis と同じく 16#3FFF# でマスクしてから画像（1）かを比べます。このマスクでは 0x8000 のビット（Wireshark ではデバイス固有の値の始まり）も消えるので、0x8001 も画像として通ります。区別したい場合は chunk のビットだけを消す 16#BFFF# でマスクします⁴⁵。

2つの方法を比べると、次のようになります。

SPARK のユーザーガイドは with Address => Y'Address の形の重ね合わせと Unchecked_Conversion も解析の対象にしています。ただし、SPARK は読む値がすべて妥当であることを求め、'Valid は常に真を返すものとして扱います。不正な値を持ちうるオブジェクトには Potentially_Invalid を付け、妥当性を契約で書く必要があります¹⁴。Format は7ビットのうち8つの値しか妥当でないので、型を重ねる方法をそのまま SPARK で証明することはできません。この記事では型を重ねる方法を GNATprove にかけてはいません。

flowchart TB
        accTitle: 型を重ねる方法を SPARK で扱うときに要るもの
        accDescr: 型を重ねて読むと Format が不正な値を持ちうるが、SPARK は読む値が妥当であることを求めて Valid を常に真とみなすので、Potentially_Invalid と妥当性の契約が要ることを示す。
        A["型を重ねて読む"] --> B["Format が不正な値を持ちうる"]
        B --> C["SPARK は読む値の妥当性を求める"]
        C --> D["Valid は常に真とみなす"]
        D --> E["Potentially_Invalid と契約が要る"]

図9: 型を重ねる方法を SPARK で扱うには、不正な値を持ちうることを Potentially_Invalid と契約で示す必要がある。

SPARK で範囲外を読まないことを証明する

読み出す関数とヘッダーを読む手続きは、パッケージに SPARK_Mode を付けて書いています。GNATprove はこの範囲のコードについて、配列の添字の検査、整数のあふれ、'Val の範囲、呼び出しのたびの事前条件、事後条件を、すべての入力について確かめます¹⁵。実行時エラーが起きないことの証明（AoRTE）は、SPARK の段階では Silver に当たります¹⁶。

flowchart TB
        accTitle: GNATprove が確かめること
        accDescr: GNATprove が SPARK_Mode のコードについて、添字の範囲、整数のあふれ、列挙型への変換、呼び出しの事前条件、事後条件をすべての入力について確かめ、証明できない検査を報告することを示す。
        A["SPARK_Mode のコードと契約"] --> B["GNATprove"]
        B --> C["添字が配列の範囲に入るか"]
        B --> D["整数があふれないか"]
        B --> E["Val が列挙型の範囲に入るか"]
        B --> F["呼び出しの事前条件と事後条件"]
        C --> G["証明の結果を報告"]
        D --> G
        E --> G
        F --> G

図10: GNATprove は実行時の検査と契約をすべての入力について確かめる。

証明は次のコマンドで行いました。-u gvsp.adb で対象をこのパッケージに絞り、--checks-as-errors=on で、証明できない検査があれば失敗として終わるようにしています¹⁷。

gnatprove -P gvsp.gpr -u gvsp.adb --level=2 --report=all --checks-as-errors=on -j0

GNATprove の出力の最後は次の1行で、66件の検査がすべて証明されました。

Success: all checks proved (66 checks).

--report=all の出力には、Read_U16 などを呼ぶ箇所ごとに precondition proved が、読み出す関数の中の添字ごとに index check proved が並びます。Parse_Header の事後条件も postcondition proved と報告されました。

長さの確認を1つ消すと証明が通らない

証明が意味を持つことを確かめるため、拡張 ID の長さの確認だけを消したコードも用意しました。

      if Header.Extended_Id then
         Header.Flags       := Read_U16 (Packet, 2);
         Header.Block_Id    := Read_U64 (Packet, 8);
         Header.Packet_Id   := Read_U32 (Packet, 16);
         Header.Data_Offset := Extended_Header_Length;

GNATprove はこのコードで証明できない検査を3件報告し、--checks-as-errors=on のため失敗として終わりました。1件目は Read_U64 (Packet, 8) の呼び出しです。

 medium: precondition might fail, cannot prove Offset <= P'Length - 8
--> gvsp.adb:45:32
   45 |             Header.Block_Id    := Read_U64 (Packet, 8);

残りの2件は次の行の Read_U32 (Packet, 16) の事前条件（Offset <= P'Length - 4）と、Parse_Header の事後条件の Header.Data_Offset <= Packet'Length でした。拡張 ID のパケットが8〜15バイトなら3つとも、16〜19バイトなら後の2つが成り立たないからです。どの報告にも「provers reached time limit before completing the proof」と添えられていて、反例は示されていません。時間内に証明できなかったという報告です。

同じコードを手元でテストのプログラムにつないで動かすと、12バイトの拡張 ID のパケットのところで止まりました。アサーションを有効にした -gnata のビルドでは Read_U64 の事前条件で、無効にしたビルドでは関数の中の添字の検査で、それぞれ例外になりました。

raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from gvsp.ads:47

raised CONSTRAINT_ERROR : gvsp.adb:8 index check failed

flowchart TB
        accTitle: 長さの確認の漏れがどこで見つかるか
        accDescr: 拡張 ID の長さの確認を消したコードは、GNATprove では実行前に事前条件の失敗として報告され、テストでは12バイトの拡張 ID のパケットを渡したときに例外として見つかることを示す。
        A["長さの確認を消したコード"] --> B["GNATprove は実行前に報告"]
        A --> C["テストでは12バイトで例外"]

図11: 長さの確認の漏れは証明なら実行前に、テストならその入力を渡したときに見つかる。

テストで見つけるには、ちょうどその長さのパケットを用意する必要があります。GNATprove なら、そうした入力を用意しなくても、すべての長さについて漏れを報告します。

証明が保証するのは、範囲外を読まないことと、契約に書いた性質だけです。フィールドの位置が実際の GVSP と一致しているかは、証明の対象ではありません。この記事では位置を Wireshark と Aravis のソースに突き合わせ、次のテストで値を確かめています。

手で組み立てたパケットで動かす

テストでは次のパケットを手で組み立てて Parse_Header に渡し、leader なら Parse_Image_Leader も呼びました。

• 標準 ID の leader の44バイト（幅640、高さ480。画素の形式には、Aravis が Mono8 として定義している 0x01080001 を入れた¹⁸）
• 同じ leader を5バイトと30バイトで切ったもの
• 拡張 ID の payload（データ4バイト）の24バイトと、それを12バイトで切ったもの
• 形式のバイトが 0x09 の8バイト

standard leader : 44 bytes, header OK, LEADER, block 42, packet 0, data 36, leader OK, 640 x 480
cut to 5 bytes  : 5 bytes, header TOO_SHORT
cut to 30 bytes : 30 bytes, header OK, LEADER, block 42, packet 0, data 22, leader TOO_SHORT
extended payload: 24 bytes, header OK, PAYLOAD, block 4294967296, packet 5, data 4
extended, 12 b  : 12 bytes, header TOO_SHORT
unknown format  : 8 bytes, header UNKNOWN_FORMAT

30バイトで切った leader は、ヘッダーは読めて、leader のデータ部が足りないので TOO_SHORT になりました。拡張 ID の payload では64ビットのブロック ID（0x0000_0001_0000_0000）と32ビットのパケット ID を読めています。

続けて、長さが0〜64バイトで中身がでたらめなパケットを100万個読ませました。形式のバイトが1〜8に入りやすいように、半分は値を0〜8に寄せています。アサーションと実行時の検査を有効にしたビルドで、例外は1回も出ませんでした。結果の内訳は次のとおりです。

OK: 361063
TOO_SHORT: 159338
UNKNOWN_FORMAT: 460233
NOT_LEADER: 0
NOT_IMAGE: 19366

NOT_LEADER が0なのは、テストが leader のときだけ Parse_Image_Leader を呼んでいるからです。NOT_IMAGE は、ヘッダーとデータ部の長さは足りているのに、Payload Type が画像でなかった leader です。でたらめな入力のテストで例外が出ないと言えるのは、試した入力の範囲だけです。すべての入力についての保証は前の節の証明で得ています。

flowchart TB
        accTitle: テストと証明の分担
        accDescr: 手で組み立てたパケットのテストがフィールドの値を確かめ、でたらめなパケットのテストが試した範囲で例外が出ないことを確かめ、GNATprove がすべての入力で範囲外を読まないことを確かめることを示す。
        A["手で組み立てたパケット"] --> D["フィールドの値が正しいか"]
        B["でたらめなパケット100万個"] --> E["試した範囲で例外が出ないか"]
        C["GNATprove"] --> F["すべての入力で範囲外を読まないか"]

図12: 値の正しさはテストで、範囲外を読まないことは証明で確かめる。

受信処理に組み込むときの位置

実際の受信処理ではソケットで受けたバッファから受信した長さだけを切り出し、Parse_Header に渡します。Packet_Index を0から始まる添字にしたので、Buffer (0 .. Received - 1) のように切り出せます。受信した長さが0でも、空の配列として渡せます。ただし、これは受信バッファを Byte_Array として持つ場合の書き方です。GNAT.Sockets の Receive_Socket は Ada.Streams.Stream_Element_Array に書き込み、この配列は Byte_Array に型変換できません（GNAT 13.3.0 では incompatible component types for array conversion のエラーになりました）。その場合は Byte_Array へ写すか、OS の recv を直接呼ぶ結合を書くなどの処理を1つ挟みます。その後の流れは形式で分かれます。leader なら Parse_Image_Leader で画像の大きさを知って領域を用意し、payload ならパケット ID の位置にデータを写します。trailer で画像の終わりを知ります。

flowchart TB
        accTitle: 受信処理の中でのパーサーの位置
        accDescr: ソケットで受けたバッファから受信した長さを切り出して Parse_Header に渡し、形式が leader なら Parse_Image_Leader で画像の大きさを知り、payload ならデータを写し、trailer で画像を完成させ、失敗した結果はパケットを捨てて数えることを示す。
        A["ソケットで受信"] --> B["受信した長さだけ切り出す"]
        B --> C["Parse_Header"]
        C -->|"leader"| D["Parse_Image_Leader で大きさを知る"]
        C -->|"payload"| E["パケット ID の位置へ写す"]
        C -->|"trailer"| F["画像を完成させる"]
        C -->|"Ok 以外"| G["捨てて数える"]

図13: パーサーは受信した直後に置き、失敗したパケットは捨てて数える。

Ok 以外の結果は例外にせずに数えておくと、短いパケットや想定外の形式がどれくらい届いているかを後から調べられます。

この記事では受信のループ、欠けたパケットの再送の要求、画像の組み立ては作っていません。欠けたパケットが画像の取りこぼしにつながる仕組みと調べ方は GigE Vision・USB3 Visionカメラの取りこぼし に、受信と処理を分けるタスクの作り方は 取りこぼさない取り込み処理をAdaのタスクで作る に書いています。SPARK の契約と証明の基本は SPARKによる形式検証入門 が詳しいです。

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

• 手元のビルドと実行: Ubuntu 24.04、GNAT 13.3.0（Ubuntu のパッケージ）、gprbuild。CPU は x86-64 です。
• CI のビルド、実行、証明: GitHub Actions の ubuntu-24.04 のランナーで、Alire 2.1.1 で入れた GNAT 16.1.0（gnat_native）と GNATprove FSF 16.1.0 を使いました。GNATprove が使った証明器は Alt-Ergo 2.6.1、cvc5 1.3.2、Z3 4.15.4 です。実行したプログラムの出力は手元と同じでした。
• 実際の GigE Vision のカメラ、ネットワークでの受信、Windows では試していません。
• GigE Vision の仕様書は参照していません。フィールドの配置は Wireshark と Aravis のソースで確かめた範囲です。chunk、multi-part、GenDC など、この記事で読まない形式の中身は扱っていません。
• 番地で重ねる方法は警告を確かめるためにコンパイルしただけで、動かして比べてはいません。
• 検証に使ったプロジェクト一式は公開しておらず、記事のコードはその抜粋です。

関連記事

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

• 画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較
• 取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
• Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る
• ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ

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

• GigE Vision・USB3 Visionカメラの取りこぼし ── 原因の切り分けとWindows側の設定
• AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる
• Ada と C / C# をつなぐ ── DLL を作って呼び出す

参考リンク

関連する記事

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

関連トピック

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

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

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

よくある質問

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

GVSPのヘッダーは、Adaの表現句で書いた型をバイト列に重ねて読めばよいですか？

ネットワークから届くバイト列にはおすすめしません。短いパケットでは型の大きさに足りず、形式のバイトに想定外の値が来ると列挙型が不正な値になります。拡張IDのフラグでヘッダーの長さも変わります。長さを確かめてから1フィールドずつ読み出し、表現句の型は配置を示す資料として使う用途や、確かめた後に使う用途に回します。

Bit_Order => High_Order_Firstを付ければ、ビッグエンディアンの値をそのまま読めますか？

読めません。Bit_Orderが決めるのは表現句のビット番号の数え方で、複数バイトの整数のバイト順は変わりません。この記事の例では、x86-64でBit_Orderだけを付けた型は42を10752と読みました。バイト順まで変えるには、GNAT独自の属性であるScalar_Storage_Orderも付けます。

SPARKで証明すると、何が保証されますか？

事前条件を満たすどんなバイト列を渡しても、配列の範囲外を読まず、整数があふれず、列挙型への変換が範囲を外れないことです。事後条件に書いた性質も成り立ちます。フィールドの位置が仕様どおりかは証明の対象ではないので、出典との突き合わせとテストで確かめます。

著者プロフィール

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

小村 豪

合同会社小村ソフト 代表

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