Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C

Two mistakes are common in machine-vision inspection programs: a 3×3 filter reads pixels beyond the edge of the image, or code writes into the wrong row because width and height were swapped. They may not show up with the image sizes used in testing and surface only when the program is connected to a different camera. In this article I write image processing in SPARK, a subset of Ada, and use GNATprove to prove that such accesses outside the image cannot happen.

Here is the gist of the answer. Once the image type and the preconditions are fixed, binarization and 3×3 smoothing can be proved free of run-time errors. If the indices of the label equivalence table are restricted by their type, the same proof also goes through for connected-component labeling. However, I did not prove that the labeling result is correct, or that the number of provisional labels never exceeds the limit. When run-time checks are suppressed only in the units that were fully proved, at -O2 the code ran at almost the same speed as the equivalent C code.

The code was checked on November 10, 2026. Builds and tests were run with GNAT 13.3.0 on Ubuntu 24.04, and also with GNAT 16.1.0 installed via Alire 2.1.1 on a GitHub Actions Ubuntu 24.04 runner. All 10 tests passed in both environments, including the build with checks suppressed. The proofs were run on the same runner with GNATprove 16.1.0. Speeds were measured with GNAT 13.3.0. The basics of SPARK and GNATprove are explained in “Introduction to Formal Verification with SPARK”, and how to read contracts in “Proving AI-Written Code with SPARK”.

Where out-of-image reads and writes happen

Mistakes that access outside the image tend to happen in a few predictable places. The first is the edge of processing that reads neighboring pixels. When you apply a 3×3 filter to the whole image, the first row tries to read the row above it and the last column tries to read the column to its right. The second is swapping rows and columns. With a test image whose width equals its height the mistake does not show up, and the index goes out of range only with a wide camera image. The third is processing that uses a value computed from pixels as an index into another table, as labeling does. If the value falls outside the expected range, the program reads or writes outside the table.

In C none of these cause an error; the program reads or writes other memory. In Ada the index checks fire at run time and raise Constraint_Error, but if an exception is raised while the inspection equipment is running, processing stops right there. With SPARK you can prove, before running anything, that these checks never fail for any input that satisfies the preconditions. The SPARK User’s Guide calls the level of proving the absence of run-time errors Silver. As its benefits, it lists that the control flow cannot be hijacked through buffer overflows or integer overflows, and that the program does not misbehave when compiled with checks suppressed¹.

flowchart TB
        accTitle: Where accesses outside the image happen
        accDescr: Shows that accesses outside the image happen in three places, at the edges of processing that reads neighbors, when rows and columns are swapped, and in processing that uses values computed from pixels as table indices, and that C reads or writes other memory without an error, Ada raises an exception through run-time checks, and SPARK finds them by proof before running.
        A["Edges of neighbor reads"] --> D["Access outside the image"]
        B["Rows and columns swapped"] --> D
        C["Pixel-derived values as indices"] --> D
        D --> E["C (reads or writes other memory)"]
        D --> F["Ada (exception from run-time checks)"]
        D --> G["SPARK (found by proof before running)"]

Figure 1: Accesses outside the image tend to happen in three places, and how they show up depends on the language.

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (11 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

Representing images with Ada types

First I decide the image type. I create subtypes with ranges for the row and column indices, and make a pixel a modular type from 0 to 255. An image is a two-dimensional array whose row and column ranges are fixed per object.

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 is a type that does not fix the array bounds, so a 640×480 image and a 1920×1200 image can be handled with the same type. The range of each image is obtained with Img'Range (1) (rows) and Img'Range (2) (columns). Same_Shape is a function that expresses that the row and column ranges of two images are equal, and I use it in preconditions later. Because it is written in the specification as an expression function, GNATprove can use the contents of this comparison in proofs of other units as well². The upper limit of the width and height is 4096. Indices start at 0 to match the indices of C and of camera SDKs.

flowchart TB
        accTitle: How the image type is built
        accDescr: Shows that the image type Image is a two-dimensional array indexed by the row subtype Row and the column subtype Column with the pixel type Pixel as its element, and that Same_Shape expresses whether the row and column ranges of two images are equal.
        R["Row (0–4095)"] --> I["Image (2D array)"]
        C["Column (0–4095)"] --> I
        P["Pixel (0–255)"] --> I
        I --> S["Same_Shape (equal ranges?)"]

Figure 2: The image type is built from the row and column ranges and the pixel type.

Binarization can be proved with types and preconditions alone

Binarization sets pixels at or above a threshold to 255 and pixels below it to 0. I write in the precondition that the input and output have the same ranges, and in the postcondition that every pixel is the result of comparing it with the threshold.

   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)));

