验证采用类型双关多字节优化的musl libc memchr实现

我正尝试验证一个采用类型双关（type-punning）多字节优化的musl libc memchr修改版本：该实现先在缓冲区前缀中查找目标值，直到指针对齐到sizeof(size_t)；随后通过位操作每次前进sizeof(size_t)字节；最后逐个检查缓冲区后缀。

使用Typed+cast模型时安全属性无问题，但正确性验证遇到困难。以下是存在问题的循环（完整代码见文末）：

// Advance i by sizeof(size_t).
  if (SS <= n && i <= (n - SS) && *(src + i) != c) {
    size_t pat = ONES * c;
    /*@
      @ loop assigns i;
      // @ loop invariant \forall integer j; 0 <= j < i ==> *(src + j) != c;
      @ loop variant n - i;
     */
    while (i <= n - SS && !HASZERO(*((size_t *) (src + i)) ^ pat)) {
      i += SS;
    }
    //@ admit \forall integer j; 0 <= j < i ==> *(src + j) != c;
  }

其中SS即sizeof(size_t)，ONES是每个字节值为1的size_t类型值，HASZERO用于一次性对比缓冲区的SS字节与模式。当前用admit注解替代了原本想要证明的注释掉的loop invariant断言。

相关宏定义如下：

#define SS (sizeof(size_t))
#define ALIGN (sizeof(size_t)-1)
#define ONES ((size_t)-1/UCHAR_MAX)
#define HIGHS (ONES * (UCHAR_MAX/2+1))
#define HASZERO(x) ((x)-ONES & ~(x) & HIGHS)

验证命令为：

frama-c -no-frama-c-stdlib -wp -wp-rte -wp-model=Typed+cast  mymemchr.c

证明循环不变式的方法 #

1. 形式化定义HASZERO的语义

首先要让Frama-C/WP理解HASZERO位操作背后的字节级含义。添加如下断言和引理，将位操作结果与“是否存在字节等于目标值”的命题关联：

/*@ 
  predicate has_target_byte(const char *src, size_t pos, unsigned char c) = 
    \exists integer k; 0 <= k < SS && (unsigned char)src[pos + k] == c;
  
  lemma has_target_HASZERO: 
    \forall const char *src, size_t pos, unsigned char c;
    ((size_t)src + pos) % SS == 0 ==>
    (has_target_byte(src, pos, c) <==> HASZERO(*((size_t*)(src+pos)) ^ (ONES * c)) != 0);
*/

这个引理明确：当src+pos对齐时，HASZERO返回非零值等价于src[pos..pos+SS-1]中存在等于c的字节。

2. 强化循环不变式与前置断言

在循环中补充对齐断言，并修复循环不变式的注释，同时在进入循环前添加辅助断言：

if (SS <= n && i <= (n - SS) && *(src + i) != c) {
  size_t pat = ONES * c;
  /*@
    @ assert ((size_t)(src + i)) & ALIGN == 0;
    @ assert \forall integer j; 0 <= j < i ==> *(src + j) != c;
    @ loop assigns i;
    @ loop invariant ((size_t)(src + i)) & ALIGN == 0;
    @ loop invariant \forall integer j; 0 <= j < i ==> *(src + j) != c;
    @ loop variant n - i;
   */
  while (i <= n - SS && !HASZERO(*((size_t *) (src + i)) ^ pat)) {
    /*@
      @ assert !has_target_byte(src, i, c);
      @ assert \forall integer k; 0 <= k < SS ==> *(src + i + k) != c;
     */
    i += SS;
  }
  // 移除admit，用循环不变式推导
}

补充的对齐断言让验证器明确类型转换的合法性，而字节级的辅助断言则连接了位操作和原始数组访问。

3. 利用归纳法推导不变式

循环不变式的证明依赖归纳逻辑：

• 初始化阶段：进入循环前，前面的对齐循环已经保证\forall j < i; src[j] != c，且src+i对齐、*(src+i) != c，不变式成立。
• 归纳步骤：假设迭代前不变式成立，循环条件!HASZERO(...)为真，结合has_target_HASZERO引理，可得src[i..i+SS-1]中没有等于c的字节。因此\forall j < i+SS; src[j] != c，迭代后i += SS，不变式依然成立。

