I'm new to ACSL and I tried to replicate the function contract of this copy function provided by "ACSL by Example" from the Fraunhofer Society. The Code below works perfectly and every goal gets proven.

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

I tried to adjust the specifications to fit my slightly different copy function. This one cannot be proven. Am I missing some important assertions that would assist the automatic prover or is my approach fundamentally flawed?

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

This is the wp output I get after running the code:

[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)

CodePudding user response：

Your loop assigns is incorrect: you should mention that the loop body is modifying the content of the dst buffer, not only the pointer itself. Something like loop assigns dst, src, len, temp, dst[0 .. \at(len, Pre)]; should be better.

Note that, in theory, you could restrict the range of changed cells to dst[len .. \at(len,Pre)]. However, in practice, WP can easily get confused when confronted to an assigned block whose length changes from one loop step to the other, so that it is usually better to give the full extent of the range directly (the drawback is that you might have to write another invariant specifying that the elements in dst[0 .. len - 1] haven't changed yet, but as far as I can tell this is not needed here, since we never use the value of these elements anywhere).

Finally, a small tip: assigns-related goal are usually quite easy to prove. If you see that some of them cannot be discharged, checking that you haven't forgotten something there is a good place to start investigating.