The output Target is in out. The bounds of an array allocated by the caller are available for an out parameter too, so it is not impossible to make it out. With out, however, GNATprove would have to be shown that the nested loop writing one element at a time initializes the whole array, which I believe requires an extra annotation (such as Relaxed_Initialization). This article did not try the out form. Because it is in out, a caller written in SPARK must initialize Target before the call. The same applies to Labels and Parent in labeling. The body loops over the input’s range and writes to the output.

   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;

The indices of Source (Y, X) are the loop ranges themselves, so it is obvious that the checks do not fail. The indices of Target (Y, X) are known to be in the same range as the input from the precondition Same_Shape. If all you want to show is that the code does not access outside the image, no loop invariants are needed.

The loop invariants were written for the postcondition. In the inner loop they state that the current row up to column X and all rows above it are correct, and in the outer loop they state that all rows up to row Y are correct. According to the SPARK User’s Guide, when a loop modifies an array, the invariant may also need to state that the parts not modified stay unchanged. This is called a frame condition³. The second invariant, which states that the rows above remain correct, plays the same role in that it shows the range already written is not disturbed.

flowchart TB
        accTitle: The range expressed by the binarization loop invariants
        accDescr: Shows that the inner loop's invariant expresses that all rows above row Y and row Y up to column X are written correctly, that the outer loop's invariant expresses all rows up to row Y, and that on leaving the loop this extends to every pixel in the postcondition.
        A["Rows above row Y (all correct)"] --> C["Inner loop invariant"]
        B["Row Y up to column X (correct)"] --> C
        C --> D["Outer loop invariant (up to row Y)"]
        D --> E["Postcondition (every pixel)"]

Figure 3: The range guaranteed by the invariants widens as the loop progresses and finally becomes the postcondition.

The mistake of reading past the border in 3×3 smoothing

Smoothing replaces each pixel with the average of the 3×3 pixels around it. First, I write code that loops over the whole image without thinking about the ranges.

      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;

The same code written in C compiles as well. When I ran GNATprove on it, it reported in four places that it could not prove the index checks on the neighbors. There was one report for each way of shifting the index (Y - 1, X - 1, Y + 1, X + 1), but there are 12 indices that can go out of range. The number of reports does not represent the number of dangerous indices. One of them is the following output.

 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

When Y is the first row, Y - 1 is outside the image’s range. For checks it could not prove, GNATprove shows the location and the condition the check requires (here, that the result of the subtraction is a valid index into the array). When --level is specified, it may also generate an example of values that make it fail (a counterexample)⁴, but in this run no counterexample was shown and it reported that the provers had reached the time limit. For code that swapped rows and columns and wrote Source (X, Y), GNATprove likewise reported that it could not prove the checks on either index of Source (X, Y).

The fixed code loops only over the interior, excluding the one-pixel border, and copies the input unchanged to the border.

   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;

Because the loop range was narrowed to the interior, everything from Y - 1 to Y + 1 and from X - 1 to X + 1 falls inside the image. If the image is less than 3 pixels in either direction, the interior range is empty and the output is a copy of the input. The array length check of Target := Source is proved from the precondition Same_Shape. The sum of nine pixels does not exceed 2295, nine times 255, so it is also proved that Natural does not overflow and that the result of dividing by 9 fits in the range of Pixel.

flowchart TB
        accTitle: The loop range of smoothing
        accDescr: Shows that code looping over the whole image makes Y-1 fall outside the range in the first row so GNATprove cannot prove the index checks, and that code looping over the interior excluding the border and copying the input to the border can have all its checks proved.
        A["3×3 smoothing"] --> B["Loop over the whole image"]
        A --> C["Loop over the interior only"]
        B --> D["Y - 1 out of range in first row"]
        D --> E["Index checks cannot be proved"]
        C --> F["Copy the input to the border"]
        F --> G["All checks proved"]

