\myheading{My homebrew algorithms formally verified using CBMC}
\label{KMP1}

\leveldown{}

\myheading{Searching for the "ok" substring}

Imagine you want to find an "ok" substring within a string. You would do:

\begin{lstlisting}[style=customc]
unsigned search_ok_1 (char *s, unsigned len)
{
        if (len<2)
                return len;       // not found
        for (unsigned i=0; i<len-1; i++)
        {
                if (s[i]=='o' && s[i+1]=='k')
                        return i; // found
        };
        return len;               // not found
};
\end{lstlisting}

You see, there are two (cache-)memory accesses per one character of the input string (at average).
Hence, the total number of all (cache-)memory accesses can be len*2 at worst.

Is it possible to reduce that number? Yes. In the following example, we have only one single memory access per character:

\begin{lstlisting}[style=customc]
unsigned search_ok_2 (char *s, unsigned len)
{
        if (len<2)
                return len;           // not found
        bool seen_o=false;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];         // this is single read operation
                if (ch=='o')
                        seen_o=true;
                else if (seen_o && ch=='k')
                        return i-1;   // found
                else
                        seen_o=false; // reset
        };
        return len; // not found
};
\end{lstlisting}

\myheading{Searching for the "eel" substring, verification using CBMC}

Can we extend that method to any 3-character strings? Let's write a function that searches for the 'eel' string
\footnote{For non-English speakers: this is indeed a word. \href{https://en.wikipedia.org/wiki/Eel}{Some kind of fish}.}

We will use the 'seen' variable, reflecting, how many characters of the sought string we've already seen:

\begin{lstlisting}[style=customc]
unsigned search_eel (char *s, unsigned len)
{
        if (len<3)
                return len;         // not found
        unsigned seen=0;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];       // this is single read operation
                if (seen==0 && ch=='e')
                        seen=1;
                else if (seen==1 && ch=='e')
                        seen=2;
                else if (seen==2 && ch=='l')
                        return i-2; // found
                else
                        seen=0;     // reset
        }
        return len;                 // not found
};
\end{lstlisting}

But this implementation has a bug.
To find it, I'll use CBMC, the excellent tool, that can verify if a C function is equivalent to another function.

This is like Test-driven development (TDD).

I'll add a 'reference' (though, slow) function, but always correct:

\begin{lstlisting}[style=customc]
unsigned search_eel_brute (char *s, unsigned len)
{
        if (len<3)
                return len; // not found
        for (unsigned i=0; i<len-2; i++)
        {
                if (s[i]=='e' && s[i+1]=='e' && s[i+2]=='l')
                        return i;
        };
        return len; // not found
};

...

void check()
{
        unsigned len=LEN;
        char s[len];
        __CPROVER_assert (search_eel_brute(s, len)==search_eel(s, len), "assert");
};
\end{lstlisting}

\begin{lstlisting}
% cbmc --trace --function check -DLEN=4 kmp_eel2.c
...

** Results:
[check.assertion.1] assert: FAILURE

Trace for check.assertion.1:

...

State 21 file kmp_eel2.c line 41 function check thread 0
----------------------------------------------------
  s={ 'e', 'e', 'e', 'l' } ({ 01100101, 01100101, 01100101, 01101100 })
...
\end{lstlisting}

It failed for the string "eeel".
After some thinking, we can find a problem.
If a third character isn't 'l', but 'e', we are in the middle of a long string of 'e' characters.
So if seen==2 and the input character isn't 'l', but 'e', we shouldn't advance the 'seen' variable:

\begin{lstlisting}[style=customc]
...
                if (seen==0 && ch=='e')
                        seen=1;
                else if (seen==1 && ch=='e')
                        seen=2;
                else if (seen==2 && ch=='l')
                        return i-2;           // found
                else if (seen==2 && ch=='e')  // fix
                        seen=2;               // fix
                else
                        seen=0;               // reset
...
\end{lstlisting}

Now the verification is successful up to strings of length 15:

\begin{lstlisting}
#!/bin/bash
for i in $( seq 0 15 ); do
    #echo $i
    cbmc --trace --function check -DLEN=$i kmp_eel2.c
done
\end{lstlisting}

Searching for the "cocos" substring, verification using CBMC

The "cocos" substring is much more problematic.
But fixing it with the help of CBMC is a great programming exercise.

\begin{lstlisting}[style=customc]
unsigned search_cocos_brute (char *s, unsigned len)
{
        if (len<5)
                return len;       // not found
        for (unsigned i=0; i<len-4; i++)
        {
                if (s[i]=='c' &&
                                s[i+1]=='o' &&
                                s[i+2]=='c' &&
                                s[i+3]=='o' &&
                                s[i+4]=='s')
                        return i; // found
        };
        return len;               // not found
};

unsigned search_cocos_naive (char *s, unsigned len)
{
        if (len<5)
                return len;          // not found
        unsigned seen=0;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];        // this is single read operation
                if (seen==0 && ch=='c')
                        seen=1;
                else if (seen==1 && ch=='o')
                        seen=2;
                else if (seen==2 && ch=='c')
                        seen=3;
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else
                        seen=0;      // reset
        }
        return len;                  // not found
};

void check()
{
        unsigned len=LEN;
        char s[len];
        __CPROVER_assert (search_cocos_brute(s, len)==search_cocos_naive(s, len), "assert");
};
\end{lstlisting}

