Frama-C anagram 函数行为验证

Question

我写了一个 C 函数来检查两个给定的字符串（C 风格）是否是字谜。我尝试使用 Frama-C 对其进行验证，但它无法验证函数的最终行为（其他规范有效）。 第一个超时（即使在 WP 中有非常高的超时值），第二个是未知的。

代码如下：

    #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;
}

Answer 1

您的规范乍一看似乎是正确的（但它又是一个非常复杂的规范。我从来没有写过任何复杂的 ACSL，我可能会遗漏一些东西）。

然而，你的函数check_anagram 中的注释显然不足以解释为什么这个函数应该遵守契约。特别要考虑 while 循环。为了真正了解函数的工作原理，每个循环的不变量应表示在任何迭代中，数组分别first 和second 包含访问的第一个和第二个字符串的字符计数，因此远。

这就是为什么在每个循环结束时，这些数组包含整个字符串的字符数。

表达这些不变量将真正展示函数的工作原理。没有他们，就没有希望得出合同得到执行的结论。

Answer 2

我不是静态分析方面的专家，但我怀疑某些静态分析引擎可能会卡住 (a[c] > 64 && a[c] < 91)、a[c]+32、first[tmp-97] 以及您在此处使用的其他 ASCII 特定代码。

记住，C 不需要 ASCII 字符集；据我们所知，您可能会尝试在 EBCDIC 是字符集的情况下运行它，在这种情况下，我预计可能存在缓冲区溢出，具体取决于输入。

您应该使用查找表（或某种字典）将每个字符转换为整数索引，并使用 toupper 和 tolower 之类的函数来转换 unsigned char 值（注意 unsigned char 的重要性在这里）便携。