Figure 4: When the loop range is narrowed to the interior, all neighbor indices fall inside the image.

Range computations overflow on an empty image

The two lines “the image is not empty” in the precondition were not there at first. When I ran GNATprove with a precondition of only Same_Shape, it reported in four places that it could not prove the overflow checks: Source'First (1) + 1 and Source'Last (1) - 1, which compute the interior range, and the same two computations for columns.

 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

The cause is the empty image. In Ada, the bounds of an empty range do not have to lie within the subtype’s range, and the ranges taken by array indices are checked by this rule too⁵⁶. So an empty image whose row range is Integer'Last .. Integer'Last - 1 can also be created as an Image. In that case Source'First (1) + 1 exceeds the range of Integer. When I actually passed this image with GNAT 13.3.0, Constraint_Error (overflow check failed) was raised at line 40 of image_ops.adb.

So I added to the precondition that the image is not empty in either direction. For a non-empty image the range bounds lie within Row and Column, so + 1 and - 1 do not overflow. The tests confirm that passing the same empty image raises Assertion_Error from the precondition check.

flowchart TB
        accTitle: Why range computations overflow on an empty image
        accDescr: Shows that because the bounds of an empty range may lie outside the subtype, an empty image whose range starts at Integer'Last can be created and its First plus 1 exceeds the range of Integer, and that adding to the precondition that the image is not empty keeps the bounds within Row and Column so nothing overflows.
        A["Empty-range bounds may lie outside the subtype"] --> B["Empty image starting at Integer'Last"]
        B --> C["First (1) + 1 overflows"]
        C --> D["Add non-empty to the precondition"]
        D --> E["Bounds lie within Row and Column"]

Figure 5: For an empty image the range bounds can lie outside the index type, so the precondition excludes empty images.

The caller is responsible for meeting the precondition

When GNATprove proves a body, it assumes the precondition holds. In exchange, a caller written in SPARK must prove that the precondition holds at every call². Overlap between arguments, such as passing the same image as both input and output, is also checked by GNATprove for SPARK callers⁷.

The problem is calls from code that is not SPARK. The part that receives images from a camera SDK and the part called from a C# application are often placed outside SPARK, and there is no guarantee that preconditions are respected there. For calling proved subprograms from unproved code, the SPARK User’s Guide recommends checking preconditions at run time with pragma Assertion_Policy⁸. So at the top of the proved image_ops.ads and labeling.ads I added a pragma that enables only the precondition checks.

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

package Image_Ops with SPARK_Mode is

With -gnata, GNAT checks preconditions, postconditions and loop invariants all together at run time⁹. I used this pragma instead of -gnata to keep only the preconditions. Checking the binarization loop invariants as well would mean evaluating, for every pixel, an expression that checks the whole range written so far.

This pragma must be written in the called unit. Looking at the code expanded by the compiler with -gnatG, the precondition checks were built into the beginning of the called Binarize and Smooth_3x3. When I tried it with GNAT 13.3.0, if image_ops.adb was compiled with -gnatp without the pragma, smoothing an empty image returned without raising an exception even when the caller was compiled with -gnata. This is erroneous execution with checks suppressed, and the standard does not define the result¹⁰. After adding the pragma, the precondition check raised Assertion_Error even when compiled with -gnatp.

flowchart TB
        accTitle: Where preconditions are checked
        accDescr: Shows that for SPARK callers GNATprove proves the precondition at every call, that for calls from non-SPARK callers the precondition is checked by run-time checks built into the called side, and that in both cases the body is proved assuming the precondition holds.
        A["SPARK caller"] -->|"Proved by GNATprove"| C["Precondition"]
        B["Non-SPARK caller"] -->|"Checked at run time by the callee"| C
        C --> D["Assumption of the body's proof"]

Figure 6: How the precondition is checked depends on whether the caller is SPARK.

