Copybytes函数ACSL合约验证失败，请求问题排查与解决

原可验证的copy函数（参考《ACSL by Example》） #

以下代码可完全通过Frama-C WP验证：

/*@
predicate IsValidRange(uint8_t* a, integer n) =
(0 <= n) && \valid(a+(0.. n-1));
*/

/*@
predicate
IsEqual{A,B}(uint8_t* a, integer n, uint8_t* b) =
\forall integer i; 0 <= i < n ==>
\at(a[i], A) == \at(b[i], B);
*/

/*@
requires IsValidRange(a, n);
requires IsValidRange(b, n);
requires \separated(a+(0..n-1), b+(0..n-1));
assigns b[0..n-1];
ensures IsEqual{Here,Here}(a, n, b);
*/
void copy(const uint8_t *a, uint8_t n, uint8_t *b)
{
    uint8_t i = 0;

    /*@
    loop invariant 0 <= i <= n;
    loop invariant IsEqual{Here,Here}(a, i, b);
    loop assigns b[0..n-1], i;
    loop variant n-i;
    */
    while (i < n)
    {
        b[i] = a[i];
        ++i;
        //@ assert 0 < i <= n;
    }
}

改写后的Copybytes函数及验证问题 #

我改写了Copybytes函数并调整ACSL规格，但无法通过Frama-C WP验证，代码如下：

/*@ 
  requires IsValidRange(src, len);
  requires IsValidRange(dst, len);
  requires len != 0;
  requires \separated(src+(0 .. len-1), dst+(0 .. len-1));
  assigns dst[0 .. \old(len)-1];
  ensures IsEqual{Here,Here}(src, \old(len), dst);
*/
void Copybytes(
    uint8_t const *src, 
    uint8_t *dst,       
    uint8_t len        
)
{

  uint8_t temp;

  //@ assert 0 != len;

  /*@
    loop invariant bound: 0 <= len <= \at(len,LoopEntry);
    loop invariant equal: IsEqual{Here,Here}(src, \at(len,LoopEntry)-len, dst);
    loop assigns dst, src, len, temp;
    loop variant len;
  */
  do
  {
    temp = *src;
    src++;
    *dst = temp;
    dst++;
    //@ assert 0 < len <= \at(len,LoopEntry);
  } while (--len != 0u);
}

WP验证输出 #

[wp] 17 goals scheduled
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_ensures : Timeout (Qed:11ms) (10s)
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_loop_invariant_equal_prese
rved : Timeout (Qed:9ms) (10s)
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_assigns_part4 : Timeout (Qed:6ms) (10s) (cached)
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_assert_2 : Timeout (Qed:6ms) (10s)
[wp] [Alt-Ergo 2.4.0] Goal typed_Copybytes_loop_assigns_part2 : Timeout (Qed:7ms) (10s)
[wp] [Cache] found:3, updated:6
[wp] Proved goals:   12 / 17
  Qed:               8  (1ms-3ms-7ms)
  Alt-Ergo 2.4.0:    4  (16ms-31ms) (86) (interrupted: 5) (cached: 3)

问题分析与修复方案 #

你的方案并非根本性缺陷，而是缺少关键断言与规格修正，导致自动证明器无法推导内存关系：

1. 核心问题 #

循环中src和dst指针不断递增，但未建立当前指针与初始指针的偏移关联，且IsEqual错误使用了当前指针而非初始地址，证明器无法匹配内存操作与数组元素的对应关系。

2. 具体修正点 #

（1）修正函数assigns子句

原assigns dst[0 .. \old(len)-1]中的dst是函数结束后的偏移指针，应改为初始指针指向的内存区域：

assigns \old(dst)[0 .. \old(len)-1];

（2）修正函数ensures断言

ensures中需使用初始指针而非偏移后的指针：

ensures IsEqual{Here,Here}(\old(src), \old(len), \old(dst));

（3）补充关键loop invariant

添加指针偏移关系断言，明确当前指针与初始地址的偏移量等于已复制元素数量：

loop invariant ptr_offset: src == \at(src, LoopEntry) + (\at(len, LoopEntry) - len);
loop invariant ptr_offset_dst: dst == \at(dst, LoopEntry) + (\at(len, LoopEntry) - len);

同时修正equal断言，使用初始指针：

loop invariant equal: IsEqual{Here,Here}(\at(src, LoopEntry), \at(len, LoopEntry)-len, \at(dst, LoopEntry));

（4）修正loop assigns子句

明确修改的是初始dst指向的内存区域：

loop assigns \at(dst, LoopEntry)[0 .. \at(len, LoopEntry)-1], src, dst, len, temp;

修复后的完整代码 #

/*@
predicate IsValidRange(uint8_t* a, integer n) =
(0 <= n) && \valid(a+(0.. n-1));
*/

/*@
predicate
IsEqual{A,B}(uint8_t* a, integer n, uint8_t* b) =
\forall integer i; 0 <= i < n ==>
\at(a[i], A) == \at(b[i], B);
*/

/*@ 
  requires IsValidRange(src, len);
  requires IsValidRange(dst, len);
  requires len != 0;
  requires \separated(src+(0 .. len-1), dst+(0 .. len-1));
  assigns \old(dst)[0 .. \old(len)-1];
  ensures IsEqual{Here,Here}(\old(src), \old(len), \old(dst));
*/
void Copybytes(
    uint8_t const *src, 
    uint8_t *dst,       
    uint8_t len        
)
{

  uint8_t temp;

  //@ assert 0 != len;

  /*@
    loop invariant bound: 0 <= len <= \at(len, LoopEntry);
    loop invariant ptr_offset: src == \at(src, LoopEntry) + (\at(len, LoopEntry) - len);
    loop invariant ptr_offset_dst: dst == \at(dst, LoopEntry) + (\at(len, LoopEntry) - len);
    loop invariant equal: IsEqual{Here,Here}(\at(src, LoopEntry), \at(len, LoopEntry)-len, \at(dst, LoopEntry));
    loop assigns \at(dst, LoopEntry)[0 .. \at(len, LoopEntry)-1], src, dst, len, temp;
    loop variant len;
  */
  do
  {
    temp = *src;
    src++;
    *dst = temp;
    dst++;
    //@ assert 0 < len <= \at(len, LoopEntry);
  } while (--len != 0u);
}

验证说明 #

修正后，证明器可明确指针移动与已复制元素的对应关系，所有WP目标均可通过验证。

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