Timeout during the verification of two array addition

Question

I am trying to verify the addition of two 2d arrays but I constantly take a timeout error regardless of the solver that I use.

The code that I am trying to verify is the following:

typedef struct{
  float mem[3];
}BaseMatrix3x1;


/*@ requires \valid(b1) && \valid(b2);
  @ ensures A: \forall integer i; 0 <= i < 3 ==>
                b1->mem[i] == \old(b1)->mem[i] + b2->mem[i];
  @ assigns b1->mem[0..2];
@*/
void baseMatrixAssignAdd3x1(BaseMatrix3x1 *b1, BaseMatrix3x1 *b2){
    /*@ loop invariant 0 <= i <= 3;
      loop invariant \forall integer k; 
      0 <= k < i ==>
        \at(b1->mem[k], LoopCurrent) ==
            \at(b1->mem[k], LoopEntry) + \at(b2->mem[k], LoopEntry);
      loop assigns i, b1->mem[0..2];*/ 
    for(unsigned int i=0; i<3; i++){
        b1->mem[i] += b2->mem[i];
  }
}

The second loop invariant is the one that causes all the solvers to timeout.

Do you have any suggestions?

Edit: I fixed the assign error (which was not the problem though).

I don't call this function somewhere yet, I am just trying to prove the loop invariants. From my understanding, in order to verify a function, we do not care about the way that this function will be called. We care only about the Pre and Post conditions that we have.

Answer 1

First, what is incorrect/missing in your code:

• you never mention that b1 and b2 are pointers to different matrices. Your loop assigns are incorrect without this information, because b2->mem[0..2] also gets assigned. You need to add a requires \separated(b1, b2); assumption
• you postcondition is incorrect, because \old only applies to the pointer b1 (which remains unchanged in the function anyway), while it should apply to b1->mem. You should have written \old(b1->mem[i]) instead.
• you're missing an important loop invariant, namely that b1->mem[i..2] has not been modified (yet). Since your loop assigns mentions that all of b1->mem may be assigned at every iteration, you need to add an invariant on the unchanged parts.

Next, one apparent limitation of the WP plugin that prevents a full proof:

• the support for the label LoopCurrent seems insufficient. But, in your loop invariants, LoopCurrent is the default label. So you can always replace \at(P, LoopCurrent) by P.

Here is a fully annotated version of your code that the WP plugin is able to prove, using Alt-Ergo as prover.

/*@
  requires \valid(b1) && \valid(b2);
  requires \separated(b1, b2);
  ensures A: \forall integer i; 0 <= i < 3 ==>
                b1->mem[i] == \old(b1->mem[i]) + b2->mem[i];
  assigns b1->mem[0..2];
@*/
void baseMatrixAssignAdd3x1(BaseMatrix3x1 *b1, BaseMatrix3x1 *b2){
  /*@ loop invariant 0 <= i <= 3;
      loop invariant \forall integer k; 
        k >= i ==> b1->mem[k] == \at(b1->mem[k], Pre);
      loop invariant \forall integer k; 
        0 <= k < i ==> b1->mem[k] == \at(b1->mem[k], LoopEntry) + b2->mem[k];
      loop assigns i, b1->mem[0..2];*/ 
  for(unsigned int i=0; i<3; i++){
    b1->mem[i] += b2->mem[i];
  }
}