flowchart TB
        accTitle: How to keep preconditions in a build with checks suppressed
        accDescr: Shows that when called from an unproved caller, the precondition check is built into the called unit, so if the callee's package specification has the Assertion_Policy pragma the precondition is checked even when compiled with -gnatp, and if not it is not checked even with -gnata on the caller, and that it returned without an exception on an empty image.
        A["Unproved caller"] --> B["Call to Smooth_3x3"]
        B --> C{"Pragma in the callee?"}
        C -->|"Yes"| D["Precondition checked even with -gnatp"]
        C -->|"No"| E["Caller's -gnata has no effect"]
        E --> F["Returned on an empty image with no exception"]

Figure 7: Precondition checks are built into the callee, so the pragma also goes in the callee’s package specification.

In labeling, restrict the equivalence table’s indices by type

Connected-component labeling assigns a number to each connected blob of pixels in a binary image. Here I use the method shown by Rosenfeld and Pfaltz that assigns labels in two scans¹¹. Pixels connected through their 4-neighborhood (up, down, left, right) are treated as the same blob.

In the first scan, for each pixel I look at the labels of the pixels above and to the left. If neither has a label, I assign a new label; if only one has a label, I copy it; if both have labels, I record in the equivalence table that the two labels belong to the same blob. In the second scan, each pixel’s label is replaced with the representative label of its blob. Finally, counting the representative labels gives the number of blobs.

flowchart TB
        accTitle: Labeling in two scans
        accDescr: Shows that the first scan looks at the labels of the pixels above and to the left and either assigns a new label, copies a label, or merges two labels into the same blob in the equivalence table, that the second scan replaces each pixel's label with the representative label, and that the representatives are finally counted.
        A["First scan"] --> B{"Labels above and left"}
        B -->|"Neither"| C["Assign a new label"]
        B -->|"Only one"| D["Copy that label"]
        B -->|"Both"| E["Merge in the table"]
        C --> F["Second scan: use representatives"]
        D --> F
        E --> F
        F --> G["Count the representative labels"]

Figure 8: The first scan records provisional labels and equivalences, and the second unifies them to representative labels.

The types were defined as follows.

with Images; use Images;

package Labeling with SPARK_Mode is

   Max_Labels : constant := 2 ** 22;

   subtype Label    is Natural range 0 .. Max_Labels;  --  0 is background
   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 has Label_Id as both its index type and its element type, so any value taken from the table is a valid index into the table. Find, which looks for the representative, just keeps following Parent (Root). Because the type of Root is also Label_Id, this index produces no check to be proved, and the GNATprove output showed 0 checks for Find. No loop invariant is needed either.

   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 is a procedure rather than a function so that I am not required to prove that it always terminates. GNATprove unconditionally verifies termination for ordinary functions, and verifies it for procedures only when Always_Terminates is specified¹². That Find terminates follows from the fact that every label in use points to a number no greater than itself, but proving that requires an invariant over the whole equivalence table. In this article I limited the proof target to the absence of run-time errors.

The first scan is as follows.

      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;  --  ran out of labels
                  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;

Because Y > Source'First (1) and X > Source'First (2) are checked before reading the pixels above and to the left, nothing outside the image is read even in the first row and column. The range of Labels equals that of Source by the precondition, so the index check of Labels (Y - 1, X) is also proved.

Before assigning a new label, the code checks whether Next exceeds Max_Labels, and if it does, returns with Success still False. Without this check, when Next became Max_Labels + 1 the code would write to Parent (Next) and the index check would fail. The limit applies not to the number of blobs but to the number of provisional labels assigned in the first scan. Provisional labels are counted one by one, including those later merged into the same blob. Pixels that get a new provisional label within one row are never adjacent, so a row needs at most half the width (rounded up), and the whole image at most “height × half the width (rounded up)”. Images for which this is at most the limit of 4,194,304 (for example up to a width of 4096 and a height of 2048) never fail, whatever the pattern. A 4096×4096 checkerboard needs 8,388,608 provisional labels, because under 4-connectivity every pixel is a separate blob. The tests confirm that Success becomes False for this image. Labeling can fail even with few blobs. A diagonally striped image whose foreground pixels are those with (X + Y) mod 3 /= 2 succeeded at 3000×3000 with 2,000 blobs. At 4096×4096 there are only about 2,730 blobs by calculation, but it ran out of provisional labels and Success became False (confirmed with GNAT 13.3.0). When it fails, Labels still holds provisional labels from partway through, so do not use it.