This is the first bug:

\begin{lstlisting}
% cbmc --trace --function check -DLEN=6 kmp_cocos.c
...
** Results:
[check.assertion.1] assert: FAILURE

Trace for check.assertion.1:

...

State 21 file kmp_cocos.c line 47 function check thread 0
----------------------------------------------------
  s={ 'c', 'c', 'o', 'c', 'o', 's' } ({ 01100011, 01100011, 01101111, 01100011, 01101111, 01110011 })

...
\end{lstlisting}

A test failed for the "ccocos" string.

Here is the fix: if the first 'c' is repeating, we shouldn't advance the 'seen' variable:

\begin{lstlisting}[style=customc]
                if (seen==0 && ch=='c')
                        seen=1;
                else if (seen==1 && ch=='o')
                        seen=2;
                else if (seen==1 && ch!='o')
                {
                                     // we can be here if the input is 'ccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0;
                }
                else if (seen==2 && ch=='c')
                        seen=3;
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else
                        seen=0;      // reset
\end{lstlisting}

CBMC can verify this function for all 6-character strings, OK.
But it can find problematic 7-character string:

\begin{lstlisting}
% cbmc --trace --function check -DLEN=7 kmp_cocos.c
...
** Results:
[check.assertion.1] assert: FAILURE

Trace for check.assertion.1:

...
State 21 file kmp_cocos.c line 79 function check thread 0
----------------------------------------------------
  s={ 'c', 'o', 'c', 'o', 'c', 'o', 's' } ({ 01100011, 01101111, 01100011, 01101111, 01100011, 01101111, 01110011 })
...
\end{lstlisting}

That is, "cococos".

And this is my fix:

\begin{lstlisting}[style=customc]
...
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else if (seen==4 && ch!='s')
                {
                        // the input string is 'cocoX' where X is not 's'
                        // (current state of ch='X')
                        // but 'X' could be 'c' if the input string is 'cococos'
                        if (ch=='c')
                        {
                                // if the string is 'cococos',
                                // we can say that we have already seen the 'coc' part of it:
                                seen=3;
                        }
                        else
                        {
                                // 'X' is not 'c', so reset
                                seen=0;
                        };
                }
                else
                        seen=0;      // reset
...
\end{lstlisting}

Now all 7-characters strings can be tested without a fail.
But not 8-character ones:

\begin{lstlisting}
% cbmc --trace --function check -DLEN=8 kmp_cocos.c
...

** Results:
[check.assertion.1] assert: FAILURE

Trace for check.assertion.1:

...

State 21 file kmp_cocos.c line 96 function check thread 0
----------------------------------------------------
  s={ 'c', 'o', 'c', 'c', 'o', 'c', 'o', 's' } ({ 01100011, 01101111, 01100011, 01100011, 01101111, 01100011, 01101111, 01110011 })

...
\end{lstlisting}

It fails with "coccocos".
We have to add another check for the repeating second 'c' character.

\begin{lstlisting}[style=customc]
...
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==3 && ch!='o')
                {
                        // if input='coccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0; // reset
                }
                else if (seen==4 && ch=='s')
...
\end{lstlisting}

Now CBMC can check it all up to 15-character strings. The whole fixed function is:

\begin{lstlisting}[style=customc]
unsigned search_cocos_fixed (char *s, unsigned len)
{
        if (len<5)
                return len;          // not found
        unsigned seen=0;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];        // this is single read operation
                if (seen==0 && ch=='c')
                        seen=1;
                else if (seen==1 && ch=='o')
                        seen=2;
                else if (seen==1 && ch!='o')
                {
                                     // we can be here if the input is 'ccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0;
                }
                else if (seen==2 && ch=='c')
                        seen=3;
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==3 && ch!='o')
                {
                        // if input='coccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0; // reset
                }
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else if (seen==4 && ch!='s')
                {
                        // the input string is 'cocoX' where X is not 's'
                        // (current state of ch='X')
                        // but 'X' could be 'c' if the input string is 'cococos'
                        if (ch=='c')
                        {
                                // if the string is 'cococos',
                                // we can say that we have already seen the 'coc' part of it:
                                seen=3;
                        }
                        else
                        {
                                // 'X' is not 'c', so reset
                                seen=0;
                        };
                }
                else
                        seen=0;      // reset
        }
        return len;                  // not found
};
\end{lstlisting}

It is capable of searching for the 'cocos' substring reading each character of the input string only once,
and it is formally verified by CBMC.

Code like that is very hard to test
(can you execute these functions with all 15-characters input strings?),
but thanks to CBMC, we can be sure it's correct, or at least, equivalent to the simple 'bruteforce' version.
I couldn't devise a correct version without it. 
In fact first versions were written in Python.
I rewritten it to pure C so that I can verify them using CBMC.

\myheading{All the files used}

\url{\RepoURL/\CURPATH/files_1}

\myheading{But what about bruteforce?}

Naive way of testing would be feeding all possible 15-character strings, that is: $256^{15}$ test strings.
But you can probably use only characters that are present in a substring: 'c', 'o', 's' for 'cocos', plus a character acting
as \textit{everything else}, say, '\_'.
That would result in $4^{15}=1,073,741,824$ test strings.
Yes, it's possible.

\levelup{}