4. 优化验证工具参数

调用多个定理证明器提升自动证明成功率，或者指定优先处理自定义引理：

frama-c -no-frama-c-stdlib -wp -wp-rte -wp-model=Typed+cast -wp-prover alt-ergo,z3 -wp-lemma has_target_HASZERO mymemchr.c

完整修改后代码示例 #

#include <string.h>
#include <stddef.h>
#include <limits.h>

#define SS (sizeof(size_t))
#define ALIGN (sizeof(size_t)-1)
#define ONES ((size_t)-1/UCHAR_MAX)
#define HIGHS (ONES * (UCHAR_MAX/2+1))
#define HASZERO(x) ((x)-ONES & ~(x) & HIGHS)

/*@ 
  predicate has_target_byte(const char *src, size_t pos, unsigned char c) = 
    \exists integer k; 0 <= k < SS && (unsigned char)src[pos + k] == c;
  
  lemma has_target_HASZERO: 
    \forall const char *src, size_t pos, unsigned char c;
    ((size_t)src + pos) % SS == 0 ==>
    (has_target_byte(src, pos, c) <==> HASZERO(*((size_t*)(src+pos)) ^ (ONES * c)) != 0);
*/

/*@
  @ requires s_valid: \valid_read(((const char *)s) + (0 .. n-1));
  @ ensures \result == 0 ||
     ((const char *)s) <= ((const char *)\result) < ((const char *)s) + n;
  @ assigns \result \from s, c, n;
 
  @ behavior not_found:
     assumes \forall integer i; 0 <= i < n ==> *(((const char *)s) + i) != ((unsigned char)c);
     ensures not_found_zero: \result == 0;
  
  @ behavior found:
     assumes \exists integer i; 0 <= i < n && *(((const char *)s) + i) == ((unsigned char)c);
     ensures found_match: *((const char *)\result) == ((unsigned char)c);
     ensures found_in_range:
       ((const char *)s) <= ((const char *)\result) < ((const char *)s) + n;
     ensures found_earliest: \forall integer i;
       ((const char *)s) <= ((const char *)s) + i < ((const char *)\result) ==>
         *(((const char *)s) + i) != ((unsigned char)c);
  
  @ complete behaviors;
  @ disjoint behaviors;
 */
void *
memchr(const void *s, int c, size_t n) {
  const char *src = (char *) s;
  c = (unsigned char) c;
  size_t i = 0;

#ifdef __GNUC__

  // Advance i until aligned on sizeof(size_t).
  /*@
    @ loop assigns i;
    @ loop invariant \forall integer j; 0 <= j < i ==> *(src + j) != c;
    @ loop variant n - i;
   */
  for (; i < n && ((size_t)(src+i)) & ALIGN && *(src + i) != c; i++);
  //@ assert i >= n || *(src + i) == c || (((size_t)(src+i)) & ALIGN) == 0;

  // Advance i by sizeof(size_t).
  if (SS <= n && i <= (n - SS) && *(src + i) != c) {
    size_t pat = ONES * c;
    /*@
      @ assert ((size_t)(src + i)) & ALIGN == 0;
      @ assert \forall integer j; 0 <= j < i ==> *(src + j) != c;
      @ loop assigns i;
      @ loop invariant ((size_t)(src + i)) & ALIGN == 0;
      @ loop invariant \forall integer j; 0 <= j < i ==> *(src + j) != c;
      @ loop variant n - i;
     */
    while (i <= n - SS && !HASZERO(*((size_t *) (src + i)) ^ pat)) {
      /*@
        @ assert !has_target_byte(src, i, c);
        @ assert \forall integer k; 0 <= k < SS ==> *(src + i + k) != c;
       */
      i += SS;
    }
  }

#endif

  /*@
    @ loop assigns i;
    @ loop invariant \forall integer j; 0 <= j < i ==> *(src + j) != c;
    @ loop variant n - i;
   */
  for (; i < n && *(src + i) != c; i++);
  return (i >= n) ? 0 : ((void *) src + i);
}

内容的提问来源于stack exchange，提问作者Tommy McGuire