flowchart TB
        accTitle: Restricting the equivalence table's indices by type
        accDescr: Shows that Parent_Table has Label_Id as both index and element, so values taken from the table are valid indices as they are and Find's indices produce no checks, and that before assigning a new label the code checks whether Next is within the limit and returns failure if it is exceeded.
        A["Parent_Table (index and element Label_Id)"] --> B["Values taken out are valid indices"]
        B --> C["No checks on Find's indices"]
        D["Assign a new label"] --> E{"Next within the limit?"}
        E -->|"Yes"| F["Write to Parent (Next)"]
        E -->|"No"| G["Return with Success still False"]

Figure 9: Separate the part where the type restricts the indices from the part that checks the limit at run time.

For labeling, what GNATprove proved is only the absence of run-time errors. I did not prove the correctness of the result, that pixels in the same blob get the same label and different blobs get different labels. The result was checked by tests. The test program checks the label values and the number of blobs for a U shape, and the number of blobs for two separate blobs and a 4×4 checkerboard. I also compared the results with the same processing written in C, and the label values matched for 64×48 (45 blobs) and 1920×1200 (10,477 blobs) images. However, the C version is a port of the same procedure, so a match shows only that the port is correct. So I also compared against a different method. On 20,000 random images from 1×1 to 9×9 (with the index starting anywhere from 0 to 4), I compared the labeling result with the blob partition obtained by flood fill, and compared the smoothing result with averages computed by adding the nine pixels directly. There were 0 mismatches. This comparison was run with GNAT 13.3.0, separately from the test program.

flowchart TB
        accTitle: What was and was not confirmed for labeling
        accDescr: Shows that the absence of run-time errors was proved with GNATprove, that the labeling result was checked by tests on small images, a comparison with flood fill on random images and a comparison with the C implementation, and that Find terminating and the number of provisional labels not exceeding the limit were not confirmed, with failure returned when the limit is exceeded.
        A["Labeling"] --> P["Proved with GNATprove"]
        A --> T["Confirmed by tests"]
        A --> U["Not confirmed"]
        P --> B["No run-time errors"]
        T --> C["Result as expected"]
        U --> D["Find terminates"]
        U --> E["Provisional labels within the limit"]
        E -.-> F["Return failure if exceeded"]

Figure 10: For labeling, treat what was proved, what was tested and what was not confirmed separately.

GNATprove results

The proof was run with GNATprove installed through Alire, using the following command.

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

With --report=all, the checks that were proved are also shown one by one.

In the run before “the image is not empty” was added to the precondition, 103 of the 107 checks were proved, and the remaining four were the computations of the interior range in smoothing shown in the previous section. All 26 checks of binarization and all 32 of labeling were proved, along with the binarization postcondition and loop invariants.

After the precondition was added, all 107 checks were proved, and Success: all checks proved (107 checks). was shown at the end of the output. They consist of 97 proved by the provers (26 for binarization, 39 for smoothing, 32 for labeling), plus 9 variable initializations and 1 subprogram termination confirmed by flow analysis. For code with deliberately introduced mistakes, as shown in the previous section, GNATprove reports that it cannot prove the index checks.

flowchart TB
        accTitle: How GNATprove proves checks
        accDescr: Shows that GNATprove tries to prove the index, range and overflow checks and the contracts in SPARK code, and separates those it proved from those it reports with a location and reason.
        A["SPARK code"] --> B["GNATprove"]
        B --> C["Index, range and overflow checks, contracts"]
        C --> D["Proved"]
        C --> E["Not proved (location and reason shown)"]

Figure 11: GNATprove proves checks and contracts one by one, and reports those it cannot prove with a location and reason.

Suppressing run-time checks only from units that were proved

GNAT enables index, range and overflow checks by default. With -gnatp, the unit is compiled as if it contained pragma Suppress (All_Checks), and validity checks are suppressed as well¹³. The Ada standard specifies that if, with a check suppressed, a situation arises in which that check would fail, the execution is erroneous¹⁰. If checks are suppressed in code that has not been proved, then just as in C, there is no telling what an access outside the image might cause.

