Applied Formal Logic: Searching in Strings

by Yannick Moy in Dev Projects, Formal Verification – June 29, 2017

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.

Contrary to strings in C which start at index 0, standard strings in SPARK range over positive numbers, and usually start at index 1. I could have made my own strings to start at index 0, but there is no reason to stick to C convention when writing the algorithm in SPARK. At the same time, it's convenient to force the string to start at index 1 with an explicit predicate, which I do like that:

   subtype Text is String with Predicate => Text'First = 1;

Following the order of exposure of Tommy M. McGuire's posts, here is the implementation for the brute force algorithm in SPARK:

   function Brute_Force (Needle, Haystack : in Text) return Natural is
      Diff : Boolean;
   begin
      for I in 1 .. Haystack'Length - Needle'Length + 1 loop
         Diff := False;

         for J in Needle'Range loop
            Diff := Needle(J) /= Haystack(J + (I - 1));
            exit when Diff;
         end loop;

         if not Diff then
            return I;
         end if;
      end loop;

      return 0;
   end Brute_Force;

I am doing here without the parameters n and h which were used in the C version to denote the length of strings needle and haystack, since these are readily available as attributes Haystack'Length and Needle'Length in SPARK. Since I'm working on strings starting at index 1, there are a few adjustments compared to the C version. The use of a temporary variable Diff is needed to detect that the inner loop was exited due to a difference between Needle and the portion of Haystack starting at J, as the for-loop in SPARK does not increment its index in the last iteration of the loop, contrary to its C version.

On this initial version, GNATprove issues one message about a possible integer overflow when computing "Haystack'Length - Needle'Length + 1". It automatically proves all other run-time checks (2 initialization checks, 1 array index check,  2 integer range checks, 2 integer overflow checks). GNATprove also provides a counterexample to understand the possible failure, which can be displayed in our IDE GPS by clicking on the magnify icon on the left of the message/line:

Counterexample displayed by GPS on Brute_Force

You have to scroll right in the IDE to see all the values, so here are the relevant ones: Haystack'First = 1 and Haystack'Last = 2147483647 and Needle'First = 1 and Needle'Last = 0. In that case, Haystack'Length is 2147483647 and Needle'Length is 0, which means that "Haystack'Length - Needle'Length + 1" is one past the largest signed 32-bits integer. Hence the overflow. One way to avoid this issue is to require that Needle is not the empty string, so its length is at least 1:

   function Brute_Force (Needle, Haystack : in Text) return Natural with
     Pre => Needle'Length >= 1;

This precondition is sufficient for GNATprove to prove all checks in Brute_Force, but I've made it stronger like done by TMM in his post, as it does not make sense to look for a needle that is longer than the haystack:

   function Brute_Force (Needle, Haystack : in Text) return Natural with
     Pre => Needle'Length in 1 .. Haystack'Length;

