Formal Verification of Legacy Code
by Yannick Moy –
Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.
Identifying the Preconditions
Initially, we extracted the Get_Line function and related subprograms in order to analyze them more easily with our various static analysis tools. Running CodePeer on the code detected some possible range check failure, that upon manual analysis corresponded to code being made unreachable by the recent fix. So we removed that dead code. In order to run SPARK on the code, we started with identifying the preconditions of the various subprograms being called. A critical precondition (leading to raising exception End_Error in the original problem reported by our partner) is that procedure Get_Line is not supposed to be called on an empty file. The same is true for the local procedure Get_Rest used in the function Get_Line. So we added an explicit precondition in both cases:
procedure Get_Line
(File : in out File_Type;
Item : out String;
Last : out Natural)
with
Pre => not End_Of_File (File);
function Get_Rest (S : String) return String with
Pre => not End_Of_File (File);We then ran GNATprove on the code, and it showed places where it could not prove that the precondition was satisfied... which made us discover that the initial fix was incomplete! The same fix was needed in another place in the code to ensure that the precondition above could be satisfied always.
Specifying the Functional Behavior of Get_Line
To go beyond that initial attempt, we had to transform the code to hide low-level address manipulations under SPARK subprogram with appropriate contracts, in order to show that the code calling these subprograms was achieving the desired functionality. For example, the low-level memcpy function from libc was originally imported directly:procedure memcpy (s1, s2 : chars; n : size_t);
pragma Import (C, memcpy);and called in the code of Get_Line:
memcpy (Item (Last + 1)'Address,
Buf (1)'Address, size_t (N - 1));The code above does not allow writing a suitable contract for memcpy. So we hide the low-level memcpy under a typed version:
procedure Memcpy
(S1 : in out String;
S2 : String;
From1, From2 : Positive;
N : Natural)
is
pragma SPARK_Mode (Off);
procedure memcpy (s1, s2 : chars; n : size_t);
pragma Import (C, memcpy);
begin
memcpy (S1 (From1)'Address, S2 (From2)'Address, size_t (N));
end Memcpy;The call to memcpy above now passes in the typed variables instead of their addresses:
Memcpy (S1 => Item, From1 => Last + 1,
S2 => Buf, From2 => 1, N => N - 1);This allows us to add a suitable functional contract to the typed version of Memcpy, stating that when N is positive, N characters are copied from string S2 at position From2 to string S1 at position From1:
procedure Memcpy
(S1 : in out String;
S2 : String;
From1, From2 : Positive;
N : Natural)
with
Pre =>
(if N /= 0 then
From1 in S1'Range and then
From1 + N - 1 in S1'Range and then
From2 in S2'Range and then
From2 + N - 1 in S2'Range),
Contract_Cases =>
(N = 0 => S1 = S1'Old,
N /= 0 => (for all Idx in S1'Range =>
(if Idx in From1 .. From1 + N - 1 then S1 (Idx) = S2 (Idx - From1 + From2)
else S1 (Idx) = S1'Old (Idx))));Note that we also added a suitable precondition to protect against possible buffer overflows, so that proof with SPARK would allow us to guarantee that no such buffer overflow can ever happen. The above contract is a simple one, that could be expressed directly in terms of the subprogram parameters. Subprograms that deal with the file system cannot be directly specified in this way. So instead we defined a ghost variable The_File to represent the file being read, and a ghost variable Cur_Position to represent the current position being read in this file:
The_File : String (Positive) with Ghost;
Cur_Position : Positive := 1 with Ghost;We could then define the functional contract of the low-level functions interacting with the file system in terms of their effect on these ghost variables. For example, here is the contract of procedure Fgetc which reads a character from a file (we used a procedure instead of a function in order to be able to update ghost variable Cur_Position in the call, something not allowed in SPARK functions):
procedure Fgetc (Stream : File_Descr; Result : out Int) with
Global => (Proof_In => The_File, In_Out => Cur_Position),
Post => (if The_File (Cur_Position'Old) = EOF_Ch then
Cur_Position = Cur_Position'Old and then
Result = EOF
elsif The_File (Cur_Position'Old) = ASCII.LF then
Cur_Position = Cur_Position'Old and then
Result = Character'Pos (ASCII.LF)
else
Cur_Position = Cur_Position'Old + 1 and then
Result = Character'Pos (The_File (Cur_Position'Old)));It says that Cur_Position is incremented unless newline or end-of-file is reached, and that the Result integer returned is the special EOF value for end-of-file, or the integer matching the position of the character otherwise. The most involved contract is the one of Fgets, which gets multiple characters at a time. Here is what the documentation for function fgets says:
The fgets() function reads at most one less than the number of characters specified by size from the given stream and stores them in the string str. Reading stops when a newline character is found, at end-of-file or error. The newline, if any, is retained. If any characters are read and there is no error, a `\0' character is appended to end the string.
Upon successful completion, fgets() returns a pointer to the string. If end-of-file occurs before any characters are read, it returns NULL and the buffer contents remain unchanged. If an error occurs, it returns NULL and the buffer contents are indeterminate.
We transformed it into a procedure in SPARK, so that it can update ghost variable Cur_Position. Here is the contract we wrote to express the informal specification above:
procedure Fgets
(Strng : in out String;
N : Natural;
Stream : File_Descr;
Success : out Boolean)
with
Global => (Proof_In => The_File, In_Out => Cur_Position),
Post => (if Success then
-- Success means no error and no empty file
(Ferror (Stream) = 0 and then Fpeek (Stream)'Old /= EOF) and then
-- Case 1: no EOF nor newline character found
-- N-1 characters are copied to Strng. Nul character is appended.
-- Previous characters in Strng are preserved beyond the Nth character.
-- Cur_Position advances N-1 characters.
(if No_Char_In_Slice (ASCII.LF, Cur_Position'Old, Cur_Position'Old + N - 2)
and then
No_Char_In_Slice (EOF_Ch, Cur_Position'Old, Cur_Position'Old + N - 2)
then
Cur_Position = Cur_Position'Old + N - 1 and then
(for all Idx in 1 .. N - 1 =>
Strng (Idx) = The_File (Cur_Position'Old + Idx - 1)) and then
Strng (N) = ASCII.NUL and then
(for all Idx in N + 1 .. Strng'Last =>
Strng (Idx) = Strng'Old (Idx))
-- Case 2: newline character is found
-- Characters up to the newline are copied to Strng. Nul character is
-- appended. Previous characters in Strng are preserved beyond the nul
-- character. Cur_Position advances to the position of the newline
-- character.
elsif Has_Char_In_Slice (ASCII.LF, Cur_Position'Old, Cur_Position'Old + N - 2)
and then
No_Char_In_Slice (EOF_Ch, Cur_Position'Old, Cur_Position'Old + N - 2)
then
declare LF_Pos = Find_Char_In_Slice (ASCII.LF, Cur_Position'Old, Cur_Position'Old + N - 2) in
Cur_Position = LF_Pos and then
(for all Idx in Cur_Position'Old .. LF_Pos - 1 =>
Strng (Idx - Cur_Position'Old + 1) = The_File (Idx)) and then
Strng (LF_Pos - Cur_Position'Old + 1) = ASCII.LF and then
Strng (LF_Pos - Cur_Position'Old + 2) = ASCII.NUL and then
(for all Idx in LF_Pos - Cur_Position'Old + 3 .. Strng'Last =>
Strng (Idx) = Strng'Old (Idx))
-- Case 3: EOF is found
-- Characters prior to EOF are copied to Strng. Nul character is
-- appended. Previous characters in Strng are preserved beyond the nul
-- character. Cur_Position advances to the position of EOF.
elsif No_Char_In_Slice (ASCII.LF, Cur_Position'Old, Cur_Position'Old + N - 2)
and then
Has_Char_In_Slice (EOF_Ch, Cur_Position'Old, Cur_Position'Old + N - 2)
then
declare EOF_Pos = Find_Char_In_Slice (EOF_Ch, Cur_Position'Old, Cur_Position'Old + N - 2) in
Cur_Position = EOF_Pos and then
(for all Idx in Cur_Position'Old .. EOF_Pos - 1 =>
Strng (Idx - Cur_Position'Old + 1) = The_File (Idx)) and then
Strng (EOF_Pos - Cur_Position'Old + 1) = ASCII.NUL and then
(for all Idx in EOF_Pos - Cur_Position'Old + 2 .. Strng'Last =>
Strng (Idx) = Strng'Old (Idx)) and then
-- redundant proposition to help automatic provers
No_Char_In_String (Strng, ASCII.LF, EOF_Pos - Cur_Position'Old + 1)
-- Case 4: both newline and EOF appear
-- In our model, we choose that this cannot occur. So we consider only
-- cases where EOF or newline character are repeated after the first
-- occurrence in the file.
else False)
-- Failure corresponds to those cases where low-level fgets
-- returns a NULL pointer: an error was issued, or the file is
-- empty. In the last case Cur_Position is not modified.
else
(Ferror (Stream) /= 0 or else
(Fpeek (Stream)'Old = EOF and then Cur_Position = Cur_Position'Old)));Wow! Not so bad for a simple low-level function everyone uses without paying so much attention. But the contract is actually quite straighforward, if you care to look at it in details. If you do so, you'll realize I've displayed it here using a declare-var-in-expr construct that is not yet available in Ada, but will hopefully be in the next version of the language. It comes handy to make the contract readable here, so I'm using it just for this blog post (not in the actual code).
What's left? Well, we should write the contract we'd like to verify for Get_Line:
procedure Get_Line
(File : in out File_Type;
Item : out String;
Last : out Natural)
with
Global => (Input => (EOF, EOF_Ch, The_File), In_Out => (Cur_Position)),
-- It is an error to call Get_Line on an empty file
Pre => not End_Of_File (File),
Contract_Cases =>
-- If Item is empty, return Item'First - 1 in Last
(Item'Last < Item'First =>
Last = Item'First - 1,
-- Otherwise, return in Last the length of the string copied, which
-- may be filling Item, or up to EOF or newline character.
others =>
(Last = Item'First - 1 or Last in Item'Range) and then
(for all Idx in Item'First .. Last =>
Item (Idx) = The_File (Idx - Item'First + Cur_Position'Old)) and then
Cur_Position = Cur_Position'Old + Last - Item'First + 1 and then
(Last = Item'Last or else
The_File (Cur_Position) = EOF_Ch or else
The_File (Cur_Position) = ASCII.LF));And now, let's run GNATprove! I'm taking a bit of a shortcut here, as there are other intermediate subprograms that need contracts, and loops that require loop invariants, for the proof to be performed automatically by GNATprove. But in the process of interacting with GNATprove to get 100% proof, we discovered two other bugs in the implementation of our trusted Get_Line!
- One test "K + 2 > Buf'Last" was incorrect, and needed to be fixed as "K + 2 > N". This caused an incorrect value to be returned for the number of characters read in some cases.
- The case where Item is empty was incorrectly handled, so that Last was left uninitialized instead of being set to Item'First prior to returning.
Epilogue
After fixing the two bugs mentioned above, we were able to formally prove with SPARK that Get_Line implemented its contract. Well, a slightly simplified version of Get_Line, where we removed the logic around page marks. As an additional verification, we also wrote an implementation of the low-level functions memcpy, memset, fgets, etc. in terms of their effect on the model of ghost variable The_File and Cur_Position. This allowed us to test the not-so-simple contracts on imported low-level functions, to gain better confidence about their correctness.
Overall, we started with a trusted piece of code that had worked for many years, and we ended up fixing 3 bugs in it. The initial bug was present since the first implementation of the function (not the procedure) Get_Line in 2005. The last two bugs were introduced by a faulty change in 2010, when changing the implementation of Get_Line to use fgets instead of fgetc to speed up the function. Interestingly, the comment for this patch said "No change in behavior and good coverage already, so no test case required." And indeed, it's unlikely that testing would have allowed detecting these bugs. Manual review by compiler experts did not find those bugs either. Only formal verification with SPARK allowed us to pinpoint quickly the places where the logic was subtly flawed.
[Cover image by Rama - Own work, CC BY-SA 2.0 fr, https://commons.wikimedia.org/w/index.php?curid=28...]
About Yannick Moy
Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.