The SPARK User’s Guide explains that applying -gnatp to the whole program or using pragma Suppress has the problem that the program is no longer protected against mistakes and attacks. It then recommends suppressing checks only in the parts whose absence of run-time errors has been proved with GNATprove¹⁴. gprbuild lets you specify compiler switches per source file¹⁵, so I applied -gnatp only to image_ops.adb and labeling.adb, which were proved.

   package Compiler is
      --  Compile C with the same GCC as Ada (so that clang is not chosen)
      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");
            --  Suppress run-time checks only from the units that were proved
            for Switches ("image_ops.adb") use (Opt, "-gnatp");
            for Switches ("labeling.adb") use (Opt, "-gnatp");
      end case;
   end Compiler;

Opt is a variable that selects the optimization switch (-O2 or -O3). The test program and the benchmark program keep their checks even in nochecks. The preconditions of the proved units are checked by the pragma Assertion_Policy from the previous section even with -gnatp. The tests also confirmed, in the nochecks build, that an empty image is stopped by the precondition check. The -gnateA in the test build is a switch that checks at run time whether the actual parameters of a call overlap⁹.

Before suppressing checks, also confirm the assumptions listed by the SPARK User’s Guide⁸. Unproved callers must respect the preconditions. Another assumption is that inputs and outputs that could interfere are not passed as overlapping objects. If C# or SDK code passes the same image as input and output, as in Smooth_3x3 (A, A), the result can be wrong without any error. When I tried it with GNAT 13.3.0, in a build without -gnateA Smooth_3x3 (A, A) returned without an exception and gave a different result from writing to a separate image. In the test build with -gnateA, the same call raised Program_Error (aliased parameters). Inputs must hold valid values; for example, receiving an array containing values outside the range of Label is not anticipated. Stack overflow (Storage_Error) is outside the scope of GNATprove. In this article’s example, the large images and the equivalence table are allocated on the heap and passed in, not placed on the stack.

flowchart TB
        accTitle: Deciding where to suppress run-time checks
        accDescr: Shows that -gnatp is applied only to units whose checks were all proved with GNATprove, that units that could not be proved keep their checks, and that when called from non-SPARK callers the preconditions are checked at run time.
        A{"All checks proved?"} -->|"Yes"| B["-gnatp on that file only"]
        A -->|"No"| C["Keep the checks"]
        B --> D{"Is the caller SPARK?"}
        D -->|"Yes"| E["Leave as is"]
        D -->|"No"| F["Check preconditions at run time"]

Figure 12: Suppress checks only from units that were proved, and keep the preconditions at the boundary.

Comparing speed with the same processing written in C

I wrote the same three processes in C (labeling also merges the equivalence table in the same order), called both from an Ada benchmark program, and compared the times. Each time I confirmed that the Ada and C results matched down to the pixel values and label values. The measurement conditions were as follows.

• The image was 1920×1200, generated with pseudo-random numbers. For labeling I used that image smoothed twice and then binarized (10,477 blobs).
• One set was 200 binarizations, 100 smoothings and 20 labelings, and the median of 7 sets was taken as the time per call. This measurement was repeated 7 times for each of the four builds in alternation, and the table shows the median of the 7 repetitions and the minimum to maximum of the Ada/C ratio.
• “With checks” means the language checks (index, range, overflow) plus the precondition checks kept by pragma Assertion_Policy. Postconditions and loop invariants were not executed in any build.
• The environment was a 4-core cloud container with an Intel Xeon at 2.10 GHz (Ubuntu 24.04, Linux 6.18), and both Ada and C were compiled with GCC 13.3.0 (GNAT 13.3.0). Other work was running in the same container, so the ratios vary by 20 to 30 percent. Read the values in the table as a rough guide.

When I first measured (with the code before the pragma that keeps the precondition checks was added), compared with Ada at -O2 with checks, C was about 20 times faster for binarization and about 7 times faster for smoothing. The reason was that gprbuild had chosen clang (18.1.3) as the C compiler, and clang’s -O2 vectorized these loops (confirmed with -Rpass=loop-vectorize). With the current code, which includes the pragma, recompiling only the C side with clang and measuring three times showed C about 9–10 times faster for binarization and about 6–8 times faster for smoothing. To compare with the same GCC as Ada, I fixed the C Driver to gcc in the gpr file in the previous section¹⁵. Before comparing the speed of languages, you need to check that both are compiled with the same compiler and the same switches.

