为什么我的ACSL合同在我的复制功能上失败了？

Question

我是ACSL的新手，我试着复制来自Fraunhofer Society的"ACSL通过示例“提供的这个复制函数的功能契约。下面的代码工作得很好，每个目标都被证明了。

/*@
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;
    }
}

我试图调整规格，以适应我略有不同的复制功能。这个是无法证明的。我是否遗漏了一些有助于自动验证的重要断言，还是我的方法存在根本缺陷？

/*@ 
  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)

Answer 1

您的loop assigns是不正确的:您应该提到循环主体正在修改dst缓冲区的内容，而不仅仅是指针本身。像loop assigns dst, src, len, temp, dst[0 .. \at(len, Pre)];这样的东西应该更好。

注意，理论上，您可以将更改的单元格的范围限制为dst[len .. \at(len,Pre)]。然而，在实践中，当遇到一个分配的块时，WP很容易被混淆，它的长度从一个循环步骤变化到另一个循环步骤，因此通常最好直接给出范围的全部范围(缺点是您可能必须编写另一个不变变量，指定dst[0 .. len - 1]中的元素尚未更改，但据我所知，这里不需要这样做，因为我们从未在任何地方使用这些元素的值)。

最后，一个小提示：assigns-related目标通常很容易证明。如果你发现他们中的一些人不能出院，检查一下你是否忘记了一些事情，就有个好地方可以开始调查了。