Constraint Errors in Ada, Detection in Spark
We all make mistakes. We’re human. In my case, I wrote a lovely off-by-one gem the other day. (Caught it before it managed to go anywhere important, but you still feel pretty dumb whenever you write something like that). I distilled the problem code down to something extremely simple in an effort to play around the latest proof tools in Spark 2014.
The Problem
An extremely simple example: write a procedure that takes an input array of integers, some of which may be gaps indicated by the zero value. This procedure should write the integers into a new array, with all gaps collapsed, leaving only a single contiguous gap at the end (if there is a gap).
package Array_Utils is
subtype Index is Integer range 1 .. 50;
type Int_Array is array (Index) of Integer;
-- Move all non-zero items to the front of the array
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array);
end Array_Utils;
package body Array_Utils is
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array) is
Current : Index := Index'First;
begin
New_Array := (others => 0);
for Idx in Old_Array'Range loop
if Old_Array(Idx) /= 0 then
New_Array(Current) := Old_Array(Idx);
Current := Current + 1;
end if;
end loop;
end Compact;
end Array_Utils;
If you were to call the code like such:
declare
Old_Arr : Array_Utils.Int_Array := (1..49 => 1, others => 0);
New_Arr : Array_Utils.Int_Array := (others => 0);
begin
Array_Utils.Compact(Old_Arr, New_Arr);
end;
Then you wouldn’t have a problem, because Current would never go past Index’Last. However, if instead of that,
Old_Arr : Array_Utils.Int_Array := (others => 1);
you would throw a constraint error on the last iteration, since Current was incremented past Index’Last. (Unfortunately, this is one of those cases where the type system works a tad against you. Yes, you did increment past the valid range, but that value was only written, never used. Have we used a plain unbounded integer, we never would have had a problem).
SPARK… to the Rescue?
So, with SPARK 2014 installed alongside the GNAT toolchain, let’s invoke the prover (having added nothing).
medium: range check might fail (e.g. when Current = 50)
Perfect! and I didn’t even have to execute my program.
So let’s take a quick pass at fixing things. First, create a new index type: ~~~ada subtype Index is Integer range 1 .. 50; subtype Super_Index is Integer range 0 .. 50; ~~~
and re-arrange the logic in our procedure so that Current is incremented first (and since it starts at 0, Current will never be incremented past the maximum end of the type range):
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array) is
Current : Super_Index := Super_Index'First;
begin
New_Array := (others => 0);
for Idx in Old_Array'Range loop
if Old_Array(Idx) /= 0 then
Current := Current + 1;
New_Array(Current) := Old_Array(Idx);
end if;
end loop;
end Compact;
Note: At this point, our constraint error has been fixed. Is that provable at this point? No… we end up with the same error message. Hrmm. At this point, SPARK doesn’t have enough information to prove that the value of Current won’t exceed its range.
This is where proof-assisting statements come in, such as Loop Invariants. Basically (and I’m heavily paraphrasing and summarizing here), if we can hint to the prover about some intermediate steps, it should be able to fill in the gap.
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array) is
Current : Super_Index := Super_Index'First;
begin
New_Array := (others => 0);
for Idx in Old_Array'Range loop
pragma Loop_Invariant
(Current < Idx);
if Old_Array(Idx) /= 0 then
Current := Current + 1;
New_Array(Current) := Old_Array(Idx);
end if;
end loop;
end Compact;
Note that the prover does in fact also prove the invariants themselves; if we were to mess up the loop invariant, SPARK would tell us. (Example: reversed the comparison direction in the Loop_Invariant)
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array) is
Current : Super_Index := Super_Index'First;
begin
New_Array := (others => 0);
for Idx in Old_Array'Range loop
pragma Loop_Invariant
(Current > Idx);
if Old_Array(Idx) /= 0 then
Current := Current + 1;
New_Array(Current) := Old_Array(Idx);
end if;
end loop;
end Compact;
This receives: ~~~array_utils.adb:17:13: medium: loop invariant might fail in first iteration, cannot prove Current > Idx (e.g. when Current = 0 and Idx = 1) array_utils.adb:17:13: medium: loop invariant might fail after first iteration, cannot prove Current > Idx (e.g. when Current = 2 and Idx = 2) array_utils.adb:21:32: medium: range check might fail (e.g. when Current = 50)~~~ ~~~
We can now be confident that we aren’t going to have a run-time error. Hooray!
Going Further
At this point we could stop, since our procedure is free from runtime errors. However, since we’ve already set up Spark on our code, we could go further and prove that our procedure does what said it was going to do (compact the gaps in the array).
I could see two additional post-conditions:
- That the array is in fact compacted (all zeroes at the end).
- That the resulting array contains all non-zero values from the original array.
Compaction
So we can add a post-condition that indicates any place in New_Array that has a zero is followed only by zeroes: ~~~ada – Move all non-zero items to the front of the array procedure Compact (Old_Array : in Int_Array; New_Array : out Int_Array) with Post => (for all J in New_Array’Range => (if New_Array(J) = 0 then (for all K in J .. New_Array’Last => New_Array(K) = 0))); ~~~
The prover cannot prove this statement outright. But with two additional loop invariants, we can.
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array) is
Current : Super_Index := Super_Index'First;
begin
New_Array := (others => 0);
for Idx in Old_Array'Range loop
pragma Loop_Invariant (Current < Idx);
pragma Loop_Invariant (for all J in New_Array'First .. Current => New_Array (J) /= 0);
pragma Loop_Invariant (for all K in Current+1..New_Array'Last => New_Array (K) = 0);
if Old_Array(Idx) /= 0 then
Current := Current + 1;
New_Array(Current) := Old_Array(Idx);
end if;
end loop;
end Compact;
Contains Original Values
Full disclosure - I really tried to make this proof happen as intended (all non-zero values from Old_Array` exist inNew_Array`). I tried to expand the post-condition as such:
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array)
with Post => ((for all J in New_Array'Range =>
(if New_Array(J) = 0 then (for all K in J .. New_Array'Last => New_Array(K) = 0))) and
(for all J in Old_Array'Range =>
(if Old_Array(J) /= 0 then (for some K in New_Array'Range =>
Old_Array(J) = New_Array(K)))));
But even with several additional loop invariants, I couldn’t manage to prove the additional clause in the post-condition.
With a tweak (that makes the proof weaker unfortunately) I did make some progress. Now, prove that New_Array only contains values from Old_Array. Unfortunately, this does not prove that New_Array has all the values it should. Alas.
procedure Compact (Old_Array : in Int_Array;
New_Array : out Int_Array)
with Post => ((for all J in New_Array'Range =>
(if New_Array(J) = 0 then (for all K in J .. New_Array'Last => New_Array(K) = 0))) and
(for all J in New_Array'Range =>
(if New_Array(J) /= 0 then (for some K in Old_Array'Range => New_Array(J) = Old_Array(K)))));
This only took an additional Loop_Invariant: ~~~ada pragma Loop_Invariant (for all J in New_Array’First .. Current => (for some K in Old_Array’First .. Idx => (Old_Array(K) = New_Array(J)))); ~~~
Caveats
I’m certainly not a SPARK expert. There are probably more effective ways to write the invariants and other suggestions to the proof tools. There’s several good books and tutorials out there (including the previously mentioned SPARK website).
https://blog.adacore.com/gnatprove-tips-and-tricks-how-to-write-loop-invariants https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_investigate_unproved_checks.html#how-to-investigate-unproved-checks
McCormick, John W., and Peter C. Chapin. Building High Integrity Applications with SPARK. Cambridge University Press, 2015.