flowchart TB
        accTitle: How the speeds were compared
        accDescr: Shows that the Ada benchmark program calls the Ada and C implementations, compiled with the same GCC, on the same image, measures the time, and confirms every time that the results match down to the pixel values and label values.
        A["Benchmark program (Ada)"] --> B["Ada implementation"]
        A --> C["C implementation"]
        B --> D["Compiled with the same GCC 13.3.0"]
        C --> D
        A --> E["Measure the time"]
        A --> F["Check the results match every time"]

Figure 13: Compile the Ada and C implementations with the same compiler and compare results and times on the same image.

The times are Ada’s time per call. The C times measured at the same time in the builds with checks (median of 7 repetitions) were 1.77 ms for binarization, 3.92 ms for smoothing and 22.6 ms for labeling at -O2, and 0.182 ms, 1.08 ms and 20.5 ms at -O3.

At -O2, keeping the checks made smoothing take 1.4 to 2.1 times as long as C and labeling about 1.2 times, and suppressing the checks in the proved units brought them almost level with C. The SPARK User’s Guide says that run-time checks usually increase execution time by around 10 percent, and that code called many times can see much larger increases¹⁴. Per-pixel loops are exactly such code. Looking at the code expanded by the front end with -gnatG (the stage before optimization), in binarization the index checks on Source had disappeared and the index checks on the rows and columns of Target were inside the per-pixel loop. In smoothing, an index check was inserted every time a neighboring pixel was read.

Only binarization ran at almost the same speed as C at -O2 even with checks kept. I believe this is because the precondition checks were kept. Measuring five times each, alternating with code without the pragma Assertion_Policy, I found that with checks kept, binarization took 2.02–2.11 times as long as C when the pragma was absent, and 0.98–1.02 times when it was present. Once Same_Shape has been checked on entry, Target is known to have the same range as Source, so GCC was presumably able to eliminate the index checks on Target inside the loop. The vectorization report in the next paragraph also changed depending on whether the pragma was present.

Since GCC 12, vectorization is enabled even at -O2, but the cost model is very-cheap, and loops that need run-time checks such as for data overlap are not vectorized¹⁶¹⁷. Checking with GCC 13.3.0’s -fopt-info-vec-missed, the binarization loop at -O2 was not vectorized in either Ada or C because it “would need a runtime alias check”. In Ada without the precondition pragma, the reason became “control flow in loop”. For the smoothing loop the reasons differed: C and Ada with checks suppressed likewise cited the overlap check, but Ada with checks kept cited “control flow in loop”. What prevented vectorization was the branches from the index checks.

flowchart TB
        accTitle: Why loops were not vectorized at -O2
        accDescr: Shows that with GCC 13.3.0 at -O2, the binarization loop in every build and the smoothing loop in C and in Ada with checks suppressed were not vectorized because overlap would need to be checked at run time, that Ada smoothing with checks kept was not vectorized because of the branches from the index checks, and that at -O3 both were vectorized by creating a version that checks overlap and by moving the branches out of the loop.
        A["Why -O2 did not vectorize"] --> B["Overlap check needed (binarization etc.)"]
        A --> C["Check branches (smoothing with checks)"]
        B --> F["-O3: create an overlap-checking version"]
        C --> G["-O3: move branches out of the loop"]
        F --> H["Vectorized at -O3"]
        G --> H

Figure 14: What prevented vectorization at -O2 differed by process and by whether checks were kept.

At -O3, the difference due to checks disappeared for binarization and smoothing. At -O3 the cost model becomes dynamic, and the compiler vectorizes by generating separate code that checks overlap at run time. Binarization was vectorized even with its checks kept. Setting only the cost model to dynamic at -O2 also vectorized binarization. Smoothing was also vectorized at -O3 with its checks kept, but with -fno-unswitch-loops it was not. I believe this is because loop unswitching, enabled at -O3 (an optimization that moves conditional branches inside a loop out of the loop), moved the check branches out¹⁷. Labeling, which is not vectorized, took longer than C with checks kept even at -O3.