Note that, compared to what is needed with Frama-C, we don't need here to provide loop assigns or loop invariants. GNATprove automatically computes the variables that are modified in a loop, as well as the range of for-loop indexes. Still following the order of exposure of TMM's posts, let's turn to the functional contract for searching a string. I'm directly translating here the functions partial_match_at and match_at given by TMM from C to SPARK, as well as the contract of brute_force. Functions Partial_Match_At and Match_At are ghost functions in SPARK (with aspect Ghost), which means that they can be used only in assertions/contracts and ghost code. A difference with Frama-C is that ghost code is executable like regular code in SPARK, so one must show absence of run-time errors in ghost code as well, hence the precondition on Partial_Match_At below:

   --  There is a partial match of the needle at location loc in the
   --  haystack, of length len.
   function Partial_Match_At
     (Needle, Haystack : Text; Loc : Positive; Len : Natural) return Boolean
   is
     (for all I in 1 .. Len => Needle(I) = Haystack(Loc + (I - 1)))
   with Ghost,
        Pre => Len <= Needle'Length
          and then Loc - 1 <= Haystack'Length - Len;

   --  There is a complete match of the needle at location loc in the
   --  haystack.
   function Match_At (Needle, Haystack : Text; Loc : Positive) return Boolean is
     (Loc - 1 <= Haystack'Length - Needle'Length
      and then Partial_Match_At (Needle, Haystack, Loc, Needle'Length))
   with Ghost;

The contract on Brute_Force is similar to the one in Frama-C, with a shift by one for the origin of strings, Brute_Force'Result instead of \result to denote the result of the function, and an if-expression instead of behaviors (SPARK has a similar notion of contract cases, but they must always have disjoint guards in SPARK, so are not applicable here):

   function Brute_Force (Needle, Haystack : in Text) return Natural with
     Pre  => Needle'Length in 1 .. Haystack'Length,
     Post => Brute_Force'Result in 0 .. Haystack'Length - Needle'Length + 1
       and then
       (if Brute_Force'Result > 0 then
          Match_At (Needle, Haystack, Brute_Force'Result)
        else
          (for all K in Haystack'Range =>
             not Match_At (Needle, Haystack, K)));

Before we even try to prove that this contract is satisfied by the implementation of Brute_Force, it is a good idea to test it on a few inputs, to get rid of silly mistakes. Here is a test driver to do precisely that:

with String_Search; use String_Search;

procedure Test_Search is
   All_Men : constant Text :=
     "We hold these truths to be self-evident, that all men are created equal,"
     & " that they are endowed by their Creator with certain unalienable "
     & "Rights, that among these are Life, Liberty and the Pursuit of "
     & "Happiness. That to secure these rights, Governments are instituted "
     & "among Men, deriving their just powers from the consent of the governed";
begin
   pragma Assert (Brute_Force (All_Men, "just powers") > 0);
   pragma Assert (Brute_Force (All_Men, "austin powers") = 0);
end Test_Search;

Just compile the code with assertions on (switch -gnata), run it, and... it fails the precondition of Brute_Force:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from string_search.ads:24

What happened here is that I put arguments in the wrong order in the call to Brute_Force. I'm not making this up, this really happened to me (I am that bad!). Anyway, that illustrates that testing is a good idea, even if here it detected a bug in the test itself. The fix in SPARK is to use named parameters to avoid such issues. They don't have to appear in the same order as in the function signature, but it's a good idea nonetheless:

   pragma Assert (Brute_Force (Needle => "just powers", Haystack => All_Men) > 0);

Once fixed, the test passes without errors. Like in the case of Frama-C, we need to add loop invariants for GNATprove to prove that Brute_Force satisfies its contract. Loop invariants in SPARK are different from the classical loop invariants used in Frama-C: you can put them anywhere in the loop, and they don't have to hold when reaching/exiting the loop but only when execution reaches the program point of the loop invariant. I prefer in general to put loop invariants at the end of loops, because it's more natural to express what has been achieved so far:

   function Brute_Force (Needle, Haystack : in Text) return Natural is
      Diff : Boolean;
   begin
      for I in 1 .. Haystack'Length - Needle'Length + 1 loop
         Diff := False;

         for J in Needle'Range loop
            Diff := Needle(J) /= Haystack(J + (I - 1));
            exit when Diff;
            pragma Loop_Invariant (Partial_Match_At (Needle, Haystack, I, J));
            pragma Loop_Invariant (Diff = (Needle(J) /= Haystack(J + (I - 1))));
         end loop;

         if not Diff then
            return I;
         end if;

         pragma Loop_Invariant
           (for all K in 1 .. I => not Match_At (Needle, Haystack, K));
      end loop;

      return 0;
   end Brute_Force;

A subtlety above is that, since we're replacing the implicit loop invariant in the inner loop (located at the start of the loop) by an explicit loop invariant at the end of the inner loop, we need to repeat in that loop invariant the information about the current value of Diff, otherwise this information is not available on the path starting from the loop invariant and exiting the loop in the last iteration. Otherwise this is similar to what was done in Frama-C. With these loop invariants, GNATprove proves all checks in Brute_Force, including its postcondition.

I kept above the implementation structure originating from the C version of brute_force, but in SPARK we can simplify it by replacing the inner loop with a direct comparison of Needle with a slice of Haystack:

   function Brute_Force (Needle, Haystack : in Text) return Natural is
   begin
      for I in 1 .. Haystack'Length - Needle'Length + 1 loop
         if Needle = Haystack(I .. I + (Needle'Last - 1)) then
            return I;
         end if;

         pragma Loop_Invariant
           (for all K in 1 .. I => not Match_At (Needle, Haystack, K));
      end loop;

      return 0;
   end Brute_Force;

This version is also completely proved by GNATprove.

Now turning to the more involved algorithm for string search called quick search presented in this other post by TMM. Translating the implementation, contracts and loop invariants in SPARK is quite easy. As for the brute force version, more precise types in SPARK allow to get rid of a number of annotations:

   type Shift_Table is array (Character) of Positive;

   procedure Make_Bad_Shift (Needle : Text; Bad_Shift : out Shift_Table) with
     Pre  => Needle'Length < Integer'Last,
     Post => (for all C in Character => Bad_Shift(C) in 1 .. Needle'Length + 1);

   function QS (Needle, Haystack : in Text) return Natural with
     Pre => Needle'Length < Integer'Last
       and then Haystack'Length < Integer'Last - 1
       and then Needle'Length in 1 .. Haystack'Length;

I am also getting rid of a loop in Make_Bad_Shift and a loop in QS compared to their C version, as we can directly assign and compare strings in SPARK:

   procedure Make_Bad_Shift (Needle : Text; Bad_Shift : out Shift_Table) is
   begin
      Bad_Shift := (others => Needle'Length + 1);

      for J in Needle'Range loop
         Bad_Shift(Needle(J)) := Needle'Length - J + 1;
         pragma Loop_Invariant (for all C in Character => Bad_Shift(C) in 1 .. Needle'Length + 1);
      end loop;
   end Make_Bad_Shift;

   function QS (Needle, Haystack : in Text) return Natural is
      Bad_Shift : Shift_Table;
      I : Positive;

   begin
      --  Preprocessing
      Make_Bad_Shift (Needle, Bad_Shift);

      --  Searching
      I := 1;
      while I <= Haystack'Length - Needle'Length + 1 loop
         if Needle = Haystack(I .. I + (Needle'Last - 1)) then
            return I;
         end if;
         I := I + Bad_Shift(Haystack(I + Needle'Length));  --  Shift
      end loop;

      return 0;
   end QS;

GNATprove proves all checks on the above code, including postconditions, except for the array index check when computing "Haystack(I + Needle'Length)". This is precisly the bug that was discovered by TMM, that he presents in his post. GNATprove further helps by providing a counterexample to understand the possible failure:

Counterexample displayed by GPS on QS

Indeed, when I=2 and Haystack'Last=2, "I + Needle'Length" is outside of the bounds of Haystack whenever Needle is not the empty string. We can fix that by exiting early from the loop before the assignment to I in the loop:

         exit when I = Haystack'Length - Needle'Length + 1;

With this fix, GNATprove proves all checks on the code of quick search.

Now turning to proving the functional behavior of quick search. The postcondition of QS is the same as the one of Brute_Force, given that only the algorithm changes between the two:

   function QS (Needle, Haystack : in Text) return Natural with
     Pre => Needle'Length < Integer'Last
       and then Haystack'Length < Integer'Last - 1
       and then Needle'Length in 1 .. Haystack'Length,
     Post => QS'Result in 0 .. Haystack'Length - Needle'Length + 1
       and then
       (if QS'Result > 0 then
          Match_At (Needle, Haystack, QS'Result)
        else
          (for all K in Haystack'Range =>
             not Match_At (Needle, Haystack, K)));

In order to prove the contract of QS, we'll need to specify and prove the functional behavior of Make_Bad_Shift first. As explained by TMM in his post, Make_Bad_Shift is used to align the last instance of a given character in the needle with a matching character in the haystack. So for every such character C, either it does not occur in the needle in which case Bad_Shift(C) has the value "Needle'Length + 1", or it occurs (possibly multiple times) in the needle in which case it occurs last at index "Needle'Length - Bad_Shift(C) + 1". This is what is expressed in the following postcondition:

   procedure Make_Bad_Shift (Needle : Text; Bad_Shift : out Shift_Table) with
     Pre  => Needle'Length < Integer'Last,
     Post => (for all C in Character => Bad_Shift(C) in 1 .. Needle'Length + 1)
       and then (for all C in Character =>
                   (if Bad_Shift(C) = Needle'Length + 1 then
                      (for all K in Needle'Range => C /= Needle(K))
                    else
                      Needle(Needle'Length - Bad_Shift(C) + 1) = C
                      and (for all K in Needle'Length - Bad_Shift(C) + 2 .. Needle'Last => Needle(K) /= C)
                 ));

In order to prove that the implementation of Make_Bad_Shift satisfies this postcondition, we simply have to repeat this postcondition as a loop invariant, accumulating that information as the loop index J progresses (see how occurrences of Needle'Last in the postcondition were replaced by occurrences of J in the loop invariant):

   procedure Make_Bad_Shift (Needle : Text; Bad_Shift : out Shift_Table) is
   begin
      Bad_Shift := (others => Needle'Length + 1);

      for J in Needle'Range loop
         Bad_Shift(Needle(J)) := Needle'Length - J + 1;
         pragma Loop_Invariant (for all C in Character => Bad_Shift(C) in 1 .. Needle'Length + 1);
         pragma Loop_Invariant (for all C in Character =>
                                  (if Bad_Shift(C) = Needle'Length + 1 then
                                     (for all K in 1 .. J => C /= Needle(K))
                                   else
                                      Needle(Needle'Length - Bad_Shift(C) + 1) = C
                                      and (for all K in Needle'Length - Bad_Shift(C) + 2 .. J => Needle(K) /= C)
                                ));
      end loop;
   end Make_Bad_Shift;

GNATprove proves all checks on the above code.

Now turning to QS, we need to establish a loop invariant very similar to the one used in Brute_Force, except here we want to establish the property that Needle does not match up to index "I + Bad_Shift(Haystack(I + Needle'Length)) - 1" instead of just I:

         pragma Loop_Invariant
           (for all K in 1 .. I + Bad_Shift(Haystack(I + Needle'Length)) - 1 => not Match_At (Needle, Haystack, K));

We also need to bound I in the loop invariant, as we're inserting the above loop invariant in the middle of the loop, hence we do not get "for free" that I satisfies the loop test:

         pragma Loop_Invariant (I <= Haystack'Length - Needle'Length);

With these additions, GNATprove proves all checks in QS, including its postcondition, but it does not prove its loop invariant:

string_search.adb:111:81: medium: loop invariant might fail after first iteration, cannot prove not Match_At (Needle, Haystack, K) (e.g. when Haystack = (0 => 'NUL', 5 => 'NUL', others => 'SOH') and Haystack'First = 1 and Haystack'Last = 6 and I = 4 and K = 5 and Needle = (0 => 'SOH', 3 => 'SOH', 4 => 'SOH', 6 => 'SOH', others => 'NUL') and Needle'First = 1 and Needle'Last = 2)
string_search.adb:111:81: medium: loop invariant might fail in first iteration, cannot prove not Match_At (Needle, Haystack, K) (e.g. when Haystack = (0 => 'NUL', 2 => 'NUL', others => 'SOH') and Haystack'First = 1 and Haystack'Last = 3 and I = 1 and K = 2 and Needle = (0 => 'SOH', 3 => 'SOH', others => 'NUL') and Needle'First = 1 and Needle'Last = 2)

This is expected. There is a big reasoning gap to go from the postcondition of Make_Bad_Shift to the loop invariant in QS. We are going to use ghost code to close that gap and convince GNATprove that the loop invariant holds in every iteration. What we need to show is that, for every starting position that is skipped (for K in the range I + 1 to I + Bad_Shift(Haystack(I + Needle'Length)) - 1), the needle cannot align with the haystack at that position. In fact, we know exactly at which position these alignments would fail: at the position "I + Needle'Length" in Haystack. Looking at the postcondition of Make_Bad_Shift, this corresponds to position "I + Needle'Length - K + 1" in Needle. Let's write it down just before the loop invariant:

         for K in I + 1 .. I + Bad_Shift(Haystack(I + Needle'Length)) - 1 loop
            pragma Assert (Haystack(I + Needle'Length) /= Needle(I + Needle'Length - K + 1));
            pragma Assert (not Match_At (Needle, Haystack, K));
         end loop;

GNATprove proves the above assertions, using the first one to prove the second one, so we can now accumulate this information in a loop invariant for all values of positions that are skipped:

         for K in I + 1 .. I + Bad_Shift(Haystack(I + Needle'Length)) - 1 loop
            pragma Assert (Haystack(I + Needle'Length) /= Needle(I + Needle'Length - K + 1));
            pragma Loop_Invariant
              (for all L in 1 .. K => not Match_At (Needle, Haystack, L));
         end loop;

With this addition of ghost code, GNATprove proves all checks in QS, including its postcondition and loop invariants. In the final version of that code, I'm using a local ghost procedure Prove_QS instead of inlining the ghost code in the implementation of QS. That way, GNATprove still internally inlines the implementation of Prove_QS to prove QS, but the compiler will completely get rid of the body and call to Prove_QS in the final executable built without assertions:

   function QS (Needle, Haystack : in Text) return Natural is
      Bad_Shift : Shift_Table;
      I : Positive;

      procedure Prove_QS with Ghost is
         Shift : constant Positive := Bad_Shift(Haystack(I + Needle'Length));
      begin
         for K in I + 1 .. I + Shift - 1 loop
            pragma Assert (Haystack(I + Needle'Length) /= Needle(I + Needle'Length - K + 1));
            pragma Loop_Invariant
              (for all L in 1 .. K => not Match_At (Needle, Haystack, L));
         end loop;
      end Prove_QS;

   begin
      --  Preprocessing
      Make_Bad_Shift (Needle, Bad_Shift);

      --  Searching
      I := 1;
      while I <= Haystack'Length - Needle'Length + 1 loop
         if Needle = Haystack(I .. I + (Needle'Last - 1)) then
            return I;
         end if;
         exit when I = Haystack'Length - Needle'Length + 1;

         Prove_QS;

         pragma Loop_Variant (Increases => I);
         pragma Loop_Invariant (I <= Haystack'Length - Needle'Length);
         pragma Loop_Invariant
           (for all K in 1 .. I + Bad_Shift(Haystack(I + Needle'Length)) - 1 => not Match_At (Needle, Haystack, K));

         I := I + Bad_Shift(Haystack(I + Needle'Length));  --  Shift
      end loop;

      return 0;
   end QS;

I also added a loop variant to ensure that the while-loop will terminate. For-loops always terminate in SPARK because the loop index cannot be assigned by the user (contrary to what C allows), but while-loops or plain-loops might not terminate, hence the use of a loop variant to verify their termination.

The code presented in this post is available on GitHub: spec and body. Now a challenge for Frama-C users is to translate back the functional proof of QS in SPARK into C and Frama-C!

The project SPARK-by-Example by Christophe Garion and Jérôme Hugues contains other examples of functionally proven string algorithms, which correspond to the SPARK version of the work done by Jens Gerlach with Frama-C in the ACSL-by-Example project.
 

comments powered by Disqus