Frama-C anagram function behavior verification

I wrote a C function that checks if two given strings (C-style) are anagrams or not. I try to verify it with Frama-C but it cannot validate the final behaviors of the function (other specifications are valid). The first one goes to timeout (even with very high timeout values in WP) and the second is unknown.

Here is the code:

    #include <string.h>
//@ ghost char alphabet[26] = {'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z'};

/*@
    // Takes a character and return it to lowercase if it's uppercase
    axiomatic ToLower
    {
        logic char to_lower(char c);

        axiom lowercase:
            \forall char c; 97 <= c <= 122 ==> to_lower(c) == c;

        axiom uppercase:
            \forall char c; 65 <= c <= 90 ==> to_lower(c) == to_lower((char) (c+32));
    }
*/
/*@
    // Count the occurences of character 'c' into 'string' that is long 'n' characters
    axiomatic CountChar
    {
        logic integer count_char(char* string, integer n, char c);

        axiom count_zero:
            \forall char* string, integer n, char c; n <= 0 ==>
            count_char(string, n, c) == 0;

        axiom count_hit:
            \forall char* string, integer n, char c; n >= 0 && to_lower(string[n]) == c ==>
            count_char(string, n+1, c) == count_char(string, n, c) + 1;

        axiom count_miss:
            \forall char* string, integer n, char c; n >= 0 && to_lower(string[n]) != c ==>
            count_char(string, n+1, c) == count_char(string, n, c);
    }
*/

/*@
    predicate are_anagrams{L}(char* s1, char* s2) = ( \forall integer i; 0 <= i < 26 ==> 
    count_char(s1, strlen(s1), alphabet[i]) == count_char(s2, strlen(s2), alphabet[i]) );
*/

/*@
    requires valid_string(a);
    requires valid_string(b);

    // Requires that strings 'a' and 'b' are composed only by alphabet's letters and that are long equally.
    requires \forall integer k; 0 <= k < strlen(a) ==> 65 <= a[k] <= 90 || 97 <= a[k] <= 122;
    requires \forall integer k; 0 <= k < strlen(b) ==> 65 <= b[k] <= 90 || 97 <= b[k] <= 122;
    requires strlen(a) == strlen(b);

    ensures 0 <= \result <= 1;
    assigns \nothing;

    behavior anagrams:
    assumes are_anagrams(a, b);
    ensures \result == 1;
    behavior not_anagrams:
    assumes !are_anagrams(a, b);
    ensures \result == 0;
    complete behaviors anagrams, not_anagrams;
    disjoint behaviors anagrams, not_anagrams;
*/
int check_anagram(const char a[], const char b[])
{
   // Create two arrays and initialize them to zero
   int first[26];
   int second[26];
   int c;
   /*@
    loop assigns first[0..(c-1)];
    loop assigns second[0..(c-1)];
    loop assigns c; 
    loop invariant 0 <= c <= 26;
    loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
    loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
    loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
    loop variant 26-c;
   */
   for(c = 0; c < 26; c++)
   {
      first[c] = 0;
      second[c] = 0;
   }

   char tmp = 'a';
   c = 0;

   // Now increment the array position related to position of character occured in the alphabet, subtracting ASCII decimal value of character from the character.
   /*@
    loop assigns first[0..25];
    loop assigns tmp;
    loop assigns c;
    loop invariant 97 <= tmp <= 122;
    loop invariant \valid(first+(0..25));
    loop invariant strlen(\at(a, Pre)) == strlen(\at(a, Here));
    loop invariant 0 <= c <= strlen(a);
    loop variant strlen(a)-c;
   */
   while (a[c] != '\0')
   {
      // This is a little trick to lowercase if the char is uppercase.
      tmp = (a[c] > 64 && a[c] < 91) ? a[c]+32 : a[c];
      first[tmp-97]++;
      c++;
   }


   c = 0;
   // Doing the same thing on second string.
   /*@
    loop assigns second[0..25];
    loop assigns tmp;
    loop assigns c;
    loop invariant 97 <= tmp <= 122;
    loop invariant \valid(second+(0..25));
    loop invariant strlen(\at(b, Pre)) == strlen(\at(b, Here));
    loop invariant 0 <= c <= strlen(b);
    loop variant strlen(b)-c;
   */
   while (b[c] != '\0')
   {
      tmp = (b[c] > 64 && b[c] < 91) ? b[c]+32 : b[c];
      second[tmp-'a']++;
      c++;
   }

   // And now compare the arrays containing the number of occurences to determine if strings are anagrams or not.
   /*@
    loop invariant strlen(\at(a, Pre)) == strlen(\at(a, Here));
    loop invariant strlen(\at(b, Pre)) == strlen(\at(b, Here));
    loop invariant 0 <= c <= 26;
    loop assigns c;
    loop variant 26-c;
   */
   for (c = 0; c < 26; c++)
   {
      if (first[c] != second[c])
         return 0;
   }

   return 1;
}

回答1:

Your specification appears to be correct at first sight (but then again it is a very sophisticated specification. I have never written any ACSL that sophisticated and I could be missing something).

The annotations inside your function check_anagram, however, are clearly not enough to explain why this function should respect the contract. In particular, consider the while loops. In order to provide a real insight into how the function works, the invariant of each of these loops should express that at any iteration, the arrays respectively first and second contain the counts of characters of the first and second string visited so far.

This is why at the end of each of these loops, these arrays contain the character counts of the entire strings.

Expressing these invariants would really show how the function works. Without them, there is no hope to reach the conclusion that the contract is implemented.

回答2:

I'm no expert in static analysis, but I suspect that some static analysis engines might choke on things like (a[c] > 64 && a[c] < 91), a[c]+32, first[tmp-97] and the other ASCII-specific code you've used here.

Remember, C does not require an ASCII character set; For all we know you could be trying to run this where EBCDIC is the character set, and in that case, I would expect that there might be buffer overflows, depending on the input.

You should use a lookup table (or dictionary of some kind) to convert each character to an integer index, and functions like toupper and tolower to convert an unsigned char value (note the importance of unsigned char here) portably.