検査装置の画面や設定、カメラの制御は C# の WPF で作ったまま、合否を決める処理だけを Ada で書きたいことがあります。判定の処理は小さくても間違いが許されない部分なので、そこだけを Ada の型と SPARK の証明で守り、ほかは使い慣れた .NET に残すという分け方です。このときに難しいのは C# と Ada の境界です。数メガバイトの画像を呼び出しのたびにコピーしたくはありませんし、C# が渡した寸法と実際のバッファの長さが食い違えば、Ada の側で範囲外のメモリを読んでしまいます。
答えの要点は4つです。画像は先頭のポインター、バッファの長さ、幅・高さ・stride（1行のバイト数）で渡し、Ada の側で寸法が長さに収まることを確かめてから、同じメモリを2次元の配列として見ます。判定の結果は構造体で返し、その大きさを C# と Ada の両方で比べてから使います。C# から直接呼ばれる Ada の関数は例外を外へ出さず、エラーコードに変えて返します。判定の中身は SPARK の範囲に置き、GNATprove で範囲外の読み出しとオーバーフローがないことを証明します。
DLL の作り方、初期化、文字列の受け渡しといった一般的な話は「Ada と C / C# をつなぐ」で扱いました。この記事はその続きとして、画像のバッファと検査の結果を渡す境界の設計に絞ります。
例はすべて実際にビルドして動かしました。Linux（Ubuntu 24.04、GNAT 13.3.0）で共有ライブラリを作って C のテストドライバーから呼び、GitHub Actions の Windows のランナーで DLL を作って .NET 10 のコンソールアプリから呼びました。証明は GitHub Actions の Linux のランナーで GNATprove を使って行いました。WPF の例はビルドだけで、画面は動かしていません。Linux の .NET のアプリから呼ぶ使い方は、シグナルの扱いが .NET と食い違うので対象から外し、外す理由を確かめるテストだけを Linux の .NET で行っています。理由は最後の節で書きます。
検査アプリのどこを Ada にするか
検査アプリの処理を画面、カメラからの取り込み、判定、結果の保存に分けて考えます。この記事で Ada にするのは判定だけです。画面と取り込みと保存は WPF と C# のまま残し、C# の薄い層が画像のバッファを Ada の DLL に渡します。
Ada の DLL の中も2つに分けます。C# から直接呼ばれる関数（以下、境界の関数）は、ポインターと寸法を受け取って確かめ、メモリを Ada の配列として判定の関数に渡します。判定の関数は Ada の配列だけを受け取るので、SPARK で証明できます。ポインターを配列として扱う部分は SPARK の外に置き、そのぶん短く保って人が読んで確かめます。
flowchart TB
accTitle: 検査アプリの構成
accDescr: WPF の画面と取り込みが C# の薄い層を通して Ada の DLL の境界の関数を呼び、境界の関数がポインターと寸法を確かめてから SPARK で証明した判定の関数を呼び、結果とエラーコードを返すことを示す。
A["WPF の画面と取り込み（C#）"] --> B["C# の薄い層（ピン留めして呼ぶ）"]
B --> C["境界の関数（Ada）"]
C --> D["判定の関数（SPARK）"]
D --> C
C -->|"結果とエラーコード"| B
E["ポインターと寸法を確かめる"] -.-> C
F["範囲外の読み出しがないことを証明"] -.-> D
図1: 判定だけを Ada の DLL にし、DLL の中を境界の関数と SPARK で証明する判定の関数に分ける。
図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全18件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle
公開する関数を C の宣言で決める
C# と Ada は直接にはつながらないので、間に C の ABI（関数の呼び方と構造体の並びの決まり）を挟みます。そこで最初に、公開する関数を C の宣言として書き、両側の型をこの宣言に合わせます。
typedef struct { int threshold; int max_defect_pixels; } inspect_params;
typedef struct {
int64_t defect_pixels;
int min_x, min_y, max_x, max_y;
int verdict;
} inspect_result;
int inspect_dark_defects(const uint8_t *pixels, size_t length,
int width, int height, int stride,
const inspect_params *params, inspect_result *result);
int inspect_result_size(void);
int inspect_elaborated(void);
例として作る検査は8ビットのグレースケール画像で、しきい値より暗い画素を欠陥として数えるものです。欠陥の画素数が上限を超えれば不合格とし、欠陥を囲む外接矩形も返します。検査の中身は単純にしてあります。この記事で扱いたいのは検査の中身ではなく画像と結果を境界でどう渡すかだからです。
引数は次の考え方で決めました。
- 画像は先頭のポインターに加えて、バッファの長さ（バイト数）も渡す。寸法だけでは、寸法がバッファに収まるかを Ada の側で確かめられない。
- 1行のバイト数（stride）を、幅とは別に渡す。
- メモリは呼び出し側が確保して解放する。Ada は呼び出しの間だけ読み、ポインターを保存しない。
- 戻り値はエラーコードにし、検査の結果は呼び出し側が用意した構造体に書く。
エラーコードは次の6つです。
| 値 | 意味 |
|---|---|
| 0 | 成功。結果の構造体に判定が入っている |
| 1 | 画像、パラメーター、結果のいずれかのポインターが NULL |
| 2 | 幅か高さが0以下、または stride が幅より小さい |
| 3 | stride × 高さがバッファの長さを超える |
| 4 | パラメーターが範囲外（しきい値が0〜255でない、上限が負） |
| 99 | 想定していない失敗（ポインターや長さの誤りでメモリを読めなかった場合を含む） |
flowchart TB
accTitle: 画像のバッファの持ち主
accDescr: 呼び出し側が画像のバッファと結果の構造体を用意し、Ada は呼び出しの間だけバッファを読んで結果を書き、戻ったあとは呼び出し側がバッファを再利用または解放することを示す。
A["呼び出し側がバッファと結果を用意"] --> B["inspect_dark_defects を呼ぶ"]
B --> C["Ada が呼び出しの間だけ読む"]
C --> D["Ada が結果とエラーコードを返す"]
D --> E["呼び出し側が再利用または解放"]
図2: バッファの確保と解放は呼び出し側が受け持ち、Ada は呼び出しの間だけ読む。
画像のバッファの寸法と stride
画像のバッファでは、1行のバイト数が幅と同じとは限りません。Microsoft の資料も、メモリ上の画像は各行の後ろに詰め物のバイトを持つことがあり、その場合は stride が幅より大きくなると説明しています1。同じ寸法の画像でも、バッファによって stride が違うことがあります。y 行目 x 列目の画素は先頭から y × stride + x バイト目にあります。
flowchart TB
accTitle: stride と詰め物
accDescr: 1行は stride バイトで、先頭の幅ぶんが画素、残りが詰め物であり、判定の関数は各行の画素の部分だけを読むことを示す。
A["1行（stride バイト）"] --> B["画素（幅ぶん）"]
A --> C["詰め物（stride − 幅）"]
B --> D["判定の関数が読む"]
C -.->|"読まない"| D
図3: 1行は画素と詰め物でできていて、判定の関数は画素の部分だけを読む。
境界の関数はメモリを読む前に次の3つを確かめます。
- ポインターが NULL でない。
- 幅と高さが1以上で、stride が幅以上である。
- stride × 高さがバッファの長さ以下である。
このほか、しきい値などのパラメーターの範囲も確かめ、範囲外ならエラーコード4を返します。こちらはあとの節で説明します。
3つ目の条件は最後の行にも stride ぶんのバイトがあることを求めています。最後の行だけ詰め物を省いたバッファなら、必要な長さは (高さ − 1) × stride + 幅で足ります。この例ではメモリを (高さ, stride) の形の配列として見るので、stride × 高さを求めました。最後の行の詰め物がないバッファも受け付けるなら、配列の形を変えるか、行ごとに読む形にします。
掛け算は64ビットの符号なし整数で行います。幅・高さ・stride は C の int なので、最大でも 2³¹ − 1 です。2つを掛けても64ビットに収まり、掛け算そのものがあふれることはありません。
stride が負の画像は受け付けません。Microsoft の資料によると、最後の行がメモリの先頭に来る bottom-up の画像では stride が負になります1。この例は先頭の行がメモリの先頭に来る top-down の画像だけを扱い、stride が負なら2つ目の条件でエラーコード2を返します。
flowchart TB
accTitle: 境界の関数が寸法を確かめる順序
accDescr: ポインターが NULL ならエラーコード1、幅と高さと stride が正しくなければ2、stride と高さの積がバッファの長さを超えれば3を返し、すべて満たしたときだけバッファを配列として読むことを示す。
A{"ポインターは NULL か"} -->|"NULL"| B["1 を返す"]
A -->|"NULL でない"| C{"幅・高さ・stride は正しいか"}
C -->|"正しくない"| D["2 を返す"]
C -->|"正しい"| E{"stride × 高さ ≤ 長さ か"}
E -->|"超える"| F["3 を返す"]
E -->|"収まる"| G["配列として読む"]
図4: 境界の関数は寸法の3つの条件を順に確かめ、すべて満たしたときだけメモリを読む。
受け取ったバッファを Ada の配列として見る
境界の関数の仕様部（.ads）です。C の構造体に対応するレコードに Convention => C を付け、関数に Export と External_Name を付けます。
with Interfaces;
with Interfaces.C; use Interfaces.C;
with System;
package Inspect_API is
-- struct inspect_params { int threshold; int max_defect_pixels; };
type Inspect_Params is record
Threshold : int; -- これより暗い画素を欠陥とみなす (0〜255)
Max_Defect_Pixels : int; -- 欠陥の画素数がこれを超えたら不合格 (0以上)
end record
with Convention => C;
-- struct inspect_result { int64_t defect_pixels;
-- int min_x, min_y, max_x, max_y; int verdict; };
type Inspect_Result is record
Defect_Pixels : Interfaces.Integer_64;
Min_X, Min_Y : int; -- 欠陥の外接矩形。欠陥がなければ -1
Max_X, Max_Y : int;
Verdict : int; -- 0 = 合格、1 = 不合格
end record
with Convention => C;
type Params_Access is access constant Inspect_Params
with Convention => C;
type Result_Access is access all Inspect_Result
with Convention => C;
Status_OK : constant int := 0;
Status_Null_Pointer : constant int := 1;
Status_Bad_Geometry : constant int := 2;
Status_Buffer_Too_Small : constant int := 3;
Status_Bad_Parameter : constant int := 4;
Status_Internal_Error : constant int := 99;
-- int inspect_dark_defects (const uint8_t *pixels, size_t length,
-- int width, int height, int stride,
-- const inspect_params *params,
-- inspect_result *result);
function Inspect_Dark_Defects
(Pixels : System.Address;
Length : size_t;
Width : int;
Height : int;
Stride : int;
Params : Params_Access;
Result : Result_Access) return int
with Export, Convention => C, External_Name => "inspect_dark_defects";
-- int inspect_result_size (void); 呼び出し側の構造体と大きさを比べる
function Result_Size return int
with Export, Convention => C, External_Name => "inspect_result_size";
-- int inspect_elaborated (void); 初期化が済んでいれば 1
function Elaborated return int
with Export, Convention => C, External_Name => "inspect_elaborated";
end Inspect_API;
パラメーターと結果はアクセス型で受けています。Ada の参照マニュアルの附属書 B は、レコード型のパラメーターも、アクセス型の in のパラメーターも、C の関数には t* として渡すと定めています2。Params : Inspect_Params や Result : out Inspect_Result と書いても C の側からはポインターに見えますが、その場合は Ada の中で NULL かどうかを確かめられません。アクセス型にすれば null と比べられるので、C の側が NULL を渡してもエラーコード1で返せます。
flowchart TB
accTitle: パラメーターの受け方と NULL の確かめ方
accDescr: C の const inspect_params へのポインターを、Ada でレコードの in のパラメーターとして受けると NULL を確かめられず、アクセス型で受けると null と比べてエラーコード1を返せることを示す。
A["C の const inspect_params*"] --> B{"Ada での受け方"}
B -->|"レコードの in"| C["NULL を確かめられない"]
B -->|"アクセス型"| D["null と比べられる"]
D --> E["エラーコード1を返す"]
図5: パラメーターをアクセス型で受けると、C の側が渡した NULL を Ada で確かめられる。
本体（.adb）は次のとおりです。
with Inspect_Core;
with System; use type System.Address;
package body Inspect_API is
use type Interfaces.Unsigned_64;
use type Interfaces.Integer_64;
Elaboration_Done : int := 0; -- パッケージ本体の初期化で 1 にする
function Inspect_Dark_Defects
(Pixels : System.Address;
Length : size_t;
Width : int;
Height : int;
Stride : int;
Params : Params_Access;
Result : Result_Access) return int
is
begin
if Result = null then
return Status_Null_Pointer;
end if;
-- どの戻り方でも、呼び出し側が読む結果を決まった値にしておく
Result.all :=
(Defect_Pixels => 0, Min_X | Min_Y | Max_X | Max_Y => -1, Verdict => 1);
if Pixels = System.Null_Address or else Params = null then
return Status_Null_Pointer;
end if;
if Width <= 0 or else Height <= 0 or else Stride < Width then
return Status_Bad_Geometry;
end if;
-- 最後の行も stride バイトぶんあることを求める
if Interfaces.Unsigned_64 (Stride) * Interfaces.Unsigned_64 (Height)
> Interfaces.Unsigned_64 (Length)
then
return Status_Buffer_Too_Small;
end if;
-- パラメーターの範囲は、例外に頼らず if で確かめる
if Params.Threshold not in 0 .. 255
or else Params.Max_Defect_Pixels < 0
then
return Status_Bad_Parameter;
end if;
declare
-- 範囲は上で確かめたので、この変換で例外は起きない
Threshold : constant Inspect_Core.Byte :=
Inspect_Core.Byte (Params.Threshold);
Max_Defects : constant Natural := Natural (Params.Max_Defect_Pixels);
-- 呼び出し側のバッファを、コピーせずに (行, 列) の配列として見る
Img : Inspect_Core.Image
(0 .. Natural (Height) - 1, 0 .. Natural (Stride) - 1)
with Import, Address => Pixels;
S : Inspect_Core.Summary;
begin
Inspect_Core.Count_Dark (Img, Positive (Width), Threshold, S);
Result.all :=
(Defect_Pixels => S.Defect_Pixels,
Min_X => int (S.Min_X),
Min_Y => int (S.Min_Y),
Max_X => int (S.Max_X),
Max_Y => int (S.Max_Y),
Verdict =>
(if S.Defect_Pixels <= Interfaces.Integer_64 (Max_Defects)
then 0 else 1));
return Status_OK;
end;
exception
when others =>
-- 想定していない失敗。呼び出し側は検査を止めて扱う
return Status_Internal_Error;
end Inspect_Dark_Defects;
function Result_Size return int is
(int (Inspect_Result'Max_Size_In_Storage_Elements));
function Elaborated return int is (Elaboration_Done);
begin
Elaboration_Done := 1;
end Inspect_API;
コピーをしないための要は Img の宣言です。Address => Pixels で、呼び出し側のバッファと同じアドレスに配列を置いています。Import を付けた変数は初期化されないので3、宣言しただけで呼び出し側の画素が上書きされることはありません。添字の範囲は寸法を確かめたあとで決まるので、Img がバッファの外まで広がることはありません。
Img を判定の関数に渡すときにもコピーは起きません。参照マニュアルはこの配列の型をパラメーターとしてコピーで渡すか参照で渡すかを処理系に任せています4。手元の GNAT 13.3.0 で、呼び出し側のバッファと、手続きが受け取った配列のアドレスが同じになることを確かめました。
2次元の配列がメモリにどう並ぶかも確かめておきます。参照マニュアルは多次元の配列を通常は行優先で並べるよう実装に勧めています（Implementation Advice）。Convention => Fortran を指定した型だけは列優先です5。GNAT は行優先で並べるので、Img (Y, X) は先頭から Y × stride + X バイト目の画素を指します。あとで示すテストで、詰め物のある画像の欠陥の位置が正しく求まったことでも確かめられます。
flowchart TB
accTitle: 同じメモリを Ada の配列として見る
accDescr: C# の byte 配列をピン留めした先頭アドレスを境界の関数が受け取り、寸法を確かめてから Ada の2次元配列 Img として重ねるので、画素はコピーされず、Img の行と列が y 行目と x 列目の画素に対応することを示す。
A["C# の byte 配列"] -->|"ピン留めした先頭アドレス"| B["境界の関数"]
B -->|"寸法を確かめてから重ねる"| C["Ada の配列 Img（行, 列）"]
C --> D["Img（y, x）は y × stride + x バイト目"]
A -.->|"同じメモリでコピーなし"| C
図6: 境界の関数は寸法を確かめてから C# の配列と同じメモリを Ada の2次元配列として見る。
Threshold と Max_Defects は C の int を Ada の範囲の決まった型に変換して作ります。Inspect_Core.Byte は0〜255の型なので、しきい値に300を渡せば変換で Constraint_Error になるところです。そこで変換の前に if で範囲を確かめ、範囲外ならエラーコード4を返します。Ada の範囲検査に任せて例外をエラーコードに変える書き方もできますが、この例では採りませんでした。理由は「例外を境界の関数で止めてエラーコードにする」の節で書きます。
判定の中身を SPARK で証明する
判定の関数は別のパッケージ Inspect_Core に置きます。こちらは SPARK_Mode を付け、GNATprove で証明します。
with Interfaces; use type Interfaces.Integer_64;
package Inspect_Core with SPARK_Mode is
type Byte is mod 2 ** 8;
-- 'Length が Integer に収まるよう、添字の上限を Natural'Last - 1 にする
subtype Index is Natural range 0 .. Natural'Last - 1;
-- 1つ目の添字が行 (y)、2つ目が列 (x)。2つ目の長さが stride になる
type Image is array (Index range <>, Index range <>) of Byte;
type Summary is record
Defect_Pixels : Interfaces.Integer_64;
Min_X, Min_Y : Integer; -- 欠陥の外接矩形。欠陥がなければ -1
Max_X, Max_Y : Integer;
end record;
-- 各行の先頭から Width 画素だけを見て、Threshold より暗い画素を数える
procedure Count_Dark
(Img : Image;
Width : Positive;
Threshold : Byte;
S : out Summary)
with
Pre => Img'Length (1) >= 1 and then Width <= Img'Length (2),
Post => S.Defect_Pixels >= 0;
end Inspect_Core;
package body Inspect_Core with SPARK_Mode is
procedure Count_Dark
(Img : Image;
Width : Positive;
Threshold : Byte;
S : out Summary)
is
X_First : constant Natural := Img'First (2);
X_Last : constant Natural := Img'First (2) + (Width - 1);
Total : Interfaces.Integer_64 := 0;
Row : Natural;
begin
S := (Defect_Pixels => 0, Min_X | Min_Y | Max_X | Max_Y => -1);
for Y in Img'Range (1) loop
Row := 0;
for X in X_First .. X_Last loop
if Img (Y, X) < Threshold then
Row := Row + 1;
declare
DX : constant Natural := X - X_First;
DY : constant Natural := Y - Img'First (1);
begin
if S.Min_X < 0 then
S.Min_X := DX;
S.Min_Y := DY;
S.Max_X := DX;
S.Max_Y := DY;
else
S.Min_X := Integer'Min (S.Min_X, DX);
S.Max_X := Integer'Max (S.Max_X, DX);
S.Max_Y := Integer'Max (S.Max_Y, DY);
end if;
end;
end if;
pragma Loop_Invariant (Row <= X - X_First + 1);
end loop;
Total := Total + Interfaces.Integer_64 (Row);
pragma Loop_Invariant
(Total >= 0
and then Total <=
(Interfaces.Integer_64 (Y) - Interfaces.Integer_64 (Img'First (1)) + 1)
* Interfaces.Integer_64 (Natural'Last));
end loop;
S.Defect_Pixels := Total;
end Count_Dark;
end Inspect_Core;
事前条件（Pre）は行が1つ以上あることと、Width が列の数（stride）以下であることだけです。この2つが成り立てば、X_First .. X_Last はいつも列の添字の範囲に収まり、Img (Y, X) が範囲外を読むことはありません。境界の関数は高さが1以上で stride が幅以上であることを確かめてから呼ぶので、事前条件を満たします。
添字の型を Natural'Last - 1 までに絞ったのは、'Length を Integer に収めるためです。添字を Natural のままにすると、0 .. Natural'Last の配列の長さは Integer'Last を1つ超えます。最初にそう書いたときは、GNATprove が事前条件の Img'Length (2) の範囲検査を証明できませんでした。
数え上げの変数はあふれないことを証明しやすい形にしました。1行の中の数 Row は Natural で、ループ不変条件で「ここまでに見た画素の数以下」と示します。画像全体の数 Total は64ビットの整数で、「見終えた行の数 × Natural'Last 以下」と示します。行の数に定数を掛けるだけなので、証明に掛け算どうしの非線形な推論が要りません。
flowchart TB
accTitle: 欠陥の画素を数える変数の分け方
accDescr: 1行の中では Row を見た画素の数以下に保ち、行を見終えるたびに Row を64ビットの Total に足し、Total を見終えた行の数と Natural'Last の積以下に保つので、どちらもあふれないことを証明できることを示す。
A["行の先頭で Row を0にする"] --> B["暗い画素なら Row を1増やす"]
B --> C["Row は見た画素の数以下"]
C --> D["行の終わりに Total に足す"]
D --> E["Total は行の数 × Natural'Last 以下"]
E -->|"次の行"| A
図7: 1行の数と全体の数を分け、どちらにも上限を示すループ不変条件を付ける。
GitHub Actions の Linux のランナーで、Alire から入れた GNATprove（FSF 16.1.0）を --level=2 で実行しました。対象になった20件の検査はすべて証明され、証明できなかった検査はありませんでした。内訳は変数の初期化が2件、添字・オーバーフロー・範囲などの実行時の検査が13件、2つのループ不変条件が成り立ち始めることと保たれることの4件、事後条件が1件です。
gnatprove -P inspect.gpr --level=2 --report=all --checks-as-errors=on -j0
--checks-as-errors=on は証明できなかった検査をエラーとして扱うスイッチです6。CI で使えば、証明が崩れたときにジョブが失敗します。
証明が保証するのは、事前条件が成り立つ限り判定の関数が範囲外を読まず、あふれないことです。境界の関数は SPARK の外にあるので、Img を正しい大きさで重ねているか、事前条件を満たしてから呼んでいるかは証明されていません。この部分は短く保ち、テストとレビューで確かめます。C# が渡す長さが本当のバッファの長さと合っていることも、Ada の側では確かめようがありません。この長さは、あとの節の C# の層が Span の長さから渡します。
flowchart TB
accTitle: 証明される範囲と人が確かめる範囲
accDescr: C# が正しい長さを渡すことと、境界の関数が寸法を確かめて配列を重ねることはテストとレビューで確かめ、その結果として成り立つ事前条件のもとで、判定の関数に範囲外の読み出しとオーバーフローがないことを GNATprove が証明することを示す。
A["C# が正しい長さを渡す"] --> B["境界の関数が寸法を確かめて重ねる"]
B --> C["事前条件が成り立つ"]
C --> D["判定の関数（GNATprove で証明）"]
D --> E["範囲外の読み出しとオーバーフローがない"]
F["テストとレビューで確かめる"] -.-> A
F -.-> B
図8: GNATprove が証明するのは判定の関数で、その前提は境界の関数と C# の層が受け持つ。
SPARK の証明の進め方、証明できたあとで実行時の検査を外す判断は「画像処理の境界外アクセスをSPARKで証明する」で扱います。
例外を境界の関数で止めてエラーコードにする
Ada の例外を C# まで届かせてはいけません。「Ada と C / C# をつなぐ」の記事の Linux での実験では、処理されなかった Ada の例外がプロセスを終了させました7。.NET の資料も、アンマネージドのコードの例外を扱えるのは Windows だけで、ほかのプラットフォームでは予測できない動作やクラッシュになりうるとしています8。
そこで、境界の関数の末尾に when others のハンドラーを置き、どの例外もエラーコード99に変えて返します。パラメーターの範囲外は前の節の if で確かめてエラーコード4を返すので、正しい呼び出しでも誤った値の呼び出しでも、例外は起きません。
例外を普通のエラーの知らせに使わないのは、複数のスレッドから同時に呼ばれたときに、ランタイムの変数を取り合うおそれがあるからです。このライブラリには Ada のタスクがないので、GNAT のランタイムは処理している例外の情報と二次スタック（大きさが前もって決まらない値を関数が返すときなどに使う領域）の位置を、1つの変数 NT_TSD にまとめて置きます9。WPF の例のように Task.Run で呼ぶと、複数のスレッドが同時に境界の関数に入ることがあります。そのときに例外が起きたり二次スタックを使ったりすると、この変数を取り合います。if で確かめておけば例外そのものは起きません。
二次スタックのほうは、ライブラリに pragma Restrictions (No_Secondary_Stack); を付けると、使うコードをコンパイラーがエラーにします。手元の GNAT 13.3.0 で、この記事のライブラリはこの指定を付けてもそのままビルドでき、C のテストドライバーの結果も変わりませんでした。試しに文字列を連結する関数を足すと、violation of restriction "No_Secondary_Stack" のエラーになりました。指定はプロジェクトファイルの Builder パッケージの Global_Configuration_Pragmas で読み込むファイルに書きます10。ただし、複数のスレッドから同時に呼ぶテストはしていません。同時に呼ぶ必要がなければ、C# の側で呼び出しを1つずつに絞る（lock で囲む）方法もあります。
flowchart TB
accTitle: 複数のスレッドから呼んだときの共有の変数
accDescr: タスクのないライブラリでは例外の情報と二次スタックの位置が1つの変数 NT_TSD にあり、複数のスレッドが同時に例外を起こしたり二次スタックを使ったりすると取り合うので、if で例外を起こさず、No_Secondary_Stack で二次スタックを使わないことを示す。
A["複数のスレッドが境界の関数に入る"] --> B["例外の情報と二次スタックの位置"]
B --> C["1つの変数 NT_TSD を共有"]
C --> D["同時に使うと取り合う"]
E["if で確かめて例外を起こさない"] -.-> D
F["No_Secondary_Stack で使わない"] -.-> D
図9: タスクのないライブラリでは例外と二次スタックの情報を1つの変数で共有するので、どちらも使わない形にする。
99 は「想定していない失敗」です。判定の関数を証明したときの前提は、C# が渡すポインターと長さが正しいことです。呼び出し側が実際より長い長さを渡すと、Ada は画像の外のメモリを読みます。読めないアドレスに当たると、Linux ではあとの節で書くように GNAT のランタイムが SIGSEGV のシグナルを例外に変えるので、99 が返ります。Linux の C のプログラムから、読めないアドレス 0x1000 と寸法どおりの長さを渡したテストでも、99 が返りました。GitHub Actions の Linux と Windows のランナーで .NET から同じ値を渡したテストでも、99 が返りました。読めてしまうアドレスなら何も検出されず、誤った判定がそのまま返ります。
そこで 99 が返ったら、その画像の結果は捨て、検査を止めてログを残し、アプリを再起動する扱いにします。
flowchart TB
accTitle: 境界の関数でのエラーと例外の扱い
accDescr: パラメーターが範囲外なら if で確かめてエラーコード4を返し、想定していない例外はすべて99に変えて返し、99 が返ったら呼び出し側は検査を止めることを示す。
A["境界の関数"] --> B{"パラメーターは範囲内か"}
B -->|"範囲外"| C["4 を返す（if で確かめる）"]
B -->|"範囲内"| D["判定して 0 を返す"]
D -.->|"想定していない例外"| E["99 を返す"]
E --> F["呼び出し側は検査を止める"]
図10: パラメーターの誤りは if で4にし、想定していない例外だけを99にする。
Linux で、共有ライブラリを C のテストドライバーから呼んだ結果です。しきい値に300、上限に −1 を渡した呼び出しは、if の確認でエラーコード4が返りました。どの戻り方でも、結果の構造体は境界の関数の最初で決まった値（欠陥0、外接矩形 −1）にしてあります。
elaborated=1 result size: C=32 Ada=32
ng (max 50) status=0 defects=100 bbox=(100,50)-(109,59) verdict=1
ok (max 200) status=0 defects=100 bbox=(100,50)-(109,59) verdict=0
padded stride status=0 defects=100 bbox=(100,50)-(109,59) verdict=0
buffer too small status=3 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
width > stride status=2 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
threshold 300 status=4 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
max -1 status=4 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
null pixels status=1 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
ALL PASSED
テストの画像は 640 × 480 で、明るさ200の背景に、明るさ20の 10 × 10 の正方形を (100, 50) に置いています。しきい値は64です。padded stride は stride を644にし、各行の末尾の4バイトの詰め物を0（暗い）にした画像です。判定の関数が詰め物まで読んでいれば欠陥は 4 × 480 画素増えますが、結果は100画素で、外接矩形も正方形の位置と一致しました。
flowchart TB
accTitle: 詰め物のある画像でのテスト
accDescr: stride が644の画像の各行の末尾4バイトを暗くしておき、判定の関数が詰め物まで読めば欠陥は2020画素になり、読まなければ正方形の100画素だけになることを示す。
A["各行の末尾4バイトを暗くする"] --> B["判定の関数で数える"]
B --> C{"欠陥の画素数"}
C -->|"100"| D["詰め物を読んでいない"]
C -->|"2020"| E["詰め物まで読んでいる"]
図11: 詰め物を暗くした画像で、欠陥が100画素なら判定の関数は詰め物を読んでいない。
C# から呼ぶ
C# の側は構造体の定義、LibraryImport の宣言、fixed でピン留めして呼ぶ関数を1つのファイルにまとめました。
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
namespace Inspection;
[StructLayout(LayoutKind.Sequential)]
public struct InspectParams
{
public int Threshold; // これより暗い画素を欠陥とみなす（0〜255）
public int MaxDefectPixels; // 欠陥の画素数がこれを超えたら不合格
}
[StructLayout(LayoutKind.Sequential)]
public struct InspectResult
{
public long DefectPixels;
public int MinX, MinY, MaxX, MaxY; // 欠陥の外接矩形。欠陥がなければ -1
public int Verdict; // 0 = 合格、1 = 不合格
}
public enum InspectStatus
{
Ok = 0,
NullPointer = 1,
BadGeometry = 2,
BufferTooSmall = 3,
BadParameter = 4,
InternalError = 99,
}
public static unsafe partial class AdaInspector
{
// Windows では libinspect.dll、Linux では libinspect.so を探す
private const string Lib = "libinspect";
[LibraryImport(Lib, EntryPoint = "inspect_dark_defects")]
[UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
private static partial int InspectDarkDefects(
byte* pixels, nuint length, int width, int height, int stride,
InspectParams* parameters, InspectResult* result);
[LibraryImport(Lib, EntryPoint = "inspect_result_size")]
[UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
public static partial int NativeResultSize();
[LibraryImport(Lib, EntryPoint = "inspect_elaborated")]
[UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
public static partial int Elaborated();
public static InspectStatus Inspect(
ReadOnlySpan<byte> pixels, int width, int height, int stride,
InspectParams parameters, out InspectResult result)
{
InspectResult r;
int status;
// fixed の中だけ、GC が配列を動かさない。Ada はこの呼び出しの間だけ読む
fixed (byte* p = pixels)
{
status = InspectDarkDefects(
p, (nuint)pixels.Length, width, height, stride, ¶meters, &r);
}
result = r;
return (InspectStatus)status;
}
}
2つの構造体は int と long だけでできていて、LayoutKind.Sequential を指定しています。Microsoft の資料はこうした構造体を blittable な型（マネージドとネイティブでビットの並びが同じ型）とし、変換せずに渡せるので使うよう勧めています11。bool は blittable ではないので、合否も int の Verdict にしました。C の int64_t は C# の long です。
画像は ReadOnlySpan<byte> で受け取り、fixed でピン留めしてから先頭のポインターを渡します。fixed の文を実行している間はガベージコレクターが配列を動かさず、宣言したポインターは fixed の中でしか使えません12。Ada は呼び出しの間だけ読み、ポインターを保存しないので、この範囲で足ります。Span を使うと、配列の一部や、ほかのバッファから作った範囲も同じ関数で渡せます。
flowchart TB
accTitle: fixed の間だけ有効なポインター
accDescr: fixed に入ると配列がピン留めされ、その中で Ada の関数を呼び、Ada が読み終えて戻ったあとで fixed を出ると、GC が再び配列を動かせるようになることを示す。
A["fixed に入る（ピン留め）"] --> B["Ada の関数を呼ぶ"]
B --> C["Ada が呼び出しの間だけ読む"]
C --> D["Ada が戻る"]
D --> E["fixed を出る（GC が動かせる）"]
E -.->|"ここから先は使わない"| F["ポインター"]
図12: ポインターが有効なのは fixed の中だけなので、Ada は呼び出しの間だけ読む。
空の Span を fixed すると、ポインターは NULL になります。ReadOnlySpan<T>.GetPinnableReference は空のときに null の参照を返すからです13。境界の関数はこれをエラーコード1で返します。パラメーターと結果は、メソッドの中の変数のアドレスを & で渡しています。メソッドの中の構造体は GC に動かされないので、呼び出し先がメソッドの終わりより後までポインターを使わなければ、そのままアドレスを渡せます11。
ライブラリ名は "libinspect" にしました。.NET は Windows では libinspect と libinspect.dll を、Linux では libinspect.so などを探します14。gprbuild が作るファイルは Windows では libinspect.dll、Linux では libinspect.so なので、同じ名前で両方に届きます。呼び出し規約は CallConvCdecl を指定しています。x64 では呼び出し規約が1つしかないので結果は変わりませんが、x86 の P/Invoke の既定は Stdcall なので、指定しておけば x86 で食い違いません15。
flowchart TB
accTitle: libinspect という名前で探されるファイル
accDescr: LibraryImport に libinspect と書くと、Windows では libinspect.dll を、Linux では libinspect.so を探し、どちらも gprbuild が作るファイル名と一致することを示す。
A["LibraryImport（libinspect）"] --> B{"実行する OS"}
B -->|"Windows"| C["libinspect.dll を探す"]
B -->|"Linux"| D["libinspect.so を探す"]
C --> E["gprbuild の出力と一致"]
D --> E
図13: libinspect という名前は、Windows と Linux のどちらでも gprbuild が作るファイルに届く。
構造体の大きさを両側で比べる
C# の構造体と Ada のレコードの並びが食い違うと、エラーにならずに誤った値を読み書きします。Microsoft の資料も、エラーなしに値がおかしくなる原因として型の大きさの違いを挙げ、マネージドとネイティブの大きさを比べるよう勧めています11。そこで Ada の側に inspect_result_size を用意し、C# の sizeof と比べてから検査を始めます。
// 構造体の大きさを両側で比べ、食い違えば検査を始めない
int managedSize;
unsafe { managedSize = sizeof(InspectResult); }
int nativeSize = AdaInspector.NativeResultSize();
Ada の側は Inspect_Result'Max_Size_In_Storage_Elements を返します。この属性は、本来はアロケーターでオブジェクトを確保するときに要る大きさの上限です。手元の GNAT 13.3.0 では、オブジェクトのバイト数を表す Inspect_Result'Object_Size / System.Storage_Unit と同じ32でした。意図をはっきりさせるなら後者を使います。Linux では、C の sizeof と Ada のどちらも32バイトでした。64ビットの整数が先頭にあり、後ろの5つの int の20バイトに4バイトの詰め物が付いて、8の倍数になっています。大きさが同じでも並びの順序まで同じとは限らないので、フィールドの順序は C の宣言を基準にして、両側をそこから書きます。
flowchart TB
accTitle: 結果の構造体を3つの言語で揃える
accDescr: C の inspect_result の宣言を基準にして Ada のレコードと C# の構造体を書き、Ada の inspect_result_size と C# の sizeof で大きさを比べ、同じときだけ検査を始めることを示す。
A["C の宣言（基準）"] --> B["Ada のレコード（Convention C）"]
A --> C["C# の構造体（Sequential）"]
B --> D["inspect_result_size"]
C --> E["sizeof"]
D --> F{"大きさは同じか"}
E --> F
F -->|"同じ"| G["検査を始める"]
F -->|"違う"| H["検査を始めない"]
図14: C の宣言を基準にして両側を書き、大きさが同じときだけ検査を始める。
GitHub Actions の Windows のランナーで、DLL を .NET 10 のコンソールアプリから呼んだ結果です。C のテストドライバーと同じ画像と値を使い、最後の行だけ空の Span に変えています。
elaborated=1 result size: C#=32 Ada=32
ng (max 50) status=Ok defects=100 bbox=(100,50)-(109,59) verdict=1
ok (max 200) status=Ok defects=100 bbox=(100,50)-(109,59) verdict=0
padded stride status=Ok defects=100 bbox=(100,50)-(109,59) verdict=0
buffer too small status=BufferTooSmall defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
width > stride status=BadGeometry defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
threshold 300 status=BadParameter defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
max -1 status=BadParameter defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
empty span status=NullPointer defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
ALL PASSED
buffer too small は 644 × 480 バイトの配列から1バイト短い Span を切り出して渡しました。寸法は同じでも、C# が渡す長さが足りないので、Ada は配列を読まずにエラーコード3を返しています。
WPF の画面から使う
WPF の画面からはボタンを押したときに画像を取り込み、表示してから検査します。カメラの代わりに、テストと同じ画像を作る関数を置いています。
private async void InspectButton_Click(object sender, RoutedEventArgs e)
{
const int width = 640, height = 480, stride = 640;
byte[] frame = CaptureFrame(width, height, stride); // カメラから受け取る画像の代わり
FrameImage.Source = BitmapSource.Create(
width, height, 96, 96, PixelFormats.Gray8, null, frame, stride);
var parameters = new InspectParams { Threshold = 64, MaxDefectPixels = 50 };
InspectButton.IsEnabled = false;
bool fatal = false;
try
{
// 検査は UI スレッドの外で行う。終わるまで frame を書き換えない
var (status, result) = await Task.Run(() =>
{
var s = AdaInspector.Inspect(frame, width, height, stride, parameters, out var r);
return (s, r);
});
// 99 は想定していない失敗。メモリの不正もありうるので、DLL をもう呼ばない
fatal = status == InspectStatus.InternalError;
ResultText.Text = status == InspectStatus.Ok
? $"{(result.Verdict == 0 ? "合格" : "不合格")} 欠陥 {result.DefectPixels} 画素"
: fatal
? "検査を止めました。ログを残してアプリを再起動してください"
: $"検査できませんでした（{status}）";
}
finally
{
InspectButton.IsEnabled = !fatal;
}
}
状態が99（InternalError）のときは、ボタンを押せないままにして、DLL をもう呼びません。「例外を境界の関数で止めてエラーコードにする」の節で書いたとおり、99 は読めないアドレスを渡したときにも返るので、検査を止めてログを残し、アプリを再起動します。
検査は Task.Run で UI スレッドの外に出します。大きな画像では判定に時間がかかることがあり、その間に画面が止まらないようにするためです。WPF の UI 要素は作ったスレッドからしか触れないので16、結果を ResultText に書くのは await のあと、UI スレッドに戻ってからにしています。WPF の async と UI スレッドの関係は「WPF/WinFormsのasyncとUIスレッドを一枚で整理」にまとめています。
Ada は frame をコピーせずに読んでいます。検査が終わる前に次の画像を同じ配列へ書き込むと、Ada は書きかけの画像を判定します。取り込みと検査を並行して進めるなら、取り込み用のバッファを複数用意し、検査中のバッファには書き込まないようにします。取りこぼさずに取り込むためのバッファの回し方は「取りこぼさない取り込み処理をAdaのタスクで作る」で扱います。
flowchart TB
accTitle: WPF の UI スレッドと検査のスレッド
accDescr: UI スレッドが画像を取り込んで表示し、Task.Run で別のスレッドに検査を任せ、検査のスレッドが Ada の関数を呼んで結果を返し、await のあとの UI スレッドが結果を表示し、その間は画像の配列を書き換えないことを示す。
A["UI スレッドが取り込んで表示"] --> B["Task.Run で検査を任せる"]
B --> C["検査のスレッドが Ada を呼ぶ"]
C --> D["await のあと UI スレッドが表示"]
E["検査が終わるまで配列を書き換えない"] -.-> C
図15: 検査は別のスレッドで行い、結果の表示は UI スレッドに戻ってから行う。
この例では、前の節で書いた構造体の大きさの比較と初期化の確認を省いています。実際のアプリでは、起動したときに一度確かめてから検査を始めます。
この WPF の例は Windows のランナーの dotnet build でビルドできることを確かめました。99 のあとにボタンを戻さないように直したコードは、手元の Linux の .NET SDK 10.0.114 で EnableWindowsTargeting を指定してビルドしました。どちらも警告もエラーも出ませんでした。画面を表示して操作してはいません。
初期化と DLL の配置
ライブラリは gprbuild のプロジェクトファイルで、自動で初期化するスタンドアロンライブラリとして作ります10。
library project Inspect is
for Source_Dirs use ("src");
for Object_Dir use "obj";
for Library_Name use "inspect";
for Library_Dir use "lib";
for Library_Kind use "dynamic";
for Library_Interface use ("Inspect_API");
for Library_Auto_Init use "true";
end Inspect;
Library_Auto_Init の意味と、Windows ではライブラリのレベルにタスクを置けない制約17は、「Ada と C / C# をつなぐ」の初期化の節で扱いました7。この例の Inspect_API と Inspect_Core にはタスクがないので、その制約には当たりません。
初期化が済んだかどうかは、inspect_elaborated で確かめられます。パッケージ本体の末尾の begin から後ろで変数を1にしているので、初期化が行われていれば1が返ります。Linux の C のテストドライバーでも、Windows のランナーの C# のアプリでも、初期化の手続きを呼ばずに1が返りました。
Linux ではシグナルハンドラーが置き換わる
Linux では、ライブラリの自動の初期化がプロセスのシグナルハンドラーを置き換えます。GNAT のランタイムは SIGSEGV などのシグナルを Ada の例外に対応づけていて18、初期化のときにそのハンドラーを入れるからです。C のプログラムで SIGSEGV、SIGBUS、SIGFPE、SIGILL、SIGABRT にハンドラーを入れてから dlopen でライブラリを読み込むと、5つとも GNAT のものに置き換わっていました。
ライブラリを読み込むプロセスが自分でシグナルを使っていると、これが問題になります。Linux の .NET 10 のコンソールアプリで、ライブラリを読み込んで初期化させてからマネージドのコードで null 参照を起こすと、NullReferenceException として catch できませんでした。次のメッセージを出して、終了コード1でプロセスが終了しています。null 参照で起きた SIGSEGV を GNAT のハンドラーが受け取り、Ada の Storage_Error に変えたことが出力から分かります。
raised STORAGE_ERROR : stack overflow or erroneous memory access
flowchart TB
accTitle: Linux でライブラリを読み込んだときのシグナルハンドラー
accDescr: ホストのプロセスが入れた SIGSEGV などのハンドラーが、ライブラリの自動の初期化で GNAT のハンドラーに置き換わり、その後のシグナルを GNAT が受け取ることを示す。
A["ホストがハンドラーを入れる"] --> B["dlopen でライブラリを読み込む"]
B --> C["自動の初期化"]
C --> D["GNAT のハンドラーに置き換わる"]
D --> E["SIGSEGV を GNAT が受け取る"]
E -.->|".NET の場合"| F["null 参照を catch できない"]
図16: Linux では、ライブラリを読み込むとホストのシグナルハンドラーが GNAT のものに置き換わる。
GNAT には、ランタイムにハンドラーを入れさせない pragma Interrupt_State があります18。手元の GNAT 13.3.0 で5つのシグナルに State => System を指定すると、ホストのハンドラーは置き換わらずに残りました。ただしこの指定でライブラリにタスクのランタイム（libgnarl）がリンクされ、読み込んだスレッドで SIGTERM やリアルタイムシグナルなど多くのシグナルがブロックされるようになりました。シグナルを自分で使うホストにこのライブラリを読み込ませるための解決にはならないので、この記事では Linux の .NET から呼ぶ使い方を対象から外しました。
flowchart TB
accTitle: pragma Interrupt_State を付けたときの結果
accDescr: pragma Interrupt_State で State に System を指定するとホストのシグナルハンドラーは残るが、タスクのランタイムがリンクされて多くのシグナルがブロックされるので、シグナルを使うホストの解決にはならないことを示す。
A["Interrupt_State（State => System）"] --> B["ホストのハンドラーは残る"]
A --> C["タスクのランタイムがリンクされる"]
C --> D["多くのシグナルがブロックされる"]
D --> E["シグナルを使うホストの解決にならない"]
図17: pragma Interrupt_State でハンドラーの置き換わりは防げるが、タスクのランタイムが入り、別のシグナルがブロックされる。
GNAT の資料によると、この pragma は Windows では使えません18。Windows のランナーではライブラリを読み込んだあとの null 参照を NullReferenceException として catch できました。
Windows でアプリのフォルダーに置く DLL
Windows のランナーで Alire の GNAT（16.1.0）が作った libinspect.dll の依存を objdump -p で調べると、Windows の KERNEL32.dll と msvcrt.dll のほかに、GNAT のランタイムの libgnat-16.dll と libgcc_s_seh-1.dll がありました。この2つは GNAT のツールチェーンの bin にあるので、libinspect.dll と一緒にアプリのフォルダーへ置きます。
GNAT のランタイムの DLL を除いたフォルダーでコンソールアプリを動かすと、次の例外が処理されないままプロセスが終了しました。libinspect.dll そのものはフォルダーにあるのに、「libinspect またはその依存の DLL を読み込めない」というメッセージになります。
Unhandled exception. System.DllNotFoundException: Unable to load DLL 'libinspect' or one of its dependencies: The specified module could not be found. (0x8007007E)
例外が出たのは、最初に呼んだ NativeResultSize のときで、プロセスの終了コードは −532462766（0xE0434352）でした。libinspect.dll があるのにこの例外が出たら、依存する DLL を疑います。
flowchart TB
accTitle: アプリのフォルダーに置くファイル
accDescr: WPF のアプリの実行ファイルと同じフォルダーに libinspect.dll と GNAT のランタイムの DLL を置き、ランタイムの DLL が欠けると DllNotFoundException になることを示す。
A["アプリのフォルダー"] --> B["WPF のアプリ（exe と dll）"]
A --> C["libinspect.dll"]
A --> D["GNAT のランタイムの DLL"]
C --> D
D -.->|"欠けると"| E["DllNotFoundException"]
図18: アプリのフォルダーには Ada の DLL と GNAT のランタイムの DLL を一緒に置く。
Windows は、同じモジュール名の DLL がすでにプロセスに読み込まれていれば、どのフォルダーから読み込んだものでもそれを使います19。同じプロセスに GNAT や MinGW で作ったほかの DLL があり、版の違う libgcc_s_seh-1.dll などを先に読み込んでいると、そちらが使われます。GNAT のランタイムまで DLL に取り込む encapsulated の指定と、そのテストの結果は「Ada と C / C# をつなぐ」で触れています。Windows が DLL を探すフォルダーと順序は「Windows DLL名前解決の仕組み」にまとめています。
試した環境と確かめていないこと
この記事のコードは2026年11月10日に次の環境で動かしました。
- Ubuntu 24.04、GNAT 13.3.0、Ubuntu の gprbuild パッケージ（2024.1）。共有ライブラリを作り、C のテストドライバーから呼んで、上の結果を得ました。読み込んだときのシグナルハンドラーの置き換わりと、読めないアドレスを渡したときの戻り値、
pragma Interrupt_Stateを付けたときのリンクとシグナルのブロックも、ここで C のプログラムで確かめました。pragma Restrictions (No_Secondary_Stack)を付けたビルド、配列のパラメーターのアドレス、属性の値もここで確かめました。99 のあとにボタンを戻さないように直した WPF の例は、ここで .NET SDK 10.0.114 を使い、EnableWindowsTargetingを指定してビルドしました。 - GitHub Actions の Linux のランナー（ubuntu-24.04）と Alire の GNAT（gnat_native 16.1.0）。GNATprove（FSF 16.1.0）で
Inspect_Coreを証明し、共有ライブラリを C のテストドライバーと .NET 10 のコンソールアプリから呼びました。null 参照のテストもここで行いました。 - GitHub Actions の Windows のランナー（windows-latest、イメージは windows-2025-vs2026）、Alire の GNAT（gnat_native 16.1.0）、.NET SDK 10.0.403。DLL を作り、コンソールアプリから呼び、ランタイムの DLL を除いた場合と読めないアドレスを渡した場合を試し、null 参照のテストもして、WPF の例をビルドしました。
WPF の画面での動作、32ビットの Windows、実際のカメラの SDK が渡すバッファ、判定の速さ、複数のスレッドから同時に呼んだときの動作は確かめていません。Linux の .NET から呼ぶ使い方は、上で書いた理由で対象から外しています。境界の関数（SPARK の外の部分）の正しさは、証明ではなく上のテストとレビューで確かめています。検証に使ったプロジェクト一式は公開しておらず、記事のコードはその抜粋です。
関連記事
この記事はシリーズ「Ada とマシンビジョン」の1本です。シリーズのほかの記事は次のとおりです。
- 画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較
- GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー
- 取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
- ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ
関係する既存の記事は次のとおりです。
- Ada と C / C# をつなぐ ── DLL を作って呼び出す
- AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる
- GigE Vision・USB3 Visionカメラの取りこぼし ── 原因の切り分けとWindows側の設定
- C#からWin32 APIを安全に呼ぶ ── P/Invoke実務ガイド(DllImport / LibraryImport / CsWin32)
参考リンク
-
Microsoft Learn, Image Stride. 各行の後ろに詰め物のバイトがある場合に stride が幅より大きくなること、同じ寸法の画像でも stride が違いうること、bottom-up の画像の stride が負になること。 ↩ ↩2
-
Ada Reference Manual (Ada 2022), B.3 Interfacing with C and C++. アクセス型の
inのパラメーター（67項）とレコード型のパラメーター（69項）を C の関数にt*として渡すこと（Implementation Advice）。 ↩ -
Ada Reference Manual (Ada 2022), B.1 Interfacing Aspects. Import を指定したオブジェクトには既定の初期化が行われないこと。 ↩
-
Ada Reference Manual (Ada 2022), 6.2 Formal Parameter Modes. コピーで渡す型（by-copy type）でも参照で渡す型（by-reference type）でもないパラメーターは、コピーで渡すか参照で渡すかが規定されていないこと（11/3項）。 ↩
-
Ada Reference Manual (Ada 2022), 3.6.2 Operations of Array Types. Implementation Advice で、多次元の配列を通常は行優先で、Convention Fortran の型は列優先で表すよう勧めていること。 ↩
-
AdaCore, SPARK User’s Guide: Command Line Invocation.
--levelと--checks-as-errorsの説明。 ↩ -
小村ソフト, Ada と C / C# をつなぐ ── DLL を作って呼び出す. Linux で、処理されなかった Ada の例外が C と C# からの呼び出しでプロセスを終了させた実験。 ↩ ↩2
-
Microsoft Learn, Exceptions Interoperability. アンマネージドのコードの例外の扱いがプラットフォームによって違うこと。 ↩
-
GCC, s-soflin.ads（System.Soft_Links、GCC 13）. Ada のタスクのランタイムを使わないときは、主タスクのタスクごとのデータ
TSDを1つの変数NT_TSDに置くこと。TSDは二次スタックの位置（Sec_Stack_Ptr）と処理している例外（Current_Excep）を含むこと。 ↩ -
AdaCore, GPRbuild and GPR Companion Tools User’s Guide: GNAT Project Manager. Library_Interface と Library_Auto_Init の説明。 ↩ ↩2
-
Microsoft Learn, Native interoperability best practices. blittable な型、メソッドの中の構造体のアドレスを渡せる条件、構造体の大きさの比べ方、
DllNotFoundExceptionなどの症状と原因の対応表。 ↩ ↩2 ↩3 -
Microsoft Learn, fixed statement.
fixedの文の間はガベージコレクターが変数を動かさないこと、宣言したポインターをfixedの中でしか使えないこと、Span<T>をピン留めできること。 ↩ -
Microsoft Learn, ReadOnlySpan<T>.GetPinnableReference Method. 空の
Spanでは null の参照を返すこと。 ↩ -
Microsoft Learn, Native library loading. プラットフォームごとに試すライブラリ名の変化。 ↩
-
Microsoft Learn, Calling conventions. x86 の Windows での既定は Stdcall で、x64 では呼び出し規約が1つであること。 ↩
-
Microsoft Learn, Threading Model - WPF. UI 要素は作ったスレッドからしか触れないことと、Dispatcher を通じて UI スレッドに処理を頼む方法。 ↩
-
AdaCore, GNAT User’s Guide: Platform-Specific Information. Windows で DLL を読み込むと DllMain が呼ばれること、DllMain の中でスレッドを作れないのでスタンドアロンライブラリにライブラリのレベルのタスクを置けないこと。 ↩
-
AdaCore, GNAT Reference Manual: Pragma Interrupt_State. SIGSEGV、SIGABRT、SIGFPE、SIGILL などのシグナルが特定の Ada の例外に対応づけられること、State に System を指定するとランタイムがハンドラーを入れないこと、この pragma が Windows では使えないこと。 ↩ ↩2 ↩3
-
Microsoft Learn, Dynamic-link library search order. 同じモジュール名の DLL がすでに読み込まれていれば、どのフォルダーから読み込んだものでもそれを使うこと。 ↩
関連する記事
同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。
Ada と C / C# をつなぐ ── DLL を作って呼び出す
Adaで共有ライブラリを作り、CとC#から呼ぶ手順を実際に動かして説明します。Interfaces.CとConvention => C、gprbuildの設定、初期化、文字列とメモリの持ち主、例外の扱い、AdaからWindowsのDLLを呼ぶ方法まで扱います。
ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ
画像の寸法検査で起きるピクセルとミリメートルの取り違えを、Adaの派生型、abstractで消す演算子、総称パッケージ、固定小数点型でコンパイル時に防ぐ方法を、GNATのエラーとともに説明します。
画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較
画像処理のコードが画像の外を読み書きしないことを、SPARKのGNATproveで証明します。2値化、3×3の平滑化、ラベリングを例に、証明の書き方と証明していない範囲、検査を外したときのCとの速度の差を実測でまとめます。
取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
カメラの画像を取り込む処理を、Adaの周期タスク、保護オブジェクトで作るリングバッファ、優先度で組み立てます。処理が遅いときに捨てた数と待ち時間を測り、Linuxで優先度が効く条件とSPARKで確かめられる範囲を書きます。
GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー
GigE Visionの画像を運ぶGVSPのヘッダーを、Adaの表現句とScalar_Storage_Orderで型に対応させる方法と落とし穴を説明します。壊れたパケットでも範囲外を読まないパーサーを書き、SPARKで証明します。
関連トピック
このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。
Windows技術トピック
Windows 開発、不具合調査、既存資産活用の技術トピックをまとめた入口です。
UI スレッド / タイマーテーマ
WPF / WinForms、UI スレッド、async/await、タイマー設計を整理するトピックです。
このテーマがつながるサービス
この記事は次のサービスページにつながります。近い入口からご覧ください。
Windowsアプリ開発
WPFやWinFormsで作った検査アプリの画面や取り込みはそのままに、合否を決める処理だけを別の言語のDLLへ切り出したい場合に、Windowsアプリ開発の一部として扱えます。
技術相談・設計レビュー
画像のバッファの渡し方、寸法の検査、結果の構造体、エラーコードの決め方など、言語をまたぐ境界の設計を整理したい場合に、技術相談・設計レビューとして扱えます。
よくある質問
この記事のテーマについて、相談時によくある質問をまとめています。
- C#の画像をAdaのDLLにコピーせずに渡すには、どうすればよいですか？
- C#ではfixedで配列やSpanをピン留めし、先頭のポインターとバッファの長さ、幅・高さ・stride（1行のバイト数）を渡します。Adaの側では寸法がバッファの長さに収まることを確かめてから、同じメモリをAddressとImportで2次元の配列として見ます。Adaは呼び出しの間だけ読み、ポインターを保存しません。
- Adaの例外がC#へ出ないようにするには、どうすればよいですか？
- C#から直接呼ばれる関数の末尾に例外ハンドラーを書き、どの例外もエラーコード99に変えて返します。パラメーターの範囲外は例外に頼らずifで確かめ、4を返します。99はポインターや長さの誤りでメモリを読めなかったときにも返りうるので、検査を止める合図として扱います。
- C#の構造体とAdaのレコードの並びが合っているかは、どう確かめますか？
- 両方にConvention => CとStructLayout(LayoutKind.Sequential)を付けて、Cの構造体と同じ並びにします。そのうえで、Adaの側に構造体の大きさを返す関数を用意し、C#のsizeofと比べてから検査を始めます。この記事の例では、どちらも32バイトでした。