Why iterating over total no of edges causing infinite or finitely many loop unwindings?

Question

#include<stdio.h>

#define N 6
#define M 10

typedef int bool;
#define true 1
#define false 0

unsigned int nondet_uint();  

typedef unsigned __CPROVER_bitvector[M] bitvector; 

unsigned int zeroTon(unsigned int n) {
   unsigned int result = nondet_uint();
   __CPROVER_assume(result >=0 && result <=n);
   return result ;
};


//Constrine the value between 0 and 1
unsigned int  nondet (){  
  unsigned int num = nondet_uint();
  __CPROVER_assume( num>= 0 && num  <= 1);
  return num;
}; 

void main() {
   unsigned int pos , i, j, k;

   unsigned int len = 0;
   bool Ch , Ck , C0 ;

  bitvector compartment1 , compartment2 , compartment3 , compartment4, compartment5, compartment6;
bitvector nodes[N] = {compartment1, compartment2, compartment3, compartment4, compartment5, compartment6};


// Represent the graph with given topology 
unsigned int graph[N][N];

for(i=0;i <N; i++) {
    for(j=0;j<N;j++) {
        graph[i][j] = nondet();
    }
}



unsigned int p[N] ;
unsigned int ticks;


   //Make sure that graph is one connected  : just find one hamiltonian cycle 
   //make sure elements are in between node no's and all are distinct

for(i=0; i<N; i++) {
    p[i] = zeroTon(5);
}

for(i=0; i <N; i++) {
     for(j=0; (j<N) && (j!=i) ; j++) {    
    if( p[i] != p[j]){
            C1 = C1 && 1;
        }
        else {
            C1 = C1 && 0;
        }

     }
}

 //hamiltonian One exists 
 for(i=0;i<N-1;i++) {
    if( graph[p[i]][p[i+1]] == 1) {
       Ch = Ch && 1;
    }
   else {
       Ch = Ch && 0;
   }
  }

 len =0;
 for(i=0;i<N;i++) {
   for(j=0;j<N; j++){
          if (graph[i][j] == 1) {
              len = len + 1;
          }
    }
  }

  //THIS IS GOING IN INFINITE LOOP ?? WHY ?? 
  for(i=0;i<len;i++) {
   printf("i'm a disco dancer ");

  }
  __CPROVER_assert(!(Ch && C1) , "Graph has an ham path");
}      

I'm only trying to get a graph that of Total nodes 6 that has a Hamiltonian path. That works well with above code. But when i try to use len i.e total no.of edges i'm getting infinite unwinding in cbmc run .

The above code works well unless i iterate using len . The cbmc run going into infinite unwinding ?? Can anyone explains that.

Answer 1

I'm Not sure about the policy of stack-overflow but in order to clarify the issue i'm posting an answer that was posted by Martin of oxford university on CBMC support forum.

The above code works well unless i iterate using len . The cbmc run going into infinite loop ?? Can anyone explains that.

Short answer : Yes, it is expected, use --unwind

Long answer : CBMC's detection of loop bounds is relatively simple; it will only stop unwinding a loop (without a loop unwind limit) if the branch condition can be statically simplified to false during symbolic execution.

Because the values of graph are non-deterministic, so the value of len will be non-deterministic. Ofcourse we know from the way the rest of the code works that len <= N*N but this cannot be obtained by simplification alone, thus CBMC does not 'realise' this and so the loop unwinding will not terminate by itself.

Why don't we make the bound detection smarter? Say, track intervals for variables? We could but unless you have a complete decision procedure there, you will always find cases like this. If you put a complete decision procedure there you are either doing path-based symbolic execution, which is what our symex tool does, or you are doing incremental BMC (we have tools available for this, they may be merged into the next version of CBMC), depending on if you are deciding on unwinding and assertions separately or together.

thanks all for helping.