flowchart TB
        accTitle: How the effect of suppressing checks differs
        accDescr: Shows that with checks kept, at -O2 the loops are not vectorized and smoothing and labeling are slower than C (binarization is on par with C because the precondition check lets GCC eliminate the index checks), that at -O3 binarization and smoothing are vectorized and only labeling is slower than C, and that in both cases suppressing the checks in the proved units brings them on par with C.
        A["Time with checks kept"] --> B["-O2 (not vectorized)"]
        A --> C["-O3 (binarization and smoothing vectorized)"]
        B --> D["Smoothing and labeling slower than C"]
        C --> E["Only labeling slower than C"]
        D -.-> F["On par with C without checks"]
        E -.-> F

Figure 15: The effect of suppressing checks depends on the optimization level and the shape of the loop.

Before deploying to the equipment, measure both with and without checks, using the compiler and switches you will actually use, and decide from that.

Test environment and what was not verified

Here is a summary of what was confirmed for the code in this article.

• Environment: Builds and tests were run with GNAT 13.3.0 on Ubuntu 24.04 and with GNAT 16.1.0 (Alire 2.1.1) on a GitHub Actions Ubuntu 24.04 runner. Proofs were run with GNATprove 16.1.0 on the same runner at --level=2. Speeds were measured with GNAT 13.3.0 (GCC 13.3.0). The full project used for verification (the gpr files and test programs) is not published, and the code in this article is an excerpt from it.
• Proved with GNATprove: For binarization, 3×3 smoothing and labeling, the index, range and overflow checks never fail for any input that satisfies the preconditions. The binarization result matches the postcondition.
• Confirmed by tests: The smoothing and labeling results are as expected (expected values on small images, agreement with a different method on 20,000 small random images, and agreement with the same processing written in C). Failure is returned for an image that runs out of provisional labels. An empty image is stopped by the smoothing precondition check (including in the build with checks suppressed). In the build with -gnateA, passing the same image as input and output raises Program_Error.
• Not confirmed: That Find always terminates. A proof of the correctness of the smoothing and labeling results. Stack overflow. Behavior on Windows and with real camera images.

Proving the correctness of the results as well would require writing, for labeling, an invariant over the whole equivalence table. If you first prove the absence of accesses outside the image and confirm the correctness of the results by tests, you can eliminate the serious defect of out-of-bounds access while writing hardly any loop invariants.

Related Articles

This article is part of the series “Ada and Machine Vision”. The other articles in the series:

• Receiving GigE Vision Packets with Ada Types — Pitfalls of Representation Clauses and a SPARK-Proved Parser
• Frame Acquisition Without Drops Using Ada Tasks — A Protected-Object Ring Buffer and Priorities
• Calling Ada Inspection Logic from a C# Inspection App — Passing Image Buffers Without Copying and Guarding the Boundary
• Separating Pixels and Millimeters with Types — Preventing Unit Mix-ups in Dimensional Inspection with Ada

Related existing articles:

• Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
• Proving AI-Written Code with SPARK ── Humans Write the Contracts, GNATprove Checks Them
• Starting an Ada Project with Alire — Creating a Project, Adding Dependencies, Build Profiles, and GNATprove
• Dropped Frames with GigE Vision and USB3 Vision Cameras — Locating the Cause and the Windows Settings to Review

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

Can SPARK prove that image-processing code never reads or writes outside the image?

Yes. In this article, for binarization, 3×3 smoothing and connected-component labeling, I used GNATprove to prove that index and range checks never fail for any input that satisfies the preconditions. The starting point is to give the image type row and column ranges and to write in the precondition that the input and output ranges are equal.

Once the code is proved, can run-time checks be suppressed?

The SPARK User's Guide recommends suppressing them only in units in which GNATprove proved all checks. To prepare for calls from unproved code, write pragma Assertion_Policy (Pre => Check) in the specification of the proved unit and keep the precondition checks. In this article's measurements, suppressing the checks in the proved units at -O2 made the code almost as fast as the same processing written in C.

What was proved about labeling, and what was not?

The absence of run-time errors was proved. That the labeling result is correct, that the search for the representative label always terminates, and that the number of provisional labels never exceeds the limit were not proved. The results were checked with tests on small images, a comparison with a different method on small random images, and a comparison with the same processing written in C. For images whose provisional labels exceed the limit, failure is returned.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.